Add the 15- and 14-state Erdős powers-of-two machines (erdos_15, erdos_14) with Lean proofs

Challenge.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.GCDMonoid.Finset
 public import Mathlib.Order.Interval.Finset.Nat
 public import Mathlib.NumberTheory.LSeries.RiemannZeta
 public import Mathlib.SetTheory.ZFC.Basic
+public import Mathlib.Data.Nat.Digits.Defs
 meta import Lean.Elab.Term
 
 /-!
@@ -19,8 +20,9 @@ Self-contained specification module audited against `Cryptids` by `leanprover/co
 
 - **Constructive gate (`comparator/constructive.json`, `goldbach_21.json`, `zf_380.json`,
   `riemann_104.json`; `permitted_axioms = ["propext", "Quot.sound"]`):**
-  The direct simulation state reductions (`Goldbach21`, `Zf380`, `Riemann104`), all four
-  `candidate_fewer_states` theorems (including `Riemann95.candidate_fewer_states`), all ZF
+  The direct simulation state reductions (`Goldbach21`, `Zf380`, `Riemann104`), the `Erdos14`
+  reduction, all five `candidate_fewer_states` theorems (including
+  `Riemann95.candidate_fewer_states`), all ZF
   machine-to-proof-search equivalences (`Zf393.halts_zf393_iff_zfInconsistent`,
   `Zf380.Semantics.halts_candidate_iff_zfInconsistent`,
   `Semantics.Zf.halts_zf432_iff_wadeZFInconsistent`), and first-order Peano Arithmetic (`PA`)
@@ -34,10 +36,12 @@ 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 26 theorems, including `Riemann95.candidate_equivalent` (which uses
+  Audits all 34 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), and analytic
-  `RiemannHypothesis` equivalences.
+  negated-`Π₁⁰` Goldbach (`¬ GoldbachConjecture`, which uses Markov's Principle), analytic
+  `RiemannHypothesis` equivalences, and the `erdos_15` and `erdos_14` equivalences with
+  `ErdosPowersOfTwoConjecture` (`Nat.digits` uses `Classical.choice`;
+  `¬ ErdosPowersOfTwoConjecture` also uses Markov's Principle).
 -/
 
 meta section
@@ -242,6 +246,12 @@ namespace Machines
 /-- Rows of `riemann95`. -/ def riemann95Rows : List (List (Option (Fin 2 × Dir × Fin 95))) :=
   load_machine_rows% "artifacts/riemann_95/machine.txt"
 /-- 95-state RH candidate. -/ def riemann95 : Machine 95 2 := Machine.ofRows riemann95Rows
+/-- Rows of `erdos15`. -/ def erdos15Rows : List (List (Option (Fin 2 × Dir × Fin 15))) :=
+  load_machine_rows% "baselines/tables/erdos_15.txt"
+/-- 15-state Erdős machine. -/ def erdos15 : Machine 15 2 := Machine.ofRows erdos15Rows
+/-- Rows of `erdos14`. -/ def erdos14Rows : List (List (Option (Fin 2 × Dir × Fin 14))) :=
+  load_machine_rows% "artifacts/erdos_14/machine.txt"
+/-- 14-state Erdős candidate. -/ def erdos14 : Machine 14 2 := Machine.ofRows erdos14Rows
 end Machines
 
 /-- **Goldbach's Conjecture**: every even integer greater than 2 is the sum of two primes. -/
@@ -725,6 +735,11 @@ def paZFInconsistent : PAFormula :=
         (.and (paBetaEq (.var 1) (.var 2) (.var 0) (.var 4))
           ((pzMem (.const 0) (.const 0)).eqFormula (.var 4) 10))))))
 
+/-- **Erdős's conjecture on powers of two** (Erdős 1979): for every `n > 8`, the base-3
+expansion of `2 ^ n` contains the digit `2`. -/
+def ErdosPowersOfTwoConjecture : Prop :=
+  ∀ n : ℕ, 8 < n → 2 ∈ Nat.digits 3 (2 ^ n)
+
 namespace Goldbach21
 /-- 25-state Goldbach reference machine (`goldbach_25`, Yao & Leng 2024). -/
 abbrev reference : BundledMachine 2 := Machines.goldbach25.bundle
@@ -824,4 +839,26 @@ theorem halts_candidate_iff_not_riemannHypothesis :
 end Semantics
 end Riemann95
 
+namespace Erdos15
+/-- 15-state Erdős powers-of-two machine (`erdos_15`, Stérin & Woods 2021). -/
+abbrev erdos15 : Machine 15 2 := Machines.erdos15
+theorem halts_erdos15_iff_exists_counterexample :
+    ConjectureMachines.Halts erdos15 ↔ ∃ n : ℕ, 8 < n ∧ 2 ∉ Nat.digits 3 (2 ^ n) := by sorry
+theorem halts_erdos15_iff_not_erdosPowersOfTwo :
+    ConjectureMachines.Halts erdos15 ↔ ¬ ErdosPowersOfTwoConjecture := by sorry
+end Erdos15
+
+namespace Erdos14
+/-- 15-state Erdős powers-of-two reference machine (`erdos_15`, Stérin & Woods 2021). -/
+abbrev reference : BundledMachine 2 := Machines.erdos15.bundle
+/-- 14-state Erdős powers-of-two candidate machine (`erdos_14`, Stérin 2026). -/
+abbrev candidate : BundledMachine 2 := Machines.erdos14.bundle
+theorem candidate_fewer_states : candidate.states < reference.states := by sorry
+theorem candidate_equivalent : Halts candidate ↔ Halts reference := by sorry
+namespace Semantics
+theorem halts_candidate_iff_not_erdosPowersOfTwo :
+    Halts candidate ↔ ¬ ErdosPowersOfTwoConjecture := by sorry
+end Semantics
+end Erdos14
+
 end ConjectureMachines

Cryptids.lean

@@ -19,20 +19,26 @@ public import Cryptids.Semantics.Riemann120
 public import Cryptids.Semantics.Riemann95
 public import Cryptids.Semantics.Zf
 public import Cryptids.Semantics.Zf393
+public import Cryptids.Erdos15
+public import Cryptids.Semantics.Erdos15
+public import Cryptids.Erdos14
+public import Cryptids.Semantics.Erdos14
 
 /-!
 # 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), and the **Riemann
-Hypothesis** (`120 → 104 → 95` states), as well as complete Lean 4 formalizations of all publicly
-known baseline machines (`goldbach_25`, `zf_432`, `zf_393`, `riemann_744`, `riemann_120`),
+(`25 → 21` states), **ZF Set Theory Consistency** (`393 → 380` states), the **Riemann
+Hypothesis** (`120 → 104 → 95` states), and **Erdős's conjecture on powers of two** (`15 → 14`
+states), as well as complete Lean 4 formalizations of all publicly
+known baseline machines (`goldbach_25`, `zf_432`, `zf_393`, `riemann_744`, `riemann_120`,
+`erdos_15`),
 linking every machine's blank-tape halting problem to Mathlib's statements:
 
 - `Cryptids.Propositions` — Shared definitions of `GoldbachConjecture`,
-  `MatiyasevichRiemannCounterexample`, `ZFInconsistent`, `WadeZFInconsistent`, and deeply embedded
-  first-order Peano Arithmetic (`PATerm`, `PAFormula`, `PAProvable`, `paHalts`,
-  `paZFInconsistent`).
+  `MatiyasevichRiemannCounterexample`, `ZFInconsistent`, `WadeZFInconsistent`,
+  `ErdosPowersOfTwoConjecture`, and deeply embedded first-order Peano Arithmetic (`PATerm`,
+  `PAFormula`, `PAProvable`, `paHalts`, `paZFInconsistent`).
 - `Cryptids.Machines` — Turing machine execution model, bundled machines (`BundledMachine`), and
   machine table definitions (`ConjectureMachines.Machines.*`).
 - `Cryptids.Goldbach21`, `Cryptids.Zf380`, `Cryptids.Riemann104` — Proofs of
@@ -57,6 +63,15 @@ linking every machine's blank-tape halting problem to Mathlib's statements:
   completeness (`paProvable_iff_holdsIn_all_models`), and object-level `PAProvable` proofs that
   `zf_380` and `zf_393` halt iff `ZF` is inconsistent (`paProvable_halts_zf380_iff_zf393`,
   `paProvable_halts_zf393_iff_zfInconsistent`, `paProvable_halts_zf380_iff_zfInconsistent`).
+- `Cryptids.Erdos15`, `Cryptids.Semantics.Erdos15` — Stérin and Woods's 15-state machine for
+  Erdős's conjecture on powers of two (`erdos15`), with a constructive proof of
+  `Halts erdos15 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` and end-to-end proofs of
+  `ConjectureMachines.Erdos15.halts_erdos15_iff_exists_counterexample` and
+  `ConjectureMachines.Erdos15.halts_erdos15_iff_not_erdosPowersOfTwo`.
+- `Cryptids.Erdos14`, `Cryptids.Semantics.Erdos14` — Stérin's 14-state machine for the same
+  conjecture (`erdos14`), with constructive proofs of `Halts erdos14 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` and
+  `Halts candidate ↔ Halts reference` relative to `erdos15`, and
+  `ConjectureMachines.Erdos14.Semantics.halts_candidate_iff_not_erdosPowersOfTwo`.
 - `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`).