Add a 21-state machine for Legendre's conjecture (legendre_21) with Lean proofs

Challenge.lean

@@ -28,7 +28,8 @@ Self-contained specification module audited against `Cryptids` by `leanprover/co
   `Semantics.Zf.halts_zf432_iff_wadeZFInconsistent`), and first-order Peano Arithmetic (`PA`)
   consistency and $\Sigma_1^0$ standard-model adequacy (`Semantics.PA.not_paProvable_false`,
   `Semantics.PA.paHalts_holds_iff_halts`, `Semantics.PA.paZFInconsistent_holds_iff_zfInconsistent`),
-  and the `brocard_28` equivalence `Brocard28.halts_brocard28_iff_exists_square`
+  the `brocard_28` equivalence `Brocard28.halts_brocard28_iff_exists_square`, and the
+  `legendre_21` equivalence `Legendre21.halts_legendre21_iff_exists_gap`
   are verified **without `Classical.choice`** (`ListBlank` uses primitive `Quot` rather than
   `Quotient` so `Halts` is choice-free). Because `Zf/Soundness.lean` proves `not_zfInconsistent`
   via `ZFSet.{0}` (`Classical.choice`)—and `CIC + EM` proves `Con(ZF)` without choice
@@ -37,13 +38,13 @@ Self-contained specification module audited against `Cryptids` by `leanprover/co
   metatheory that cannot prove `Con(PA)` or `Con(ZF)` (see `Cryptids/Semantics/README.md`).
 - **Full gate (`comparator/all.json`; `permitted_axioms = ["propext", "Quot.sound",
   "Classical.choice"]`):**
-  Audits all 36 theorems, including `Riemann95.candidate_equivalent` (which uses `Classical.choice`
+  Audits all 38 theorems, including `Riemann95.candidate_equivalent` (which uses `Classical.choice`
   via `Nat.Prime`), classical `PA` and `ZFSet.{0}` soundness/non-halting, negated-`Π₁⁰` Goldbach
   (`¬ GoldbachConjecture`, which uses Markov's Principle), analytic `RiemannHypothesis`
   equivalences, and the `erdos_ternary_15` and `erdos_ternary_14` equivalences with
   `ErdosTernaryConjecture` (`Nat.digits` uses `Classical.choice`; `¬ ErdosTernaryConjecture` also
-  uses Markov's Principle), and the `brocard_28` equivalence with `¬ BrocardConjecture` (Markov's
-  Principle).
+  uses Markov's Principle), and the `brocard_28` and `legendre_21` equivalences with
+  `¬ BrocardConjecture` and `¬ LegendreConjecture` (Markov's Principle).
 -/
 
 meta section
@@ -263,6 +264,11 @@ def brocard28Rows : List (List (Option (Fin 2 × Dir × Fin 28))) :=
   load_machine_rows% "artifacts/brocard_28/machine.txt"
 /-- 28-state Brocard machine. -/
 def brocard28 : Machine 28 2 := Machine.ofRows brocard28Rows
+/-- Rows of `legendre21`. -/
+def legendre21Rows : List (List (Option (Fin 2 × Dir × Fin 21))) :=
+  load_machine_rows% "artifacts/legendre_21/machine.txt"
+/-- 21-state Legendre machine. -/
+def legendre21 : Machine 21 2 := Machine.ofRows legendre21Rows
 end Machines
 
 /-- **Goldbach's Conjecture**: every even integer greater than 2 is the sum of two primes. -/
@@ -760,6 +766,11 @@ solutions; none exist for `n ≤ 10 ^ 12` (Matson 2017). -/
 def BrocardConjecture : Prop :=
   ∀ n : ℕ, 7 < n → ¬ IsSquare (n.factorial + 1)
 
+/-- **Legendre's conjecture** (one of Landau's four problems, 1912): for every `n ≥ 1` there is
+a prime `p` with `n ^ 2 < p < (n + 1) ^ 2`. -/
+def LegendreConjecture : Prop :=
+  ∀ n : ℕ, 1 ≤ n → ∃ p : ℕ, p.Prime ∧ n ^ 2 < p ∧ p < (n + 1) ^ 2
+
 namespace Goldbach21
 /-- 25-state Goldbach reference machine (`goldbach_25`, Yao & Leng 2024). -/
 abbrev reference : BundledMachine 2 := Machines.goldbach25.bundle
@@ -890,4 +901,14 @@ theorem halts_brocard28_iff_not_brocard :
     ConjectureMachines.Halts brocard28 ↔ ¬ BrocardConjecture := by sorry
 end Brocard28
 
+namespace Legendre21
+/-- 21-state Legendre machine (`legendre_21`, Veljjanoski 2026). -/
+abbrev legendre21 : Machine 21 2 := Machines.legendre21
+theorem halts_legendre21_iff_exists_gap :
+    ConjectureMachines.Halts legendre21 ↔
+      ∃ n : ℕ, 1 ≤ n ∧ ∀ p : ℕ, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2) := by sorry
+theorem halts_legendre21_iff_not_legendre :
+    ConjectureMachines.Halts legendre21 ↔ ¬ LegendreConjecture := by sorry
+end Legendre21
+
 end ConjectureMachines

Cryptids.lean

@@ -25,14 +25,17 @@ public import Cryptids.ErdosTernary14
 public import Cryptids.Semantics.ErdosTernary14
 public import Cryptids.Brocard28
 public import Cryptids.Semantics.Brocard28
+public import Cryptids.Legendre21
+public import Cryptids.Semantics.Legendre21
 
 /-!
 # Certified State Reductions & Formalized Conjecture-Checking Turing Machines
 
 This library formalizes record smaller 2-symbol Turing machines for **Goldbach's Conjecture**
 (`25 → 21` states), **ZF Set Theory Consistency** (`393 → 380` states), the **Riemann
 Hypothesis** (`120 → 104 → 95` states), and **Erdős's ternary conjecture** (`15 → 14`
-states), a 28-state machine for **Brocard's problem** (`brocard_28`), as well as complete
+states), a 28-state machine for **Brocard's problem** (`brocard_28`), a 21-state machine for
+**Legendre's conjecture** (`legendre_21`), as well as complete
 Lean 4 formalizations of all publicly
 known baseline machines (`goldbach_25`, `zf_432`, `zf_393`, `riemann_744`, `riemann_120`,
 `erdos_ternary_15`),
@@ -81,6 +84,12 @@ linking every machine's blank-tape halting problem to Mathlib's statements:
   (`V n = n! / 8`) and `ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square`
   (`Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n! + 1)`), and
   `ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard`.
+- `Cryptids.Legendre21`, `Cryptids.Semantics.Legendre21` — A 21-state machine for Legendre's
+  conjecture (`legendre21`), built on the primality test of `goldbach_21`, with constructive
+  proofs of `Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ EmptyInterval n` and
+  `ConjectureMachines.Legendre21.halts_legendre21_iff_exists_gap`
+  (`Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ ∀ p, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2)`), and
+  `ConjectureMachines.Legendre21.halts_legendre21_iff_not_legendre`.
 - `Cryptids.Semantics.Goldbach`, `Cryptids.Semantics.Zf`, `Cryptids.Semantics.Riemann` —
   End-to-end proofs linking halting from the blank tape to the corresponding mathematical
   conjectures across all baseline machines (`goldbach25`, `zf432`, `riemann744`).