diff --git a/Challenge.lean b/Challenge.lean index 1ecb9b8e..3f77eb26 100644 --- a/Challenge.lean +++ b/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 diff --git a/Cryptids.lean b/Cryptids.lean index 85f33bd5..4c4a2815 100644 --- a/Cryptids.lean +++ b/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`). diff --git a/Cryptids/Erdos14.lean b/Cryptids/Erdos14.lean new file mode 100644 index 00000000..87321778 --- /dev/null +++ b/Cryptids/Erdos14.lean @@ -0,0 +1,715 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.Erdos15 + +/-! +# Erdos14 + +The 14-state Turing machine `erdos_14` halts on the blank tape if and only if some power `2 ^ n` +with `n > 8` has no digit `2` in base `3`. So it halts if and only if the 15-state machine +`erdos_15` does (`candidate_equivalent`). Neither proof uses `Classical.choice`. + +## Provenance and Attribution + +Tristan Stérin announced the machine on the bbchallenge Discord in October 2026 +(). +It is listed on the Cryptids page of the bbchallenge wiki +() as + +``` +1LB1RA_1LC1LB_0RD0RA_1LM0RE_1LF1RE_0LJ1LG_1RK0LH_1RI1LH_0LJ0RE_0RD1LJ_0LL1RK_1RN0LC_0LN---_0RK0LM +``` + +and `artifacts/erdos_14/machine.txt` is this table with the states `A`–`N` numbered `0`–`13`. + +## Machine Layout + +The machine keeps `2 ^ n` in unary: a block of `2 ^ n` ones, with a separator `0` and a counter +to its left. Each stage reads the base-3 digits of the block length by repeated division by `3`, +with a single `0` (the hole) in the block marking where the quotient ends. + +* `D` (state `3`) starts dividing the `q` ones before the hole: it erases the first one, making a + new hole. Each round `E`, `F`, `G` (`4`–`6`) move the old hole two cells left and `H`, `I` (`7`, + `8`) move the new hole one cell right. If `q % 3 = 2` (a digit `2`), `G` fills the new hole and + the stage ends. Otherwise `J` (`9`) returns to the start, and the hole now follows `q / 3` ones. +* When `q` reaches `0` with no digit `2`, `D` fills the hole and `M`, `N`, `K`, `L` (`12`, `13`, + `10`, `11`) advance the counter (`000`, `100`, `111` left of the separator); the third such stage + halts in `M`. +* At the end of a stage `K`, `L` remove one cell and `A`, `B`, `C` (`0`–`2`) double the block: `C` + takes a cell from the part still to double, `A` adds a cell at the right end and `B` fills the + gap. + +The boot writes `11`, so the first stage checks `2 ^ 1` and the counter skips `2 ^ 0`. The machine +halts at the third power `2 ^ n` with `n ≥ 1` and no digit `2`; the first two are `2 ^ 2` and +`2 ^ 8`. +-/ + +@[expose] public section + +namespace ConjectureMachines.Erdos14 + +open Turing (Dir) +open StateTransition +open Erdos15 (B0 B0_cons_zero pw pw_lt dbl cnt cnt_succ_of_mem cnt_succ_of_not_mem cnt_stays + first_free free_or_none) + +local notation "mkL" => Erdos15.Tape.mkL + +/-- 15-state Erdős reference machine (`erdos_15`, Stérin & Woods 2021). -/ +abbrev reference : BundledMachine 2 := Machines.erdos15.bundle + +/-- 14-state Erdős candidate machine (`erdos_14`, Stérin 2026). -/ +abbrev candidate : BundledMachine 2 := Machines.erdos14.bundle + +/-- The candidate as a `Machine 14 2`. -/ +abbrev erdos14 : Machine 14 2 := Machines.erdos14 + +/-! ## Base-3 Digits by Division -/ + +/-- `2` is a base-3 digit of `m`. -/ +def Has2 (m : ℕ) : Prop := ∃ k, m / 3 ^ k % 3 = 2 + +theorem not_has2_zero : ¬ Has2 0 := by + rintro ⟨k, hk⟩ + rw [Nat.zero_div] at hk + omega + +theorem has2_iff (m : ℕ) : Has2 m ↔ m % 3 = 2 ∨ Has2 (m / 3) := by + constructor + · rintro ⟨k, hk⟩ + cases k with + | zero => + rw [pow_zero, Nat.div_one] at hk + exact Or.inl hk + | succ k => + rw [pow_succ', ← Nat.div_div_eq_div_mul] at hk + exact Or.inr ⟨k, hk⟩ + · rintro (h | ⟨k, hk⟩) + · exact ⟨0, by rw [pow_zero, Nat.div_one]; exact h⟩ + · exact ⟨k + 1, by rw [pow_succ', ← Nat.div_div_eq_div_mul]; exact hk⟩ + +/-- The number with base-3 digits `ds`, least significant first. -/ +def val : List ℕ → ℕ + | [] => 0 + | d :: ds => d + 3 * val ds + +theorem val_dbl (ds : List ℕ) (hds : ∀ d ∈ ds, d < 3) (c : ℕ) (hc : c ≤ 1) : + val (dbl ds c) = 2 * val ds + c := by + induction ds generalizing c with + | nil => + rcases (by omega : c = 0 ∨ c = 1) with rfl | rfl + · rfl + · rfl + | cons d ds ih => + have hd := hds d (by simp) + simp only [dbl, val] + rw [ih (fun x hx => hds x (List.mem_cons_of_mem d hx)) _ (by omega)] + omega + +theorem val_pw (n : ℕ) : val (pw n) = 2 ^ n := by + induction n with + | zero => rfl + | succ n ih => + rw [pw, val_dbl _ (pw_lt n) 0 (by omega), ih, pow_succ] + omega + +theorem has2_val (ds : List ℕ) (hds : ∀ d ∈ ds, d < 3) : Has2 (val ds) ↔ 2 ∈ ds := by + induction ds with + | nil => exact ⟨fun h => absurd h not_has2_zero, fun h => absurd h List.not_mem_nil⟩ + | cons d ds ih => + have hd := hds d (by simp) + rw [val, has2_iff, show (d + 3 * val ds) % 3 = d by omega, + show (d + 3 * val ds) / 3 = val ds by omega, + ih (fun x hx => hds x (List.mem_cons_of_mem d hx)), List.mem_cons, eq_comm] + +/-- `2 ^ n` has a digit `2` in base `3` if and only if `pw n` contains `2`. -/ +theorem has2_pow (n : ℕ) : Has2 (2 ^ n) ↔ 2 ∈ pw n := by + rw [← val_pw] + exact has2_val _ (pw_lt n) + +/-! ## Tape Encoding -/ + +/-- `k` ones followed by `L`. -/ +def ones (k : ℕ) (L : ListBlank (Fin 2)) : ListBlank (Fin 2) := + ListBlank.append (List.replicate k 1) L + +theorem ones_succ' (k : ℕ) (L : ListBlank (Fin 2)) : ones (k + 1) L = ones k (L.cons 1) := by + rw [ones, List.replicate_succ', ListBlank.append_assoc] + rfl + +theorem ones_add (j k : ℕ) (L : ListBlank (Fin 2)) : ones (j + k) L = ones j (ones k L) := by + rw [ones, List.replicate_add, ListBlank.append_assoc] + rfl + +/-- The counter cells left of the separator, nearest first: `000`, `100` or `111`. -/ +def CT : ℕ → ListBlank (Fin 2) + | 0 => ListBlank.append [0, 0, 0] B0 + | 1 => ListBlank.append [1, 0, 0] B0 + | _ => ListBlank.append [1, 1, 1] B0 + +/-- The cells left of the block: the separator `0`, then the counter. -/ +def CL (c : ℕ) : ListBlank (Fin 2) := (CT c).cons 0 + +/-- `D` at the start of the block, which holds `q` ones, the hole, then `r` ones. -/ +def divCfg (c q r : ℕ) : Cfg 14 2 := + ⟨3, Tape.mk' (CL c) (ones q ((ones r B0).cons 0))⟩ + +/-- Start of the stage that checks `2 ^ n`, with counter `c`. -/ +def stageCfg (c n : ℕ) : Cfg 14 2 := divCfg c (2 ^ n) 0 + +/-- `E` on the first of the `b` cells between the two holes, with `a` ones before the first hole +and `r` ones after the second. -/ +def cfgE (c a b r : ℕ) : Cfg 14 2 := + ⟨4, Tape.mk' ((ones a (CL c)).cons 0) (ones b ((ones r B0).cons 0))⟩ + +/-- `C` on the last of the `j + 1` cells still to double, with `t` doubled cells after it. -/ +def cfgC (c j t : ℕ) : Cfg 14 2 := + ⟨2, Tape.mk' (ones j (CL c)) (ones (t + 1) B0)⟩ + +theorem divCfg_top (c M : ℕ) : divCfg c M 0 = ⟨3, Tape.mk' (CL c) (ones M B0)⟩ := by + change (⟨3, Tape.mk' (CL c) (ones M (B0.cons 0))⟩ : Cfg 14 2) = _ + rw [B0_cons_zero] + +theorem mkL_B0 (R : ListBlank (Fin 2)) : mkL B0 R = ⟨0, B0, R⟩ := rfl + +/-! ## Step Infrastructure -/ + +/-- `n` steps of `M` from `c`, or `none` if `M` halts first. -/ +def nSteps (M : Machine 14 2) (n : ℕ) : Cfg 14 2 → Option (Cfg 14 2) := + Nat.rec (motive := fun _ => Cfg 14 2 → Option (Cfg 14 2)) + (fun c => some c) + (fun _ ih c => (step M c).bind ih) + n + +@[simp] +theorem nSteps_zero (M : Machine 14 2) (c : Cfg 14 2) : + nSteps M 0 c = some c := rfl + +@[simp] +theorem nSteps_succ (M : Machine 14 2) (n : ℕ) (c : Cfg 14 2) : + nSteps M (n + 1) c = (step M c).bind (nSteps M n) := rfl + +attribute [eqns nSteps_zero nSteps_succ] nSteps + +theorem nSteps_reaches {M : Machine 14 2} {n : ℕ} {c c' : Cfg 14 2} + (h : nSteps M n c = some c') : Reaches (step M) c c' := by + induction n generalizing c with + | zero => + injection h with h' + subst h' + exact Relation.ReflTransGen.refl + | succ n ih => + simp only [nSteps, Option.bind_eq_some_iff] at h + obtain ⟨c₁, hstep, hrest⟩ := h + exact Relation.ReflTransGen.head hstep (ih hrest) + +theorem nSteps_add {M : Machine 14 2} (m n : ℕ) (c : Cfg 14 2) : + nSteps M (m + n) c = (nSteps M m c).bind (nSteps M n) := by + induction m generalizing c with + | zero => simp [nSteps] + | succ m ih => + rw [Nat.succ_add, nSteps, nSteps] + cases step M c <;> simp [ih] + +theorem nSteps_bind_eq {M : Machine 14 2} {m n : ℕ} {c c₁ c₂ : Cfg 14 2} + (h₁ : nSteps M m c = some c₁) (h₂ : nSteps M n c₁ = some c₂) : + nSteps M (m + n) c = some c₂ := by + rw [nSteps_add, h₁, Option.bind_some, h₂] + +theorem nSteps_cons {M : Machine 14 2} {n : ℕ} {c c₁ c₂ : Cfg 14 2} + (h₁ : step M c = some c₁) (h₂ : nSteps M n c₁ = some c₂) : + nSteps M (n + 1) c = some c₂ := by + rw [nSteps_succ, h₁, Option.bind_some, h₂] + +theorem step_one {M : Machine 14 2} {c c₁ : Cfg 14 2} (h : step M c = some c₁) : + nSteps M 1 c = some c₁ := by + rw [nSteps, h]; rfl + +theorem reaches_imp_nSteps {M : Machine 14 2} {a b : Cfg 14 2} + (h : Reaches (step M) a b) : ∃ k, nSteps M k a = some b := by + induction h with + | refl => exact ⟨0, rfl⟩ + | tail _ hstep ih => + obtain ⟨k, hk⟩ := ih + exact ⟨k + 1, nSteps_bind_eq hk (step_one hstep)⟩ + +theorem nSteps_eq_none_of_step_none {M : Machine 14 2} {k : ℕ} (s : ℕ) {a b : Cfg 14 2} + (hk : nSteps M k a = some b) (hnone : step M b = none) (hks : k < s) : + nSteps M s a = none := by + have hs : s = k + ((s - k - 1) + 1) := by omega + rw [hs, nSteps_add, hk, Option.bind_some, nSteps_succ, hnone, Option.bind_none] + +/-! ## Transition Table -/ + +theorem stepR {q q' : Fin 14} {a b : Fin 2} (h : erdos14.transition q a = some (b, .right, q')) + (L R : ListBlank (Fin 2)) : + step erdos14 ⟨q, ⟨a, L, R⟩⟩ = some ⟨q', Tape.mk' (L.cons b) R⟩ := by + simp only [step, h, Option.map_some]; rfl + +theorem stepL {q q' : Fin 14} {a b : Fin 2} (h : erdos14.transition q a = some (b, .left, q')) + (L R : ListBlank (Fin 2)) : + step erdos14 ⟨q, ⟨a, L, R⟩⟩ = some ⟨q', mkL L (R.cons b)⟩ := by + simp only [step, h, Option.map_some]; rfl + +theorem sA_0 (L R) : step erdos14 ⟨0, ⟨0, L, R⟩⟩ = some ⟨1, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sA_1 (L R) : step erdos14 ⟨0, ⟨1, L, R⟩⟩ = some ⟨0, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem sB_0 (L R) : step erdos14 ⟨1, ⟨0, L, R⟩⟩ = some ⟨2, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sB_1 (L R) : step erdos14 ⟨1, ⟨1, L, R⟩⟩ = some ⟨1, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sC_0 (L R) : step erdos14 ⟨2, ⟨0, L, R⟩⟩ = some ⟨3, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem sC_1 (L R) : step erdos14 ⟨2, ⟨1, L, R⟩⟩ = some ⟨0, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem sD_0 (L R) : step erdos14 ⟨3, ⟨0, L, R⟩⟩ = some ⟨12, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sD_1 (L R) : step erdos14 ⟨3, ⟨1, L, R⟩⟩ = some ⟨4, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem sE_0 (L R) : step erdos14 ⟨4, ⟨0, L, R⟩⟩ = some ⟨5, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sE_1 (L R) : step erdos14 ⟨4, ⟨1, L, R⟩⟩ = some ⟨4, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem sF_0 (L R) : step erdos14 ⟨5, ⟨0, L, R⟩⟩ = some ⟨9, mkL L (R.cons 0)⟩ := stepL rfl L R +theorem sF_1 (L R) : step erdos14 ⟨5, ⟨1, L, R⟩⟩ = some ⟨6, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sG_0 (L R) : step erdos14 ⟨6, ⟨0, L, R⟩⟩ = some ⟨10, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem sG_1 (L R) : step erdos14 ⟨6, ⟨1, L, R⟩⟩ = some ⟨7, mkL L (R.cons 0)⟩ := stepL rfl L R +theorem sH_0 (L R) : step erdos14 ⟨7, ⟨0, L, R⟩⟩ = some ⟨8, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem sH_1 (L R) : step erdos14 ⟨7, ⟨1, L, R⟩⟩ = some ⟨7, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sI_0 (L R) : step erdos14 ⟨8, ⟨0, L, R⟩⟩ = some ⟨9, mkL L (R.cons 0)⟩ := stepL rfl L R +theorem sI_1 (L R) : step erdos14 ⟨8, ⟨1, L, R⟩⟩ = some ⟨4, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem sJ_0 (L R) : step erdos14 ⟨9, ⟨0, L, R⟩⟩ = some ⟨3, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem sJ_1 (L R) : step erdos14 ⟨9, ⟨1, L, R⟩⟩ = some ⟨9, mkL L (R.cons 1)⟩ := stepL rfl L R +theorem sK_0 (L R) : step erdos14 ⟨10, ⟨0, L, R⟩⟩ = some ⟨11, mkL L (R.cons 0)⟩ := stepL rfl L R +theorem sK_1 (L R) : step erdos14 ⟨10, ⟨1, L, R⟩⟩ = some ⟨10, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sL_0 (L R) : step erdos14 ⟨11, ⟨0, L, R⟩⟩ = some ⟨13, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sL_1 (L R) : step erdos14 ⟨11, ⟨1, L, R⟩⟩ = some ⟨2, mkL L (R.cons 0)⟩ := stepL rfl L R +theorem sM_0 (L R) : step erdos14 ⟨12, ⟨0, L, R⟩⟩ = some ⟨13, mkL L (R.cons 0)⟩ := stepL rfl L R +theorem sM_1 (L R : ListBlank (Fin 2)) : step erdos14 ⟨12, ⟨1, L, R⟩⟩ = none := rfl +theorem sN_0 (L R) : step erdos14 ⟨13, ⟨0, L, R⟩⟩ = some ⟨10, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sN_1 (L R) : step erdos14 ⟨13, ⟨1, L, R⟩⟩ = some ⟨12, mkL L (R.cons 0)⟩ := stepL rfl L R + +/-- Runs the machine through a fixed sequence of steps on a concrete tape. -/ +local macro "tm_run" : tactic => `(tactic| simp only [nSteps_succ, nSteps_zero, Option.bind_some, + sA_0, sA_1, sB_0, sB_1, sC_0, sC_1, sD_0, sD_1, sE_0, sE_1, sF_0, sF_1, sG_0, sG_1, sH_0, sH_1, + sI_0, sI_1, sJ_0, sJ_1, sK_0, sK_1, sL_0, sL_1, sM_0, sN_0, sN_1, Erdos15.Tape.mk'_cons, + Erdos15.Tape.mkL_cons, Erdos15.Tape.mk'_B0, mkL_B0, ListBlank.append, B0_cons_zero]) + +/-! ## Sweeps over Ones -/ + +theorem sweepR {q : Fin 14} + (h : ∀ L R, step erdos14 ⟨q, ⟨1, L, R⟩⟩ = some ⟨q, Tape.mk' (L.cons 1) R⟩) + (k : ℕ) (L R : ListBlank (Fin 2)) : + nSteps erdos14 k ⟨q, Tape.mk' L (ones k R)⟩ = some ⟨q, Tape.mk' (ones k L) R⟩ := by + induction k generalizing L with + | zero => rfl + | succ k ih => + rw [nSteps_succ, show ones (k + 1) R = (ones k R).cons 1 from rfl, Erdos15.Tape.mk'_cons, h, + Option.bind_some, ih, ones_succ'] + +theorem sweepL {q : Fin 14} + (h : ∀ L R, step erdos14 ⟨q, ⟨1, L, R⟩⟩ = some ⟨q, mkL L (R.cons 1)⟩) + (k : ℕ) (L R : ListBlank (Fin 2)) : + nSteps erdos14 k ⟨q, mkL (ones k L) R⟩ = some ⟨q, mkL L (ones k R)⟩ := by + induction k generalizing R with + | zero => rfl + | succ k ih => + rw [nSteps_succ, show ones (k + 1) L = (ones k L).cons 1 from rfl, Erdos15.Tape.mkL_cons, h, + Option.bind_some, ih, ones_succ'] + +/-- `J` returns over `a` ones to the separator and hands over to `D`. -/ +theorem j_return (c a : ℕ) (Y : ListBlank (Fin 2)) : + ∃ s, nSteps erdos14 s ⟨9, mkL (ones a (CL c)) Y⟩ = some ⟨3, Tape.mk' (CL c) (ones a Y)⟩ := by + have h₁ := sweepL sJ_1 a (CL c) Y + have h₂ : step erdos14 ⟨9, mkL (CL c) (ones a Y)⟩ = some ⟨3, Tape.mk' (CL c) (ones a Y)⟩ := by + rw [CL, Erdos15.Tape.mkL_cons, sJ_0] + exact ⟨_, nSteps_bind_eq h₁ (step_one h₂)⟩ + +/-- After a stage, `K` stands right of the block of `j + 2` ones; `K`, `L` remove the last one +and hand over to `C`. -/ +theorem kl_finish (c j : ℕ) : + nSteps erdos14 2 ⟨10, Tape.mk' (ones (j + 2) (CL c)) B0⟩ = some (cfgC c j 0) := by + change nSteps erdos14 2 ⟨10, Tape.mk' (((ones j (CL c)).cons 1).cons 1) B0⟩ = + some ⟨2, Tape.mk' (ones j (CL c)) (B0.cons 1)⟩ + tm_run + +/-! ## Doubling (States `A`, `B`, `C`) -/ + +/-- One doubling round: `C` takes the last cell, `A` adds a cell at the right end and `B` fills +the gap. -/ +theorem dbl_round (c j t : ℕ) : + ∃ s, nSteps erdos14 s (cfgC c j t) = some ⟨2, mkL (ones j (CL c)) (ones (t + 2) B0)⟩ := by + have h₁ : step erdos14 (cfgC c j t) = + some ⟨0, Tape.mk' ((ones j (CL c)).cons 0) (ones t B0)⟩ := by + change step erdos14 ⟨2, Tape.mk' (ones j (CL c)) ((ones t B0).cons 1)⟩ = _ + rw [Erdos15.Tape.mk'_cons, sC_1] + have h₂ := sweepR sA_1 t ((ones j (CL c)).cons 0) B0 + have h₃ : step erdos14 ⟨0, Tape.mk' (ones t ((ones j (CL c)).cons 0)) B0⟩ = + some ⟨1, mkL (ones t ((ones j (CL c)).cons 0)) (B0.cons 1)⟩ := by + rw [Erdos15.Tape.mk'_B0, sA_0] + have h₄ := sweepL sB_1 t ((ones j (CL c)).cons 0) (B0.cons 1) + have h₅ : step erdos14 ⟨1, mkL ((ones j (CL c)).cons 0) (ones t (B0.cons 1))⟩ = + some ⟨2, mkL (ones j (CL c)) (ones (t + 2) B0)⟩ := by + rw [Erdos15.Tape.mkL_cons, sB_0, ones_succ' (t + 1)] + rfl + exact ⟨_, nSteps_cons h₁ (nSteps_bind_eq h₂ (nSteps_cons h₃ (nSteps_bind_eq h₄ + (step_one h₅))))⟩ + +/-- Doubling the `j + 1` cells before `t` doubled cells ends at the next stage start. -/ +theorem dbl_loop (c j : ℕ) : + ∀ t, ∃ s, 1 ≤ s ∧ nSteps erdos14 s (cfgC c j t) = some (divCfg c (t + 2 * (j + 1)) 0) := by + induction j with + | zero => + intro t + obtain ⟨s, hs⟩ := dbl_round c 0 t + have h : step erdos14 ⟨2, mkL (ones 0 (CL c)) (ones (t + 2) B0)⟩ = + some (divCfg c (t + 2 * (0 + 1)) 0) := by + rw [divCfg_top] + change step erdos14 ⟨2, mkL ((CT c).cons 0) (ones (t + 2) B0)⟩ = + some ⟨3, Tape.mk' ((CT c).cons 0) (ones (t + 2) B0)⟩ + rw [Erdos15.Tape.mkL_cons, sC_0] + exact ⟨s + 1, by omega, nSteps_bind_eq hs (step_one h)⟩ + | succ j ih => + intro t + obtain ⟨s₁, hs₁⟩ := dbl_round c (j + 1) t + obtain ⟨s₂, hs₂1, hs₂⟩ := ih (t + 2) + have e : (⟨2, mkL (ones (j + 1) (CL c)) (ones (t + 2) B0)⟩ : Cfg 14 2) = cfgC c j (t + 2) := by + change (⟨2, mkL ((ones j (CL c)).cons 1) (ones (t + 2) B0)⟩ : Cfg 14 2) = + ⟨2, Tape.mk' (ones j (CL c)) ((ones (t + 2) B0).cons 1)⟩ + rw [Erdos15.Tape.mkL_cons, Erdos15.Tape.mk'_cons] + rw [e] at hs₁ + refine ⟨s₁ + s₂, by omega, ?_⟩ + rw [show t + 2 * (j + 1 + 1) = t + 2 + 2 * (j + 1) by omega] + exact nSteps_bind_eq hs₁ hs₂ + +/-! ## Division by `3` (States `D`–`J`) -/ + +theorem div_start (c q r : ℕ) : step erdos14 (divCfg c (q + 1) r) = some (cfgE c 0 q r) := by + change step erdos14 ⟨3, Tape.mk' (CL c) ((ones q ((ones r B0).cons 0)).cons 1)⟩ = _ + rw [Erdos15.Tape.mk'_cons, sD_1] + rfl + +/-- `E` runs to the second hole and fills it, and `F` steps back. -/ +theorem e_pass (c a b r : ℕ) : ∃ s, nSteps erdos14 s (cfgE c a b r) = + some ⟨5, mkL (ones b ((ones a (CL c)).cons 0)) (ones (r + 1) B0)⟩ := by + have h₁ := sweepR sE_1 b ((ones a (CL c)).cons 0) ((ones r B0).cons 0) + have h₂ : step erdos14 ⟨4, Tape.mk' (ones b ((ones a (CL c)).cons 0)) ((ones r B0).cons 0)⟩ = + some ⟨5, mkL (ones b ((ones a (CL c)).cons 0)) (ones (r + 1) B0)⟩ := by + rw [Erdos15.Tape.mk'_cons, sE_0] + rfl + exact ⟨_, nSteps_bind_eq h₁ (step_one h₂)⟩ + +/-- No cell between the holes: the quotient is `a` and the digit is `1`. -/ +theorem out_x (c a r : ℕ) : ∃ s, nSteps erdos14 s (cfgE c a 0 r) = some (divCfg c a (r + 1)) := by + obtain ⟨s₁, hs₁⟩ := e_pass c a 0 r + have h₂ : step erdos14 ⟨5, mkL (ones 0 ((ones a (CL c)).cons 0)) (ones (r + 1) B0)⟩ = + some ⟨9, mkL (ones a (CL c)) ((ones (r + 1) B0).cons 0)⟩ := by + change step erdos14 ⟨5, mkL ((ones a (CL c)).cons 0) (ones (r + 1) B0)⟩ = _ + rw [Erdos15.Tape.mkL_cons, sF_0] + obtain ⟨s₃, hs₃⟩ := j_return c a ((ones (r + 1) B0).cons 0) + exact ⟨_, nSteps_bind_eq hs₁ (nSteps_cons h₂ hs₃)⟩ + +/-- One cell between the holes: the digit is `2`; `G` fills the first hole and `K` runs to the +end of the block. -/ +theorem out_y (c a r : ℕ) : + ∃ s, nSteps erdos14 s (cfgE c a 1 r) = some (cfgC c (a + r + 1) 0) := by + obtain ⟨s₁, hs₁⟩ := e_pass c a 1 r + have h₂ : nSteps erdos14 2 ⟨5, mkL (ones 1 ((ones a (CL c)).cons 0)) (ones (r + 1) B0)⟩ = + some ⟨10, Tape.mk' ((ones a (CL c)).cons 1) (ones (r + 2) B0)⟩ := by + change nSteps erdos14 2 ⟨5, mkL (((ones a (CL c)).cons 0).cons 1) (ones (r + 1) B0)⟩ = + some ⟨10, Tape.mk' ((ones a (CL c)).cons 1) ((ones (r + 1) B0).cons 1)⟩ + tm_run + have h₃ := sweepR sK_1 (r + 2) ((ones a (CL c)).cons 1) B0 + have e : ones (r + 2) ((ones a (CL c)).cons 1) = ones (a + r + 1 + 2) (CL c) := by + rw [show a + r + 1 + 2 = (r + 2) + (a + 1) by omega, ones_add (r + 2) (a + 1)] + rfl + rw [e] at h₃ + exact ⟨_, nSteps_bind_eq hs₁ (nSteps_bind_eq h₂ (nSteps_bind_eq h₃ (kl_finish c (a + r + 1))))⟩ + +/-- Two cells between the holes: the quotient is `a + 1` and the digit is `0`. -/ +theorem out_z (c a r : ℕ) : + ∃ s, nSteps erdos14 s (cfgE c a 2 r) = some (divCfg c (a + 1) (r + 2)) := by + obtain ⟨s₁, hs₁⟩ := e_pass c a 2 r + have h₂ : nSteps erdos14 4 ⟨5, mkL (ones 2 ((ones a (CL c)).cons 0)) (ones (r + 1) B0)⟩ = + some ⟨9, mkL (ones (a + 1) (CL c)) ((ones (r + 2) B0).cons 0)⟩ := by + change nSteps erdos14 4 ⟨5, mkL ((((ones a (CL c)).cons 0).cons 1).cons 1) (ones (r + 1) B0)⟩ = + some ⟨9, mkL ((ones a (CL c)).cons 1) (((ones (r + 1) B0).cons 1).cons 0)⟩ + tm_run + obtain ⟨s₃, hs₃⟩ := j_return c (a + 1) ((ones (r + 2) B0).cons 0) + exact ⟨_, nSteps_bind_eq hs₁ (nSteps_bind_eq h₂ hs₃)⟩ + +/-- A full round with at least three cells between the holes. -/ +theorem div_round (c a b r : ℕ) : + ∃ s, nSteps erdos14 s (cfgE c a (b + 3) r) = some (cfgE c (a + 1) b (r + 2)) := by + obtain ⟨s₁, hs₁⟩ := e_pass c a (b + 3) r + have h₂ : nSteps erdos14 2 + ⟨5, mkL (ones (b + 3) ((ones a (CL c)).cons 0)) (ones (r + 1) B0)⟩ = + some ⟨7, mkL (ones (b + 1) ((ones a (CL c)).cons 0)) + (((ones (r + 1) B0).cons 1).cons 0)⟩ := by + change nSteps erdos14 2 + ⟨5, mkL (((ones (b + 1) ((ones a (CL c)).cons 0)).cons 1).cons 1) (ones (r + 1) B0)⟩ = _ + tm_run + have h₃ := sweepL sH_1 (b + 1) ((ones a (CL c)).cons 0) (((ones (r + 1) B0).cons 1).cons 0) + have h₄ : nSteps erdos14 2 + ⟨7, mkL ((ones a (CL c)).cons 0) (ones (b + 1) (((ones (r + 1) B0).cons 1).cons 0))⟩ = + some (cfgE c (a + 1) b (r + 2)) := by + change nSteps erdos14 2 + ⟨7, mkL ((ones a (CL c)).cons 0) ((ones b (((ones (r + 1) B0).cons 1).cons 0)).cons 1)⟩ = + some ⟨4, Tape.mk' (((ones a (CL c)).cons 1).cons 0) + (ones b (((ones (r + 1) B0).cons 1).cons 0))⟩ + tm_run + exact ⟨_, nSteps_bind_eq hs₁ (nSteps_bind_eq h₂ (nSteps_bind_eq h₃ h₄))⟩ + +theorem loop0 (c k : ℕ) : ∀ a r, + ∃ s, nSteps erdos14 s (cfgE c a (3 * k) r) = some (divCfg c (a + k) (r + 2 * k + 1)) := by + induction k with + | zero => exact out_x c + | succ k ih => + intro a r + obtain ⟨s₁, hs₁⟩ := div_round c a (3 * k) r + obtain ⟨s₂, hs₂⟩ := ih (a + 1) (r + 2) + rw [show 3 * (k + 1) = 3 * k + 3 by omega, show a + (k + 1) = a + 1 + k by omega, + show r + 2 * (k + 1) + 1 = r + 2 + 2 * k + 1 by omega] + exact ⟨_, nSteps_bind_eq hs₁ hs₂⟩ + +theorem loop1 (c k : ℕ) : ∀ a r, + ∃ s, nSteps erdos14 s (cfgE c a (3 * k + 1) r) = some (cfgC c (a + k + (r + 2 * k) + 1) 0) := by + induction k with + | zero => exact out_y c + | succ k ih => + intro a r + obtain ⟨s₁, hs₁⟩ := div_round c a (3 * k + 1) r + obtain ⟨s₂, hs₂⟩ := ih (a + 1) (r + 2) + rw [show 3 * (k + 1) + 1 = 3 * k + 1 + 3 by omega, + show a + (k + 1) + (r + 2 * (k + 1)) + 1 = a + 1 + k + (r + 2 + 2 * k) + 1 by omega] + exact ⟨_, nSteps_bind_eq hs₁ hs₂⟩ + +theorem loop2 (c k : ℕ) : ∀ a r, + ∃ s, nSteps erdos14 s (cfgE c a (3 * k + 2) r) = + some (divCfg c (a + k + 1) (r + 2 * k + 2)) := by + induction k with + | zero => exact out_z c + | succ k ih => + intro a r + obtain ⟨s₁, hs₁⟩ := div_round c a (3 * k + 2) r + obtain ⟨s₂, hs₂⟩ := ih (a + 1) (r + 2) + rw [show 3 * (k + 1) + 2 = 3 * k + 2 + 3 by omega, + show a + (k + 1) + 1 = a + 1 + k + 1 by omega, + show r + 2 * (k + 1) + 2 = r + 2 + 2 * k + 2 by omega] + exact ⟨_, nSteps_bind_eq hs₁ hs₂⟩ + +/-- Dividing `3 * k + 1` ones: digit `1`, quotient `k`. -/ +theorem level_one (c k r : ℕ) : + ∃ s, nSteps erdos14 s (divCfg c (3 * k + 1) r) = some (divCfg c k (r + 2 * k + 1)) := by + obtain ⟨s, hs⟩ := loop0 c k 0 r + rw [Nat.zero_add] at hs + exact ⟨_, nSteps_cons (div_start c (3 * k) r) hs⟩ + +/-- Dividing `3 * k + 2` ones: digit `2`. -/ +theorem level_two (c k r : ℕ) : + ∃ s, nSteps erdos14 s (divCfg c (3 * k + 2) r) = some (cfgC c (3 * k + 1 + r) 0) := by + obtain ⟨s, hs⟩ := loop1 c k 0 r + rw [show 0 + k + (r + 2 * k) + 1 = 3 * k + 1 + r by omega] at hs + exact ⟨_, nSteps_cons (div_start c (3 * k + 1) r) hs⟩ + +/-- Dividing `3 * k + 3` ones: digit `0`, quotient `k + 1`. -/ +theorem level_zero (c k r : ℕ) : + ∃ s, nSteps erdos14 s (divCfg c (3 * k + 3) r) = some (divCfg c (k + 1) (r + 2 * k + 2)) := by + obtain ⟨s, hs⟩ := loop2 c k 0 r + rw [show 0 + k + 1 = k + 1 by omega] at hs + exact ⟨_, nSteps_cons (div_start c (3 * k + 2) r) hs⟩ + +/-- Repeated division of the `q` ones before the hole either finds a digit `2` and reaches the +doubling phase, or finds none and reaches `q = 0`. -/ +theorem descend (c n : ℕ) : ∀ q r, q ≤ n → + (Has2 q ∧ ∃ s, nSteps erdos14 s (divCfg c q r) = some (cfgC c (q + r - 1) 0)) ∨ + (¬ Has2 q ∧ ∃ s, nSteps erdos14 s (divCfg c q r) = some (divCfg c 0 (q + r))) := by + induction n with + | zero => + intro q r hq + obtain rfl : q = 0 := by omega + exact Or.inr ⟨not_has2_zero, 0, by rw [Nat.zero_add]; rfl⟩ + | succ n ih => + intro q r hq + rcases Nat.eq_zero_or_pos q with rfl | hq0 + · exact Or.inr ⟨not_has2_zero, 0, by rw [Nat.zero_add]; rfl⟩ + obtain ⟨k, hk⟩ : ∃ k, q = 3 * k + 1 ∨ q = 3 * k + 2 ∨ q = 3 * k + 3 := + ⟨(q - 1) / 3, by omega⟩ + rcases hk with rfl | rfl | rfl + · obtain ⟨s₁, hs₁⟩ := level_one c k r + have hdiv : (3 * k + 1) / 3 = k := by omega + rcases ih k (r + 2 * k + 1) (by omega) with ⟨h2, s₂, hs₂⟩ | ⟨h2, s₂, hs₂⟩ + · refine Or.inl ⟨(has2_iff _).mpr (Or.inr (by rw [hdiv]; exact h2)), s₁ + s₂, ?_⟩ + rw [show 3 * k + 1 + r - 1 = k + (r + 2 * k + 1) - 1 by omega] + exact nSteps_bind_eq hs₁ hs₂ + · refine Or.inr ⟨fun h => ?_, s₁ + s₂, ?_⟩ + · rcases (has2_iff _).mp h with h | h + · omega + · rw [hdiv] at h + exact h2 h + · rw [show 3 * k + 1 + r = k + (r + 2 * k + 1) by omega] + exact nSteps_bind_eq hs₁ hs₂ + · obtain ⟨s₁, hs₁⟩ := level_two c k r + refine Or.inl ⟨(has2_iff _).mpr (Or.inl (by omega)), s₁, ?_⟩ + rw [show 3 * k + 2 + r - 1 = 3 * k + 1 + r by omega] + exact hs₁ + · obtain ⟨s₁, hs₁⟩ := level_zero c k r + have hdiv : (3 * k + 3) / 3 = k + 1 := by omega + rcases ih (k + 1) (r + 2 * k + 2) (by omega) with ⟨h2, s₂, hs₂⟩ | ⟨h2, s₂, hs₂⟩ + · refine Or.inl ⟨(has2_iff _).mpr (Or.inr (by rw [hdiv]; exact h2)), s₁ + s₂, ?_⟩ + rw [show 3 * k + 3 + r - 1 = k + 1 + (r + 2 * k + 2) - 1 by omega] + exact nSteps_bind_eq hs₁ hs₂ + · refine Or.inr ⟨fun h => ?_, s₁ + s₂, ?_⟩ + · rcases (has2_iff _).mp h with h | h + · omega + · rw [hdiv] at h + exact h2 h + · rw [show 3 * k + 3 + r = k + 1 + (r + 2 * k + 2) by omega] + exact nSteps_bind_eq hs₁ hs₂ + +/-! ## Counter (States `K`–`N`) -/ + +theorem counter_zero (X : ListBlank (Fin 2)) : + nSteps erdos14 6 ⟨3, Tape.mk' (CL 0) (X.cons 0)⟩ = some ⟨10, Tape.mk' (CL 1) (X.cons 1)⟩ := by + simp only [CL, CT] + tm_run + +theorem counter_one (X : ListBlank (Fin 2)) : + nSteps erdos14 14 ⟨3, Tape.mk' (CL 1) (X.cons 0)⟩ = some ⟨10, Tape.mk' (CL 2) (X.cons 1)⟩ := by + simp only [CL, CT] + tm_run + +theorem counter_two (X : ListBlank (Fin 2)) : + nSteps erdos14 3 ⟨3, Tape.mk' (CL 2) (X.cons 0)⟩ = + some ⟨12, ⟨1, B0.cons 1, ((X.cons 1).cons 0).cons 0⟩⟩ := by + simp only [CL, CT] + tm_run + +/-- A stage without a digit `2` advances the counter, then `K` runs to the end of the block. -/ +theorem counter_inc (c r : ℕ) (hc : c < 2) : + ∃ s, nSteps erdos14 s (divCfg c 0 (r + 1)) = some (cfgC (c + 1) r 0) := by + have h₁ : ∃ s, nSteps erdos14 s (divCfg c 0 (r + 1)) = + some ⟨10, Tape.mk' (CL (c + 1)) (ones (r + 2) B0)⟩ := by + rcases (by omega : c = 0 ∨ c = 1) with rfl | rfl + · exact ⟨6, counter_zero _⟩ + · exact ⟨14, counter_one _⟩ + obtain ⟨s₁, hs₁⟩ := h₁ + have h₂ := sweepR sK_1 (r + 2) (CL (c + 1)) B0 + exact ⟨_, nSteps_bind_eq hs₁ (nSteps_bind_eq h₂ (kl_finish (c + 1) r))⟩ + +/-- The third stage without a digit `2` halts. -/ +theorem counter_halt (r : ℕ) : + ∃ s cfg, nSteps erdos14 s (divCfg 2 0 r) = some cfg ∧ step erdos14 cfg = none := + ⟨3, _, counter_two _, sM_1 _ _⟩ + +/-! ## Stages -/ + +private theorem two_mul_pow (n : ℕ) : 0 + 2 * (2 ^ n + 0 - 1 + 1) = 2 ^ (n + 1) := by + have := Nat.two_pow_pos n + rw [pow_succ] + omega + +theorem stage_keep (c n : ℕ) (h : 2 ∈ pw n) : + ∃ s, 1 ≤ s ∧ nSteps erdos14 s (stageCfg c n) = some (stageCfg c (n + 1)) := by + rcases descend c (2 ^ n) (2 ^ n) 0 le_rfl with ⟨-, s₁, hs₁⟩ | ⟨hn, -⟩ + · obtain ⟨s₂, hs₂1, hs₂⟩ := dbl_loop c (2 ^ n + 0 - 1) 0 + rw [two_mul_pow] at hs₂ + exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + · exact absurd ((has2_pow n).mpr h) hn + +theorem stage_inc (c n : ℕ) (hc : c < 2) (h : 2 ∉ pw n) : + ∃ s, 1 ≤ s ∧ nSteps erdos14 s (stageCfg c n) = some (stageCfg (c + 1) (n + 1)) := by + rcases descend c (2 ^ n) (2 ^ n) 0 le_rfl with ⟨hn, -⟩ | ⟨-, s₁, hs₁⟩ + · exact absurd ((has2_pow n).mp hn) h + · have := Nat.two_pow_pos n + rw [show 2 ^ n + 0 = 2 ^ n + 0 - 1 + 1 by omega] at hs₁ + obtain ⟨s₂, hs₂⟩ := counter_inc c (2 ^ n + 0 - 1) hc + obtain ⟨s₃, hs₃1, hs₃⟩ := dbl_loop (c + 1) (2 ^ n + 0 - 1) 0 + rw [two_mul_pow] at hs₃ + exact ⟨s₁ + s₂ + s₃, by omega, nSteps_bind_eq (nSteps_bind_eq hs₁ hs₂) hs₃⟩ + +theorem stage_halt (n : ℕ) (h : 2 ∉ pw n) : + ∃ s cfg, nSteps erdos14 s (stageCfg 2 n) = some cfg ∧ step erdos14 cfg = none := by + rcases descend 2 (2 ^ n) (2 ^ n) 0 le_rfl with ⟨hn, -⟩ | ⟨-, s₁, hs₁⟩ + · exact absurd ((has2_pow n).mp hn) h + · obtain ⟨s₂, cfg, hs₂, hnone⟩ := counter_halt (2 ^ n + 0) + exact ⟨s₁ + s₂, cfg, nSteps_bind_eq hs₁ hs₂, hnone⟩ + +theorem init_eq : (init : Cfg 14 2) = ⟨0, Tape.mk' B0 B0⟩ := rfl + +/-- The boot writes `11` and starts the stage that checks `2 ^ 1`. -/ +theorem boot : nSteps erdos14 3 init = some (stageCfg 0 1) := by + rw [init_eq] + change nSteps erdos14 3 ⟨0, Tape.mk' B0 B0⟩ = + some ⟨3, Tape.mk' (CL 0) (((B0.cons 0).cons 1).cons 1)⟩ + simp only [CL, CT] + tm_run + +/-! ## Counting Powers Without a Digit `2` -/ + +theorem cnt_pos (n : ℕ) : 1 ≤ cnt n := by + induction n with + | zero => exact le_rfl + | succ n ih => + by_cases h : 2 ∈ pw (n + 1) + · rw [cnt_succ_of_mem h]; exact ih + · rw [cnt_succ_of_not_mem h]; omega + +theorem reach (n : ℕ) (hn : cnt n ≤ 3) : + ∃ s, n ≤ s ∧ nSteps erdos14 s init = some (stageCfg (cnt n - 1) (n + 1)) := by + induction n with + | zero => exact ⟨3, by omega, boot⟩ + | succ n ih => + have hpos := cnt_pos n + by_cases h : 2 ∈ pw (n + 1) + · rw [cnt_succ_of_mem h] at hn ⊢ + obtain ⟨s₁, hs₁n, hs₁⟩ := ih hn + obtain ⟨s₂, hs₂1, hs₂⟩ := stage_keep (cnt n - 1) (n + 1) h + exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + · rw [cnt_succ_of_not_mem h] at hn ⊢ + obtain ⟨s₁, hs₁n, hs₁⟩ := ih (by omega) + obtain ⟨s₂, hs₂1, hs₂⟩ := stage_inc (cnt n - 1) (n + 1) (by omega) h + refine ⟨s₁ + s₂, by omega, ?_⟩ + rw [show cnt n + 1 - 1 = cnt n - 1 + 1 by omega] + exact nSteps_bind_eq hs₁ hs₂ + +theorem halt_of (n : ℕ) (h3 : cnt n = 3) (h : 2 ∉ pw (n + 1)) : + ∃ s cfg, nSteps erdos14 s init = some cfg ∧ step erdos14 cfg = none := by + obtain ⟨s₁, -, hs₁⟩ := reach n (by omega) + rw [h3] at hs₁ + obtain ⟨s₂, cfg, hs₂, hnone⟩ := stage_halt (n + 1) h + exact ⟨s₁ + s₂, cfg, nSteps_bind_eq hs₁ hs₂, hnone⟩ + +/-! ## Halting Equivalence -/ + +/-- The 14-state machine `erdos14` (`erdos_14`) halts on the blank tape if and only if some +power `2 ^ n` with `n > 8` has no digit `2` in base `3`, with the digits computed by `pw`. -/ +theorem halts_erdos14_iff_exists_free : + ConjectureMachines.Halts erdos14 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n := by + unfold ConjectureMachines.Halts + constructor + · intro hdom + rw [Part.dom_iff_mem] at hdom + obtain ⟨b, hb⟩ := hdom + rw [mem_eval'] at hb + obtain ⟨hreach, hnone⟩ := hb + obtain ⟨k, hk⟩ := reaches_imp_nSteps hreach + rcases free_or_none (k + 9) with ⟨m, hm, -, hfree⟩ | hall + · exact ⟨m, hm, hfree⟩ + · have h3 := cnt_stays (k + 9) (by omega) hall + obtain ⟨s, hks, hs⟩ := reach (k + 9) (by omega) + rw [nSteps_eq_none_of_step_none s hk hnone (by omega)] at hs + cases hs + · rintro ⟨n, h8, hfree⟩ + obtain ⟨m, h3, hm⟩ := first_free n h8 hfree + obtain ⟨s, cfg, hs, hnone⟩ := halt_of m h3 hm + rw [Part.dom_iff_mem] + exact ⟨cfg, mem_eval'.mpr ⟨nSteps_reaches hs, hnone⟩⟩ + +/-- The 14-state machine halts on the blank tape if and only if the 15-state machine does. -/ +theorem candidate_equivalent : Halts candidate ↔ Halts reference := + halts_erdos14_iff_exists_free.trans Erdos15.halts_erdos15_iff_exists_free.symm + +/-- The candidate has one state fewer than the 15-state reference. -/ +theorem candidate_fewer_states : candidate.states < reference.states := by + decide +kernel + +end ConjectureMachines.Erdos14 diff --git a/Cryptids/Erdos15.lean b/Cryptids/Erdos15.lean new file mode 100644 index 00000000..fd9aad83 --- /dev/null +++ b/Cryptids/Erdos15.lean @@ -0,0 +1,545 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.Machines + +/-! +# Erdos15 + +The 15-state Turing machine `erdos_15` halts on the blank tape if and only if some power `2 ^ n` +with `n > 8` has no digit `2` in base `3`, i.e. if and only if Erdős's conjecture on the ternary +digits of powers of two is false. + +## Provenance and Attribution + +* Tristan Stérin and Damien Woods, *Hardness of busy beaver value BB(15)* + (, 2021): the 5-state, 4-symbol machine `powers_of_two_5_4` + and its 15-state, 2-symbol compilation `powers_of_two_15_2`, published in + (`machines/powers_of_two_15_2.txt`, commit `3f655ba2c73b`) and + mirrored at . The file is kept + verbatim in `baselines/sources/erdos_15_sterin_woods.txt`; `verify.py` re-derives + `baselines/tables/erdos_15.txt` from it and checks that they match: the start state `mul2_G_sim` + becomes `0`, the other states are numbered in order of appearance, and the blank symbol `b` + becomes `0` and `a` becomes `1`. Their correctness proof is on paper; this file gives a Lean + proof. + +## Machine Layout + +The machine simulates a 4-symbol machine whose symbols `0`, `1`, `2`, `#` are stored as cell +pairs `01`, `10`, `11`, `00`. Between two passes the tape reads, from left to right, +`[counter] # d₀ d₁ … dₖ`, where `d₀ … dₖ` are the base-3 digits of `2 ^ n`, least significant +first, and the counter cell holds `#`, `0`, `1` or `2` when `0`, `1`, `2` or `3` of the powers +`2 ^ 0, …, 2 ^ n` have no digit `2`. One pass doubles the number (states `0`–`3`, `7`–`9`), scans +the digits from the most significant one for a `2` (states `4`–`6`), returns to the first digit +(states `10`–`12`) and, if no `2` was found, increments the counter (states `13`, `14`). Some +states are shared: rewinding also uses `8`, and incrementing the counter also uses `8`, `9` and +`12`. The machine halts at the fourth power without a digit `2`; the first three are `2 ^ 0`, +`2 ^ 2` and `2 ^ 8`. +-/ + +@[expose] public section + +namespace ConjectureMachines.Erdos15 + +open Turing (Dir) +open StateTransition + +/-- 15-state Erdős powers-of-two machine (`erdos_15`, Stérin & Woods 2021). -/ +abbrev erdos15 : Machine 15 2 := Machines.erdos15 + +/-! ## Base-3 Doubling -/ + +/-- Doubles a base-3 digit list (least significant digit first) and adds the carry `c`. -/ +def dbl : List ℕ → ℕ → List ℕ + | [], c => if c = 0 then [] else [c] + | d :: ds, c => (2 * d + c) % 3 :: dbl ds ((2 * d + c) / 3) + +theorem dbl_lt (ds : List ℕ) (hds : ∀ d ∈ ds, d < 3) (c : ℕ) (hc : c ≤ 1) : + ∀ d ∈ dbl ds c, d < 3 := by + induction ds generalizing c with + | nil => + intro d hd + rcases (by omega : c = 0 ∨ c = 1) with rfl | rfl + · simp [dbl] at hd + · simp [dbl] at hd; omega + | cons x xs ih => + intro d hd + have hx := hds x (by simp) + simp only [dbl, List.mem_cons] at hd + rcases hd with rfl | hd + · omega + · exact ih (fun y hy => hds y (List.mem_cons_of_mem x hy)) _ (by omega) d hd + +/-- The base-3 digits of `2 ^ n`, computed by repeated doubling. -/ +def pw : ℕ → List ℕ + | 0 => [1] + | n + 1 => dbl (pw n) 0 + +theorem pw_lt (n : ℕ) : ∀ d ∈ pw n, d < 3 := by + induction n with + | zero => simp [pw] + | succ n ih => exact dbl_lt (pw n) ih 0 (by omega) + +/-- The number of `k ≤ n` such that `2 ^ k` has no digit `2` in base `3`. -/ +def cnt : ℕ → ℕ + | 0 => 1 + | n + 1 => cnt n + if 2 ∈ pw (n + 1) then 0 else 1 + +theorem cnt_succ_of_mem {n : ℕ} (h : 2 ∈ pw (n + 1)) : cnt (n + 1) = cnt n := by + simp [cnt, h] + +theorem cnt_succ_of_not_mem {n : ℕ} (h : 2 ∉ pw (n + 1)) : cnt (n + 1) = cnt n + 1 := by + simp [cnt, h] + +/-- `2 ^ 0 = 1`, `2 ^ 2 = 11₃` and `2 ^ 8 = 100111₃` are the only powers `2 ^ k` with `k ≤ 8` +without a digit `2`. -/ +theorem cnt_eight : cnt 8 = 3 := by decide + +/-! ## Tape Encoding -/ + +/-- Left cell of the pair encoding the digit `d` (`0 ↦ 01`, `1 ↦ 10`, `2 ↦ 11`). -/ +def hi : ℕ → Fin 2 + | 0 => 0 + | _ => 1 + +/-- Right cell of the pair encoding the digit `d`. -/ +def lo : ℕ → Fin 2 + | 1 => 0 + | _ => 1 + +@[simp] theorem hi_zero : hi 0 = 0 := rfl +@[simp] theorem hi_one : hi 1 = 1 := rfl +@[simp] theorem hi_two : hi 2 = 1 := rfl +@[simp] theorem lo_zero : lo 0 = 1 := rfl +@[simp] theorem lo_one : lo 1 = 0 := rfl +@[simp] theorem lo_two : lo 2 = 1 := rfl + +/-- The cells of a digit list, read from left to right. -/ +def encR : List ℕ → List (Fin 2) + | [] => [] + | d :: ds => hi d :: lo d :: encR ds + +/-- The cells of a digit list, read from right to left. -/ +def encL : List ℕ → List (Fin 2) + | [] => [] + | d :: ds => encL ds ++ [lo d, hi d] + +/-- Left cell of the counter pair (`0 ↦ 00`, `1 ↦ 01`, `2 ↦ 10`, `3 ↦ 11`). -/ +def chi : ℕ → Fin 2 + | 0 => 0 + | 1 => 0 + | _ => 1 + +/-- Right cell of the counter pair. -/ +def clo : ℕ → Fin 2 + | 1 => 1 + | 3 => 1 + | _ => 0 + +def B0 : ListBlank (Fin 2) := ListBlank.mk [] + +theorem B0_cons_zero : B0.cons 0 = B0 := + Quot.sound (Or.inr ⟨1, rfl⟩) + +/-- Head on the first cell of `L`. -/ +def Tape.mkL (L R : ListBlank (Fin 2)) : Tape (Fin 2) := + ⟨L.head, L.tail, R⟩ + +@[simp] +theorem Tape.mkL_cons (a : Fin 2) (L R : ListBlank (Fin 2)) : + Tape.mkL (L.cons a) R = ⟨a, L, R⟩ := by + simp [Tape.mkL] + +@[simp] +theorem Tape.mk'_cons (a : Fin 2) (L R : ListBlank (Fin 2)) : + Tape.mk' L (R.cons a) = ⟨a, L, R⟩ := by + simp [Tape.mk'] + +@[simp] +theorem Tape.mk'_B0 (L : ListBlank (Fin 2)) : Tape.mk' L B0 = ⟨0, L, B0⟩ := + rfl + +/-- The cells left of the first digit: the `#` pair, then the counter pair. -/ +def LH (c : ℕ) : ListBlank (Fin 2) := + ListBlank.append [0, 0, clo c, chi c] B0 + +/-- Start of the pass that doubles `2 ^ n`, with counter `c`. -/ +def stageCfg (c n : ℕ) : Cfg 15 2 := + ⟨1, Tape.mk' (LH c) (ListBlank.append (encR (pw n)) B0)⟩ + +/-! ## Step Infrastructure -/ + +def nSteps (M : Machine 15 2) (n : ℕ) : Cfg 15 2 → Option (Cfg 15 2) := + Nat.rec (motive := fun _ => Cfg 15 2 → Option (Cfg 15 2)) + (fun c => some c) + (fun _ ih c => (step M c).bind ih) + n + +@[simp] +theorem nSteps_zero (M : Machine 15 2) (c : Cfg 15 2) : + nSteps M 0 c = some c := rfl + +@[simp] +theorem nSteps_succ (M : Machine 15 2) (n : ℕ) (c : Cfg 15 2) : + nSteps M (n + 1) c = (step M c).bind (nSteps M n) := rfl + +attribute [eqns nSteps_zero nSteps_succ] nSteps + +theorem nSteps_reaches {M : Machine 15 2} {n : ℕ} {c c' : Cfg 15 2} + (h : nSteps M n c = some c') : Reaches (step M) c c' := by + induction n generalizing c with + | zero => + injection h with h' + subst h' + exact Relation.ReflTransGen.refl + | succ n ih => + simp only [nSteps, Option.bind_eq_some_iff] at h + obtain ⟨c₁, hstep, hrest⟩ := h + exact Relation.ReflTransGen.head hstep (ih hrest) + +theorem nSteps_add {M : Machine 15 2} (m n : ℕ) (c : Cfg 15 2) : + nSteps M (m + n) c = (nSteps M m c).bind (nSteps M n) := by + induction m generalizing c with + | zero => simp [nSteps] + | succ m ih => + rw [Nat.succ_add, nSteps, nSteps] + cases step M c <;> simp [ih] + +theorem nSteps_bind_eq {M : Machine 15 2} {m n : ℕ} {c c₁ c₂ : Cfg 15 2} + (h₁ : nSteps M m c = some c₁) (h₂ : nSteps M n c₁ = some c₂) : + nSteps M (m + n) c = some c₂ := by + rw [nSteps_add, h₁, Option.bind_some, h₂] + +theorem step_one {M : Machine 15 2} {c c₁ : Cfg 15 2} (h : step M c = some c₁) : + nSteps M 1 c = some c₁ := by + rw [nSteps, h]; rfl + +theorem reaches_imp_nSteps {M : Machine 15 2} {a b : Cfg 15 2} + (h : Reaches (step M) a b) : ∃ k, nSteps M k a = some b := by + induction h with + | refl => exact ⟨0, rfl⟩ + | tail _ hstep ih => + obtain ⟨k, hk⟩ := ih + exact ⟨k + 1, nSteps_bind_eq hk (step_one hstep)⟩ + +theorem nSteps_eq_none_of_step_none {M : Machine 15 2} {k : ℕ} (s : ℕ) {a b : Cfg 15 2} + (hk : nSteps M k a = some b) (hnone : step M b = none) (hks : k < s) : + nSteps M s a = none := by + have hs : s = k + ((s - k - 1) + 1) := by omega + rw [hs, nSteps_add, hk, Option.bind_some, nSteps_succ, hnone, Option.bind_none] + +/-! ## Transition Table -/ + +theorem stepR {q q' : Fin 15} {a b : Fin 2} (h : erdos15.transition q a = some (b, .right, q')) + (L R : ListBlank (Fin 2)) : + step erdos15 ⟨q, ⟨a, L, R⟩⟩ = some ⟨q', Tape.mk' (L.cons b) R⟩ := by + simp only [step, h, Option.map_some]; rfl + +theorem stepL {q q' : Fin 15} {a b : Fin 2} (h : erdos15.transition q a = some (b, .left, q')) + (L R : ListBlank (Fin 2)) : + step erdos15 ⟨q, ⟨a, L, R⟩⟩ = some ⟨q', Tape.mkL L (R.cons b)⟩ := by + simp only [step, h, Option.map_some]; rfl + +theorem s0_0 (L R) : step erdos15 ⟨0, ⟨0, L, R⟩⟩ = some ⟨8, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem s0_1 (L R) : step erdos15 ⟨0, ⟨1, L, R⟩⟩ = some ⟨7, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem s1_0 (L R) : step erdos15 ⟨1, ⟨0, L, R⟩⟩ = some ⟨3, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem s1_1 (L R) : step erdos15 ⟨1, ⟨1, L, R⟩⟩ = some ⟨2, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem s2_0 (L R) : step erdos15 ⟨2, ⟨0, L, R⟩⟩ = some ⟨1, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem s2_1 (L R) : step erdos15 ⟨2, ⟨1, L, R⟩⟩ = some ⟨0, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem s3_0 (L R) : step erdos15 ⟨3, ⟨0, L, R⟩⟩ = some ⟨5, Tape.mkL L (R.cons 0)⟩ := stepL rfl L R +theorem s3_1 (L R) : step erdos15 ⟨3, ⟨1, L, R⟩⟩ = some ⟨1, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem s4_0 (L R) : step erdos15 ⟨4, ⟨0, L, R⟩⟩ = some ⟨6, Tape.mkL L (R.cons 0)⟩ := stepL rfl L R +theorem s4_1 (L R) : step erdos15 ⟨4, ⟨1, L, R⟩⟩ = some ⟨5, Tape.mkL L (R.cons 1)⟩ := stepL rfl L R +theorem s5_0 (L R) : step erdos15 ⟨5, ⟨0, L, R⟩⟩ = some ⟨4, Tape.mkL L (R.cons 0)⟩ := stepL rfl L R +theorem s5_1 (L R) : step erdos15 ⟨5, ⟨1, L, R⟩⟩ = some ⟨10, Tape.mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem s6_0 (L R) : step erdos15 ⟨6, ⟨0, L, R⟩⟩ = some ⟨13, Tape.mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem s6_1 (L R) : step erdos15 ⟨6, ⟨1, L, R⟩⟩ = some ⟨4, Tape.mkL L (R.cons 1)⟩ := stepL rfl L R +theorem s7_0 (L R) : step erdos15 ⟨7, ⟨0, L, R⟩⟩ = some ⟨9, Tape.mkL L (R.cons 1)⟩ := stepL rfl L R +theorem s7_1 (L R) : step erdos15 ⟨7, ⟨1, L, R⟩⟩ = some ⟨0, Tape.mk' (L.cons 1) R⟩ := stepR rfl L R +theorem s8_0 (L R) : step erdos15 ⟨8, ⟨0, L, R⟩⟩ = some ⟨1, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem s8_1 (L R) : step erdos15 ⟨8, ⟨1, L, R⟩⟩ = some ⟨1, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem s9_0 (L R) : step erdos15 ⟨9, ⟨0, L, R⟩⟩ = some ⟨12, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem s9_1 (L R) : step erdos15 ⟨9, ⟨1, L, R⟩⟩ = some ⟨7, Tape.mk' (L.cons 0) R⟩ := stepR rfl L R +theorem s10_0 (L R) : step erdos15 ⟨10, ⟨0, L, R⟩⟩ = some ⟨12, Tape.mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem s10_1 (L R) : step erdos15 ⟨10, ⟨1, L, R⟩⟩ = some ⟨11, Tape.mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem s11_0 (L R) : step erdos15 ⟨11, ⟨0, L, R⟩⟩ = some ⟨10, Tape.mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem s11_1 (L R) : step erdos15 ⟨11, ⟨1, L, R⟩⟩ = some ⟨10, Tape.mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem s12_0 (L R) : step erdos15 ⟨12, ⟨0, L, R⟩⟩ = some ⟨8, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem s12_1 (L R) : step erdos15 ⟨12, ⟨1, L, R⟩⟩ = some ⟨10, Tape.mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem s13_0 (L R) : step erdos15 ⟨13, ⟨0, L, R⟩⟩ = some ⟨12, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem s13_1 (L R) : step erdos15 ⟨13, ⟨1, L, R⟩⟩ = some ⟨14, Tape.mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem s14_0 (L R) : step erdos15 ⟨14, ⟨0, L, R⟩⟩ = some ⟨9, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R + +theorem s14_1 (L R : ListBlank (Fin 2)) : step erdos15 ⟨14, ⟨1, L, R⟩⟩ = none := rfl + +/-- Runs the machine through a fixed sequence of steps on a concrete tape. -/ +local macro "tm_run" : tactic => `(tactic| simp only [nSteps_succ, nSteps_zero, Option.bind_some, + s0_0, s0_1, s1_0, s1_1, s2_0, s2_1, s3_0, s3_1, s4_0, s4_1, s5_0, s5_1, s6_0, s6_1, s7_0, + s7_1, s8_0, s8_1, s9_0, s9_1, s10_0, s10_1, s11_0, s11_1, s12_0, s12_1, s13_0, s13_1, s14_0, + Tape.mk'_cons, Tape.mkL_cons, Tape.mk'_B0, ListBlank.append, hi_zero, hi_one, hi_two, lo_zero, + lo_one, lo_two]) + +/-! ## Doubling Pass (States `0`–`3`, `7`–`9`) -/ + +/-- The doubling state for carry `c`: `mul2_F` (`1`) for carry `0`, `mul2_G` (`0`) for carry `1`. -/ +def st : ℕ → Fin 15 + | 0 => 1 + | _ => 0 + +theorem digit_step (d c : ℕ) (hd : d < 3) (hc : c ≤ 1) (L R : ListBlank (Fin 2)) : + ∃ s, nSteps erdos15 s ⟨st c, ⟨hi d, L, R.cons (lo d)⟩⟩ = + some ⟨st ((2 * d + c) / 3), + Tape.mk' (ListBlank.append [lo ((2 * d + c) % 3), hi ((2 * d + c) % 3)] L) R⟩ := by + rcases (by omega : d = 0 ∨ d = 1 ∨ d = 2) with rfl | rfl | rfl <;> + rcases (by omega : c = 0 ∨ c = 1) with rfl | rfl <;> + simp only [st, Nat.reduceMul, Nat.reduceAdd, Nat.reduceMod, Nat.reduceDiv] + · exact ⟨2, by tm_run⟩ + · exact ⟨2, by tm_run⟩ + · exact ⟨2, by tm_run⟩ + · exact ⟨4, by tm_run⟩ + · exact ⟨2, by tm_run⟩ + · exact ⟨2, by tm_run⟩ + +theorem blank_step (L : ListBlank (Fin 2)) : + nSteps erdos15 3 ⟨1, Tape.mk' L B0⟩ = some ⟨4, Tape.mkL L B0⟩ := by + tm_run + rw [B0_cons_zero, B0_cons_zero] + +/-- One pass doubles the digit list `ds` with carry `c`; it ends in state `4` on the right cell +of the most significant digit. -/ +theorem mul2_pass (ds : List ℕ) (hds : ∀ d ∈ ds, d < 3) (c : ℕ) (hc : c ≤ 1) + (L : ListBlank (Fin 2)) : + ∃ s, nSteps erdos15 s ⟨st c, Tape.mk' L (ListBlank.append (encR ds) B0)⟩ = + some ⟨4, Tape.mkL (ListBlank.append (encL (dbl ds c)) L) B0⟩ := by + induction ds generalizing c L with + | nil => + rcases (by omega : c = 0 ∨ c = 1) with rfl | rfl + · exact ⟨3, blank_step L⟩ + · refine ⟨2 + 3, nSteps_bind_eq (c₁ := ⟨1, Tape.mk' ((L.cons 1).cons 0) B0⟩) ?_ ?_⟩ + · simp only [st, encR, ListBlank.append]; tm_run + · exact blank_step _ + | cons d ds ih => + have hd := hds d (by simp) + obtain ⟨s₁, hs₁⟩ := digit_step d c hd hc L (ListBlank.append (encR ds) B0) + obtain ⟨s₂, hs₂⟩ := ih (fun x hx => hds x (by simp [hx])) ((2 * d + c) / 3) (by omega) + (ListBlank.append [lo ((2 * d + c) % 3), hi ((2 * d + c) % 3)] L) + have e : ListBlank.append (encL (dbl (d :: ds) c)) L = + ListBlank.append (encL (dbl ds ((2 * d + c) / 3))) + (ListBlank.append [lo ((2 * d + c) % 3), hi ((2 * d + c) % 3)] L) := by + simp only [dbl, encL, ListBlank.append_assoc] + rw [e] + refine ⟨s₁ + s₂, nSteps_bind_eq ?_ hs₂⟩ + simpa only [encR, ListBlank.append, Tape.mk'_cons] using hs₁ + +/-! ## Search for a `2` (States `4`–`6`, `10`–`12`) -/ + +theorem pair_scan (q : Fin 15) (hq : q = 4 ∨ q = 10) (d : ℕ) (hd : d < 3) + (L R : ListBlank (Fin 2)) : + nSteps erdos15 2 ⟨q, ⟨lo d, L.cons (hi d), R⟩⟩ = + some ⟨if q = 10 ∨ d = 2 then 10 else 4, Tape.mkL L ((R.cons (lo d)).cons (hi d))⟩ := by + rcases hq with rfl | rfl <;> rcases (by omega : d = 0 ∨ d = 1 ∨ d = 2) with rfl | rfl | rfl <;> + tm_run <;> simp + +/-- Scanning left over `ds` from its most significant digit finds a `2` iff `2 ∈ ds`; after a +`2` the machine keeps moving left in the rewind states. -/ +theorem find2_scan (ds : List ℕ) (hds : ∀ d ∈ ds, d < 3) (L R : ListBlank (Fin 2)) : + nSteps erdos15 (2 * ds.length) ⟨4, Tape.mkL (ListBlank.append (encL ds) L) R⟩ = + some ⟨if 2 ∈ ds then 10 else 4, Tape.mkL L (ListBlank.append (encR ds) R)⟩ := by + induction ds generalizing L with + | nil => simp [encL, encR] + | cons d ds ih => + have hd := hds d (by simp) + have h₁ := ih (fun x hx => hds x (by simp [hx])) + (ListBlank.append [lo d, hi d] L) + rw [show 2 * (d :: ds).length = 2 * ds.length + 2 by rw [List.length_cons]; omega, encL, + ListBlank.append_assoc, nSteps_add, h₁, Option.bind_some] + have hq : (if 2 ∈ ds then (10 : Fin 15) else 4) = 4 ∨ + (if 2 ∈ ds then (10 : Fin 15) else 4) = 10 := by + by_cases h : 2 ∈ ds <;> simp [h] + simp only [ListBlank.append, Tape.mkL_cons] + rw [pair_scan _ hq d hd] + congr 2 + by_cases h₂ : 2 ∈ ds <;> by_cases hd₂ : d = 2 <;> simp [h₂, hd₂, eq_comm] + +/-! ## The `#` Cell and the Counter -/ + +theorem hash_rewind (c : ℕ) (R : ListBlank (Fin 2)) : + nSteps erdos15 3 ⟨10, Tape.mkL (LH c) R⟩ = some ⟨1, Tape.mk' (LH c) R⟩ := by + simp only [LH, ListBlank.append, Tape.mkL_cons] + tm_run + +theorem hash_find (c : ℕ) (R : ListBlank (Fin 2)) : + nSteps erdos15 2 ⟨4, Tape.mkL (LH c) R⟩ = + some ⟨13, Tape.mkL (ListBlank.append [clo c, chi c] B0) ((R.cons 0).cons 0)⟩ := by + simp only [LH, ListBlank.append, Tape.mkL_cons] + tm_run + +theorem counter_inc (c : ℕ) (hc : c < 3) (R : ListBlank (Fin 2)) : + ∃ s, nSteps erdos15 s + ⟨13, Tape.mkL (ListBlank.append [clo c, chi c] B0) ((R.cons 0).cons 0)⟩ = + some ⟨1, Tape.mk' (LH (c + 1)) R⟩ := by + rcases (by omega : c = 0 ∨ c = 1 ∨ c = 2) with rfl | rfl | rfl + · exact ⟨3, by simp only [LH, clo, chi, ListBlank.append, Tape.mkL_cons]; tm_run⟩ + · exact ⟨5, by simp only [LH, clo, chi, ListBlank.append, Tape.mkL_cons]; tm_run⟩ + · exact ⟨3, by simp only [LH, clo, chi, ListBlank.append, Tape.mkL_cons]; tm_run⟩ + +theorem counter_halt (R : ListBlank (Fin 2)) : + ∃ cfg, nSteps erdos15 1 + ⟨13, Tape.mkL (ListBlank.append [clo 3, chi 3] B0) ((R.cons 0).cons 0)⟩ = some cfg ∧ + step erdos15 cfg = none := by + refine ⟨⟨14, ⟨1, B0, (((R.cons 0).cons 0).cons 0)⟩⟩, ?_, s14_1 _ _⟩ + simp only [clo, chi, ListBlank.append, Tape.mkL_cons] + tm_run + +/-! ## Stages -/ + +theorem stage_scan (c n : ℕ) : + ∃ s, nSteps erdos15 s (stageCfg c n) = some + ⟨if 2 ∈ pw (n + 1) then 10 else 4, + Tape.mkL (LH c) (ListBlank.append (encR (pw (n + 1))) B0)⟩ := by + obtain ⟨s₁, hs₁⟩ := mul2_pass (pw n) (pw_lt n) 0 (by omega) (LH c) + have h₂ := find2_scan (pw (n + 1)) (pw_lt (n + 1)) (LH c) B0 + exact ⟨s₁ + 2 * (pw (n + 1)).length, nSteps_bind_eq hs₁ h₂⟩ + +theorem stage_keep (c n : ℕ) (h : 2 ∈ pw (n + 1)) : + ∃ s, 1 ≤ s ∧ nSteps erdos15 s (stageCfg c n) = some (stageCfg c (n + 1)) := by + obtain ⟨s₁, hs₁⟩ := stage_scan c n + simp only [h, ↓reduceIte] at hs₁ + exact ⟨s₁ + 3, by omega, nSteps_bind_eq hs₁ (hash_rewind c _)⟩ + +theorem stage_inc (c n : ℕ) (hc : c < 3) (h : 2 ∉ pw (n + 1)) : + ∃ s, 1 ≤ s ∧ nSteps erdos15 s (stageCfg c n) = some (stageCfg (c + 1) (n + 1)) := by + obtain ⟨s₁, hs₁⟩ := stage_scan c n + simp only [h, ↓reduceIte] at hs₁ + obtain ⟨s₃, hs₃⟩ := counter_inc c hc (ListBlank.append (encR (pw (n + 1))) B0) + exact ⟨s₁ + 2 + s₃, by omega, + nSteps_bind_eq (nSteps_bind_eq hs₁ (hash_find c _)) hs₃⟩ + +theorem stage_halt (n : ℕ) (h : 2 ∉ pw (n + 1)) : + ∃ s cfg, nSteps erdos15 s (stageCfg 3 n) = some cfg ∧ step erdos15 cfg = none := by + obtain ⟨s₁, hs₁⟩ := stage_scan 3 n + simp only [h, ↓reduceIte] at hs₁ + obtain ⟨cfg, hcfg, hnone⟩ := counter_halt (ListBlank.append (encR (pw (n + 1))) B0) + exact ⟨s₁ + 2 + 1, cfg, nSteps_bind_eq (nSteps_bind_eq hs₁ (hash_find 3 _)) hcfg, hnone⟩ + +theorem init_eq : (init : Cfg 15 2) = ⟨st 1, Tape.mk' (LH 0) (ListBlank.append (encR []) B0)⟩ := by + have : LH 0 = ListBlank.mk [] := Quot.sound (Or.inr ⟨4, rfl⟩) + rw [this] + rfl + +theorem boot : ∃ s, nSteps erdos15 s init = some (stageCfg 1 0) := by + obtain ⟨s₁, hs₁⟩ := mul2_pass [] (by simp) 1 (by omega) (LH 0) + have h₂ := find2_scan (dbl [] 1) (by simp [dbl]) (LH 0) B0 + simp only [show 2 ∉ dbl [] 1 by simp [dbl], ↓reduceIte] at h₂ + obtain ⟨s₃, hs₃⟩ := counter_inc 0 (by omega) (ListBlank.append (encR (dbl [] 1)) B0) + rw [init_eq] + exact ⟨s₁ + _ + 2 + s₃, + nSteps_bind_eq (nSteps_bind_eq (nSteps_bind_eq hs₁ h₂) (hash_find 0 _)) hs₃⟩ + +/-! ## Counting Powers Without a Digit `2` -/ + +theorem reach (n : ℕ) (hn : cnt n ≤ 3) : + ∃ s, n ≤ s ∧ nSteps erdos15 s init = some (stageCfg (cnt n) n) := by + induction n with + | zero => + obtain ⟨s, hs⟩ := boot + exact ⟨s, Nat.zero_le s, hs⟩ + | succ n ih => + by_cases h : 2 ∈ pw (n + 1) + · rw [cnt_succ_of_mem h] at hn ⊢ + obtain ⟨s₁, hs₁n, hs₁⟩ := ih hn + obtain ⟨s₂, hs₂1, hs₂⟩ := stage_keep (cnt n) n h + exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + · rw [cnt_succ_of_not_mem h] at hn ⊢ + obtain ⟨s₁, hs₁n, hs₁⟩ := ih (by omega) + obtain ⟨s₂, hs₂1, hs₂⟩ := stage_inc (cnt n) n (by omega) h + exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + +theorem halt_of (n : ℕ) (h3 : cnt n = 3) (h : 2 ∉ pw (n + 1)) : + ∃ s cfg, nSteps erdos15 s init = some cfg ∧ step erdos15 cfg = none := by + obtain ⟨s₁, -, hs₁⟩ := reach n (by omega) + rw [h3] at hs₁ + obtain ⟨s₂, cfg, hs₂, hnone⟩ := stage_halt n h + exact ⟨s₁ + s₂, cfg, nSteps_bind_eq hs₁ hs₂, hnone⟩ + +theorem cnt_stays (K : ℕ) (hK : 8 ≤ K) (hall : ∀ m, 8 < m → m ≤ K → 2 ∈ pw m) : cnt K = 3 := by + induction K, hK using Nat.le_induction with + | base => exact cnt_eight + | succ K hK ih => + rw [cnt_succ_of_mem (hall (K + 1) (by omega) le_rfl)] + exact ih fun m hm hmK => hall m hm (by omega) + +theorem first_free (n : ℕ) (h8 : 8 < n) (h : 2 ∉ pw n) : + ∃ m, cnt m = 3 ∧ 2 ∉ pw (m + 1) := by + have key : ∀ j, 8 ≤ j → cnt j = 3 ∨ ∃ m, cnt m = 3 ∧ 2 ∉ pw (m + 1) := by + intro j hj + induction j, hj using Nat.le_induction with + | base => exact Or.inl cnt_eight + | succ j _ ih => + rcases ih with h3 | hm + · by_cases hj2 : 2 ∈ pw (j + 1) + · exact Or.inl (by rw [cnt_succ_of_mem hj2, h3]) + · exact Or.inr ⟨j, h3, hj2⟩ + · exact Or.inr hm + rcases key (n - 1) (by omega) with h3 | hm + · exact ⟨n - 1, h3, by rwa [Nat.sub_add_cancel (by omega)]⟩ + · exact hm + +theorem free_or_none (K : ℕ) : + (∃ m, 8 < m ∧ m ≤ K ∧ 2 ∉ pw m) ∨ (∀ m, 8 < m → m ≤ K → 2 ∈ pw m) := by + induction K with + | zero => exact Or.inr fun m hm hmK => absurd hmK (by omega) + | succ K ih => + rcases ih with ⟨m, hm, hmK, hfree⟩ | hall + · exact Or.inl ⟨m, hm, by omega, hfree⟩ + · by_cases h : 2 ∈ pw (K + 1) + · refine Or.inr fun m hm hmK => ?_ + rcases (by omega : m ≤ K ∨ m = K + 1) with hmK' | rfl + · exact hall m hm hmK' + · exact h + · by_cases hK : 8 < K + 1 + · exact Or.inl ⟨K + 1, hK, le_rfl, h⟩ + · exact Or.inr fun m hm hmK => absurd hm (by omega) + +/-! ## Halting Equivalence -/ + +/-- The 15-state machine `erdos15` (`erdos_15`) halts on the blank tape if and only if some +power `2 ^ n` with `n > 8` has no digit `2` in base `3`, with the digits computed by `pw`. -/ +theorem halts_erdos15_iff_exists_free : + ConjectureMachines.Halts erdos15 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n := by + unfold ConjectureMachines.Halts + constructor + · intro hdom + rw [Part.dom_iff_mem] at hdom + obtain ⟨b, hb⟩ := hdom + rw [mem_eval'] at hb + obtain ⟨hreach, hnone⟩ := hb + obtain ⟨k, hk⟩ := reaches_imp_nSteps hreach + rcases free_or_none (k + 9) with ⟨m, hm, -, hfree⟩ | hall + · exact ⟨m, hm, hfree⟩ + · have h3 := cnt_stays (k + 9) (by omega) hall + obtain ⟨s, hks, hs⟩ := reach (k + 9) (by omega) + rw [nSteps_eq_none_of_step_none s hk hnone (by omega)] at hs + cases hs + · rintro ⟨n, h8, hfree⟩ + obtain ⟨m, h3, hm⟩ := first_free n h8 hfree + obtain ⟨s, cfg, hs, hnone⟩ := halt_of m h3 hm + rw [Part.dom_iff_mem] + exact ⟨cfg, mem_eval'.mpr ⟨nSteps_reaches hs, hnone⟩⟩ + +end ConjectureMachines.Erdos15 diff --git a/Cryptids/Machines.lean b/Cryptids/Machines.lean index d2bcc047..1bf5e2e2 100644 --- a/Cryptids/Machines.lean +++ b/Cryptids/Machines.lean @@ -225,6 +225,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 attribute [-simp] Nat.add_eq_right Order.add_one_le_iff Order.lt_add_one_iff diff --git a/Cryptids/Propositions.lean b/Cryptids/Propositions.lean index 9aac66a6..0f026f9e 100644 --- a/Cryptids/Propositions.lean +++ b/Cryptids/Propositions.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 public import Cryptids.Machines /-! @@ -35,6 +36,8 @@ constructions and halting proofs: `10fcf152b3`), which differs from `ZFProvable` in clauses `B6a`, `B8a`, and `B8c` due to a register-restoration bug in `B6a` (`main().n_140.1` restoring `scratch1` into `param1` instead of `param3`). +4. **Erdős's Conjecture on Powers of Two** (`ErdosPowersOfTwoConjecture`): + For every `n > 8`, the base-3 expansion of `2 ^ n` contains the digit `2` (`erdos_15`). -/ @[expose] public section @@ -693,4 +696,11 @@ def paZFInconsistent : PAFormula := (.and (paBetaEq (.var 1) (.var 2) (.var 0) (.var 4)) ((pzMem (.const 0) (.const 0)).eqFormula (.var 4) 10)))))) +/-! ## 5. Erdős's Conjecture on Powers of Two -/ + +/-- **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) + end ConjectureMachines diff --git a/Cryptids/README.md b/Cryptids/README.md index 4d1fec4a..3860cad1 100644 --- a/Cryptids/README.md +++ b/Cryptids/README.md @@ -1,6 +1,6 @@ # Certified State Reductions and Semantics of Conjecture-Checking Turing Machines (`Cryptids/`) -This library contains formally verified 2-symbol Turing machines and Lean 4 semantics proofs for **Goldbach's Conjecture**, **ZF Set Theory Consistency**, and the **Riemann Hypothesis**, developed by Maxence Faldor and Moritz Firsching using Gemini Argon. +This library contains formally verified 2-symbol Turing machines and Lean 4 semantics proofs for **Goldbach's Conjecture**, **ZF Set Theory Consistency**, and the **Riemann Hypothesis**, developed by Maxence Faldor and Moritz Firsching using Gemini Argon. The `erdos_15` and `erdos_14` formalizations (Erdős's conjecture on powers of two) are by Daniel Veljjanoski, with Claude (Anthropic) as assistant. ## Formalized Machines @@ -14,6 +14,8 @@ This library contains formally verified 2-symbol Turing machines and Lean 4 sema | Riemann Hypothesis | `riemann_104` | `104` | Reduced from `riemann_120` (`120` states, Shunia Sept 2026) | `¬ RiemannHypothesis` | [`Riemann104.lean`](./Riemann104.lean), [`Semantics/Riemann120.lean`](./Semantics/Riemann120.lean) | | Riemann Hypothesis | `riemann_120` | `120` | Joseph M. Shunia ([`arXiv:2609.30306`](https://arxiv.org/abs/2609.30306), Sept 2026) | `¬ RiemannHypothesis` | [`Riemann120.lean`](./Riemann120.lean), [`Semantics/Riemann120.lean`](./Semantics/Riemann120.lean) | | Riemann Hypothesis | `riemann_744` | `744` | Matiyasevich, O'Rear & Aaronson (`riemann_744_sorear.tm`, 2016) | `¬ RiemannHypothesis` | [`Semantics/Riemann.lean`](./Semantics/Riemann.lean) | +| Erdős's conjecture on powers of two | `erdos_14` | `14` | Tristan Stérin ([bbchallenge Discord](https://discord.com/channels/960643023006490684/1561295445312151622/1562203343114473472), Oct 2026; [Cryptids wiki](https://wiki.bbchallenge.org/w/index.php?title=Cryptids&oldid=9722)) | `¬ ErdosPowersOfTwoConjecture` | [`Erdos14.lean`](./Erdos14.lean), [`Semantics/Erdos14.lean`](./Semantics/Erdos14.lean) | +| Erdős's conjecture on powers of two | `erdos_15` | `15` | Tristan Stérin & Damien Woods ([`arXiv:2107.12475`](https://arxiv.org/abs/2107.12475), 2021) | `¬ ErdosPowersOfTwoConjecture` | [`Erdos15.lean`](./Erdos15.lean), [`Semantics/Erdos15.lean`](./Semantics/Erdos15.lean) | See [`RELATED_WORK.md`](../RELATED_WORK.md) for the historical progression across each domain. @@ -21,11 +23,12 @@ See [`RELATED_WORK.md`](../RELATED_WORK.md) for the historical progression acros All proofs in [`Cryptids/`](./) are checked by the Lean 4 kernel (`v4.35.0-rc4`) without `sorry`: -1. **State reductions:** Each reduced machine (`goldbach_21`, `zf_380`, `riemann_104`, `riemann_95`) has fewer states than its reference machine (`goldbach_25`, `zf_393`, `riemann_120`, `riemann_104`) and halts from the blank tape if and only if the reference machine halts ([`Goldbach21.lean`](./Goldbach21.lean), [`Zf380.lean`](./Zf380.lean), [`Riemann104.lean`](./Riemann104.lean), [`Riemann95.lean`](./Riemann95.lean)). The direct simulation reductions (`goldbach_21`, `zf_380`, `riemann_104`) and all four `candidate_fewer_states` theorems are completely constructive (`["propext", "Quot.sound"]`, zero `Classical.choice`), audited via [`comparator/constructive.json`](../comparator/constructive.json), [`comparator/goldbach_21.json`](../comparator/goldbach_21.json), [`comparator/zf_380.json`](../comparator/zf_380.json), and [`comparator/riemann_104.json`](../comparator/riemann_104.json), while [`riemann_95`](./Riemann95.lean) routes through the arithmetic stage predicate `ShuniaCounterexample` (`Nat.Prime`, audited via [`comparator/riemann_95.json`](../comparator/riemann_95.json)). +1. **State reductions:** Each reduced machine (`goldbach_21`, `zf_380`, `riemann_104`, `riemann_95`, `erdos_14`) has fewer states than its reference machine (`goldbach_25`, `zf_393`, `riemann_120`, `riemann_104`, `erdos_15`) and halts from the blank tape if and only if the reference machine halts ([`Goldbach21.lean`](./Goldbach21.lean), [`Zf380.lean`](./Zf380.lean), [`Riemann104.lean`](./Riemann104.lean), [`Riemann95.lean`](./Riemann95.lean), [`Erdos14.lean`](./Erdos14.lean)). The direct simulation reductions (`goldbach_21`, `zf_380`, `riemann_104`), the `erdos_14` reduction, and all five `candidate_fewer_states` theorems are completely constructive (`["propext", "Quot.sound"]`, zero `Classical.choice`), audited via [`comparator/constructive.json`](../comparator/constructive.json), [`comparator/goldbach_21.json`](../comparator/goldbach_21.json), [`comparator/zf_380.json`](../comparator/zf_380.json), and [`comparator/riemann_104.json`](../comparator/riemann_104.json), while [`riemann_95`](./Riemann95.lean) routes through the arithmetic stage predicate `ShuniaCounterexample` (`Nat.Prime`, audited via [`comparator/riemann_95.json`](../comparator/riemann_95.json)). 2. **End-to-end mathematical semantics ([`Cryptids/Semantics/`](./Semantics/README.md)):** - **ZF Consistency (`zf_380`, `zf_393`, and `zf_432`):** Both `zf_380` and Wade's 393-state machine `zf_393` (incorporating upstream fix `10fcf152b3`) halt if and only if O'Rear's `zf2.nql` Hilbert system proves $v_0 \in v_0$ (`Halts candidate ↔ ZFInconsistent`, `Halts zf393 ↔ ZFInconsistent`), while `zf_432` halts if and only if the 20-clause deductive system enumerated by `zf_432_wade.tm` derives $v_0 \in v_0$ (`WadeZFInconsistent`). **All three proof-search equivalences are proved constructively in Lean using only `["propext", "Quot.sound"]` (no `Classical.choice`, no Excluded Middle, and no Markov's Principle)** and audited via [`comparator/constructive.json`](../comparator/constructive.json), blocking classical `Con(ZF)` shortcuts via [`Zf/Soundness.lean`](./Semantics/Zf/Soundness.lean) or `Classical.em` (object-level `PA` internalization for `zf_393` and `zf_380` is proved separately below via `PAProvable`, while `zf_432` internalization and establishing full two-way `ZF`-independence remain separate; see [`Semantics/README.md`](./Semantics/README.md#foundational-note-conzf-in-lean-and-constructive-equivalence)). Separately, [`Zf/Soundness.lean`](./Semantics/Zf/Soundness.lean) uses classical `ZFSet.{0}` (`Classical.choice`) to establish `not_zfInconsistent` and deduce unconditional non-halting (`not_halts_zf393`, `not_halts_candidate`) inside Lean's stronger meta-theory. - **First-Order Peano Arithmetic (`PAProvable`, [`Semantics/PA.lean`](./Semantics/PA.lean)):** Deeply embeds first-order Peano Arithmetic (`PATerm`, `PAFormula`, `PAProvable`) and $\Sigma_1^0$ encodings `paHalts M` and `paZFInconsistent` in [`Propositions.lean`](./Propositions.lean) and [`Challenge.lean`](../Challenge.lean), proving constructive consistency (`not_paProvable_false`) and constructive standard-model adequacy (`paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`; all three audited without `Classical.choice` in [`comparator/constructive.json`](../comparator/constructive.json)), along with classical standard-model soundness (`paProvable_sound_nat`) and full object-level `PA` 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`, audited in [`comparator/pa_semantics.json`](../comparator/pa_semantics.json) and [`comparator/all.json`](../comparator/all.json); these three `PAProvable` theorems use `Classical.choice` because they reason in arbitrary `PAModel`s and reflect back to `PAProvable` via internal Gödel–Henkin completeness `paProvable_iff_holdsIn_all_models`). - **Goldbach (`goldbach_21` and `goldbach_25`):** Both `goldbach_21` and `goldbach_25` constructively satisfy `Halts M ↔ ∃ w, ¬ HasGoldbachPair (2 * w + 4)` without `Classical.choice` ([`Goldbach21.lean`](./Goldbach21.lean)), and with `Classical.choice` (for Markov's Principle on `¬ ∀ n, ...`) satisfy `Halts candidate ↔ ¬ GoldbachConjecture` ([`Semantics/Goldbach.lean`](./Semantics/Goldbach.lean)). + - **Erdős's conjecture on powers of two (`erdos_15` and `erdos_14`):** Stérin and Woods's 15-state machine constructively satisfies `Halts erdos15 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n`, where `pw n` is the base-3 digit list of `2 ^ n` computed by repeated doubling ([`Erdos15.lean`](./Erdos15.lean)), and with `Classical.choice` (Mathlib's `Nat.digits`, and Markov's Principle on `¬ ∀ n, ...`) satisfies `Halts erdos15 ↔ ¬ ErdosPowersOfTwoConjecture` ([`Semantics/Erdos15.lean`](./Semantics/Erdos15.lean)). Stérin's 14-state machine `erdos_14` constructively satisfies `Halts erdos14 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` and hence `Halts candidate ↔ Halts reference` against `erdos_15` ([`Erdos14.lean`](./Erdos14.lean)), and `Halts candidate ↔ ¬ ErdosPowersOfTwoConjecture` ([`Semantics/Erdos14.lean`](./Semantics/Erdos14.lean)). - **Riemann Hypothesis (`riemann_95`, `riemann_104`, `riemann_120`, and `riemann_744`):** All four machines (`riemann_95`, `riemann_104`, Shunia's 120-state machine `riemann_120`, and the 744-state machine `riemann_744`) halt if and only if Mathlib's `RiemannHypothesis` is false (`Halts candidate ↔ ¬ RiemannHypothesis`, `Halts riemann120 ↔ ¬ RiemannHypothesis`, and `Halts riemann744 ↔ ¬ RiemannHypothesis`). Details on the proof architecture and the foundational distinction between constructive proof-search equivalence and meta-theoretic non-halting are in [`Cryptids/Semantics/README.md`](./Semantics/README.md). @@ -44,6 +47,7 @@ For the reduced machines in [`artifacts/`](../artifacts/), the state-space trans - **`zf_380` (`+0.093%` step overhead at `1,000,000` steps; `0` step overhead during `39,753`-step bootstrap):** Eliminating 13 states (`65, 68, 266, 278, 322, 335, 341, 353, 359, 361, 379, 387, 389`) via a 5-cell sliding-window invariant (`validState`) and non-destructive leftward head bounces (`1, 3, 5, 7, 9` steps) preserves 100% bit-exact tape equality after every macro-step. - **`riemann_104` (`9,037` vs. `89,775,610` bootstrap steps, `9,934.23x` faster initialization; `498,382` vs. `111,294,346` total steps over the first `1,000` register instructions, `223.31x` speedup):** Eliminating 16 states (`120 -> 104`) splits merged scanner state `32` via a 5-cell window invariant (`120 -> 121`), replaces the two-phase `89.8M`-step bootstrap (`-9` states) with a self-bootstrapping header and dynamic on-demand zero padding (`padTotal -> padTotal + 1`), and consolidates return scanners and binary call-stack frames (`mapStack`, `-8` states). - **`riemann_95` (`3,634` vs. `9,037` bootstrap steps, `2.49x` faster initialization):** Retaining the stage counter after `FOLD` removes the subsequent counter transfer. A permutation of the physical register banks permits the shorter blank initializer. The proof covers its complete tape and all subsequent stages. +- **`erdos_14` (`208,865` vs. `212` steps to reach the stage for `2 ^ 9`; `13,104,473` vs. `322` for `2 ^ 12`):** The saved state costs speed: keeping `2 ^ n` in unary and dividing it by `3` in place makes each stage about `4x` longer than the previous one, while `erdos_15` keeps the base-3 digits and needs only a few dozen steps per stage at this size. ## Building and Verifying diff --git a/Cryptids/Semantics/Erdos14.lean b/Cryptids/Semantics/Erdos14.lean new file mode 100644 index 00000000..ae57b499 --- /dev/null +++ b/Cryptids/Semantics/Erdos14.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.Erdos14 +public import Cryptids.Semantics.Erdos15 + +@[expose] public section + +namespace ConjectureMachines.Erdos14.Semantics + +/-- The 14-state machine (`erdos_14`) halts on the blank tape if and only if Erdős's conjecture on +powers of two is false. -/ +theorem halts_candidate_iff_not_erdosPowersOfTwo : + Halts ConjectureMachines.Erdos14.candidate ↔ ¬ ErdosPowersOfTwoConjecture := + ConjectureMachines.Erdos14.candidate_equivalent.trans + ConjectureMachines.Erdos15.halts_erdos15_iff_not_erdosPowersOfTwo + +end ConjectureMachines.Erdos14.Semantics diff --git a/Cryptids/Semantics/Erdos15.lean b/Cryptids/Semantics/Erdos15.lean new file mode 100644 index 00000000..ecc11e17 --- /dev/null +++ b/Cryptids/Semantics/Erdos15.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.Erdos15 +public import Cryptids.Propositions + +/-! +# Semantics of the Erdős Powers-of-Two Turing Machine (`erdos_15`) + +This file proves that the 15-state Turing machine `erdos15` (`erdos_15`) halts on the blank tape +if and only if Erdős's conjecture on powers of two is false (i.e., there exists `n > 8` such that +the base-3 expansion of `2 ^ n` has no digit `2`). + +`Cryptids.Erdos15` proves `Halts erdos15 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` without `Classical.choice`, +where `pw n` is the digit list of `2 ^ n` computed by repeated doubling. This file identifies +`pw n` with Mathlib's `Nat.digits 3 (2 ^ n)`, whose definition and lemmas use `Classical.choice`. +The negated form `¬ ErdosPowersOfTwoConjecture` also uses Markov's Principle (`not_forall`), as +for `¬ GoldbachConjecture`. + +## Provenance and Attribution + +* Tristan Stérin and Damien Woods, *Hardness of busy beaver value BB(15)* + (, 2021; machine file in ): + the machine and its pen-and-paper correctness proof. +* Paul Erdős, *Some unconventional problems in number theory*, Math. Mag. 52 (1979): the + conjecture. +-/ + +@[expose] public section + +namespace ConjectureMachines.Erdos15 + +/-- Doubling with carry `c ≤ 1` on base-3 digit lists agrees with `Nat.digits`. -/ +theorem dbl_digits (x c : ℕ) (hc : c ≤ 1) : + dbl (Nat.digits 3 x) c = Nat.digits 3 (2 * x + c) := by + induction x using Nat.strong_induction_on generalizing c with + | _ x ih => + rcases Nat.eq_zero_or_pos x with rfl | hx + · rcases Nat.le_one_iff_eq_zero_or_eq_one.mp hc with rfl | rfl + · simp [dbl] + · simp [dbl] + · rw [Nat.digits_def' (by omega) hx, dbl, ih (x / 3) (by omega) _ (by omega), + Nat.digits_def' (b := 3) (n := 2 * x + c) (by omega) (by omega)] + have e₁ : (2 * (x % 3) + c) % 3 = (2 * x + c) % 3 := by omega + have e₂ : 2 * (x / 3) + (2 * (x % 3) + c) / 3 = (2 * x + c) / 3 := by omega + rw [e₁, e₂] + +/-- `pw n` is the list of base-3 digits of `2 ^ n`, least significant first. -/ +theorem pw_eq (n : ℕ) : pw n = Nat.digits 3 (2 ^ n) := by + induction n with + | zero => simp [pw] + | succ n ih => rw [pw, ih, dbl_digits _ _ (by omega), pow_succ, Nat.mul_comm, Nat.add_zero] + +/-- The 15-state machine `erdos15` (`erdos_15`) halts on the blank tape if and only if some +power `2 ^ n` with `n > 8` has no digit `2` in base `3`. -/ +theorem halts_erdos15_iff_exists_counterexample : + ConjectureMachines.Halts erdos15 ↔ ∃ n : ℕ, 8 < n ∧ 2 ∉ Nat.digits 3 (2 ^ n) := by + simp only [← pw_eq] + exact halts_erdos15_iff_exists_free + +/-- The 15-state machine `erdos15` (`erdos_15`) halts on the blank tape if and only if Erdős's +conjecture on powers of two is false. -/ +theorem halts_erdos15_iff_not_erdosPowersOfTwo : + ConjectureMachines.Halts erdos15 ↔ ¬ ErdosPowersOfTwoConjecture := by + rw [halts_erdos15_iff_exists_counterexample] + simp only [ErdosPowersOfTwoConjecture, not_forall, exists_prop] + +end ConjectureMachines.Erdos15 diff --git a/Cryptids/Semantics/README.md b/Cryptids/Semantics/README.md index 29150438..863993ea 100644 --- a/Cryptids/Semantics/README.md +++ b/Cryptids/Semantics/README.md @@ -360,7 +360,7 @@ Care is required when interpreting a Lean theorem of type `Halts M ↔ ZFInconsi 1. **Why classical Lean vacuously satisfies `Halts M ↔ ZFInconsistent` for any non-halting machine:** Lean's type theory is proof-theoretically stronger than first-order $\mathrm{ZF}$. Using `Classical.choice` and Mathlib's cumulative hierarchy `ZFSet.{0} : Type 1`, [`Zf/Soundness.lean`](./Zf/Soundness.lean) proves `not_zfInconsistent : ¬ ZFInconsistent` inside Lean itself (and deduces `not_halts_zf393` and `not_halts_candidate`). Moreover, as noted by Elliot Glazer and formalized in Lean 4 by Mario Carneiro ([`digama0/ConZF`](https://github.com/digama0/ConZF), *"CIC + EM $\vdash$ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice"*), Lean's Calculus of Inductive Constructions (`CIC`) plus Excluded Middle alone (or `¬¬ ∀ p : Prop, p ∨ ¬p`, via large elimination of `Acc`) proves $\operatorname{Con}(\mathrm{ZF})$ without `Classical.choice`, `propext`, or `Quot.sound`. Consequently, if `Classical.choice` (which yields Excluded Middle together with `propext` and `Quot.sound` by Diaconescu's theorem) or `not_zfInconsistent` is allowed, **any** provably non-halting machine—such as the 1-state machine `0R0 0R0` that moves right forever—vacuously satisfies the bare material biconditional `Halts M ↔ ZFInconsistent` (`False ↔ False`). 2. **Constructive proof-search equivalence (`["propext", "Quot.sound"]` only, enforced by `comparator`):** - To rule out classical shortcuts through `Classical.choice`, `Classical.em`, or `not_zfInconsistent`, `ConjectureMachines.ListBlank` quotients half-tapes directly via Lean's primitive `Quot (@Turing.BlankRel Γ _)` (`Challenge.lean`, `Cryptids/Machines.lean`), and **the direct state-reduction halting equivalences (`Goldbach21.candidate_equivalent`, `Zf380.candidate_equivalent`, `Riemann104.candidate_equivalent`), all four `candidate_fewer_states` theorems (including `Riemann95.candidate_fewer_states`; `Riemann95.candidate_equivalent` uses `Classical.choice`), and all three ZF machine-to-proof-search equivalences (`Zf393.halts_zf393_iff_zfInconsistent`, `Zf380.Semantics.halts_candidate_iff_zfInconsistent`, `Semantics.Zf.halts_zf432_iff_wadeZFInconsistent`)** are proved **constructively in Lean** using only `["propext", "Quot.sound"]`—with **zero `Classical.choice`, zero Excluded Middle, and zero Markov's Principle**: + To rule out classical shortcuts through `Classical.choice`, `Classical.em`, or `not_zfInconsistent`, `ConjectureMachines.ListBlank` quotients half-tapes directly via Lean's primitive `Quot (@Turing.BlankRel Γ _)` (`Challenge.lean`, `Cryptids/Machines.lean`), and **the direct state-reduction halting equivalences (`Goldbach21.candidate_equivalent`, `Zf380.candidate_equivalent`, `Riemann104.candidate_equivalent`), the `Erdos14.candidate_equivalent` reduction, all five `candidate_fewer_states` theorems (including `Riemann95.candidate_fewer_states`; `Riemann95.candidate_equivalent` uses `Classical.choice`), and all three ZF machine-to-proof-search equivalences (`Zf393.halts_zf393_iff_zfInconsistent`, `Zf380.Semantics.halts_candidate_iff_zfInconsistent`, `Semantics.Zf.halts_zf432_iff_wadeZFInconsistent`)** are proved **constructively in Lean** using only `["propext", "Quot.sound"]`—with **zero `Classical.choice`, zero Excluded Middle, and zero Markov's Principle**: - **Forward completeness (`ZFInconsistent → Halts M`):** Given a finite derivation tree `d : ZFProvable (zfMem 0 0)`, structural induction extracts an explicit step count `s` and halting configuration `c` with `nSteps M s init = some c ∧ step M c = none` (no `by_contra` / unbounded search). - **Backward soundness (`Halts M → ZFInconsistent`):** Given `h : Halts M`, constructive induction along `StateTransition.evalInduction'` extracts the finite execution trace from `init` and decodes a valid `ZFProvable (zfMem 0 0)` derivation. - **Comparator gate:** [`comparator/constructive.json`](../../comparator/constructive.json), [`comparator/zf_380.json`](../../comparator/zf_380.json), [`comparator/goldbach_21.json`](../../comparator/goldbach_21.json), and [`comparator/riemann_104.json`](../../comparator/riemann_104.json) enforce `"permitted_axioms": ["propext", "Quot.sound"]` in CI, automatically rejecting any proof that invokes `Classical.choice` (including `not_zfInconsistent` in [`Zf/Soundness.lean`](./Zf/Soundness.lean) or `Classical.em` + [`digama0/ConZF`](https://github.com/digama0/ConZF)). @@ -587,3 +587,59 @@ theorem paProvable_halts_zf380_iff_zfInconsistent : and 20 reordered `ZF` axiom/rule clauses along the 125-step `main()` spine, and bidirectional soundness and completeness against `MZFInconsistent M`, yielding `paProvable_halts_zf393_iff_zfInconsistent` and `paProvable_halts_zf380_iff_zfInconsistent`. + +--- + +## 7. Stérin and Woods's 15-State Erdős Machine ([`Erdos15.lean`](./Erdos15.lean)) + +In [`Cryptids/Erdos15.lean`](../Erdos15.lean) and [`Cryptids/Semantics/Erdos15.lean`](./Erdos15.lean), +we formalize Tristan Stérin and Damien Woods's 15-state binary Turing machine (`erdos_15`, +[`arXiv:2107.12475`](https://arxiv.org/abs/2107.12475), 2021) for Erdős's conjecture that `2 ^ n` +has a digit `2` in base `3` for every `n > 8`: + +```lean +theorem halts_erdos15_iff_exists_counterexample : + Halts erdos15 ↔ ∃ n : ℕ, 8 < n ∧ 2 ∉ Nat.digits 3 (2 ^ n) + +theorem halts_erdos15_iff_not_erdosPowersOfTwo : + Halts erdos15 ↔ ¬ ErdosPowersOfTwoConjecture +``` + +1. **Machine (`Erdos15.lean`)**: Proves the tape layout of every stage (counter cell pair, `#`, + base-3 digits of `2 ^ n` as cell pairs), one lemma per routine (doubling pass, scan for a `2`, + rewind, counter increment, halt), and `Halts erdos15 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` with `propext` + and `Quot.sound` only, where `pw n` is the digit list of `2 ^ n` computed by repeated doubling. +2. **Digits (`Semantics/Erdos15.lean`)**: Proves `pw n = Nat.digits 3 (2 ^ n)` and derives both + theorems above (`Classical.choice` enters through `Nat.digits`, and the negated form also uses + Markov's Principle via `not_forall`, as for `¬ GoldbachConjecture`). + +--- + +## 8. Stérin's 14-State Erdős Machine ([`Erdos14.lean`](./Erdos14.lean)) + +In [`Cryptids/Erdos14.lean`](../Erdos14.lean) and [`Cryptids/Semantics/Erdos14.lean`](./Erdos14.lean), +we formalize Tristan Stérin's 14-state binary Turing machine for the same conjecture (`erdos_14`, +[announced](https://discord.com/channels/960643023006490684/1561295445312151622/1562203343114473472) on the bbchallenge Discord in October 2026 and listed on the +[Cryptids](https://wiki.bbchallenge.org/w/index.php?title=Cryptids&oldid=9722) page of the bbchallenge wiki): + +```lean +theorem candidate_fewer_states : candidate.states < reference.states + +theorem candidate_equivalent : Halts candidate ↔ Halts reference + +theorem halts_candidate_iff_not_erdosPowersOfTwo : + Halts candidate ↔ ¬ ErdosPowersOfTwoConjecture +``` + +with `candidate = erdos14` and `reference = erdos15`. + +1. **Machine (`Erdos14.lean`)**: The machine keeps `2 ^ n` in unary and reads its base-3 digits + by repeated division by `3`, with a single `0` in the block marking where the quotient ends. + One lemma per routine (division round and its three outcomes, return to the start, counter + increment, halt, doubling) gives `Halts erdos14 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` with `propext` and + `Quot.sound` only, using `Has2 (2 ^ n) ↔ 2 ∈ pw n` to connect the divisions with `pw`. + `candidate_equivalent` follows from the same statement for `erdos15`, so it is also + constructive. +2. **Semantics (`Semantics/Erdos14.lean`)**: Composes `candidate_equivalent` with + `halts_erdos15_iff_not_erdosPowersOfTwo` (`Classical.choice` through `Nat.digits`, and + Markov's Principle via `not_forall`, as in Section 7). diff --git a/README.md b/README.md index 2b036fa7..4e7f2ba1 100644 --- a/README.md +++ b/README.md @@ -2,19 +2,19 @@ This repository contains two Lean 4 (`v4.35.0-rc4`) formalization libraries for small Turing machines whose halting behavior encodes deep mathematical problems or complex dynamical invariants: -1. **[Conjecture-Checking Turing Machines (`Cryptids/`)](Cryptids/README.md)** — Certified state reductions (`goldbach_21`, `zf_380`, `riemann_95`) and end-to-end Lean 4 mathematical semantics proofs (`Halts M ↔ ...`) for **Goldbach's Conjecture**, **ZF Set Theory Consistency**, and the **Riemann Hypothesis**. +1. **[Conjecture-Checking Turing Machines (`Cryptids/`)](Cryptids/README.md)** — Certified state reductions (`goldbach_21`, `zf_380`, `riemann_95`, `erdos_14`) and end-to-end Lean 4 mathematical semantics proofs (`Halts M ↔ ...`) for **Goldbach's Conjecture**, **ZF Set Theory Consistency**, the **Riemann Hypothesis**, and **Erdős's conjecture on powers of two**. 2. **[Busy Beaver Holdouts (`BusyBeaver/`)](BusyBeaver/README.md)** — Kernel-verified behavioral proofs (`IsHalt`, `IsNotHalt`, `HasCollatzReduction`, `HasStackedCollatzReduction`, `IsValidAcceleration`) for **Busy Beaver 6 (`BB(6)`)** and **Busy Beaver (3, 3) (`BB(3, 3)`)** holdouts—covering both community-documented machines and novel Collatz-like accelerations discovered via the autonomous agentic pipeline of [*At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier*](https://arxiv.org/abs/2610.22603) (some are potential Cryptids, subject to community acceptance)—connected to `ConjectureMachines.Machine` via [`BusyBeaver/Bridge.lean`](BusyBeaver/Bridge.lean). ## Overview | Library | Scope | Key Results | Documentation | | :--- | :--- | :--- | :--- | -| [`Cryptids/`](Cryptids/) | `(Q, 2)` Turing machines for Goldbach, ZF consistency, and the Riemann Hypothesis | Certified state reductions (`25 → 21`, `393 → 380`, `120 → 104 → 95`) and end-to-end halting equivalences (`Halts M ↔ ¬ GoldbachConjecture`, `ZFInconsistent`, `¬ RiemannHypothesis`) | [`Cryptids/README.md`](Cryptids/README.md), [`Cryptids/Semantics/README.md`](Cryptids/Semantics/README.md) | +| [`Cryptids/`](Cryptids/) | `(Q, 2)` Turing machines for Goldbach, ZF consistency, the Riemann Hypothesis, and Erdős's conjecture on powers of two | Certified state reductions (`25 → 21`, `393 → 380`, `120 → 104 → 95`, `15 → 14`) and end-to-end halting equivalences (`Halts M ↔ ¬ GoldbachConjecture`, `ZFInconsistent`, `¬ RiemannHypothesis`, `¬ ErdosPowersOfTwoConjecture`) | [`Cryptids/README.md`](Cryptids/README.md), [`Cryptids/Semantics/README.md`](Cryptids/Semantics/README.md) | | [`BusyBeaver/`](BusyBeaver/) | `BB(6)` `(6, 2)` and `BB(3, 3)` `(3, 3)` holdout Turing machines (some are potential Cryptids, subject to community acceptance) | Shared execution semantics (`BusyBeaver/Defs.lean`), foundational lemmas (`BusyBeaver/Basic.lean`), RLE loader and `ConjectureMachines` bridge (`BusyBeaver/Bridge.lean`), and certified behavioral proofs in [`BusyBeaver/BB6/`](BusyBeaver/BB6/README.md) (53 machines) and [`BusyBeaver/BB33/`](BusyBeaver/BB33/README.md) (6 machines) | [`BusyBeaver/README.md`](BusyBeaver/README.md), [`BusyBeaver/BB6/README.md`](BusyBeaver/BB6/README.md), [`BusyBeaver/BB33/README.md`](BusyBeaver/BB33/README.md) | All Lean 4 proofs are checked by the kernel without `sorry` and depend only on standard Lean axioms: -- **Constructive (`["propext", "Quot.sound"]`, no `Classical.choice`):** All ZF machine-to-proof-search equivalences (`halts_zf393_iff_zfInconsistent`, `Zf380.Semantics.halts_candidate_iff_zfInconsistent`, `halts_zf432_iff_wadeZFInconsistent`), first-order Peano Arithmetic (`PAProvable`) consistency and $\Sigma_1^0$ standard-model adequacy (`not_paProvable_false`, `paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent` in [`Cryptids/Semantics/PA/`](Cryptids/Semantics/PA/)), the direct simulation state reductions ([`Goldbach21.lean`](Cryptids/Goldbach21.lean), [`Zf380.lean`](Cryptids/Zf380.lean), [`Riemann104.lean`](Cryptids/Riemann104.lean)), and all four `candidate_fewer_states` theorems, audited in CI via [`comparator/constructive.json`](comparator/constructive.json). Because classical Lean (`ZFSet.{0}` in [`Soundness.lean`](Cryptids/Semantics/Zf/Soundness.lean)) proves `¬ ZFInconsistent`—so any non-halting machine would vacuously satisfy `Halts M ↔ ZFInconsistent` under `Classical.choice`—excluding `Classical.choice` blocks classical `Con(ZF)` shortcuts, while deeply embedded `PAProvable` provides a weak first-order metatheory strictly below `ZF` (see [Foundational Note on `Con(ZF)` and Constructive Equivalence](Cryptids/Semantics/README.md#foundational-note-conzf-in-lean-and-constructive-equivalence)). -- **Classical (`["propext", "Classical.choice", "Quot.sound"]`):** First-order `PA` standard-model soundness and object-level `PAProvable` proofs that `zf_380` and `zf_393` halt iff `ZF` is inconsistent (`paProvable_sound_nat`, `paProvable_halts_zf380_iff_zf393`, `paProvable_halts_zf393_iff_zfInconsistent`, `paProvable_halts_zf380_iff_zfInconsistent`; proved semantically in arbitrary `PAModel`s via first-order induction and reflected to `PAProvable` via internal Gödel–Henkin completeness `paProvable_iff_holdsIn_all_models`, which uses `Classical.choice`), set-theoretic soundness and non-halting in `ZFSet.{0}` (`zfProvable_sound_zfSet`, `not_zfInconsistent`, `not_halts_zf393`, `not_halts_candidate`), negated-$\Pi_1^0$ Goldbach equivalence (`¬ GoldbachConjecture`, which uses Markov's Principle), the arithmetic-stage `riemann_95` reduction (`Nat.Prime`), complex-analytic `RiemannHypothesis` equivalences, and the `BB(6)` and `BB(3, 3)` holdout reductions, audited via [`comparator/all.json`](comparator/all.json), [`comparator/pa_semantics.json`](comparator/pa_semantics.json), and [`comparator/busy_beaver.json`](comparator/busy_beaver.json). +- **Constructive (`["propext", "Quot.sound"]`, no `Classical.choice`):** All ZF machine-to-proof-search equivalences (`halts_zf393_iff_zfInconsistent`, `Zf380.Semantics.halts_candidate_iff_zfInconsistent`, `halts_zf432_iff_wadeZFInconsistent`), first-order Peano Arithmetic (`PAProvable`) consistency and $\Sigma_1^0$ standard-model adequacy (`not_paProvable_false`, `paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent` in [`Cryptids/Semantics/PA/`](Cryptids/Semantics/PA/)), the direct simulation state reductions ([`Goldbach21.lean`](Cryptids/Goldbach21.lean), [`Zf380.lean`](Cryptids/Zf380.lean), [`Riemann104.lean`](Cryptids/Riemann104.lean)), the `erdos_14` reduction ([`Erdos14.lean`](Cryptids/Erdos14.lean)), and all five `candidate_fewer_states` theorems, audited in CI via [`comparator/constructive.json`](comparator/constructive.json). Because classical Lean (`ZFSet.{0}` in [`Soundness.lean`](Cryptids/Semantics/Zf/Soundness.lean)) proves `¬ ZFInconsistent`—so any non-halting machine would vacuously satisfy `Halts M ↔ ZFInconsistent` under `Classical.choice`—excluding `Classical.choice` blocks classical `Con(ZF)` shortcuts, while deeply embedded `PAProvable` provides a weak first-order metatheory strictly below `ZF` (see [Foundational Note on `Con(ZF)` and Constructive Equivalence](Cryptids/Semantics/README.md#foundational-note-conzf-in-lean-and-constructive-equivalence)). +- **Classical (`["propext", "Classical.choice", "Quot.sound"]`):** First-order `PA` standard-model soundness and object-level `PAProvable` proofs that `zf_380` and `zf_393` halt iff `ZF` is inconsistent (`paProvable_sound_nat`, `paProvable_halts_zf380_iff_zf393`, `paProvable_halts_zf393_iff_zfInconsistent`, `paProvable_halts_zf380_iff_zfInconsistent`; proved semantically in arbitrary `PAModel`s via first-order induction and reflected to `PAProvable` via internal Gödel–Henkin completeness `paProvable_iff_holdsIn_all_models`, which uses `Classical.choice`), set-theoretic soundness and non-halting in `ZFSet.{0}` (`zfProvable_sound_zfSet`, `not_zfInconsistent`, `not_halts_zf393`, `not_halts_candidate`), negated-$\Pi_1^0$ Goldbach equivalence (`¬ GoldbachConjecture`, which uses Markov's Principle), the arithmetic-stage `riemann_95` reduction (`Nat.Prime`), complex-analytic `RiemannHypothesis` equivalences, the `erdos_15` and `erdos_14` equivalences with `ErdosPowersOfTwoConjecture` (`Nat.digits`, and Markov's Principle for `¬ ErdosPowersOfTwoConjecture`), and the `BB(6)` and `BB(3, 3)` holdout reductions, audited via [`comparator/all.json`](comparator/all.json), [`comparator/pa_semantics.json`](comparator/pa_semantics.json), and [`comparator/busy_beaver.json`](comparator/busy_beaver.json). The [95-state Riemann machine](artifacts/riemann_95/README.md) has a kernel-checked blank-tape halting equivalence to the 104-state machine and to `¬ RiemannHypothesis`. @@ -49,7 +49,7 @@ lake comparator --config comparator/busy_beaver.json - [`Cryptids/`](Cryptids/README.md) — Conjecture-checking Turing machines ([`Machines.lean`](Cryptids/Machines.lean), [`Propositions.lean`](Cryptids/Propositions.lean)), state-reduction proofs ([`Goldbach21.lean`](Cryptids/Goldbach21.lean), [`Zf380.lean`](Cryptids/Zf380.lean), [`Riemann95.lean`](Cryptids/Riemann95.lean)), and end-to-end mathematical semantics ([`Cryptids/Semantics/`](Cryptids/Semantics/README.md)). - [`BusyBeaver/`](BusyBeaver/README.md) — Busy Beaver holdout specifications ([`Defs.lean`](BusyBeaver/Defs.lean)), foundational lemmas ([`Basic.lean`](BusyBeaver/Basic.lean)), RLE loader and bridge to `ConjectureMachines` ([`Bridge.lean`](BusyBeaver/Bridge.lean)), and machine behavioral proofs. - [`Challenge.lean`](Challenge.lean), [`BusyBeaverChallenge.lean`](BusyBeaverChallenge.lean) & [`comparator/`](comparator/) — Self-contained target theorem specifications and configuration files for [`leanprover/comparator`](comparator/README.md). -- [`artifacts/`](artifacts/) — Canonical `machine.txt` transition tables and reduction write-ups for [`goldbach_21`](artifacts/goldbach_21/README.md), [`zf_380`](artifacts/zf_380/README.md), [`riemann_104`](artifacts/riemann_104/README.md), and [`riemann_95`](artifacts/riemann_95/README.md). +- [`artifacts/`](artifacts/) — Canonical `machine.txt` transition tables and reduction write-ups for [`goldbach_21`](artifacts/goldbach_21/README.md), [`zf_380`](artifacts/zf_380/README.md), [`riemann_104`](artifacts/riemann_104/README.md), [`riemann_95`](artifacts/riemann_95/README.md), and [`erdos_14`](artifacts/erdos_14/README.md). - [`baselines/`](baselines/) — Verbatim upstream source files, canonical 5-tuple tables, and [`PROVENANCE.md`](baselines/PROVENANCE.md). - [`RELATED_WORK.md`](RELATED_WORK.md) — Literature lineage and `(Q, 2)` Turing machine conventions. - [`verify.py`](verify.py) — Standalone Python 3 verification script for the conjecture-checking machines. @@ -60,7 +60,7 @@ Pull requests and issues are welcome, especially for smaller Turing machines for ## Acknowledgements -We thank Eric Wieser for careful review, as well as the Busy Beaver Challenge community, `int-y1` (whose `BusyLean` project pioneered Lean 4 Busy Beaver formalizations and directed-head configuration representations), Yijun Leng, Stefan O'Rear, Yuri Matiyasevich, Scott Aaronson, Adam Yedidia, Andrew Wade, and Joseph Shunia for the baseline Turing machines and compilers, and the Mathlib community. +We thank Eric Wieser for careful review, as well as the Busy Beaver Challenge community, `int-y1` (whose `BusyLean` project pioneered Lean 4 Busy Beaver formalizations and directed-head configuration representations), Yijun Leng, Stefan O'Rear, Yuri Matiyasevich, Scott Aaronson, Adam Yedidia, Andrew Wade, Joseph Shunia, Tristan Stérin, and Damien Woods for the baseline Turing machines and compilers, and the Mathlib community. ## License and disclaimer diff --git a/RELATED_WORK.md b/RELATED_WORK.md index 4f28cb53..1f17fe98 100644 --- a/RELATED_WORK.md +++ b/RELATED_WORK.md @@ -20,6 +20,7 @@ Community records for conjecture-checking and ZFC-independent Turing machines ar - **Goldbach (`goldbach_21`):** Reduces `goldbach_25` (`25 -> 21` states). - **ZF Consistency (`zf_380`, `zf_393`, `zf_432`) and Riemann Hypothesis (`riemann_104`, `riemann_120`, `riemann_744`):** Compiler and algorithmic reworks by Andrew Wade (`zf_393`, `393` states for ZF, Aug 2026) and Joseph M. Shunia (`riemann_120`, `120` states for RH, Sept 2026) improved over `zf_432` (`432` states, 2025) and `riemann_744` (`744` states, 2016); `zf_380` (`393 -> 380` states) and `riemann_104` (`120 -> 104` states) further reduce both record baselines. This repository provides Lean 4 end-to-end semantics proofs across all of `goldbach_21`, `goldbach_25`, `zf_380`, `zf_393`, `zf_432`, `riemann_104`, `riemann_120`, and `riemann_744`. +- **Erdős's conjecture on powers of two (`erdos_15`, `erdos_14`):** Tristan Stérin and Damien Woods's 15-state machine (2021) and Tristan Stérin's 14-state machine (Oct 2026), with Lean 4 semantics proofs in this repository. ### 1. Goldbach's Conjecture (`goldbach`) @@ -57,3 +58,11 @@ Enumerates positive integers $n$ and tests an elementary arithmetic inequality e | 2026 | Faldor & Firsching, using Gemini Argon (`riemann_104`) | `104` | State reduction of `riemann_120` (`120 -> 104`): 5-cell window de-merging (`+1`), dynamic-padding self-bootstrap (`-9`), and return-scanner & call-stack consolidation (`-8`) | Lean 4 proofs ([`Cryptids/Riemann104.lean`](Cryptids/Riemann104.lean), [`Cryptids/Semantics/Riemann120.lean`](Cryptids/Semantics/Riemann120.lean)) | | 2026 | Vladislav Isenbaev, using GPT-6.1 Sol and Aleph Prover (`riemann_95`) | `95` | Retains the stage counter after `FOLD`, permutes the operand banks, and initializes in 3,634 steps | Lean 4 proofs ([`Cryptids/Riemann95.lean`](Cryptids/Riemann95.lean), [`Cryptids/Semantics/Riemann95.lean`](Cryptids/Semantics/Riemann95.lean)); [construction and proof guide](artifacts/riemann_95/README.md) | +### 4. Erdős's Conjecture on Powers of Two (`erdos`) + +`erdos_15` doubles a base-3 number on the tape and halts at the fourth power `2 ^ n` without a digit `2` in base `3` (counting `2 ^ 0`); `erdos_14` keeps `2 ^ n` in unary, reads its base-3 digits by repeated division by `3`, and halts at the third such power (counting from `2 ^ 1`). The conjecture (Erdős, 1979) is that `2 ^ 0`, `2 ^ 2`, and `2 ^ 8` are the only such powers. + +| Year | Authors / Source | States (`(Q, 2)`) | Construction / Reduction Method | Formal Proof | +| :--- | :--- | :--- | :--- | :--- | +| 2021 | Tristan Stérin & Damien Woods ([`arXiv:2107.12475`](https://arxiv.org/abs/2107.12475), [`tcosmo/bbsim`](https://github.com/tcosmo/bbsim) `machines/powers_of_two_15_2.txt`) | `15` | 5-state, 4-symbol machine (reverse-ternary doubling, scan for a `2`, counter of exceptions) compiled to 2 symbols (`0 → ba`, `1 → ab`, `2 → aa`, `# → bb`) | Pen-and-paper proof in the paper; Lean 4 proofs in this repo by Daniel Veljjanoski, with Claude (Anthropic) as assistant ([`Cryptids/Erdos15.lean`](Cryptids/Erdos15.lean), [`Cryptids/Semantics/Erdos15.lean`](Cryptids/Semantics/Erdos15.lean)) | +| 2026 | Tristan Stérin ([bbchallenge Discord](https://discord.com/channels/960643023006490684/1561295445312151622/1562203343114473472), Oct 2026; [Cryptids wiki](https://wiki.bbchallenge.org/w/index.php?title=Cryptids&oldid=9722)) | `14` | Keeps `2 ^ n` in unary and reads its base-3 digits by repeated division by `3`, with one `0` marking the quotient; doubles the block in place and counts exceptions | Lean 4 proofs in this repo by Daniel Veljjanoski, with Claude (Anthropic) as assistant ([`Cryptids/Erdos14.lean`](Cryptids/Erdos14.lean), [`Cryptids/Semantics/Erdos14.lean`](Cryptids/Semantics/Erdos14.lean)) | diff --git a/artifacts/erdos_14/README.md b/artifacts/erdos_14/README.md new file mode 100644 index 00000000..435daba9 --- /dev/null +++ b/artifacts/erdos_14/README.md @@ -0,0 +1,54 @@ +# 14-state Erdős powers-of-two machine + +This binary Turing machine has **14 states**, 27 defined transitions, and one halting transition +(`12/ONE`, state `M` reading `1`). It starts in state 0 on the blank tape. Lean proves that it +halts if and only if some `2 ^ n` with `n > 8` has no digit `2` in base `3`, so it halts if and +only if the 15-state machine `erdos_15` does. + +The machine is due to Tristan Stérin, who [announced it](https://discord.com/channels/960643023006490684/1561295445312151622/1562203343114473472) +on the bbchallenge Discord in October 2026; it is listed on the +[Cryptids](https://wiki.bbchallenge.org/w/index.php?title=Cryptids&oldid=9722) page of the bbchallenge wiki +(revision 9722) as + +``` +1LB1RA_1LC1LB_0RD0RA_1LM0RE_1LF1RE_0LJ1LG_1RK0LH_1RI1LH_0LJ0RE_0RD1LJ_0LL1RK_1RN0LC_0LN---_0RK0LM +``` + +[`machine.txt`](machine.txt) is this table with the states `A`–`N` numbered `0`–`13`. + +Unlike `erdos_15`, which keeps the base-3 digits of `2 ^ n`, this machine keeps `2 ^ n` in unary +and reads its base-3 digits by repeated division by `3`. A single `0` in the block of ones marks +where the quotient ends; a digit `2` ends the stage, and a stage that reaches quotient `0` +advances a counter, which halts at the third such stage (after `2 ^ 2` and `2 ^ 8`). The block is +then doubled in place. The layout is described in the docstring of +[`Erdos14.lean`](../../Cryptids/Erdos14.lean). + +## Review entry points + +- [`Machines.lean`](../../Cryptids/Machines.lean): transition table loaded from `machine.txt`. +- [`Erdos14.lean`](../../Cryptids/Erdos14.lean): `halts_erdos14_iff_exists_free`, + `candidate_equivalent`, and `candidate_fewer_states` relative to `Erdos15`. +- [`Semantics/Erdos14.lean`](../../Cryptids/Semantics/Erdos14.lean): + `halts_candidate_iff_not_erdosPowersOfTwo`. + +`halts_erdos14_iff_exists_free` and `candidate_equivalent` use only `propext` and `Quot.sound`. + +## Verification + +From the repository root: + +```sh +lake build +lake comparator --config comparator/erdos_14.json +python3 verify.py +``` + +The comparator checks the three public theorems against independent challenge definitions loaded +from [`machine.txt`](machine.txt). `candidate_fewer_states` and `candidate_equivalent` are also +checked without `Classical.choice` in `comparator/constructive.json`, and all three in +`comparator/all.json`. + +The root Python verifier checks the table's SHA-256, compares the cells loaded by the +implementation and challenge, and simulates the machine on the blank tape, checking the full tape +at every entry to the division state `D` against the configurations used in the proof. This +finite check supplements the unbounded Lean proof. diff --git a/artifacts/erdos_14/machine.txt b/artifacts/erdos_14/machine.txt new file mode 100644 index 00000000..63fe8922 --- /dev/null +++ b/artifacts/erdos_14/machine.txt @@ -0,0 +1,14 @@ +1L1 1R0 +1L2 1L1 +0R3 0R0 +1L12 0R4 +1L5 1R4 +0L9 1L6 +1R10 0L7 +1R8 1L7 +0L9 0R4 +0R3 1L9 +0L11 1R10 +1R13 0L2 +0L13 --- +0R10 0L12 diff --git a/baselines/PROVENANCE.md b/baselines/PROVENANCE.md index 5baa95c8..a72b8cef 100644 --- a/baselines/PROVENANCE.md +++ b/baselines/PROVENANCE.md @@ -1,6 +1,6 @@ # Baseline Provenance & Upstream Re-Compilation (`baselines/PROVENANCE.md`) -All five upstream Turing machine transition tables (`baselines/tables/*.txt`) are deterministically compiled from their verbatim published upstream source files (`baselines/sources/*`). Our standalone verifier (`verify.py`) parses each upstream source from first principles and verifies byte-for-byte identity against the canonical 5-tuple tables and Lean 4 definitions. +All six upstream Turing machine transition tables (`baselines/tables/*.txt`) are deterministically compiled from their verbatim published upstream source files (`baselines/sources/*`). Our standalone verifier (`verify.py`) parses each upstream source from first principles and verifies byte-for-byte identity against the canonical 5-tuple tables and Lean 4 definitions. | Domain | Upstream Source File | Upstream Format | Source SHA-256 | Canonical Table File | Table SHA-256 | Canonical Machine SHA-256 | | :--- | :--- | :--- | :--- | :--- | :--- | :--- | @@ -9,8 +9,9 @@ All five upstream Turing machine transition tables (`baselines/tables/*.txt`) ar | `riemann` (`744` states) | `sources/riemann_744_sorear.tm` | `nql` (Stefan O'Rear 2016 named-state NQL output) | `de0084433909f2600a5052eeb0bb2acd9b0ac315078abd1b92d4f3595601dd31` | `tables/riemann_744.txt` | `9866af71143c85cceeaf2e05be8fef1c3ccb226fe04640b23b7b887f815a25d0` | `4f629ed5be1715747f3d467dbb35bded647a25dc740a80b5208c14f65d7d5f44` | | `zf_393` (`393` states) | `sources/zf_393_wade.tm` | `tursi` (Andrew Wade Aug 2026 commit `9c5c2e82`) | `a1a777fb3994c5b098228f0bd6f27fefcb47a091f36ef8c723bb668c43caf135` | `tables/zf_393.txt` | `f0acf81abb428d9407a9ddd837a1bee07a709634692862386dd6d3e25cc45a97` | `dcb8680665d4ec9667a1b6de6edf136e6bb0255a2f73a69c4d4f2e068dba23b2` | | `riemann_120` (`120` states) | `sources/riemann_120_shunia.tm` | `tursi` (Joseph M. Shunia Sept 2026 `arXiv:2609.30306`) | `b4b0f07607fc92dae6940f6e6c2d184fec3c13bbfc8cd00a0253321be6009db5` | `tables/riemann_120.txt` | `ec3d408bbeba415afb0666573354bb1e1f2b3f4290b84b8745a3d84c841ab6d0` | `a6f0c72649252257bf193268235d0cf9cd847d507d7b241627be7d818c3b86a8` | +| `erdos_15` (`15` states) | `sources/erdos_15_sterin_woods.txt` | `bbsim` (Tristan Stérin & Damien Woods 2021 `arXiv:2107.12475`, [`tcosmo/bbsim`](https://github.com/tcosmo/bbsim) commit `3f655ba2c73b` `machines/powers_of_two_15_2.txt`, mirrored at [docs.bbchallenge.org](https://docs.bbchallenge.org/other/powers_of_two_15_2.txt); blank `b` ↦ `0`, `a` ↦ `1`) | `f9de29f3b3b06e55afbe61baddf317347b224a1a2203b4cf35f4027da1ecd9ac` | `tables/erdos_15.txt` | `f70b7e4ada6b48644f02377bf1d045b3518e5a640a959a10442bace4311a98dd` | `2c38f44a6b344291c1169c35f348ed29d9ee51c1e922e1c43ebba5aeb3326c37` | ## Lean 4 Machine Specification ([`Cryptids/Machines.lean`](../Cryptids/Machines.lean)) * **File:** [`Cryptids/Machines.lean`](../Cryptids/Machines.lean) -* **Contents:** Defines `ConjectureMachines.Machine`, `ConjectureMachines.Cfg`, `ConjectureMachines.step`, `ConjectureMachines.init`, `ConjectureMachines.Halts`, and `load_machine_rows%` definitions for all machines (`goldbach25`, `goldbach21`, `zf432`, `zf393`, `zf380`, `riemann744`, `riemann120`, `riemann104`). +* **Contents:** Defines `ConjectureMachines.Machine`, `ConjectureMachines.Cfg`, `ConjectureMachines.step`, `ConjectureMachines.init`, `ConjectureMachines.Halts`, and `load_machine_rows%` definitions for all machines (`goldbach25`, `goldbach21`, `zf432`, `zf393`, `zf380`, `riemann744`, `riemann120`, `riemann104`, `erdos15`). diff --git a/baselines/sources/erdos_15_sterin_woods.txt b/baselines/sources/erdos_15_sterin_woods.txt new file mode 100644 index 00000000..506ddf38 --- /dev/null +++ b/baselines/sources/erdos_15_sterin_woods.txt @@ -0,0 +1,77 @@ +; This machine halts if and only if Erdős' conjecture on powers of two is false: +; +; "For all n > 8, there is at least one 2 in the ternary representation of 2^n" +; +; P. Erdős. Some unconventional problems in number theory. Mathematics Magazine, 52(2):67–70, 1979. +; +; The machine has 15 states and 2 symbols. +; The machine simulates 'powers_of_two_5_4.txt' with the following encoding table: +; +; 0: ba, 1: ab, 2: aa, #: bb +; +; This machine was proven correct: + +initial_state: mul2_G_sim +redundancy: 2 +blank_symbol: b + +mul2_F_sim +a a R mul2_F_a +b b R mul2_F_b + +mul2_F_a +a b R mul2_G_sim +b a R mul2_F_sim + +mul2_F_b +a a R mul2_F_sim +b b L find_2_a + +find_2_sim +a a L find_2_a +b b L find_2_b + +find_2_a +a a L rewind_sim +b b L find_2_sim + +find_2_b +a a L find_2_sim +b b L check_halt_sim + +mul2_G_sim +a a R mul2_G_a +b a R mul2_G_b + +mul2_G_a +a a R mul2_G_sim +b a L mul2_G_extra + +mul2_G_b +a b R mul2_F_sim +b b R mul2_F_sim + +mul2_G_extra +a b R mul2_G_a +b b R rewind_b + +rewind_sim +a a L rewind_a +b b L rewind_b + +rewind_a +a a L rewind_sim +b b L rewind_sim + +rewind_b +a a L rewind_sim +b b R mul2_G_b + +check_halt_sim +a b L check_halt_a +b a R rewind_b + +check_halt_a +a HALT +b a R mul2_G_extra + diff --git a/baselines/tables/erdos_15.txt b/baselines/tables/erdos_15.txt new file mode 100644 index 00000000..c752aba4 --- /dev/null +++ b/baselines/tables/erdos_15.txt @@ -0,0 +1,33 @@ +# Derived from sources/erdos_15_sterin_woods.txt (bbsim, SHA-256 f9de29f3b3b06e55afbe61baddf317347b224a1a2203b4cf35f4027da1ecd9ac). +# 15 states, 2 symbols; the start state is 0 and the others follow the published order. +# Symbols: the blank `b` is 0 and `a` is 1. +# state 0: mul2_G_sim +# state 1: mul2_F_sim +# state 2: mul2_F_a +# state 3: mul2_F_b +# state 4: find_2_sim +# state 5: find_2_a +# state 6: find_2_b +# state 7: mul2_G_a +# state 8: mul2_G_b +# state 9: mul2_G_extra +# state 10: rewind_sim +# state 11: rewind_a +# state 12: rewind_b +# state 13: check_halt_sim +# state 14: check_halt_a +1R8 1R7 +0R3 1R2 +1R1 0R0 +0L5 1R1 +0L6 1L5 +0L4 1L10 +0L13 1L4 +1L9 1R0 +0R1 0R1 +0R12 0R7 +0L12 1L11 +0L10 1L10 +0R8 1L10 +1R12 0L14 +1R9 --- diff --git a/comparator/README.md b/comparator/README.md index e913838e..407d043d 100644 --- a/comparator/README.md +++ b/comparator/README.md @@ -11,8 +11,9 @@ using [`leanprover/comparator`](https://github.com/leanprover/comparator). defines all conjecture-checking baseline and candidate machines (`reference` and `candidate`), states the target mathematical propositions (`GoldbachConjecture`, `MatiyasevichRiemannCounterexample`, `ZFProvable`, `WadeZFProvable`, `PAProvable`, `paHalts`, - `paZFInconsistent`, etc.), and states all 29 target state-reduction, equivalence, `PA` - metatheory & internalized `ZF` provability, and semantics theorems with `sorry`. + `paZFInconsistent`, `ErdosPowersOfTwoConjecture`, etc.), and states all 34 target + state-reduction, equivalence, `PA` metatheory & internalized `ZF` provability, and semantics + theorems with `sorry`. - [`BusyBeaverChallenge.lean`](../BusyBeaverChallenge.lean) imports **only** Mathlib and Lean core (`Lean.Elab.Term`), defines the shared `BusyBeaver` Post-Turing execution model, accelerated `TapePatternSet`, `StackPatternSet`, stack/odometer/transducer reductions, and Collatz-like @@ -41,7 +42,8 @@ that: `halts_zf432_iff_wadeZFInconsistent`), first-order `PA` consistency and $\Sigma_1^0$ adequacy (`not_paProvable_false`, `paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`), the direct simulation reductions (`Goldbach21`, - `Zf380`, `Riemann104`), and all four `candidate_fewer_states` theorems (13 theorems total). + `Zf380`, `Riemann104`), the `Erdos14` reduction, and all five `candidate_fewer_states` + theorems (15 theorems total). Disallowing `Classical.choice` blocks classical `Con(ZF)` shortcuts (`not_zfInconsistent` in `ZFSet.{0}` or `Classical.em` + `digama0/ConZF`) for `Halts M ↔ ZFInconsistent`, while deeply embedded `PAProvable` provides a weak first-order metatheory strictly below `ZF` (see @@ -49,15 +51,16 @@ that: - **`["propext", "Quot.sound", "Classical.choice"]`:** allowed in [`all.json`](./all.json), [`busy_beaver.json`](./busy_beaver.json), and the classical model-theoretic / arithmetic-stage / analytic configs (`pa_semantics.json`, `zf_393.json`, `zf_semantics.json`, - `goldbach_semantics.json`, `riemann_95.json`, `riemann_120.json`, `riemann_semantics.json`). + `goldbach_semantics.json`, `riemann_95.json`, `riemann_120.json`, `riemann_semantics.json`, + `erdos_15.json`, `erdos_14.json`). 3. The exported proof terms are accepted by the Lean default kernel. ## Configurations | Config File | Challenge Module | Solution Module | Permitted Axioms | Verified Theorems | | :--- | :--- | :--- | :--- | :--- | -| [`constructive.json`](./constructive.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound` | All 13 constructive theorems: all 3 ZF proof-search equivalences (`zf_393`, `zf_380`, `zf_432`), first-order `PA` consistency & $\Sigma_1^0$ adequacy (`not_paProvable_false`, `paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`), direct state reductions (`Goldbach21`, `Zf380`, `Riemann104`), and `Riemann95.candidate_fewer_states` | -| [`all.json`](./all.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound`, `Classical.choice` | All 29 conjecture-checking state-reduction, equivalence, `PA` metatheory & internalized `ZF` provability, and semantics theorems | +| [`constructive.json`](./constructive.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound` | All 15 constructive theorems: all 3 ZF proof-search equivalences (`zf_393`, `zf_380`, `zf_432`), first-order `PA` consistency & $\Sigma_1^0$ adequacy (`not_paProvable_false`, `paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`), direct state reductions (`Goldbach21`, `Zf380`, `Riemann104`), `Riemann95.candidate_fewer_states`, and the `Erdos14` reduction | +| [`all.json`](./all.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound`, `Classical.choice` | All 34 conjecture-checking state-reduction, equivalence, `PA` metatheory & internalized `ZF` provability, and semantics theorems | | [`pa_semantics.json`](./pa_semantics.json) | `Challenge` | `Cryptids.Semantics.PA` | `propext`, `Quot.sound`, `Classical.choice` | `not_paProvable_false`, `paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`, `paProvable_sound_nat`, `paProvable_halts_zf380_iff_zf393`, `paProvable_halts_zf393_iff_zfInconsistent`, `paProvable_halts_zf380_iff_zfInconsistent` | | [`busy_beaver.json`](./busy_beaver.json) | `BusyBeaverChallenge` | `BusyBeaver` | `propext`, `Quot.sound`, `Classical.choice` | All 425 `BB(6)` and `BB(3, 3)` holdout theorems: Level A and Level B reductions (`is_closed_pattern_set`, `has_collatz_reduction`, `is_closed_stack_pattern_set`, `has_stacked_collatz_reduction`, `has_stack_reduction`, `has_odometer_reduction`, `has_transducer_reduction`, `is_valid_acceleration`, `isHalt_iff_acceleration`, `is_valid_highLevel_acceleration`, `isHalt_iff_highLevel_acceleration`, `acceleration_iff_highLevel_acceleration`) and A6 `is_not_halt` | | [`a6.json`](./a6.json) | `BusyBeaverChallenge` | `BusyBeaver.BB6.M_1RB0LF_1RC0RA_1LD0RB_0LE0LC_0LA0LC_0LBHHH` | `propext`, `Quot.sound`, `Classical.choice` | A6 `is_not_halt` | @@ -70,6 +73,8 @@ that: | [`riemann_95.json`](./riemann_95.json) | `Challenge` | `Cryptids.Semantics.Riemann95` | `propext`, `Quot.sound`, `Classical.choice` | `candidate_fewer_states`, `candidate_equivalent`, `halts_candidate_iff_not_riemannHypothesis` | | [`riemann_120.json`](./riemann_120.json) | `Challenge` | `Cryptids.Semantics.Riemann120` | `propext`, `Quot.sound`, `Classical.choice` | `halts_riemann120_iff_not_riemannHypothesis`, `halts_candidate_iff_not_riemannHypothesis` | | [`riemann_semantics.json`](./riemann_semantics.json) | `Challenge` | `Cryptids.Semantics.Riemann` | `propext`, `Quot.sound`, `Classical.choice` | `halts_riemann744_iff_exists_counterexample`, `halts_riemann744_iff_not_riemannHypothesis` | +| [`erdos_15.json`](./erdos_15.json) | `Challenge` | `Cryptids.Semantics.Erdos15` | `propext`, `Quot.sound`, `Classical.choice` | `halts_erdos15_iff_exists_counterexample`, `halts_erdos15_iff_not_erdosPowersOfTwo` | +| [`erdos_14.json`](./erdos_14.json) | `Challenge` | `Cryptids.Semantics.Erdos14` | `propext`, `Quot.sound`, `Classical.choice` | `candidate_fewer_states`, `candidate_equivalent`, `halts_candidate_iff_not_erdosPowersOfTwo` | The focused [`a6.json`](a6.json) configuration checks the A6 `IsNotHalt` theorem against `BusyBeaverChallenge`, using only its machine module as the diff --git a/comparator/all.json b/comparator/all.json index dc44d821..3b9b80ee 100644 --- a/comparator/all.json +++ b/comparator/all.json @@ -30,7 +30,12 @@ "ConjectureMachines.Riemann104.Semantics.halts_candidate_iff_not_riemannHypothesis", "ConjectureMachines.Riemann95.candidate_fewer_states", "ConjectureMachines.Riemann95.candidate_equivalent", - "ConjectureMachines.Riemann95.Semantics.halts_candidate_iff_not_riemannHypothesis" + "ConjectureMachines.Riemann95.Semantics.halts_candidate_iff_not_riemannHypothesis", + "ConjectureMachines.Erdos15.halts_erdos15_iff_exists_counterexample", + "ConjectureMachines.Erdos15.halts_erdos15_iff_not_erdosPowersOfTwo", + "ConjectureMachines.Erdos14.candidate_fewer_states", + "ConjectureMachines.Erdos14.candidate_equivalent", + "ConjectureMachines.Erdos14.Semantics.halts_candidate_iff_not_erdosPowersOfTwo" ], "permitted_axioms": [ "propext", diff --git a/comparator/constructive.json b/comparator/constructive.json index 5229c744..71b634a0 100644 --- a/comparator/constructive.json +++ b/comparator/constructive.json @@ -14,7 +14,9 @@ "ConjectureMachines.Semantics.PA.paZFInconsistent_holds_iff_zfInconsistent", "ConjectureMachines.Riemann104.candidate_fewer_states", "ConjectureMachines.Riemann104.candidate_equivalent", - "ConjectureMachines.Riemann95.candidate_fewer_states" + "ConjectureMachines.Riemann95.candidate_fewer_states", + "ConjectureMachines.Erdos14.candidate_fewer_states", + "ConjectureMachines.Erdos14.candidate_equivalent" ], "permitted_axioms": [ "propext", diff --git a/comparator/erdos_14.json b/comparator/erdos_14.json new file mode 100644 index 00000000..dc7e451d --- /dev/null +++ b/comparator/erdos_14.json @@ -0,0 +1,14 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Cryptids.Semantics.Erdos14", + "theorem_names": [ + "ConjectureMachines.Erdos14.candidate_fewer_states", + "ConjectureMachines.Erdos14.candidate_equivalent", + "ConjectureMachines.Erdos14.Semantics.halts_candidate_iff_not_erdosPowersOfTwo" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ] +} diff --git a/comparator/erdos_15.json b/comparator/erdos_15.json new file mode 100644 index 00000000..350eea2e --- /dev/null +++ b/comparator/erdos_15.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Cryptids.Semantics.Erdos15", + "theorem_names": [ + "ConjectureMachines.Erdos15.halts_erdos15_iff_exists_counterexample", + "ConjectureMachines.Erdos15.halts_erdos15_iff_not_erdosPowersOfTwo" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ] +} diff --git a/formalization.yaml b/formalization.yaml index 0d38853e..429ef352 100644 --- a/formalization.yaml +++ b/formalization.yaml @@ -9,9 +9,12 @@ project: reducing Andrew Wade's August 2026 machine zf_393, plus Wade's August 2025 432-state machine zf_432), and the Riemann Hypothesis (120 -> 104 -> 95 states reducing Joseph M. Shunia's September 2026 machine riemann_120, plus - the 2016 744-state machine riemann_744), proving halting equivalences and - connecting every machine's blank-tape halting behavior to the corresponding - statement in Mathlib. + the 2016 744-state machine riemann_744), and Erdős's conjecture on powers + of two (15 -> 14 states: Tristan Stérin and Damien Woods's 2021 15-state + machine erdos_15 and Tristan Stérin's October 2026 14-state machine + erdos_14), + proving halting equivalences and connecting every machine's blank-tape + halting behavior to the corresponding statement in Mathlib. authors: - "Maxence Faldor" - "Moritz Firsching" @@ -27,6 +30,7 @@ classification: msc2020: - "03D10" - "03E30" + - "11A63" - "11M26" - "11P32" - "68Q04" @@ -104,6 +108,63 @@ sources: location: "Math. Ann. 57 (1903), 195-204" relationship: "background" author_endorsement: "n/a" + - title: "Hardness of busy beaver value BB(15)" + authors: + - "Tristan Stérin" + - "Damien Woods" + id: "https://arxiv.org/abs/2107.12475" + type: "article" + relationship: "background" + author_endorsement: "not-contacted" + note: >- + Constructs the 15-state, 2-symbol machine erdos_15 (powers_of_two_15_2, + simulating a 5-state, 4-symbol machine) that halts iff Erdős's conjecture + on powers of two is false, with a pen-and-paper correctness proof + (machine file machines/powers_of_two_15_2.txt in + https://github.com/tcosmo/bbsim, commit 3f655ba2c73b, mirrored at + docs.bbchallenge.org); formalized here in Cryptids/Erdos15.lean and + Cryptids/Semantics/Erdos15.lean. + - title: "Some unconventional problems in number theory" + authors: + - "Paul Erdős" + id: "https://doi.org/10.1080/0025570X.1979.11976756" + type: "article" + location: "Math. Mag. 52 (1979), 67-70" + relationship: "background" + author_endorsement: "n/a" + - title: "Lean 4 formalization of the 15-state Erdős powers-of-two machine (erdos_15)" + authors: + - "Daniel Veljjanoski" + type: "original-proof" + relationship: "other" + note: >- + First Lean 4 proof that erdos_15 halts iff Erdős's conjecture on powers + of two is false (Cryptids/Erdos15.lean, Cryptids/Semantics/Erdos15.lean). + - title: "Cryptids (bbchallenge wiki): 14-state Erdős powers-of-two machine" + authors: + - "Tristan Stérin" + id: "https://wiki.bbchallenge.org/w/index.php?title=Cryptids&oldid=9722" + type: "web post" + relationship: "background" + author_endorsement: "not-contacted" + note: >- + The 14-state, 2-symbol machine erdos_14 + (1LB1RA_1LC1LB_0RD0RA_1LM0RE_1LF1RE_0LJ1LG_1RK0LH_1RI1LH_0LJ0RE_0RD1LJ_0LL1RK_1RN0LC_0LN---_0RK0LM), + announced by Tristan Stérin on the bbchallenge Discord in October 2026 + (https://discord.com/channels/960643023006490684/1561295445312151622/1562203343114473472) + and listed on the wiki (revision 9722, 28 Oct 2026) as not independently + verified as of October 2026; stored as + artifacts/erdos_14/machine.txt and formalized here in + Cryptids/Erdos14.lean and Cryptids/Semantics/Erdos14.lean. + - title: "Lean 4 formalization of the 14-state Erdős powers-of-two machine (erdos_14)" + authors: + - "Daniel Veljjanoski" + type: "original-proof" + relationship: "other" + note: >- + First Lean 4 proof that erdos_14 halts iff erdos_15 halts, and hence iff + Erdős's conjecture on powers of two is false (Cryptids/Erdos14.lean, + Cryptids/Semantics/Erdos14.lean). related_formalizations: - id: "https://github.com/lengyijun/goldbach_tm" @@ -117,9 +178,9 @@ related_formalizations: status: scope: >- All three ZF machine-to-proof-search equivalences (zf_393, zf_380, zf_432) - and the state-reduction halting equivalences for goldbach_21, zf_380, and - riemann_104 (along with all four candidate_fewer_states theorems, 10 - theorems total) are proved constructively using only propext and Quot.sound + and the state-reduction halting equivalences for goldbach_21, zf_380, + riemann_104, and erdos_14 (along with all five candidate_fewer_states + theorems, 12 theorems total) are proved constructively using only propext and Quot.sound (zero Classical.choice, audited via comparator/constructive.json so classical Con(ZF) shortcuts such as Soundness.lean's not_zfInconsistent are excluded; this establishes a constructive meta-level correspondence in Lean @@ -132,7 +193,15 @@ status: 120-state machine riemann_120, riemann_104 (Cryptids/Semantics/Riemann120.lean), and the 95-state arithmetic-stage reduction riemann_95 (Cryptids/Riemann95.lean, - Cryptids/Semantics/Riemann95.lean)—are proved with zero sorrys. + Cryptids/Semantics/Riemann95.lean)—are proved with zero sorrys. The + 15-state machine erdos_15 satisfies Halts erdos15 <-> ∃ n, 8 < n ∧ 2 ∉ pw n + constructively (Cryptids/Erdos15.lean, pw = base-3 digits of 2^n by + repeated doubling) and Halts erdos15 <-> ¬ ErdosPowersOfTwoConjecture via + Mathlib's Nat.digits (Cryptids/Semantics/Erdos15.lean). The 14-state + machine erdos_14 satisfies Halts erdos14 <-> ∃ n, 8 < n ∧ 2 ∉ pw n and + hence Halts candidate <-> Halts reference against erdos_15 constructively + (Cryptids/Erdos14.lean), and Halts candidate <-> ¬ + ErdosPowersOfTwoConjecture (Cryptids/Semantics/Erdos14.lean). sorry_count: 0 sorry_in_definitions: 0 axioms: @@ -250,6 +319,31 @@ status: sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator/riemann_95.json" + - declaration: "ConjectureMachines.Erdos15.halts_erdos15_iff_exists_counterexample" + file: "Cryptids/Semantics/Erdos15.lean" + sorry_count: 0 + axioms: ["propext", "Classical.choice", "Quot.sound"] + comparator_config: "comparator/erdos_15.json" + - declaration: "ConjectureMachines.Erdos15.halts_erdos15_iff_not_erdosPowersOfTwo" + file: "Cryptids/Semantics/Erdos15.lean" + sorry_count: 0 + axioms: ["propext", "Classical.choice", "Quot.sound"] + comparator_config: "comparator/erdos_15.json" + - declaration: "ConjectureMachines.Erdos14.candidate_fewer_states" + file: "Cryptids/Erdos14.lean" + sorry_count: 0 + axioms: ["propext"] + comparator_config: "comparator/constructive.json" + - declaration: "ConjectureMachines.Erdos14.candidate_equivalent" + file: "Cryptids/Erdos14.lean" + sorry_count: 0 + axioms: ["propext", "Quot.sound"] + comparator_config: "comparator/constructive.json" + - declaration: "ConjectureMachines.Erdos14.Semantics.halts_candidate_iff_not_erdosPowersOfTwo" + file: "Cryptids/Semantics/Erdos14.lean" + sorry_count: 0 + axioms: ["propext", "Classical.choice", "Quot.sound"] + comparator_config: "comparator/erdos_14.json" automation: methods: @@ -263,11 +357,23 @@ automation: spend_usd: "" hardware: "" prompting_notes: "" + - method: "agent" + models: + - "Claude Opus 5.5" + framework: "Claude Code" + tool_setup: "Lean 4 (v4.35.0-rc4), Mathlib" + prompting_notes: >- + Used as assistant for the erdos_15 and erdos_14 proofs + (Cryptids/Erdos15.lean, Cryptids/Semantics/Erdos15.lean, + Cryptids/Erdos14.lean, Cryptids/Semantics/Erdos14.lean). spend_usd: "" notes: >- Candidate state reductions and halting-equivalence proofs were discovered using Gemini Argon with an experimental harness; end-to-end - semantics proofs were developed interactively using Gemini Argon. + semantics proofs were developed interactively using Gemini Argon. The + erdos_15 machine is by Tristan Stérin and Damien Woods and the erdos_14 + machine by Tristan Stérin; the erdos_15 and erdos_14 proofs were written + by Daniel Veljjanoski with Claude (Anthropic) as assistant. fidelity: divergences: >- @@ -379,9 +485,30 @@ alignment: lean: "ConjectureMachines.Riemann95.Semantics.halts_candidate_iff_not_riemannHypothesis" module: "Cryptids.Semantics.Riemann95" status: "proved" + - source: "erdos_15 <-> ∃ n > 8, 2 ∉ Nat.digits 3 (2 ^ n)" + lean: "ConjectureMachines.Erdos15.halts_erdos15_iff_exists_counterexample" + module: "Cryptids.Semantics.Erdos15" + status: "proved" + - source: "erdos_15 <-> ¬ ErdosPowersOfTwoConjecture" + lean: "ConjectureMachines.Erdos15.halts_erdos15_iff_not_erdosPowersOfTwo" + module: "Cryptids.Semantics.Erdos15" + status: "proved" + - source: "erdos_14 < erdos_15 state reduction" + lean: "ConjectureMachines.Erdos14.candidate_fewer_states" + module: "Cryptids.Erdos14" + status: "proved" + - source: "erdos_14 <-> erdos_15 halting equivalence" + lean: "ConjectureMachines.Erdos14.candidate_equivalent" + module: "Cryptids.Erdos14" + status: "proved" + - source: "erdos_14 <-> ¬ ErdosPowersOfTwoConjecture" + lean: "ConjectureMachines.Erdos14.Semantics.halts_candidate_iff_not_erdosPowersOfTwo" + module: "Cryptids.Semantics.Erdos14" + status: "proved" acknowledgements: >- We thank Eric Wieser for careful review, the Busy Beaver Challenge community, Yijun Leng, Stefan O'Rear, Yuri Matiyasevich, Scott Aaronson, Adam Yedidia, - Andrew Wade, and Joseph M. Shunia for the Turing machines and compilers, and + Andrew Wade, Joseph M. Shunia, Tristan Stérin, and Damien Woods for the + Turing machines and compilers, and the Mathlib community. diff --git a/verify.py b/verify.py index dda00d31..d6f06454 100755 --- a/verify.py +++ b/verify.py @@ -21,8 +21,9 @@ (`baselines/sources/`) and re-compiles them from first principles into canonical transition tables, verifying byte-for-byte identity with `baselines/tables/`. -2. Verifies `Cryptids/Machines.lean` and checks that all 4 record candidate - machines (`goldbach_21`, `zf_380`, `riemann_104`, `riemann_95`) are well-formed +2. Verifies `Cryptids/Machines.lean` and checks that all 5 record candidate + machines (`goldbach_21`, `zf_380`, `riemann_104`, `riemann_95`, + `erdos_14`) are well-formed 2-symbol Turing machines matching their recorded state counts and SHA-256 digests, and that their `load_machine_rows%` tables in `Cryptids/Machines.lean` and `Challenge.lean` match `baselines/tables/` and `artifacts/*/machine.txt`. @@ -40,6 +41,10 @@ - Riemann (120 vs 104 states): 9,037-step self-bootstrap to `rhRootCfg` (`state 19`) and >1,000 post-boot root register-machine dispatches. - Riemann (95 states): exact 3,634-step bootstrap, including the entire tape. + - Erdos (15 states): at every stage the tape holds the base-3 digits of + `2^k` and the count of powers without a digit 2 (`Cryptids/Erdos15.lean`). + - Erdos (14 states): at every entry to the division state `D` the tape is + the configuration predicted by `Cryptids/Erdos14.lean`. """ from __future__ import annotations @@ -146,6 +151,24 @@ "states": 120, "symbols": 2, }, + "erdos_15": { + "source_file": "baselines/sources/erdos_15_sterin_woods.txt", + "source_sha256": ( + "f9de29f3b3b06e55afbe61baddf317347b224a1a2203b4cf35f4027da1ecd9ac" + ), + "table_file": "baselines/tables/erdos_15.txt", + "table_file_sha256": ( + "f70b7e4ada6b48644f02377bf1d045b3518e5a640a959a10442bace4311a98dd" + ), + "canonical_machine_sha256": ( + "2c38f44a6b344291c1169c35f348ed29d9ee51c1e922e1c43ebba5aeb3326c37" + ), + "lean_file": "Cryptids/Machines.lean", + "lean_def": "erdos15", + "format": "bbsim", + "states": 15, + "symbols": 2, + }, } CANDIDATES = [ @@ -209,6 +232,20 @@ "7e9731ed1b7c63d4e67c0f8d646f8498d9645f26e237a8604d4b7f91a6ab398d" ), }, + { + "id": "erdos_14", + "instance": "erdos_15", + "path": "artifacts/erdos_14", + "lean_file": "Cryptids/Machines.lean", + "lean_def": "erdos14", + "proof_path": "Cryptids/Erdos14.lean", + "challenge_path": "Challenge.lean", + "states": 14, + "baseline_states": 15, + "machine_sha256": ( + "ce72a09211f6118caadd4ed3cbdfb309a56574f2c49a36f0d82aa75eb2376f70" + ), + }, ] @@ -299,7 +336,10 @@ def parse_canonical_machine(text: str) -> Machine: def derive_machine_from_source(source_text: str, fmt: str) -> Machine: - """Re-derives canonical Machine from published source format (standard, tursi, nql).""" + """Re-derives canonical Machine from published source format. + + Formats: standard, tursi, nql, bbsim. + """ if fmt == "standard": blocks = source_text.strip().split("_") lines = [] @@ -353,6 +393,48 @@ def derive_machine_from_source(source_text: str, fmt: str) -> Machine: (st, r_sym): (w_sym, d, nxt if nxt in defined else None) for st, r_sym, w_sym, d, nxt in rows } + elif fmt == "bbsim": + # Stérin & Woods's `tcosmo/bbsim` machine files: `initial_state:` and + # `blank_symbol:` headers, then a state name followed by + # `read write move next` or `read HALT` lines, with letter symbols. + start = "" + blank = "" + order = [] + named_rows: list[tuple[str, str, str | None, str, str]] = [] + current = "" + for raw_line in source_text.splitlines(): + line = raw_line.split(";", 1)[0].strip() + if not line: + continue + key, sep, value = line.partition(":") + if sep: + if key.strip() == "initial_state": + start = value.strip() + elif key.strip() == "blank_symbol": + blank = value.strip() + continue + fields = line.split() + if len(fields) == 1: + current = fields[0] + order.append(current) + elif fields[1:] == ["HALT"]: + named_rows.append((current, fields[0], None, "", "")) + else: + r_sym, w_sym, move, nxt = fields + named_rows.append((current, r_sym, w_sym, move, nxt)) + letters = {r_sym for _, r_sym, _, _, _ in named_rows} + if len(letters) != 2 or blank not in letters: + raise ValueError(f"Expected 2 symbols including blank {blank!r}") + symbol = {blank: 0, (letters - {blank}).pop(): 1} + table = { + (st, symbol[r_sym]): ( + symbol[w_sym], + "L" if move.upper().startswith("L") else "R", + nxt, + ) + for st, r_sym, w_sym, move, nxt in named_rows + if w_sym is not None + } else: raise ValueError(f"Unknown format: {fmt}") @@ -653,6 +735,150 @@ def verify_riemann_95_bootstrap(machine: Machine) -> dict[str, object]: } +def verify_erdos_15_stages(machine: Machine, steps: int) -> dict[str, object]: + """Checks the stage layout of `Cryptids/Erdos15.lean` on the blank tape. + + Whenever `erdos_15` is in state 1 (`mul2_F_sim`) on cell 0, cells 0, 1, ... + hold the base-3 digits of `2^k` (least significant first, `0 -> 01`, + `1 -> 10`, `2 -> 11`), cells -2, -1 hold `#` (`00`), and cells -4, -3 hold + the number of `j <= k` such that `2^j` has no digit 2 (`00`, `01`, `10`, + `11`). + """ + proof_text = (ROOT / "Cryptids/Erdos15.lean").read_text(encoding="utf-8") + assert "theorem halts_erdos15_iff_exists_free" in proof_text + halting = [ + (q, sym) + for q, row in enumerate(machine.table) + for sym, tr in enumerate(row) + if tr is None + ] + assert halting == [(14, 1)], f"erdos_15 halting entries: {halting}" + + pair = {(0, 1): 0, (1, 0): 1, (1, 1): 2} + tape: dict[int, int] = {} + head = 0 + state = 0 + stage = 0 + free = 0 + for _ in range(steps): + if state == 1 and head == 0: + power = 2**stage + digits = [] + while power: + digits.append(power % 3) + power //= 3 + if 2 not in digits: + free += 1 + read = [] + pos = 0 + while (tape.get(pos, 0), tape.get(pos + 1, 0)) in pair: + read.append(pair[(tape.get(pos, 0), tape.get(pos + 1, 0))]) + pos += 2 + counter = 2 * tape.get(-4, 0) + tape.get(-3, 0) + assert read == digits, f"erdos_15 stage {stage}: {read} != {digits}" + assert counter == free, f"erdos_15 stage {stage}: counter {counter}" + assert tape.get(-2, 0) == tape.get(-1, 0) == 0 + assert all(-4 <= cell < pos for cell in tape) + stage += 1 + tr = machine.table[state][tape.get(head, 0)] + assert tr is not None and tr.next_state is not None, "erdos_15 halted" + if tr.write: + tape[head] = 1 + else: + tape.pop(head, None) + head += tr.direction + state = tr.next_state + + expected_free = len([k for k in (0, 2, 8) if k < stage]) + assert free == expected_free, f"Expected {expected_free} powers, got {free}" + return { + "steps_simulated": steps, + "stages_verified": stage, + "powers_without_digit_2": free, + } + + +def verify_erdos_14_stages(machine: Machine, steps: int) -> dict[str, object]: + """Checks the division layout of `Cryptids/Erdos14.lean` on the blank tape. + + Every time `erdos_14` enters state 3 (`D`), the head is on cell -1 and the + tape is `divCfg c q r`: cells -1, 0, ... hold `q` ones, a `0` and `r` ones, + cell -2 holds the separator `0`, and cells -3, -4, -5 hold the counter + (`000`, `100`, `111`, nearest first). The stage for `2^n` starts with + `q = 2^n, r = 0`; while `q % 3 != 2` and `q > 0` the next entry has + `q // 3` ones before the `0`. The counter `c` is the number of `1 <= j < n` + such that `2^j` has no digit 2, and the machine halts at the third. + """ + proof_text = (ROOT / "Cryptids/Erdos14.lean").read_text(encoding="utf-8") + assert "theorem halts_erdos14_iff_exists_free" in proof_text + halting = [ + (q, sym) + for q, row in enumerate(machine.table) + for sym, tr in enumerate(row) + if tr is None + ] + assert halting == [(12, 1)], f"erdos_14 halting entries: {halting}" + + counters = {0: (0, 0, 0), 1: (1, 0, 0), 2: (1, 1, 1)} + + def has_digit_2(m: int) -> bool: + while m: + if m % 3 == 2: + return True + m //= 3 + return False + + def expected_entries(): + c, n = 0, 1 + while True: + size = 2**n + q = size + while True: + yield c, n, q, size - q + if q == 0: + # Self-check of this model: the division finds a 2 iff 2^n has one. + assert not has_digit_2(size), f"erdos_14 model: stage {n}" + c += 1 + break + if q % 3 == 2: + assert has_digit_2(size), f"erdos_14 model: stage {n}" + break + q //= 3 + n += 1 + + entries = expected_entries() + ones: set[int] = set() + head = 0 + state = 0 + entries_verified = 0 + stage = 0 + for _ in range(steps): + tr = machine.table[state][int(head in ones)] + assert tr is not None and tr.next_state is not None, "erdos_14 halted" + if tr.write: + ones.add(head) + else: + ones.discard(head) + head += tr.direction + state = tr.next_state + if state == 3: + c, stage, q, r = next(entries) + expected = {-1 + i for i in range(q)} | {q + i for i in range(r)} + expected |= {-3 - i for i, bit in enumerate(counters[c]) if bit} + assert head == -1, f"erdos_14 stage {stage}: D entered at {head}" + assert ones == expected, f"erdos_14 stage {stage}: tape mismatch at q={q}" + entries_verified += 1 + + # Stage 9 (after both counter steps) starts at step 208,865. + if steps >= 210_000: + assert stage >= 9, f"erdos_14 reached only stage {stage}" + return { + "steps_simulated": steps, + "d_entries_verified": entries_verified, + "last_stage": stage, + } + + def extract_goldbach_chk0( machine: Machine, steps: int, is_candidate: bool ) -> dict[str, object]: @@ -928,6 +1154,24 @@ def run_verification( " t=3,634 (state 15, head -4) verified" ) + erdos_sim = verify_erdos_15_stages(baseline_machines["erdos_15"], steps) + report["simulations"]["erdos_15"] = erdos_sim + if verbose: + print( + f"[PASS] Erdos 15 stage simulation ({steps:,} steps):" + f" digits of 2^k and counter verified for k <" + f" {erdos_sim['stages_verified']}" + ) + + erdos14_sim = verify_erdos_14_stages(cand_machines["erdos_14"], steps) + report["simulations"]["erdos_14"] = erdos14_sim + if verbose: + print( + f"[PASS] Erdos 14 stage simulation ({steps:,} steps):" + f" {erdos14_sim['d_entries_verified']} division entries verified" + f" up to the start of stage n = {erdos14_sim['last_stage']}" + ) + # 5. Concrete blank-tape lockstep simulations gb_ref_sim = extract_goldbach_chk0( baseline_machines["goldbach"], steps, is_candidate=False