diff --git a/Challenge.lean b/Challenge.lean index 69e0957d..60991aec 100644 --- a/Challenge.lean +++ b/Challenge.lean @@ -27,7 +27,8 @@ Self-contained specification module audited against `Cryptids` by `leanprover/co `Zf380.Semantics.halts_candidate_iff_zfInconsistent`, `Semantics.Zf.halts_zf432_iff_wadeZFInconsistent`), and first-order Peano Arithmetic (`PA`) consistency and $\Sigma_1^0$ standard-model adequacy (`Semantics.PA.not_paProvable_false`, - `Semantics.PA.paHalts_holds_iff_halts`, `Semantics.PA.paZFInconsistent_holds_iff_zfInconsistent`) + `Semantics.PA.paHalts_holds_iff_halts`, `Semantics.PA.paZFInconsistent_holds_iff_zfInconsistent`), + and the `brocard_28` equivalence `Brocard28.halts_brocard28_iff_exists_square` are verified **without `Classical.choice`** (`ListBlank` uses primitive `Quot` rather than `Quotient` so `Halts` is choice-free). Because `Zf/Soundness.lean` proves `not_zfInconsistent` via `ZFSet.{0}` (`Classical.choice`)—and `CIC + EM` proves `Con(ZF)` without choice @@ -36,12 +37,13 @@ Self-contained specification module audited against `Cryptids` by `leanprover/co metatheory that cannot prove `Con(PA)` or `Con(ZF)` (see `Cryptids/Semantics/README.md`). - **Full gate (`comparator/all.json`; `permitted_axioms = ["propext", "Quot.sound", "Classical.choice"]`):** - Audits all 34 theorems, including `Riemann95.candidate_equivalent` (which uses `Classical.choice` + Audits all 36 theorems, including `Riemann95.candidate_equivalent` (which uses `Classical.choice` via `Nat.Prime`), classical `PA` and `ZFSet.{0}` soundness/non-halting, negated-`Π₁⁰` Goldbach (`¬ GoldbachConjecture`, which uses Markov's Principle), analytic `RiemannHypothesis` equivalences, and the `erdos_ternary_15` and `erdos_ternary_14` equivalences with `ErdosTernaryConjecture` (`Nat.digits` uses `Classical.choice`; `¬ ErdosTernaryConjecture` also - uses Markov's Principle). + uses Markov's Principle), and the `brocard_28` equivalence with `¬ BrocardConjecture` (Markov's + Principle). -/ meta section @@ -256,6 +258,11 @@ def erdosTernary14Rows : List (List (Option (Fin 2 × Dir × Fin 14))) := load_machine_rows% "artifacts/erdos_ternary_14/machine.txt" /-- 14-state Erdős candidate. -/ def erdosTernary14 : Machine 14 2 := Machine.ofRows erdosTernary14Rows +/-- Rows of `brocard28`. -/ +def brocard28Rows : List (List (Option (Fin 2 × Dir × Fin 28))) := + load_machine_rows% "artifacts/brocard_28/machine.txt" +/-- 28-state Brocard machine. -/ +def brocard28 : Machine 28 2 := Machine.ofRows brocard28Rows end Machines /-- **Goldbach's Conjecture**: every even integer greater than 2 is the sum of two primes. -/ @@ -747,6 +754,12 @@ and it implies Erdős Problem 406 def ErdosTernaryConjecture : Prop := ∀ n : ℕ, 8 < n → 2 ∈ Nat.digits 3 (2 ^ n) +/-- **Brocard's problem** (Brocard 1876, 1885; Ramanujan 1913): `n! + 1` is a perfect square +only for `n = 4, 5, 7` (`5 ^ 2`, `11 ^ 2`, `71 ^ 2`). Erdős conjectured that there are no other +solutions; none exist for `n ≤ 10 ^ 12` (Matson 2017). -/ +def BrocardConjecture : Prop := + ∀ n : ℕ, 7 < n → ¬ IsSquare (n.factorial + 1) + namespace Goldbach21 /-- 25-state Goldbach reference machine (`goldbach_25`, Yao & Leng 2024). -/ abbrev reference : BundledMachine 2 := Machines.goldbach25.bundle @@ -868,4 +881,13 @@ theorem halts_candidate_iff_not_erdosTernary : end Semantics end ErdosTernary14 +namespace Brocard28 +/-- 28-state Brocard machine (`brocard_28`, Veljjanoski 2026). -/ +abbrev brocard28 : Machine 28 2 := Machines.brocard28 +theorem halts_brocard28_iff_exists_square : + ConjectureMachines.Halts brocard28 ↔ ∃ n : ℕ, 7 < n ∧ IsSquare (n.factorial + 1) := by sorry +theorem halts_brocard28_iff_not_brocard : + ConjectureMachines.Halts brocard28 ↔ ¬ BrocardConjecture := by sorry +end Brocard28 + end ConjectureMachines diff --git a/Cryptids.lean b/Cryptids.lean index 8d75fcb9..7a1d5979 100644 --- a/Cryptids.lean +++ b/Cryptids.lean @@ -23,6 +23,8 @@ public import Cryptids.ErdosTernary15 public import Cryptids.Semantics.ErdosTernary15 public import Cryptids.ErdosTernary14 public import Cryptids.Semantics.ErdosTernary14 +public import Cryptids.Brocard28 +public import Cryptids.Semantics.Brocard28 /-! # Certified State Reductions & Formalized Conjecture-Checking Turing Machines @@ -30,7 +32,8 @@ public import Cryptids.Semantics.ErdosTernary14 This library formalizes record smaller 2-symbol Turing machines for **Goldbach's Conjecture** (`25 → 21` states), **ZF Set Theory Consistency** (`393 → 380` states), the **Riemann Hypothesis** (`120 → 104 → 95` states), and **Erdős's ternary conjecture** (`15 → 14` -states), as well as complete Lean 4 formalizations of all publicly +states), a 28-state machine for **Brocard's problem** (`brocard_28`), as well as complete +Lean 4 formalizations of all publicly known baseline machines (`goldbach_25`, `zf_432`, `zf_393`, `riemann_744`, `riemann_120`, `erdos_ternary_15`), linking every machine's blank-tape halting problem to Mathlib's statements: @@ -73,6 +76,11 @@ linking every machine's blank-tape halting problem to Mathlib's statements: `Halts erdosTernary14 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` and `Halts candidate ↔ Halts reference` relative to `erdosTernary15`, and `ConjectureMachines.ErdosTernary14.Semantics.halts_candidate_iff_not_erdosTernary`. +- `Cryptids.Brocard28`, `Cryptids.Semantics.Brocard28` — A 28-state machine for Brocard's problem + (`brocard28`), with constructive proofs of `Halts brocard28 ↔ ∃ n, 8 ≤ n ∧ IsTri (V n)` + (`V n = n! / 8`) and `ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square` + (`Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n! + 1)`), and + `ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard`. - `Cryptids.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/Brocard28.lean b/Cryptids/Brocard28.lean new file mode 100644 index 00000000..4fcbc748 --- /dev/null +++ b/Cryptids/Brocard28.lean @@ -0,0 +1,1068 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.ErdosTernary14 + +/-! +# Brocard28 + +The 28-state Turing machine `brocard_28` halts on the blank tape if and only if Brocard's +problem `n! + 1 = m ^ 2` has a solution with `n > 7`, i.e. beyond the three known solutions +`n = 4, 5, 7`. + +## Provenance and Attribution + +The machine and the proofs are by Daniel Veljjanoski, with Claude (Anthropic) as assistant +(November 2026). Earlier machines for the same problem are Charlie Reams's 61-state machine +with a Lean proof (`calr3/tinycryptids`, November 2026) and a 43-state table without a +machine-checked proof by Tandi, Gonzalez-Hendrix and Brown (); +Gasarch's SIGACT News Open Problems Column (September 2026, Open Problem 6.2) asks to improve +the 43-state count and reports Jonathan Brown's conjecture that about 30 states may suffice. + +## Machine Layout + +The tape holds, left to right, a block `N` of `n` ones, a separator, and a block `B` of ones, +all in unary. Between rounds `B` holds `n! / 8` ones (`3` at `n = 4`). A round multiplies `B` +by `n + 1` and grows `N` by one cell, then tests whether `(n + 1)! / 8` is a triangular number +`1 + 2 + ⋯ + k`; this holds if and only if `(n + 1)! + 1` is a perfect square (`m = 2k + 1`). + +* Multiply (states `2`–`11`): `LN0`/`LN1` walk left and write a `1` left of `N`; `EN` walks a + hole through `N`, and for every cell `R0`/`R1`/`L0`/`L1`/`EC` copy the template `B` once, + cell by cell, to the right end; `X` merges. `B` becomes `(n + 1) B + 1` ones. +* Test (states `1`, `12`–`19`): a hole walks right through `B` (`TLs`/`TLx` create it, `TE` + moves it); a block `S` right of `B` holds the current chunk size with a hole walking left + (`TR0`/`TR1`, `SB`); each wrap of `S` adds a cell to `S` for free (the blank beyond `S` + acts as the hole), and `SC` then checks whether `B` is exhausted: if so, success. +* Fail (states `20`–`22`): `ER`/`ER2`/`ER3` erase `S`, and `ER3` erases the last cell of `B` + on the way back, which cancels the extra cell left by the merge. +* Gate (states `23`–`27`): on success `M0`–`M3` walk left over `B` counting its ones modulo + `4`. At the separator, residue `0` halts (`M0` reading `0` is undefined); residues `2` and `3` + return via `Bs`, which fills the hole of `B`, and `ER` erases `S`. Since `32 ∣ n!` for + `n ≥ 8`, a success with `n ≥ 8` has residue `0`, while the known solutions have + `5! / 8 = 15 ≡ 3` and `7! / 8 = 630 ≡ 2 (mod 4)` and are suppressed. Residue `1` never + occurs at a success, so `M1` reading `0` is free for the start. +* Start: the machine starts in `GO` (state `0`) on the blank tape. `GO` and the two cells the + loop never reads (`TLx` and `M1` reading `0`) steer the loop's own states to write + `1111 0 111` in `46` steps, ending in `LN1` on the blank left of `N`: the configuration + every round passes through. +-/ + +@[expose] public section + +namespace ConjectureMachines.Brocard28 + +open Turing (Dir) +open StateTransition +open ErdosTernary15 (B0 B0_cons_zero nSteps nSteps_zero nSteps_succ nSteps_reaches nSteps_add + nSteps_bind_eq step_one reaches_imp_nSteps nSteps_eq_none_of_step_none) +open ErdosTernary14 (ones ones_succ' ones_add) + +local notation "mkL" => ErdosTernary15.Tape.mkL + +/-- The 28-state Brocard machine (`brocard_28`), loaded from `artifacts/brocard_28/machine.txt` +in `Machines.lean`. -/ +abbrev brocard28 : Machine 28 2 := Machines.brocard28 + +theorem mkL_B0 (R : ListBlank (Fin 2)) : mkL B0 R = ⟨0, B0, R⟩ := rfl + +theorem nSteps_cons {M : Machine 28 2} {n : ℕ} {c c₁ c₂ : Cfg 28 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 stepR {q q' : Fin 28} {a b : Fin 2} + (h : brocard28.transition q a = some (b, .right, q')) + (L R : ListBlank (Fin 2)) : + step brocard28 ⟨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 28} {a b : Fin 2} + (h : brocard28.transition q a = some (b, .left, q')) + (L R : ListBlank (Fin 2)) : + step brocard28 ⟨q, ⟨a, L, R⟩⟩ = some ⟨q', mkL L (R.cons b)⟩ := by + simp only [step, h, Option.map_some]; rfl + +/-! ## Transition Table + +States in file order: +`0` = GO, `1` = TLx, `2` = LN0, `3` = LN1, `4` = EN, `5` = S1, `6` = R0, `7` = R1, `8` = L0, +`9` = L1, `10` = EC, `11` = X, `12` = TLs, `13` = TR0, `14` = TR1, `15` = SB, `16` = SC, +`17` = TL0, `18` = TL1, `19` = TE, `20` = ER, `21` = ER2, `22` = ER3, `23` = M0, `24` = M1, +`25` = M2, `26` = M3, `27` = Bs. +-/ + +theorem sGO_0 (L R) : step brocard28 ⟨0, ⟨0, L, R⟩⟩ = some ⟨10, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sGO_1 (L R) : step brocard28 ⟨0, ⟨1, L, R⟩⟩ = some ⟨3, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sTLx_0 (L R) : step brocard28 ⟨1, ⟨0, L, R⟩⟩ = some ⟨10, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sTLx_1 (L R) : step brocard28 ⟨1, ⟨1, L, R⟩⟩ = some ⟨13, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sLN0_0 (L R) : step brocard28 ⟨2, ⟨0, L, R⟩⟩ = some ⟨3, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sLN0_1 (L R) : step brocard28 ⟨2, ⟨1, L, R⟩⟩ = some ⟨2, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sLN1_0 (L R) : step brocard28 ⟨3, ⟨0, L, R⟩⟩ = some ⟨4, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sLN1_1 (L R) : step brocard28 ⟨3, ⟨1, L, R⟩⟩ = some ⟨3, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sEN_0 (L R) : step brocard28 ⟨4, ⟨0, L, R⟩⟩ = some ⟨11, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sEN_1 (L R) : step brocard28 ⟨4, ⟨1, L, R⟩⟩ = some ⟨5, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sS1_0 (L R) : step brocard28 ⟨5, ⟨0, L, R⟩⟩ = some ⟨10, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sS1_1 (L R) : step brocard28 ⟨5, ⟨1, L, R⟩⟩ = some ⟨5, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sR0_0 (L R) : step brocard28 ⟨6, ⟨0, L, R⟩⟩ = some ⟨7, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sR0_1 (L R) : step brocard28 ⟨6, ⟨1, L, R⟩⟩ = some ⟨6, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sR1_0 (L R) : step brocard28 ⟨7, ⟨0, L, R⟩⟩ = some ⟨8, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sR1_1 (L R) : step brocard28 ⟨7, ⟨1, L, R⟩⟩ = some ⟨7, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sL0_0 (L R) : step brocard28 ⟨8, ⟨0, L, R⟩⟩ = some ⟨9, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sL0_1 (L R) : step brocard28 ⟨8, ⟨1, L, R⟩⟩ = some ⟨8, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sL1_0 (L R) : step brocard28 ⟨9, ⟨0, L, R⟩⟩ = some ⟨10, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sL1_1 (L R) : step brocard28 ⟨9, ⟨1, L, R⟩⟩ = some ⟨9, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sEC_0 (L R) : step brocard28 ⟨10, ⟨0, L, R⟩⟩ = some ⟨2, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sEC_1 (L R) : step brocard28 ⟨10, ⟨1, L, R⟩⟩ = some ⟨6, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sX_0 (L R) : step brocard28 ⟨11, ⟨0, L, R⟩⟩ = some ⟨12, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sX_1 (L R) : step brocard28 ⟨11, ⟨1, L, R⟩⟩ = some ⟨11, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sTLs_0 (L R) : step brocard28 ⟨12, ⟨0, L, R⟩⟩ = some ⟨1, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sTLs_1 (L R) : step brocard28 ⟨12, ⟨1, L, R⟩⟩ = some ⟨12, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sTR0_0 (L R) : step brocard28 ⟨13, ⟨0, L, R⟩⟩ = some ⟨14, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sTR0_1 (L R) : step brocard28 ⟨13, ⟨1, L, R⟩⟩ = some ⟨13, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sTR1_0 (L R) : step brocard28 ⟨14, ⟨0, L, R⟩⟩ = some ⟨15, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sTR1_1 (L R) : step brocard28 ⟨14, ⟨1, L, R⟩⟩ = some ⟨14, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sSB_0 (L R) : step brocard28 ⟨15, ⟨0, L, R⟩⟩ = some ⟨16, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sSB_1 (L R) : step brocard28 ⟨15, ⟨1, L, R⟩⟩ = some ⟨17, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sSC_0 (L R) : step brocard28 ⟨16, ⟨0, L, R⟩⟩ = some ⟨23, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sSC_1 (L R) : step brocard28 ⟨16, ⟨1, L, R⟩⟩ = some ⟨13, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sTL0_0 (L R) : step brocard28 ⟨17, ⟨0, L, R⟩⟩ = some ⟨18, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sTL0_1 (L R) : step brocard28 ⟨17, ⟨1, L, R⟩⟩ = some ⟨17, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sTL1_0 (L R) : step brocard28 ⟨18, ⟨0, L, R⟩⟩ = some ⟨19, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sTL1_1 (L R) : step brocard28 ⟨18, ⟨1, L, R⟩⟩ = some ⟨18, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sTE_0 (L R) : step brocard28 ⟨19, ⟨0, L, R⟩⟩ = some ⟨20, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sTE_1 (L R) : step brocard28 ⟨19, ⟨1, L, R⟩⟩ = some ⟨13, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sER_0 (L R) : step brocard28 ⟨20, ⟨0, L, R⟩⟩ = some ⟨21, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sER_1 (L R) : step brocard28 ⟨20, ⟨1, L, R⟩⟩ = some ⟨20, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sER2_0 (L R) : step brocard28 ⟨21, ⟨0, L, R⟩⟩ = some ⟨22, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sER2_1 (L R) : step brocard28 ⟨21, ⟨1, L, R⟩⟩ = some ⟨21, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sER3_0 (L R) : step brocard28 ⟨22, ⟨0, L, R⟩⟩ = some ⟨22, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sER3_1 (L R) : step brocard28 ⟨22, ⟨1, L, R⟩⟩ = some ⟨2, mkL L (R.cons 0)⟩ := + stepL rfl L R +theorem sM0_0 (L R : ListBlank (Fin 2)) : step brocard28 ⟨23, ⟨0, L, R⟩⟩ = none := rfl +theorem sM0_1 (L R) : step brocard28 ⟨23, ⟨1, L, R⟩⟩ = some ⟨24, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sM1_0 (L R) : step brocard28 ⟨24, ⟨0, L, R⟩⟩ = some ⟨0, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sM1_1 (L R) : step brocard28 ⟨24, ⟨1, L, R⟩⟩ = some ⟨25, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sM2_0 (L R) : step brocard28 ⟨25, ⟨0, L, R⟩⟩ = some ⟨27, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sM2_1 (L R) : step brocard28 ⟨25, ⟨1, L, R⟩⟩ = some ⟨26, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sM3_0 (L R) : step brocard28 ⟨26, ⟨0, L, R⟩⟩ = some ⟨27, Tape.mk' (L.cons 0) R⟩ := + stepR rfl L R +theorem sM3_1 (L R) : step brocard28 ⟨26, ⟨1, L, R⟩⟩ = some ⟨23, mkL L (R.cons 1)⟩ := + stepL rfl L R +theorem sBs_0 (L R) : step brocard28 ⟨27, ⟨0, L, R⟩⟩ = some ⟨20, Tape.mk' (L.cons 1) R⟩ := + stepR rfl L R +theorem sBs_1 (L R) : step brocard28 ⟨27, ⟨1, L, R⟩⟩ = some ⟨27, Tape.mk' (L.cons 1) R⟩ := + stepR 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, + sGO_0, sGO_1, sTLx_0, sTLx_1, sLN0_0, sLN0_1, sLN1_0, sLN1_1, sEN_0, sEN_1, sS1_0, sS1_1, + sR0_0, sR0_1, sR1_0, sR1_1, sL0_0, sL0_1, sL1_0, sL1_1, sEC_0, sEC_1, sX_0, sX_1, sTLs_0, + sTLs_1, sTR0_0, sTR0_1, sTR1_0, sTR1_1, sSB_0, sSB_1, sSC_0, sSC_1, sTL0_0, sTL0_1, sTL1_0, + sTL1_1, sTE_0, sTE_1, sER_0, sER_1, sER2_0, sER2_1, sER3_0, sER3_1, sM0_1, sM1_0, sM1_1, + sM2_0, sM2_1, sM3_0, sM3_1, sBs_0, sBs_1, + ErdosTernary15.Tape.mk'_cons, ErdosTernary15.Tape.mkL_cons, ErdosTernary15.Tape.mk'_B0, mkL_B0, + ListBlank.append, B0_cons_zero]) + +/-! ## Sweeps over Ones -/ + +theorem sweepR {q : Fin 28} + (h : ∀ L R, step brocard28 ⟨q, ⟨1, L, R⟩⟩ = some ⟨q, Tape.mk' (L.cons 1) R⟩) + (k : ℕ) (L R : ListBlank (Fin 2)) : + nSteps brocard28 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, + ErdosTernary15.Tape.mk'_cons, h, Option.bind_some, ih, ones_succ'] + +theorem sweepL {q : Fin 28} + (h : ∀ L R, step brocard28 ⟨q, ⟨1, L, R⟩⟩ = some ⟨q, mkL L (R.cons 1)⟩) + (k : ℕ) (L R : ListBlank (Fin 2)) : + nSteps brocard28 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, + ErdosTernary15.Tape.mkL_cons, h, Option.bind_some, ih, ones_succ'] + +/-! ## Tape Encoding and Configurations -/ + +/-- The cells left of `B`: the separator, then the `n` cells of `N`. -/ +def NL (n : ℕ) : ListBlank (Fin 2) := (ones n B0).cons 0 + +/-- Start of a round: `LN0` on the last of the `v + 1` cells of `B`, `N` has `n` cells. -/ +def roundCfg (n v : ℕ) : Cfg 28 2 := ⟨2, Tape.mk' (ones v (NL n)) (B0.cons 1)⟩ + +/-- Start of a test: `TLx` on the first of the `M` cells of `B`. -/ +def testCfg (n M : ℕ) : Cfg 28 2 := ⟨1, Tape.mk' (NL n) (ones M B0)⟩ + +/-- Inside the copy loop: `R0` right of the cursor hole; `u` template cells are done and `v` +remain, `M` has `m` cells, and `N`'s hole has `a` cells to its left and `b` to its right. -/ +def copyCfg (a b u v m : ℕ) : Cfg 28 2 := + ⟨6, Tape.mk' ((ones u ((ones b ((ones a B0).cons 0)).cons 0)).cons 0) + (ones v ((ones m B0).cons 0))⟩ + +/-- `EN` on the first of the `b` remaining cells of `N`, `a` cells to its left; the template +has `V` cells and `M` has `m`. -/ +def enCfg (a b V m : ℕ) : Cfg 28 2 := + ⟨4, Tape.mk' (ones a B0) (ones b ((ones V ((ones m B0).cons 0)).cons 0))⟩ + +/-- Inside the test: `TR0` on the separator right of `B`; the hole of `B` has `a` cells to its +left and `r` to its right; `S` has `p` cells, a hole, and `q` cells (`q = 0` and the blank +beyond `S` as the hole for a solid `S` of `p` cells). -/ +def advCfg (n a r p q : ℕ) : Cfg 28 2 := + ⟨13, Tape.mk' (ones r ((ones a (NL n)).cons 0)) ((ones p ((ones q B0).cons 0)).cons 0)⟩ + +theorem ones_zero (L : ListBlank (Fin 2)) : ones 0 L = L := rfl + +theorem ones_zero_B0 : ones 0 B0 = B0 := rfl + +theorem advCfg_solid (n a r p : ℕ) : + advCfg n a r p 0 = ⟨13, Tape.mk' (ones r ((ones a (NL n)).cons 0)) ((ones p B0).cons 0)⟩ := by + simp only [advCfg, ones_zero_B0, B0_cons_zero] + +/-! ## Multiply (States `2`–`11`) -/ + +/-- One copy step: the cursor moves one cell right and `M` gains a cell. -/ +theorem copy_step (a b u v m : ℕ) : + ∃ s, nSteps brocard28 s (copyCfg a b u (v + 1) m) = some (copyCfg a b (u + 1) v (m + 1)) := by + set W := (ones b ((ones a B0).cons 0)).cons 0 with hW + set Y := ones u W with hY + have h₁ := sweepR sR0_1 (v + 1) (Y.cons 0) ((ones m B0).cons 0) + have h₂ : step brocard28 ⟨6, Tape.mk' (ones (v + 1) (Y.cons 0)) ((ones m B0).cons 0)⟩ = + some ⟨7, Tape.mk' ((ones (v + 1) (Y.cons 0)).cons 0) (ones m B0)⟩ := by + rw [ErdosTernary15.Tape.mk'_cons, sR0_0] + have h₃ := sweepR sR1_1 m ((ones (v + 1) (Y.cons 0)).cons 0) B0 + have h₄ : step brocard28 ⟨7, Tape.mk' (ones m ((ones (v + 1) (Y.cons 0)).cons 0)) B0⟩ = + some ⟨8, mkL (ones m ((ones (v + 1) (Y.cons 0)).cons 0)) (B0.cons 1)⟩ := by + rw [ErdosTernary15.Tape.mk'_B0, sR1_0] + have h₅ := sweepL sL0_1 m ((ones (v + 1) (Y.cons 0)).cons 0) (B0.cons 1) + have h₆ : step brocard28 ⟨8, mkL ((ones (v + 1) (Y.cons 0)).cons 0) (ones m (B0.cons 1))⟩ = + some ⟨9, mkL (ones (v + 1) (Y.cons 0)) ((ones (m + 1) B0).cons 0)⟩ := by + rw [ErdosTernary15.Tape.mkL_cons, sL0_0, ones_succ' m] + have h₇ := sweepL sL1_1 (v + 1) (Y.cons 0) ((ones (m + 1) B0).cons 0) + have h₈ : nSteps brocard28 2 ⟨9, mkL (Y.cons 0) (ones (v + 1) ((ones (m + 1) B0).cons 0))⟩ = + some (copyCfg a b (u + 1) v (m + 1)) := by + change nSteps brocard28 2 ⟨9, mkL (Y.cons 0) ((ones v ((ones (m + 1) B0).cons 0)).cons 1)⟩ = + some ⟨6, Tape.mk' ((Y.cons 1).cons 0) (ones v ((ones (m + 1) B0).cons 0))⟩ + tm_run + exact ⟨_, nSteps_bind_eq h₁ (nSteps_cons h₂ (nSteps_bind_eq h₃ (nSteps_cons h₄ + (nSteps_bind_eq h₅ (nSteps_cons h₆ (nSteps_bind_eq h₇ h₈))))))⟩ + +/-- The last copy step: the cursor leaves the template, `LN0`/`LN1` return to the hole of `N` +and fill it, and `EN` reads the next cell of `N`. -/ +theorem copy_done (a b u m : ℕ) : + ∃ s, nSteps brocard28 s (copyCfg a b u 0 m) = some (enCfg (a + 1) b (u + 1) (m + 1)) := by + set W := (ones b ((ones a B0).cons 0)).cons 0 with hW + set Y := ones u W with hY + have h₂ : step brocard28 (copyCfg a b u 0 m) = + some ⟨7, Tape.mk' ((Y.cons 0).cons 0) (ones m B0)⟩ := by + change step brocard28 ⟨6, Tape.mk' (Y.cons 0) ((ones m B0).cons 0)⟩ = _ + rw [ErdosTernary15.Tape.mk'_cons, sR0_0] + have h₃ := sweepR sR1_1 m ((Y.cons 0).cons 0) B0 + have h₄ : step brocard28 ⟨7, Tape.mk' (ones m ((Y.cons 0).cons 0)) B0⟩ = + some ⟨8, mkL (ones m ((Y.cons 0).cons 0)) (B0.cons 1)⟩ := by + rw [ErdosTernary15.Tape.mk'_B0, sR1_0] + have h₅ := sweepL sL0_1 m ((Y.cons 0).cons 0) (B0.cons 1) + have h₆ : nSteps brocard28 3 ⟨8, mkL ((Y.cons 0).cons 0) (ones m (B0.cons 1))⟩ = + some ⟨2, mkL (Y.cons 1) ((ones (m + 1) B0).cons 0)⟩ := by + rw [ones_succ' m] + tm_run + have h₇ := sweepL sLN0_1 (u + 1) W ((ones (m + 1) B0).cons 0) + have h₈ : step brocard28 ⟨2, mkL W (ones (u + 1) ((ones (m + 1) B0).cons 0))⟩ = + some ⟨3, mkL (ones b ((ones a B0).cons 0)) + ((ones (u + 1) ((ones (m + 1) B0).cons 0)).cons 0)⟩ := by + rw [hW, ErdosTernary15.Tape.mkL_cons, sLN0_0] + have h₉ := sweepL sLN1_1 b ((ones a B0).cons 0) + ((ones (u + 1) ((ones (m + 1) B0).cons 0)).cons 0) + have h₁₀ : step brocard28 ⟨3, mkL ((ones a B0).cons 0) + (ones b ((ones (u + 1) ((ones (m + 1) B0).cons 0)).cons 0))⟩ = + some (enCfg (a + 1) b (u + 1) (m + 1)) := by + rw [ErdosTernary15.Tape.mkL_cons, sLN1_0] + rfl + have hY1 : Y.cons 1 = ones (u + 1) W := rfl + rw [hY1] at h₆ + exact ⟨_, nSteps_cons h₂ (nSteps_bind_eq h₃ (nSteps_cons h₄ (nSteps_bind_eq h₅ + (nSteps_bind_eq h₆ (nSteps_bind_eq h₇ (nSteps_cons h₈ (nSteps_bind_eq h₉ + (step_one h₁₀))))))))⟩ + +/-- A whole copy of the template. -/ +theorem copy_loop (a b u : ℕ) : ∀ v m, ∃ s, nSteps brocard28 s (copyCfg a b u v m) = + some (enCfg (a + 1) b (u + v + 1) (m + v + 1)) := by + intro v + induction v generalizing u with + | zero => intro m; simpa using copy_done a b u m + | succ v ih => + intro m + obtain ⟨s₁, hs₁⟩ := copy_step a b u v m + obtain ⟨s₂, hs₂⟩ := ih (u + 1) (m + 1) + refine ⟨s₁ + s₂, ?_⟩ + rw [show u + (v + 1) + 1 = u + 1 + v + 1 by omega, + show m + (v + 1) + 1 = m + 1 + v + 1 by omega] + exact nSteps_bind_eq hs₁ hs₂ + +/-- `EN` finds a cell of `N`: it becomes the hole, `S1` runs to `B`, and `EC` makes the cursor. -/ +theorem en_step (a c w m : ℕ) : + ∃ s, nSteps brocard28 s (enCfg a (c + 1) (w + 1) m) = some (copyCfg a c 0 w m) := by + have h₁ : step brocard28 (enCfg a (c + 1) (w + 1) m) = + some ⟨5, Tape.mk' ((ones a B0).cons 0) + (ones c ((ones (w + 1) ((ones m B0).cons 0)).cons 0))⟩ := by + change step brocard28 ⟨4, Tape.mk' (ones a B0) + ((ones c ((ones (w + 1) ((ones m B0).cons 0)).cons 0)).cons 1)⟩ = _ + rw [ErdosTernary15.Tape.mk'_cons, sEN_1] + have h₂ := sweepR sS1_1 c ((ones a B0).cons 0) ((ones (w + 1) ((ones m B0).cons 0)).cons 0) + have h₃ : nSteps brocard28 2 ⟨5, Tape.mk' (ones c ((ones a B0).cons 0)) + ((ones (w + 1) ((ones m B0).cons 0)).cons 0)⟩ = some (copyCfg a c 0 w m) := by + change nSteps brocard28 2 ⟨5, Tape.mk' (ones c ((ones a B0).cons 0)) + (((ones w ((ones m B0).cons 0)).cons 1).cons 0)⟩ = + some ⟨6, Tape.mk' (((ones c ((ones a B0).cons 0)).cons 0).cons 0) + (ones w ((ones m B0).cons 0))⟩ + tm_run + exact ⟨_, nSteps_cons h₁ (nSteps_bind_eq h₂ h₃)⟩ + +/-- The hole of `N` walks through the `b` remaining cells, one copy of the template each. -/ +theorem en_loop (w : ℕ) : ∀ a b m, ∃ s, nSteps brocard28 s (enCfg a b (w + 1) m) = + some (enCfg (a + b) 0 (w + 1) (m + b * (w + 1))) := by + intro a b + induction b generalizing a with + | zero => intro m; exact ⟨0, by simp [enCfg]⟩ + | succ c ih => + intro m + obtain ⟨s₁, hs₁⟩ := en_step a c w m + obtain ⟨s₂, hs₂⟩ := copy_loop a c 0 w m + obtain ⟨s₃, hs₃⟩ := ih (a + 1) (m + w + 1) + refine ⟨s₁ + s₂ + s₃, ?_⟩ + rw [show a + (c + 1) = a + 1 + c by omega, + show m + (c + 1) * (w + 1) = m + w + 1 + c * (w + 1) by ring] + simp only [Nat.zero_add] at hs₂ + exact nSteps_bind_eq (nSteps_bind_eq hs₁ hs₂) hs₃ + +/-- `N` exhausted: `X` merges the template and `M`, `TLs` returns to the start of `B`. -/ +theorem en_exit (a V m : ℕ) : + ∃ s, nSteps brocard28 s (enCfg a 0 V (m + 1)) = some (testCfg a (V + m + 2)) := by + have h₁ : step brocard28 (enCfg a 0 V (m + 1)) = + some ⟨11, Tape.mk' ((ones a B0).cons 0) (ones V ((ones (m + 1) B0).cons 0))⟩ := by + change step brocard28 ⟨4, Tape.mk' (ones a B0) + ((ones V ((ones (m + 1) B0).cons 0)).cons 0)⟩ = _ + rw [ErdosTernary15.Tape.mk'_cons, sEN_0] + have h₂ := sweepR sX_1 V ((ones a B0).cons 0) ((ones (m + 1) B0).cons 0) + have h₃ : step brocard28 ⟨11, Tape.mk' (ones V ((ones a B0).cons 0)) + ((ones (m + 1) B0).cons 0)⟩ = some ⟨12, mkL (ones (V + 2) (NL a)) (ones m B0)⟩ := by + rw [ErdosTernary15.Tape.mk'_cons, sX_0] + change some (⟨12, Tape.mk' ((ones V (NL a)).cons 1) ((ones m B0).cons 1)⟩ : Cfg 28 2) = + some (⟨12, mkL (((ones V (NL a)).cons 1).cons 1) (ones m B0)⟩ : Cfg 28 2) + rw [ErdosTernary15.Tape.mk'_cons, ErdosTernary15.Tape.mkL_cons] + have h₄ := sweepL sTLs_1 (V + 2) (NL a) (ones m B0) + have h₅ : step brocard28 ⟨12, mkL (NL a) (ones (V + 2) (ones m B0))⟩ = + some (testCfg a (V + m + 2)) := by + rw [NL, ErdosTernary15.Tape.mkL_cons, sTLs_0, ← ones_add] + rw [show V + 2 + m = V + m + 2 by omega] + rfl + exact ⟨_, nSteps_cons h₁ (nSteps_bind_eq h₂ (nSteps_cons h₃ (nSteps_bind_eq h₄ + (step_one h₅))))⟩ + +/-- `LN1` on the blank left of `N` writes the new cell of `N`, and `EN` reads `N`'s first +cell. -/ +theorem ln_exit (n v : ℕ) : + step brocard28 ⟨3, mkL B0 (ones n ((ones (v + 1) B0).cons 0))⟩ = + some (enCfg 1 n (v + 1) 0) := by + rw [mkL_B0, sLN1_0] + change _ = some (⟨4, Tape.mk' (B0.cons 1) + (ones n ((ones (v + 1) ((ones 0 B0).cons 0)).cons 0))⟩ : Cfg 28 2) + rw [ones_zero_B0, B0_cons_zero] + +/-- The start of a round: `LN0`/`LN1` write a cell left of `N` and `EN` reads its first cell. -/ +theorem round_start (n v : ℕ) : + ∃ s, nSteps brocard28 s (roundCfg n v) = some (enCfg 1 n (v + 1) 0) := by + have h₁ : roundCfg n v = ⟨2, mkL (ones (v + 1) (NL n)) B0⟩ := by + change (⟨2, Tape.mk' (ones v (NL n)) (B0.cons 1)⟩ : Cfg 28 2) = + ⟨2, mkL ((ones v (NL n)).cons 1) B0⟩ + rw [ErdosTernary15.Tape.mk'_cons, ErdosTernary15.Tape.mkL_cons] + have h₂ := sweepL sLN0_1 (v + 1) (NL n) B0 + have h₃ : step brocard28 ⟨2, mkL (NL n) (ones (v + 1) B0)⟩ = + some ⟨3, mkL (ones n B0) ((ones (v + 1) B0).cons 0)⟩ := by + rw [NL, ErdosTernary15.Tape.mkL_cons, sLN0_0] + have h₄ := sweepL sLN1_1 n B0 ((ones (v + 1) B0).cons 0) + rw [h₁] + exact ⟨_, nSteps_bind_eq h₂ (nSteps_cons h₃ (nSteps_bind_eq h₄ (step_one (ln_exit n v))))⟩ + +/-- From `EN` on the first cell of `N`: `B` with `v + 1` cells becomes `(n + 1) (v + 1) + 1` +cells and the test starts. -/ +theorem multiply_en (n v : ℕ) (hn : 1 ≤ n) : + ∃ s, nSteps brocard28 s (enCfg 1 n (v + 1) 0) = + some (testCfg (n + 1) ((n + 1) * (v + 1) + 1)) := by + obtain ⟨s₂, hs₂⟩ := en_loop v 1 n 0 + obtain ⟨m, hm⟩ : ∃ m, 0 + n * (v + 1) = m + 1 := ⟨n * (v + 1) - 1, by + have : 1 ≤ n * (v + 1) := Nat.one_le_iff_ne_zero.mpr (Nat.mul_ne_zero (by omega) (by omega)) + omega⟩ + rw [hm] at hs₂ + obtain ⟨s₃, hs₃⟩ := en_exit (1 + n) (v + 1) m + refine ⟨s₂ + s₃, ?_⟩ + have e : (n + 1) * (v + 1) + 1 = v + 1 + m + 2 := by + have : (n + 1) * (v + 1) = v + 1 + n * (v + 1) := by ring + omega + rw [show n + 1 = 1 + n by omega] at e ⊢ + rw [e] + exact nSteps_bind_eq hs₂ hs₃ + +/-- A whole round: `B` with `v + 1` cells becomes `(n + 1) (v + 1) + 1` cells and `N` grows. -/ +theorem multiply (n v : ℕ) (hn : 1 ≤ n) : + ∃ s, 1 ≤ s ∧ nSteps brocard28 s (roundCfg n v) = + some (testCfg (n + 1) ((n + 1) * (v + 1) + 1)) := by + obtain ⟨s₁, hs₁⟩ := round_start n v + obtain ⟨s₂, hs₂⟩ := multiply_en n v hn + refine ⟨s₁ + s₂, ?_, nSteps_bind_eq hs₁ hs₂⟩ + have : 1 ≤ s₁ := by + rcases Nat.eq_zero_or_pos s₁ with rfl | h + · simp [roundCfg, enCfg] at hs₁ + · exact h + omega + +/-! ## Test and Fail (States `1`, `12`–`22`) -/ + +/-- `k` zeros followed by `L`. -/ +def zeros (k : ℕ) (L : ListBlank (Fin 2)) : ListBlank (Fin 2) := + ListBlank.append (List.replicate k 0) L + +theorem zeros_succ' (k : ℕ) (L : ListBlank (Fin 2)) : zeros (k + 1) L = zeros k (L.cons 0) := by + rw [zeros, List.replicate_succ', ListBlank.append_assoc] + rfl + +theorem zeros_B0 (k : ℕ) : zeros k B0 = B0 := by + induction k with + | zero => rfl + | succ k ih => rw [zeros_succ', B0_cons_zero, ih] + +/-- A state that erases ones while moving right. -/ +theorem sweepR_erase {q : Fin 28} + (h : ∀ L R, step brocard28 ⟨q, ⟨1, L, R⟩⟩ = some ⟨q, Tape.mk' (L.cons 0) R⟩) + (k : ℕ) (L R : ListBlank (Fin 2)) : + nSteps brocard28 k ⟨q, Tape.mk' L (ones k R)⟩ = some ⟨q, Tape.mk' (zeros 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, + ErdosTernary15.Tape.mk'_cons, h, Option.bind_some, ih, zeros_succ'] + +/-- A state that moves left over zeros. -/ +theorem sweepL_zeros {q : Fin 28} + (h : ∀ L R, step brocard28 ⟨q, ⟨0, L, R⟩⟩ = some ⟨q, mkL L (R.cons 0)⟩) + (k : ℕ) (L R : ListBlank (Fin 2)) : + nSteps brocard28 k ⟨q, mkL (zeros k L) R⟩ = some ⟨q, mkL L (zeros k R)⟩ := by + induction k generalizing R with + | zero => rfl + | succ k ih => + rw [nSteps_succ, show zeros (k + 1) L = (zeros k L).cons 0 from rfl, + ErdosTernary15.Tape.mkL_cons, h, Option.bind_some, ih, zeros_succ'] + +/-- `TR0` right after the hole of `B`, with `r` cells of `B` still to pass. -/ +def tCfg (n a r p q : ℕ) : Cfg 28 2 := + ⟨13, Tape.mk' ((ones a (NL n)).cons 0) (ones r ((ones p ((ones q B0).cons 0)).cons 0))⟩ + +theorem t_to_adv (n a r p q : ℕ) : + nSteps brocard28 r (tCfg n a r p q) = some (advCfg n a r p q) := + sweepR sTR0_1 r _ _ + +/-- The test starts: `TLx` erases the first cell of `B`. -/ +theorem test_start (n r : ℕ) : + ∃ s, nSteps brocard28 s (testCfg n (r + 1)) = some (advCfg n 0 r 0 0) := by + have h₁ : step brocard28 (testCfg n (r + 1)) = some (tCfg n 0 r 0 0) := by + change step brocard28 ⟨1, Tape.mk' (NL n) ((ones r B0).cons 1)⟩ = + some ⟨13, Tape.mk' ((NL n).cons 0) (ones r ((ones 0 ((ones 0 B0).cons 0)).cons 0))⟩ + rw [ErdosTernary15.Tape.mk'_cons, sTLx_1, ones_zero_B0, B0_cons_zero, ones_zero_B0, + B0_cons_zero] + exact ⟨_, nSteps_cons h₁ (t_to_adv n 0 r 0 0)⟩ + +/-- One unit: the hole of `S` moves one cell left and the hole of `B` one cell right. -/ +theorem adv_step (n a r p q : ℕ) : + ∃ s, nSteps brocard28 s (advCfg n a (r + 1) (p + 1) q) = some (tCfg n (a + 1) r p (q + 1)) := by + set H := (ones a (NL n)).cons 0 with hH + set Lr := ones (r + 1) H with hLr + have h₁ : step brocard28 (advCfg n a (r + 1) (p + 1) q) = + some ⟨14, Tape.mk' (Lr.cons 0) (ones (p + 1) ((ones q B0).cons 0))⟩ := by + change step brocard28 ⟨13, Tape.mk' Lr ((ones (p + 1) ((ones q B0).cons 0)).cons 0)⟩ = _ + rw [ErdosTernary15.Tape.mk'_cons, sTR0_0] + have h₂ := sweepR sTR1_1 (p + 1) (Lr.cons 0) ((ones q B0).cons 0) + have h₃ : nSteps brocard28 2 ⟨14, Tape.mk' (ones (p + 1) (Lr.cons 0)) ((ones q B0).cons 0)⟩ = + some ⟨17, mkL (ones p (Lr.cons 0)) ((ones (q + 1) B0).cons 0)⟩ := by + change nSteps brocard28 2 ⟨14, Tape.mk' ((ones p (Lr.cons 0)).cons 1) ((ones q B0).cons 0)⟩ = + some ⟨17, mkL (ones p (Lr.cons 0)) (((ones q B0).cons 1).cons 0)⟩ + tm_run + have h₄ := sweepL sTL0_1 p (Lr.cons 0) ((ones (q + 1) B0).cons 0) + have h₅ : step brocard28 ⟨17, mkL (Lr.cons 0) (ones p ((ones (q + 1) B0).cons 0))⟩ = + some ⟨18, mkL Lr ((ones p ((ones (q + 1) B0).cons 0)).cons 0)⟩ := by + rw [ErdosTernary15.Tape.mkL_cons, sTL0_0] + have h₆ := sweepL sTL1_1 (r + 1) H ((ones p ((ones (q + 1) B0).cons 0)).cons 0) + have h₇ : nSteps brocard28 2 + ⟨18, mkL H (ones (r + 1) ((ones p ((ones (q + 1) B0).cons 0)).cons 0))⟩ = + some (tCfg n (a + 1) r p (q + 1)) := by + change nSteps brocard28 2 ⟨18, mkL ((ones a (NL n)).cons 0) + ((ones r ((ones p ((ones (q + 1) B0).cons 0)).cons 0)).cons 1)⟩ = + some ⟨13, Tape.mk' (((ones a (NL n)).cons 1).cons 0) + (ones r ((ones p ((ones (q + 1) B0).cons 0)).cons 0))⟩ + tm_run + exact ⟨_, nSteps_cons h₁ (nSteps_bind_eq h₂ (nSteps_bind_eq h₃ (nSteps_bind_eq h₄ + (nSteps_cons h₅ (nSteps_bind_eq h₆ h₇)))))⟩ + +/-- `p` units in a row, while `B` has enough cells. -/ +theorem adv_many (n : ℕ) : ∀ p a r p' q, ∃ s, nSteps brocard28 s (advCfg n a (r + p) (p + p') q) = + some (advCfg n (a + p) r p' (q + p)) := by + intro p + induction p with + | zero => intro a r p' q; exact ⟨0, by simp⟩ + | succ p ih => + intro a r p' q + obtain ⟨s₁, hs₁⟩ := adv_step n a (r + p) (p + p') q + have h₂ := t_to_adv n (a + 1) (r + p) (p + p') (q + 1) + obtain ⟨s₃, hs₃⟩ := ih (a + 1) r p' (q + 1) + refine ⟨s₁ + (r + p) + s₃, ?_⟩ + rw [show r + (p + 1) = r + p + 1 by omega, show p + 1 + p' = p + p' + 1 by omega, + show a + (p + 1) = a + 1 + p by omega, show q + (p + 1) = q + 1 + p by omega] + exact nSteps_bind_eq (nSteps_bind_eq hs₁ h₂) hs₃ + +/-- The wrap: the hole of `S` is at its first cell, `B` has cells left; `S` becomes solid with +one more cell and the next chunk starts. -/ +theorem adv_wrap (n a r q : ℕ) : + nSteps brocard28 4 (advCfg n a (r + 1) 0 q) = some (advCfg n a (r + 1) (q + 1) 0) := by + rw [advCfg_solid] + change nSteps brocard28 4 ⟨13, Tape.mk' ((ones r ((ones a (NL n)).cons 0)).cons 1) + (((ones q B0).cons 0).cons 0)⟩ = + some ⟨13, Tape.mk' ((ones r ((ones a (NL n)).cons 0)).cons 1) + ((((ones q B0).cons 1).cons 0))⟩ + tm_run + +/-- The wrap with `B` exhausted: success, `M0` starts the gate on the last cell of `B`. -/ +theorem adv_success (n a q : ℕ) : + nSteps brocard28 4 (advCfg n a 0 0 q) = + some ⟨23, mkL (ones a (NL n)) (((ones (q + 1) B0).cons 0).cons 0)⟩ := by + change nSteps brocard28 4 ⟨13, Tape.mk' ((ones a (NL n)).cons 0) (((ones q B0).cons 0).cons 0)⟩ = + some ⟨23, mkL (ones a (NL n)) ((((ones q B0).cons 1).cons 0).cons 0)⟩ + tm_run + +/-- A unit with `B` exhausted: `TE` finds the separator, `ER`/`ER2` erase `S`, `ER3` returns, +erasing the last cell of `B`, and the next round starts. -/ +theorem adv_fail (n a p q : ℕ) : + ∃ s, nSteps brocard28 s (advCfg n (a + 1) 0 (p + 1) q) = some (roundCfg n a) := by + set H := (ones (a + 1) (NL n)).cons 0 with hH + have h₁ : step brocard28 (advCfg n (a + 1) 0 (p + 1) q) = + some ⟨14, Tape.mk' (H.cons 0) (ones (p + 1) ((ones q B0).cons 0))⟩ := by + change step brocard28 ⟨13, Tape.mk' H ((ones (p + 1) ((ones q B0).cons 0)).cons 0)⟩ = _ + rw [ErdosTernary15.Tape.mk'_cons, sTR0_0] + have h₂ := sweepR sTR1_1 (p + 1) (H.cons 0) ((ones q B0).cons 0) + have h₃ : nSteps brocard28 2 ⟨14, Tape.mk' (ones (p + 1) (H.cons 0)) ((ones q B0).cons 0)⟩ = + some ⟨17, mkL (ones p (H.cons 0)) ((ones (q + 1) B0).cons 0)⟩ := by + change nSteps brocard28 2 ⟨14, Tape.mk' ((ones p (H.cons 0)).cons 1) ((ones q B0).cons 0)⟩ = + some ⟨17, mkL (ones p (H.cons 0)) (((ones q B0).cons 1).cons 0)⟩ + tm_run + have h₄ := sweepL sTL0_1 p (H.cons 0) ((ones (q + 1) B0).cons 0) + have h₅ : nSteps brocard28 3 ⟨17, mkL (H.cons 0) (ones p ((ones (q + 1) B0).cons 0))⟩ = + some ⟨20, Tape.mk' (((ones (a + 1) (NL n)).cons 1).cons 0) + (ones p ((ones (q + 1) B0).cons 0))⟩ := by + rw [hH] + tm_run + have h₆ := sweepR_erase sER_1 p (((ones (a + 1) (NL n)).cons 1).cons 0) ((ones (q + 1) B0).cons 0) + set W := ((ones (a + 1) (NL n)).cons 1).cons 0 with hW + have h₇ : step brocard28 ⟨20, Tape.mk' (zeros p W) ((ones (q + 1) B0).cons 0)⟩ = + some ⟨21, Tape.mk' ((zeros p W).cons 0) (ones (q + 1) B0)⟩ := by + rw [ErdosTernary15.Tape.mk'_cons, sER_0] + have h₈ := sweepR_erase sER2_1 (q + 1) ((zeros p W).cons 0) B0 + have h₉ : step brocard28 ⟨21, Tape.mk' (zeros (q + 1) ((zeros p W).cons 0)) B0⟩ = + some ⟨22, mkL (zeros (q + 1) ((zeros p W).cons 0)) B0⟩ := by + rw [ErdosTernary15.Tape.mk'_B0, sER2_0, B0_cons_zero] + have h₁₀ := sweepL_zeros sER3_0 (q + 1) ((zeros p W).cons 0) B0 + rw [zeros_B0] at h₁₀ + have h₁₁ : step brocard28 ⟨22, mkL ((zeros p W).cons 0) B0⟩ = some ⟨22, mkL (zeros p W) B0⟩ := by + rw [ErdosTernary15.Tape.mkL_cons, sER3_0, B0_cons_zero] + have h₁₂ := sweepL_zeros sER3_0 p W B0 + rw [zeros_B0] at h₁₂ + have h₁₃ : nSteps brocard28 2 ⟨22, mkL W B0⟩ = some (roundCfg n a) := by + rw [hW] + change nSteps brocard28 2 ⟨22, mkL ((((ones a (NL n)).cons 1).cons 1).cons 0) B0⟩ = + some ⟨2, Tape.mk' (ones a (NL n)) (B0.cons 1)⟩ + tm_run + exact ⟨_, nSteps_cons h₁ (nSteps_bind_eq h₂ (nSteps_bind_eq h₃ (nSteps_bind_eq h₄ + (nSteps_bind_eq h₅ (nSteps_bind_eq h₆ (nSteps_cons h₇ (nSteps_bind_eq h₈ (nSteps_cons h₉ + (nSteps_bind_eq h₁₀ (nSteps_cons h₁₁ (nSteps_bind_eq h₁₂ h₁₃)))))))))))⟩ + +/-! ## Triangular Numbers and the Chunk Loop -/ + +/-- `pre s = 0 + 1 + ⋯ + (s - 1)`: the cells of `B` consumed before the chunk of size `s`. -/ +def pre : ℕ → ℕ + | 0 => 0 + | s + 1 => pre s + s + +/-- `tri k = 1 + 2 + ⋯ + k`. -/ +def tri (k : ℕ) : ℕ := pre (k + 1) + +theorem tri_succ (k : ℕ) : tri (k + 1) = tri k + (k + 1) := rfl + +theorem tri_strictMono : StrictMono tri := + strictMono_nat_of_lt_succ fun k => by rw [tri_succ]; omega + +theorem tri_eq_iff (j k : ℕ) : tri j = tri k ↔ j = k := tri_strictMono.injective.eq_iff + +/-- Nothing strictly between two consecutive triangular numbers is triangular. -/ +theorem not_tri_between {k x : ℕ} (h₁ : tri k < x) (h₂ : x < tri (k + 1)) : ¬ ∃ j, x = tri j := by + rintro ⟨j, rfl⟩ + have := tri_strictMono.lt_iff_lt.mp h₁ + have := tri_strictMono.lt_iff_lt.mp h₂ + omega + +/-- The success configuration: `M0` on the last cell of `B` (`a` ones, the hole after them), +`S` solid with `S` cells. -/ +def succCfg (n a S : ℕ) : Cfg 28 2 := + ⟨23, mkL (ones a (NL n)) (((ones S B0).cons 0).cons 0)⟩ + +/-- From the start of the chunk of size `s ≥ 1` with `r + 1` cells of `B` left: success if the +cells of `B` form a triangular number, otherwise the next round. -/ +theorem chunk_loop (n : ℕ) : ∀ r s a, 1 ≤ s → a = pre s → + (∃ j, a + r + 1 = tri j ∧ ∃ t, nSteps brocard28 t (advCfg n a (r + 1) s 0) = + some (succCfg n (a + r + 1) (j + 1))) ∨ + ((¬ ∃ j, a + r + 1 = tri j) ∧ ∃ t, nSteps brocard28 t (advCfg n a (r + 1) s 0) = + some (roundCfg n (a + r))) := by + intro r + induction r using Nat.strong_induction_on with + | _ r ih => + intro s a hs ha + rcases Nat.lt_or_ge (r + 1) s with hlt | hge + · -- not enough cells: fail inside this chunk + obtain ⟨p', hp'⟩ : ∃ p', s = r + 1 + (p' + 1) := ⟨s - r - 2, by omega⟩ + obtain ⟨t₁, ht₁⟩ := adv_many n (r + 1) a 0 (p' + 1) 0 + rw [Nat.zero_add, ← hp', show a + (r + 1) = a + r + 1 by omega] at ht₁ + obtain ⟨t₂, ht₂⟩ := adv_fail n (a + r) p' (r + 1) + refine Or.inr ⟨?_, t₁ + t₂, nSteps_bind_eq ht₁ ht₂⟩ + obtain ⟨s', rfl⟩ : ∃ s', s = s' + 1 := ⟨s - 1, by omega⟩ + have e1 : tri s' = pre s' + s' := rfl + have e2 : tri (s' + 1) = pre s' + s' + (s' + 1) := rfl + have e3 : pre (s' + 1) = pre s' + s' := rfl + have h1 : tri s' < a + r + 1 := by omega + have h2 : a + r + 1 < tri (s' + 1) := by omega + exact not_tri_between h1 h2 + · -- the whole chunk fits + obtain ⟨r', hr'⟩ : ∃ r', r + 1 = r' + s := ⟨r + 1 - s, by omega⟩ + obtain ⟨t₁, ht₁⟩ := adv_many n s a r' 0 0 + rw [Nat.zero_add, Nat.add_zero, ← hr'] at ht₁ + rcases Nat.eq_zero_or_pos r' with rfl | hr'pos + · -- exhausted exactly at the wrap: success + have ht₂ := adv_success n (a + s) s + refine Or.inl ⟨s, ?_, t₁ + 4, ?_⟩ + · rw [tri, pre, ha]; omega + · rw [show a + r + 1 = a + s by omega] + exact nSteps_bind_eq ht₁ ht₂ + · obtain ⟨r'', rfl⟩ : ∃ r'', r' = r'' + 1 := ⟨r' - 1, by omega⟩ + have ht₂ := adv_wrap n (a + s) r'' s + obtain ⟨j, hj, t₃, ht₃⟩ | ⟨hj, t₃, ht₃⟩ := + ih r'' (by omega) (s + 1) (a + s) (by omega) (by rw [ha]; rfl) + · refine Or.inl ⟨j, ?_, t₁ + 4 + t₃, ?_⟩ + · rw [← hj]; omega + · rw [show a + r + 1 = a + s + r'' + 1 by omega] + exact nSteps_bind_eq (nSteps_bind_eq ht₁ ht₂) ht₃ + · refine Or.inr ⟨?_, t₁ + 4 + t₃, ?_⟩ + · rw [show a + r + 1 = a + s + r'' + 1 by omega]; exact hj + · rw [show a + r = a + s + r'' by omega] + exact nSteps_bind_eq (nSteps_bind_eq ht₁ ht₂) ht₃ + +/-- The test of `B` with `M + 1` cells: the first cell is consumed; if `M` is triangular the +machine reaches the success configuration, otherwise the next round with `M` cells. -/ +theorem test_run (n M : ℕ) : + (∃ j, M = tri j ∧ ∃ t, nSteps brocard28 t (testCfg n (M + 1)) = + some (succCfg n M (j + 1))) ∨ + ((¬ ∃ j, M = tri j) ∧ ∃ t, nSteps brocard28 t (testCfg n (M + 1)) = + some (roundCfg n (M - 1))) := by + obtain ⟨t₀, ht₀⟩ := test_start n M + cases M with + | zero => + exact Or.inl ⟨0, rfl, t₀ + 4, nSteps_bind_eq ht₀ (adv_success n 0 0)⟩ + | succ r => + have ht₁ := adv_wrap n 0 r 0 + obtain ⟨j, hj, t, ht⟩ | ⟨hj, t, ht⟩ := chunk_loop n r 1 0 le_rfl rfl + · simp only [Nat.zero_add] at hj ht + exact Or.inl ⟨j, hj, t₀ + 4 + t, nSteps_bind_eq (nSteps_bind_eq ht₀ ht₁) ht⟩ + · simp only [Nat.zero_add] at hj ht + rw [Nat.add_sub_cancel] + exact Or.inr ⟨hj, t₀ + 4 + t, nSteps_bind_eq (nSteps_bind_eq ht₀ ht₁) ht⟩ + +/-! ## Gate (States `23`–`27`) and Start (State `0`) -/ + +/-- `M0`–`M3` count the ones of `B` modulo `4` walking left: four ones return to `M0`. -/ +theorem gate_four (k : ℕ) (L R : ListBlank (Fin 2)) : + nSteps brocard28 4 ⟨23, mkL (ones (k + 4) L) R⟩ = some ⟨23, mkL (ones k L) (ones 4 R)⟩ := by + change nSteps brocard28 4 ⟨23, mkL (((((ones k L).cons 1).cons 1).cons 1).cons 1) R⟩ = + some ⟨23, mkL (ones k L) ((((R.cons 1).cons 1).cons 1).cons 1)⟩ + tm_run + +/-- `4 j` ones of `B` bring `M0` back to `M0`. -/ +theorem gate_mult (j : ℕ) : ∀ (k : ℕ) (L R : ListBlank (Fin 2)), + nSteps brocard28 (4 * j) ⟨23, mkL (ones (4 * j + k) L) R⟩ = + some ⟨23, mkL (ones k L) (ones (4 * j) R)⟩ := by + induction j with + | zero => intro k L R; simp only [Nat.mul_zero, Nat.zero_add, ones_zero]; rfl + | succ j ih => + intro k L R + have h₁ : nSteps brocard28 4 ⟨23, mkL (ones (4 * (j + 1) + k) L) R⟩ = + some ⟨23, mkL (ones (4 * j + k) L) (ones 4 R)⟩ := by + rw [show 4 * (j + 1) + k = 4 * j + k + 4 by omega]; exact gate_four _ L R + have := nSteps_bind_eq h₁ (ih k L (ones 4 R)) + rwa [← ones_add, show 4 * j + 4 = 4 * (j + 1) by omega, + show 4 + 4 * j = 4 * (j + 1) by omega] at this + +/-- Residue `0`: `M0` reaches the separator and halts (`M0` reading `0` is undefined). -/ +theorem gate_halt (n j : ℕ) (Y : ListBlank (Fin 2)) : + ∃ cfg, nSteps brocard28 (4 * j) ⟨23, mkL (ones (4 * j) (NL n)) Y⟩ = some cfg ∧ + step brocard28 cfg = none := by + refine ⟨⟨23, mkL (NL n) (ones (4 * j) Y)⟩, ?_, ?_⟩ + · have := gate_mult j 0 (NL n) Y + rwa [Nat.add_zero, ones_zero] at this + · rw [NL, ErdosTernary15.Tape.mkL_cons, sM0_0] + +/-- Residue `2`: `M2` reads the separator and steps right into `Bs`. -/ +theorem gate_two (n j : ℕ) (Y : ListBlank (Fin 2)) : + nSteps brocard28 (4 * j + 3) ⟨23, mkL (ones (4 * j + 2) (NL n)) Y⟩ = + some ⟨27, Tape.mk' (NL n) (ones (4 * j + 2) Y)⟩ := by + have h₁ := gate_mult j 2 (NL n) Y + have h₂ : nSteps brocard28 3 ⟨23, mkL (ones 2 (NL n)) (ones (4 * j) Y)⟩ = + some ⟨27, Tape.mk' (NL n) (ones (4 * j + 2) Y)⟩ := by + change nSteps brocard28 3 ⟨23, mkL ((((ones n B0).cons 0).cons 1).cons 1) (ones (4 * j) Y)⟩ = + some ⟨27, Tape.mk' ((ones n B0).cons 0) (((ones (4 * j) Y).cons 1).cons 1)⟩ + tm_run + exact nSteps_bind_eq h₁ h₂ + +/-- Residue `3`: `M3` reads the separator and steps right into `Bs`. -/ +theorem gate_three (n j : ℕ) (Y : ListBlank (Fin 2)) : + nSteps brocard28 (4 * j + 4) ⟨23, mkL (ones (4 * j + 3) (NL n)) Y⟩ = + some ⟨27, Tape.mk' (NL n) (ones (4 * j + 3) Y)⟩ := by + have h₁ := gate_mult j 3 (NL n) Y + have h₂ : nSteps brocard28 4 ⟨23, mkL (ones 3 (NL n)) (ones (4 * j) Y)⟩ = + some ⟨27, Tape.mk' (NL n) (ones (4 * j + 3) Y)⟩ := by + change nSteps brocard28 4 + ⟨23, mkL (((((ones n B0).cons 0).cons 1).cons 1).cons 1) (ones (4 * j) Y)⟩ = + some ⟨27, Tape.mk' ((ones n B0).cons 0) ((((ones (4 * j) Y).cons 1).cons 1).cons 1)⟩ + tm_run + exact nSteps_bind_eq h₁ h₂ + +/-- After a suppressed success, `Bs` returns over `B` and fills its hole, `ER`/`ER2` erase the +solid `S`, and `ER3` erases the last cell of `B`: the next round. -/ +theorem gate_back (n a S : ℕ) : + ∃ s, nSteps brocard28 s + ⟨27, Tape.mk' (NL n) (ones (a + 1) (((ones S B0).cons 0).cons 0))⟩ = + some (roundCfg n a) := by + set R := ((ones S B0).cons 0).cons 0 with hR + have h₃ := sweepR sBs_1 (a + 1) (NL n) R + have h₄ : nSteps brocard28 2 ⟨27, Tape.mk' (ones (a + 1) (NL n)) R⟩ = + some ⟨21, Tape.mk' (((ones (a + 1) (NL n)).cons 1).cons 0) (ones S B0)⟩ := by + rw [hR] + tm_run + set W := ((ones (a + 1) (NL n)).cons 1).cons 0 with hW + have h₅ := sweepR_erase sER2_1 S W B0 + have h₆ : step brocard28 ⟨21, Tape.mk' (zeros S W) B0⟩ = some ⟨22, mkL (zeros S W) B0⟩ := by + rw [ErdosTernary15.Tape.mk'_B0, sER2_0, B0_cons_zero] + have h₇ := sweepL_zeros sER3_0 S W B0 + rw [zeros_B0] at h₇ + have h₈ : nSteps brocard28 2 ⟨22, mkL W B0⟩ = some (roundCfg n a) := by + rw [hW] + change nSteps brocard28 2 ⟨22, mkL ((((ones a (NL n)).cons 1).cons 1).cons 0) B0⟩ = + some ⟨2, Tape.mk' (ones a (NL n)) (B0.cons 1)⟩ + tm_run + exact ⟨_, nSteps_bind_eq h₃ (nSteps_bind_eq h₄ (nSteps_bind_eq h₅ (nSteps_cons h₆ + (nSteps_bind_eq h₇ h₈))))⟩ + +/-- A success whose `B` has `a + 1 ≡ 2` or `3 (mod 4)` ones is suppressed: the next round +starts. -/ +theorem gate_suppressed (n a S : ℕ) (h : (a + 1) % 4 = 2 ∨ (a + 1) % 4 = 3) : + ∃ s, nSteps brocard28 s (succCfg n (a + 1) S) = some (roundCfg n a) := by + obtain ⟨s₃, hs₃⟩ := gate_back n a S + rcases h with h | h + · have h₂ := gate_two n ((a + 1) / 4) (((ones S B0).cons 0).cons 0) + rw [show 4 * ((a + 1) / 4) + 2 = a + 1 by omega] at h₂ + exact ⟨_, nSteps_bind_eq h₂ hs₃⟩ + · have h₂ := gate_three n ((a + 1) / 4) (((ones S B0).cons 0).cons 0) + rw [show 4 * ((a + 1) / 4) + 3 = a + 1 by omega] at h₂ + exact ⟨_, nSteps_bind_eq h₂ hs₃⟩ + +/-- A success whose `B` has `a + 1 ≡ 0 (mod 4)` ones halts. -/ +theorem gate_live (n a S : ℕ) (h : (a + 1) % 4 = 0) : + ∃ s cfg, nSteps brocard28 s (succCfg n (a + 1) S) = some cfg ∧ + step brocard28 cfg = none := by + obtain ⟨cfg, h₁, hnone⟩ := gate_halt n ((a + 1) / 4) (((ones S B0).cons 0).cons 0) + rw [show 4 * ((a + 1) / 4) = a + 1 by omega] at h₁ + exact ⟨_, cfg, h₁, hnone⟩ + +theorem init_eq : (init : Cfg 28 2) = ⟨0, Tape.mk' B0 B0⟩ := rfl + +/-- Start, steps `1`–`12`: `GO`, `EC`, `LN0`, `LN1`, `EN`, `X` write `1 0 1 1`; `TLs`, `TLx`, +`TR0` turn it into `1 0 0 1` and move on. -/ +theorem seed₁ : nSteps brocard28 12 ⟨0, Tape.mk' B0 B0⟩ = + some ⟨14, Tape.mk' (((((B0.cons 1).cons 0).cons 0).cons 1).cons 0) B0⟩ := by + tm_run + +/-- Start, steps `13`–`24`: one chunk of the test runs on `1 0 0 1`. -/ +theorem seed₂ : nSteps brocard28 12 + ⟨14, Tape.mk' (((((B0.cons 1).cons 0).cons 0).cons 1).cons 0) B0⟩ = + some ⟨14, Tape.mk' (((((B0.cons 1).cons 0).cons 1).cons 0).cons 0) ((B0.cons 1).cons 0)⟩ := by + tm_run + +/-- Start, steps `25`–`36`: `TR1`, `SB`, `SC` end the chunk as a success; `M0`, `M1` reading `0`, +`GO`, `LN1`, `EN`, `X` write `1111 0 111`; `TLs` reading `0` enters `TLx`. -/ +theorem seed₃ : nSteps brocard28 12 + ⟨14, Tape.mk' (((((B0.cons 1).cons 0).cons 1).cons 0).cons 0) ((B0.cons 1).cons 0)⟩ = + some ⟨1, Tape.mk' (ListBlank.cons 0 + ((((((((B0.cons 1).cons 1).cons 1).cons 1).cons 0).cons 1).cons 1).cons 1)) B0⟩ := by + tm_run + +/-- Start, steps `37`–`46`: `TLx` reading `0`, `EC`, `LN0`, `LN1` walk left to the blank left of +`N`. -/ +theorem seed₄ : nSteps brocard28 10 + ⟨1, Tape.mk' (ListBlank.cons 0 + ((((((((B0.cons 1).cons 1).cons 1).cons 1).cons 0).cons 1).cons 1).cons 1)) B0⟩ = + some ⟨3, mkL B0 (ones 4 ((ones 3 B0).cons 0))⟩ := by + change _ = some (⟨3, mkL B0 (ListBlank.cons 1 + (((((((B0.cons 1).cons 1).cons 1).cons 0).cons 1).cons 1).cons 1))⟩ : Cfg 28 2) + tm_run + +/-- The start writes `1111 0 111` in `46` steps and ends in `LN1` on the blank left of `N`, the +configuration every round passes through (`ln_exit`). -/ +theorem seed : nSteps brocard28 46 init = some ⟨3, mkL B0 (ones 4 ((ones 3 B0).cons 0))⟩ := by + rw [init_eq] + exact nSteps_bind_eq seed₁ (nSteps_bind_eq seed₂ (nSteps_bind_eq seed₃ seed₄)) + +/-! ## Stages -/ + +/-- `V n = n! / 8`, the number of cells of `B` between rounds. -/ +def V (n : ℕ) : ℕ := n.factorial / 8 + +theorem eight_dvd_factorial {n : ℕ} (hn : 4 ≤ n) : 8 ∣ n.factorial := + Nat.dvd_trans (by decide : 8 ∣ Nat.factorial 4) (Nat.factorial_dvd_factorial hn) + +theorem V_succ {n : ℕ} (hn : 4 ≤ n) : V (n + 1) = (n + 1) * V n := by + rw [V, V, Nat.factorial_succ, Nat.mul_div_assoc _ (eight_dvd_factorial hn)] + +theorem V_pos {n : ℕ} (hn : 4 ≤ n) : 1 ≤ V n := by + induction n, hn using Nat.le_induction with + | base => decide + | succ n hn ih => rw [V_succ hn]; exact le_trans ih (Nat.le_mul_of_pos_left _ (by omega)) + +/-- For `n ≥ 8`, `32 ∣ n!`, so `4 ∣ n! / 8`: the gate halts on every success with `n ≥ 8`. -/ +theorem V_mod_four {n : ℕ} (hn : 8 ≤ n) : V n % 4 = 0 := by + obtain ⟨t, ht⟩ := + Nat.dvd_trans (by decide : 32 ∣ Nat.factorial 8) (Nat.factorial_dvd_factorial hn) + rw [V, ht]; omega + +/-- `x` is a triangular number `1 + 2 + ⋯ + j`. -/ +def IsTri (x : ℕ) : Prop := ∃ j, x = tri j + +theorem le_tri (j : ℕ) : j ≤ tri j := by + induction j with + | zero => exact le_rfl + | succ j ih => rw [tri_succ]; omega + +theorem isTri_iff (x : ℕ) : IsTri x ↔ ∃ j < x + 1, x = tri j := + ⟨fun ⟨j, h⟩ => ⟨j, by have := le_tri j; omega, h⟩, fun ⟨j, _, h⟩ => ⟨j, h⟩⟩ + +instance : DecidablePred IsTri := fun x => decidable_of_iff _ (isTri_iff x).symm + +/-- The configuration at the start of the round that multiplies by `n + 1`. -/ +def stage (n : ℕ) : Cfg 28 2 := roundCfg n (V n - 1) + +theorem stage_to_test {n : ℕ} (hn : 4 ≤ n) : + ∃ s, 1 ≤ s ∧ nSteps brocard28 s (stage n) = some (testCfg (n + 1) (V (n + 1) + 1)) := by + obtain ⟨s, hs1, hs⟩ := multiply n (V n - 1) (by omega) + have := V_pos hn + rw [show V n - 1 + 1 = V n by omega, ← V_succ hn] at hs + exact ⟨s, hs1, hs⟩ + +/-- A round whose test fails. -/ +theorem stage_fail {n : ℕ} (hn : 4 ≤ n) (h : ¬ IsTri (V (n + 1))) : + ∃ s, 1 ≤ s ∧ nSteps brocard28 s (stage n) = some (stage (n + 1)) := by + obtain ⟨s₁, hs₁1, hs₁⟩ := stage_to_test hn + rcases test_run (n + 1) (V (n + 1)) with ⟨j, hj, -⟩ | ⟨-, s₂, hs₂⟩ + · exact absurd ⟨j, hj⟩ h + · exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + +/-- A round whose test succeeds with `n + 1 = 5` (`V 5 = 15 ≡ 3`) or `n + 1 = 7` +(`V 7 = 630 ≡ 2 (mod 4)`): suppressed. -/ +theorem stage_suppressed {n : ℕ} (hn : 4 ≤ n) (h : IsTri (V (n + 1))) + (h57 : n + 1 = 5 ∨ n + 1 = 7) : + ∃ s, 1 ≤ s ∧ nSteps brocard28 s (stage n) = some (stage (n + 1)) := by + obtain ⟨s₁, hs₁1, hs₁⟩ := stage_to_test hn + rcases test_run (n + 1) (V (n + 1)) with ⟨j, -, s₂, hs₂⟩ | ⟨h', -⟩ + · have hV := V_pos (show 4 ≤ n + 1 by omega) + obtain ⟨a, ha⟩ : ∃ a, V (n + 1) = a + 1 := ⟨V (n + 1) - 1, by omega⟩ + have hres : (a + 1) % 4 = 2 ∨ (a + 1) % 4 = 3 := by + rw [← ha] + rcases h57 with h5 | h7 + · right; rw [h5]; decide + · left; rw [h7]; decide + rw [ha] at hs₁ hs₂ + obtain ⟨s₃, hs₃⟩ := gate_suppressed (n + 1) a (j + 1) hres + refine ⟨s₁ + s₂ + s₃, by omega, ?_⟩ + change nSteps brocard28 (s₁ + s₂ + s₃) (stage n) = some (roundCfg (n + 1) (V (n + 1) - 1)) + rw [ha, Nat.add_sub_cancel] + exact nSteps_bind_eq (nSteps_bind_eq hs₁ hs₂) hs₃ + · exact absurd h h' + +/-- A round whose test succeeds with `n + 1 ≥ 8` halts. -/ +theorem stage_halt {n : ℕ} (hn : 7 ≤ n) (h : IsTri (V (n + 1))) : + ∃ s cfg, nSteps brocard28 s (stage n) = some cfg ∧ step brocard28 cfg = none := by + obtain ⟨s₁, -, hs₁⟩ := stage_to_test (show 4 ≤ n by omega) + rcases test_run (n + 1) (V (n + 1)) with ⟨j, -, s₂, hs₂⟩ | ⟨h', -⟩ + · have hV := V_pos (show 4 ≤ n + 1 by omega) + obtain ⟨a, ha⟩ : ∃ a, V (n + 1) = a + 1 := ⟨V (n + 1) - 1, by omega⟩ + have hres : (a + 1) % 4 = 0 := by rw [← ha]; exact V_mod_four (by omega) + rw [ha] at hs₁ hs₂ + obtain ⟨s₃, cfg, hs₃, hnone⟩ := gate_live (n + 1) a (j + 1) hres + exact ⟨s₁ + s₂ + s₃, cfg, nSteps_bind_eq (nSteps_bind_eq hs₁ hs₂) hs₃, hnone⟩ + · exact absurd h h' + +theorem isTri_V5 : IsTri (V 5) := ⟨5, by decide⟩ + +theorem not_isTri_V6 : ¬ IsTri (V 6) := + not_tri_between (k := 12) (by decide) (by decide) + +theorem isTri_V7 : IsTri (V 7) := ⟨35, by decide⟩ + +/-- The start reaches the beginning of round `5`: `46` steps write `1111 0 111`, the first +round multiplies by `5`, its test finds `15 = tri 5`, and the gate suppresses the success +(`15 ≡ 3 (mod 4)`). -/ +theorem seed_stage : ∃ s, 5 ≤ s ∧ nSteps brocard28 s init = some (stage 5) := by + obtain ⟨s₃, hs₃⟩ := multiply_en 4 2 (by omega) + rcases test_run 5 15 with ⟨j, -, s₄, hs₄⟩ | ⟨h, -⟩ + · obtain ⟨s₅, hs₅⟩ := gate_suppressed 5 14 (j + 1) (Or.inr rfl) + refine ⟨46 + 1 + s₃ + s₄ + s₅, by omega, ?_⟩ + have hV : V 5 - 1 = 14 := by decide + rw [stage, hV] + exact nSteps_bind_eq (nSteps_bind_eq (nSteps_bind_eq (nSteps_bind_eq seed + (step_one (ln_exit 4 2))) hs₃) hs₄) hs₅ + · exact absurd isTri_V5 h + +/-- No counterexample with `8 ≤ m ≤ K`. -/ +def Clear (K : ℕ) : Prop := ∀ m, 8 ≤ m → m ≤ K → ¬ IsTri (V m) + +theorem clear_or_witness (K : ℕ) : Clear K ∨ ∃ m, 8 ≤ m ∧ m ≤ K ∧ IsTri (V m) := by + induction K with + | zero => exact Or.inl fun m h8 h0 => absurd (le_trans h8 h0) (by decide) + | succ K ih => + rcases ih with hc | ⟨m, hm8, hmK, hm⟩ + · by_cases hK : 8 ≤ K + 1 + · by_cases ht : IsTri (V (K + 1)) + · exact Or.inr ⟨K + 1, hK, le_rfl, ht⟩ + · refine Or.inl fun m h8 hK1 => ?_ + rcases Nat.lt_or_ge m (K + 1) with h | h + · exact hc m h8 (by omega) + · rw [show m = K + 1 by omega]; exact ht + · exact Or.inl fun m h8 hK1 => absurd (le_trans h8 hK1) hK + · exact Or.inr ⟨m, hm8, by omega, hm⟩ + +/-- Without a counterexample up to `n`, the machine reaches the start of round `n` in at least +`n` steps. -/ +theorem reach (n : ℕ) (hn : 5 ≤ n) (hc : Clear n) : + ∃ s, n ≤ s ∧ nSteps brocard28 s init = some (stage n) := by + induction n, hn using Nat.le_induction with + | base => exact seed_stage + | succ n hn ih => + obtain ⟨s₁, hs₁n, hs₁⟩ := ih fun m h8 hm => hc m h8 (by omega) + have step : ∃ s, 1 ≤ s ∧ nSteps brocard28 s (stage n) = some (stage (n + 1)) := by + rcases Nat.lt_or_ge (n + 1) 8 with h | h + · obtain rfl | rfl : n = 5 ∨ n = 6 := by omega + · exact stage_fail (by omega) not_isTri_V6 + · exact stage_suppressed (by omega) isTri_V7 (Or.inr rfl) + · exact stage_fail (by omega) (hc (n + 1) h le_rfl) + obtain ⟨s₂, hs₂1, hs₂⟩ := step + exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + +/-- The first counterexample halts the machine. -/ +theorem halt_of (m : ℕ) (hm : 8 ≤ m) (h : IsTri (V m)) (hc : Clear (m - 1)) : + ∃ s cfg, nSteps brocard28 s init = some cfg ∧ step brocard28 cfg = none := by + obtain ⟨s₁, -, hs₁⟩ := reach (m - 1) (by omega) hc + obtain ⟨s₂, cfg, hs₂, hnone⟩ := stage_halt (n := m - 1) (by omega) + (by rw [show m - 1 + 1 = m by omega]; exact h) + exact ⟨s₁ + s₂, cfg, nSteps_bind_eq hs₁ hs₂, hnone⟩ + +/-- The least counterexample has none below it. -/ +theorem first_witness (n : ℕ) : 8 ≤ n → IsTri (V n) → + ∃ m, 8 ≤ m ∧ IsTri (V m) ∧ Clear (m - 1) := by + induction n using Nat.strong_induction_on with + | _ n ih => + intro h8 hn + rcases clear_or_witness (n - 1) with hc | ⟨m, hm8, hmn, hm⟩ + · exact ⟨n, h8, hn, hc⟩ + · exact ih m (by omega) hm8 hm + +/-! ## Halting Equivalence -/ + +/-- The 28-state machine `brocard28` (`brocard_28`) halts on the blank tape if and only if +`n! / 8` is a triangular number for some `n ≥ 8`. -/ +theorem halts_brocard28_iff_exists_tri : + ConjectureMachines.Halts brocard28 ↔ ∃ n, 8 ≤ n ∧ IsTri (V 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 clear_or_witness (k + 8) with hc | ⟨m, hm8, -, hm⟩ + · obtain ⟨s, hks, hs⟩ := reach (k + 8) (by omega) hc + rw [nSteps_eq_none_of_step_none s hk hnone (by omega)] at hs + cases hs + · exact ⟨m, hm8, hm⟩ + · rintro ⟨n, h8, hn⟩ + obtain ⟨m, hm8, hm, hc⟩ := first_witness n h8 hn + obtain ⟨s, cfg, hs, hnone⟩ := halt_of m hm8 hm hc + rw [Part.dom_iff_mem] + exact ⟨cfg, mem_eval'.mpr ⟨nSteps_reaches hs, hnone⟩⟩ + +end ConjectureMachines.Brocard28 diff --git a/Cryptids/Machines.lean b/Cryptids/Machines.lean index 67e4453a..345a59a2 100644 --- a/Cryptids/Machines.lean +++ b/Cryptids/Machines.lean @@ -235,6 +235,11 @@ def erdosTernary14Rows : List (List (Option (Fin 2 × Dir × Fin 14))) := load_machine_rows% "artifacts/erdos_ternary_14/machine.txt" /-- 14-state Erdős candidate. -/ def erdosTernary14 : Machine 14 2 := Machine.ofRows erdosTernary14Rows +/-- Rows of `brocard28`. -/ +def brocard28Rows : List (List (Option (Fin 2 × Dir × Fin 28))) := + load_machine_rows% "artifacts/brocard_28/machine.txt" +/-- 28-state Brocard machine. -/ +def brocard28 : Machine 28 2 := Machine.ofRows brocard28Rows 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 5f569129..1a27139c 100644 --- a/Cryptids/Propositions.lean +++ b/Cryptids/Propositions.lean @@ -38,6 +38,8 @@ constructions and halting proofs: of `param3`). 4. **Erdős's Ternary Conjecture** (`ErdosTernaryConjecture`): For every `n > 8`, the base-3 expansion of `2 ^ n` contains the digit `2` (`erdos_ternary_15`). +5. **Brocard's Problem** (`BrocardConjecture`): + `n! + 1` is a perfect square only for `n = 4, 5, 7` (`brocard_28`). -/ @[expose] public section @@ -706,4 +708,12 @@ and it implies Erdős Problem 406 def ErdosTernaryConjecture : Prop := ∀ n : ℕ, 8 < n → 2 ∈ Nat.digits 3 (2 ^ n) +/-! ## 6. Brocard's Problem -/ + +/-- **Brocard's problem** (Brocard 1876, 1885; Ramanujan 1913): `n! + 1` is a perfect square +only for `n = 4, 5, 7` (`5 ^ 2`, `11 ^ 2`, `71 ^ 2`). Erdős conjectured that there are no other +solutions; none exist for `n ≤ 10 ^ 12` (Matson 2017). -/ +def BrocardConjecture : Prop := + ∀ n : ℕ, 7 < n → ¬ IsSquare (n.factorial + 1) + end ConjectureMachines diff --git a/Cryptids/README.md b/Cryptids/README.md index 095f1c17..3702997a 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. The `erdos_ternary_15` and `erdos_ternary_14` formalizations (Erdős's ternary conjecture) are by Daniel Veljjanoski, with Claude (Anthropic) as assistant. +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_ternary_15` and `erdos_ternary_14` formalizations (Erdős's ternary conjecture) and the `brocard_28` machine and proofs (Brocard's problem) are by Daniel Veljjanoski, with Claude (Anthropic) as assistant. ## Formalized Machines @@ -15,6 +15,7 @@ This library contains formally verified 2-symbol Turing machines and Lean 4 sema | 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 ternary conjecture | `erdos_ternary_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)) | `¬ ErdosTernaryConjecture` | [`ErdosTernary14.lean`](./ErdosTernary14.lean), [`Semantics/ErdosTernary14.lean`](./Semantics/ErdosTernary14.lean) | +| Brocard's problem | `brocard_28` | `28` | Daniel Veljjanoski (Nov 2026); earlier: Charlie Reams's 61-state machine ([`calr3/tinycryptids`](https://github.com/calr3/tinycryptids), Nov 2026) and a 43-state table without a machine-checked proof ([`arXiv:2605.20215`](https://arxiv.org/abs/2605.20215)) | `¬ BrocardConjecture` | [`Brocard28.lean`](./Brocard28.lean), [`Semantics/Brocard28.lean`](./Semantics/Brocard28.lean) | | Erdős's ternary conjecture | `erdos_ternary_15` | `15` | Tristan Stérin & Damien Woods ([`arXiv:2107.12475`](https://arxiv.org/abs/2107.12475), 2021) | `¬ ErdosTernaryConjecture` | [`ErdosTernary15.lean`](./ErdosTernary15.lean), [`Semantics/ErdosTernary15.lean`](./Semantics/ErdosTernary15.lean) | See [`RELATED_WORK.md`](../RELATED_WORK.md) for the historical progression across each domain. @@ -29,6 +30,7 @@ All proofs in [`Cryptids/`](./) are checked by the Lean 4 kernel (`v4.35.0-rc4`) - **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 ternary conjecture (`erdos_ternary_15` and `erdos_ternary_14`):** Stérin and Woods's 15-state machine constructively satisfies `Halts erdosTernary15 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n`, where `pw n` is the base-3 digit list of `2 ^ n` computed by repeated doubling ([`ErdosTernary15.lean`](./ErdosTernary15.lean)), and with `Classical.choice` (Mathlib's `Nat.digits`, and Markov's Principle on `¬ ∀ n, ...`) satisfies `Halts erdosTernary15 ↔ ¬ ErdosTernaryConjecture` ([`Semantics/ErdosTernary15.lean`](./Semantics/ErdosTernary15.lean)). Stérin's 14-state machine `erdos_ternary_14` constructively satisfies `Halts erdosTernary14 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n` and hence `Halts candidate ↔ Halts reference` against `erdos_ternary_15` ([`ErdosTernary14.lean`](./ErdosTernary14.lean)), and `Halts candidate ↔ ¬ ErdosTernaryConjecture` ([`Semantics/ErdosTernary14.lean`](./Semantics/ErdosTernary14.lean)). + - **Brocard's problem (`brocard_28`):** The machine keeps `n! / 8` in unary and tests it for triangularity by subtracting `1, 2, 3, …`; it constructively satisfies `Halts brocard28 ↔ ∃ n, 8 ≤ n ∧ IsTri (n! / 8)` and `Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n! + 1)` without `Classical.choice` ([`Brocard28.lean`](./Brocard28.lean), [`Semantics/Brocard28.lean`](./Semantics/Brocard28.lean)), and with Markov's Principle `Halts brocard28 ↔ ¬ BrocardConjecture`. - **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). diff --git a/Cryptids/Semantics/Brocard28.lean b/Cryptids/Semantics/Brocard28.lean new file mode 100644 index 00000000..97e25a4b --- /dev/null +++ b/Cryptids/Semantics/Brocard28.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.Brocard28 +public import Cryptids.Propositions + +/-! +# Semantics of `brocard_28` + +`Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n ! + 1)`: the machine's triangular test of +`n! / 8` is equivalent to `n! + 1` being a perfect square, since `n! + 1 = m ^ 2` forces `m` odd, +`m = 2k + 1`, and then `n! / 8 = k (k + 1) / 2 = tri k`. +-/ + +@[expose] public section + +namespace ConjectureMachines.Brocard28 + +/-- `tri k = k * (k + 1) / 2`. -/ +theorem two_mul_tri (k : ℕ) : 2 * tri k = k * (k + 1) := by + induction k with + | zero => rfl + | succ k ih => rw [tri_succ, Nat.mul_add, ih]; ring + +/-- For `n ≥ 4`, `n! + 1` is a square if and only if `n! / 8` is triangular. -/ +theorem isSquare_iff_isTri {n : ℕ} (hn : 4 ≤ n) : IsSquare (n.factorial + 1) ↔ IsTri (V n) := by + obtain ⟨c, hc⟩ := eight_dvd_factorial hn + have hV : V n = c := by rw [V, hc, Nat.mul_div_cancel_left _ (by decide)] + rw [hV, hc] + constructor + · rintro ⟨m, hm⟩ + obtain ⟨k, hk | hk⟩ : ∃ k, m = 2 * k ∨ m = 2 * k + 1 := ⟨m / 2, by omega⟩ + · -- `m` even: `m * m` is even, but `8 c + 1` is odd + exfalso + rw [hk] at hm + have : 8 * c + 1 = 4 * (k * k) := by rw [hm]; ring + omega + · refine ⟨k, ?_⟩ + rw [hk] at hm + have h1 : 8 * c + 1 = 4 * (k * k) + 4 * k + 1 := by rw [hm]; ring + have h2 := two_mul_tri k + rw [Nat.mul_succ] at h2 + omega + · rintro ⟨k, hk⟩ + refine ⟨2 * k + 1, ?_⟩ + have h2 := two_mul_tri k + rw [Nat.mul_succ] at h2 + have h3 : (2 * k + 1) * (2 * k + 1) = 4 * (k * k) + 4 * k + 1 := by ring + omega + +/-- The 28-state machine halts on the blank tape if and only if Brocard's problem has a +solution beyond `n = 4, 5, 7`. -/ +theorem halts_brocard28_iff_exists_square : + ConjectureMachines.Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n.factorial + 1) := by + rw [halts_brocard28_iff_exists_tri] + constructor + · rintro ⟨n, h8, hn⟩ + exact ⟨n, by omega, (isSquare_iff_isTri (by omega)).mpr hn⟩ + · rintro ⟨n, h7, hn⟩ + exact ⟨n, by omega, (isSquare_iff_isTri (by omega)).mp hn⟩ + +/-- The 28-state machine halts if and only if Brocard's conjecture is false. -/ +theorem halts_brocard28_iff_not_brocard : + ConjectureMachines.Halts brocard28 ↔ ¬ BrocardConjecture := by + rw [halts_brocard28_iff_exists_square] + exact ⟨fun ⟨n, h7, hn⟩ hB => hB n h7 hn, + fun h => by_contra fun hne => h fun n h7 hn => hne ⟨n, h7, hn⟩⟩ + +end ConjectureMachines.Brocard28 diff --git a/Cryptids/Semantics/README.md b/Cryptids/Semantics/README.md index a295ee0b..dab7e202 100644 --- a/Cryptids/Semantics/README.md +++ b/Cryptids/Semantics/README.md @@ -643,3 +643,39 @@ with `candidate = erdosTernary14` and `reference = erdosTernary15`. 2. **Semantics (`Semantics/ErdosTernary14.lean`)**: Composes `candidate_equivalent` with `halts_erdosTernary15_iff_not_erdosTernary` (`Classical.choice` through `Nat.digits`, and Markov's Principle via `not_forall`, as in Section 7). + +## 9. A 28-State Brocard Machine ([`Brocard28.lean`](./Brocard28.lean)) + +In [`Cryptids/Brocard28.lean`](../Brocard28.lean) and [`Cryptids/Semantics/Brocard28.lean`](./Brocard28.lean), +we formalize a new 28-state binary Turing machine for Brocard's problem (`brocard_28`, Daniel Veljjanoski with +Claude (Anthropic) as assistant, November 2026): + +```lean +theorem halts_brocard28_iff_exists_tri : + ConjectureMachines.Halts brocard28 ↔ ∃ n, 8 ≤ n ∧ IsTri (V n) + +theorem halts_brocard28_iff_exists_square : + ConjectureMachines.Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n.factorial + 1) + +theorem halts_brocard28_iff_not_brocard : + ConjectureMachines.Halts brocard28 ↔ ¬ BrocardConjecture +``` + +with `V n = n.factorial / 8` and `IsTri x ↔ ∃ k, x = 1 + 2 + ⋯ + k`. + +1. **Machine (`Brocard28.lean`)**: The tape holds `n` cells and `n! / 8` cells in unary. A round + multiplies the second block by `n + 1` (a hole walks through the first block, one copy per + cell, and at the start of each round `LN0`/`LN1` write one cell left of the first block), then + tests the result by subtracting `1, 2, 3, …` with a chunk block whose hole walks left; the + blank beyond the chunk block acts as its hole, so each wrap grows it for free. A success + counts the ones of the second block modulo `4` on the way back: residue `0` halts, which by + `32 ∣ n!` is exactly the case `n ≥ 8`; the known solutions give `15 ≡ 3` and `630 ≡ 2 (mod 4)` + and return to the next round. + One lemma per routine (copy step and loop, counter step and loop, merge, unit, chunk loop by + strong induction, fail, wrap, success, gate, start) gives `halts_brocard28_iff_exists_tri` with + `propext` and `Quot.sound` only. +2. **Semantics (`Semantics/Brocard28.lean`)**: `n! + 1 = m ^ 2` with `n ≥ 4` forces `m = 2k + 1` + and `n! / 8 = k (k + 1) / 2`, so `IsSquare (n! + 1) ↔ IsTri (n! / 8)` (`isSquare_iff_isTri`, + constructive), which gives `halts_brocard28_iff_exists_square` without `Classical.choice`; + `halts_brocard28_iff_not_brocard` uses Markov's Principle via `by_contra` (as with `not_forall` + in Section 7). diff --git a/README.md b/README.md index 979d9ea0..8430e160 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`, `erdos_ternary_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 ternary conjecture**. +1. **[Conjecture-Checking Turing Machines (`Cryptids/`)](Cryptids/README.md)** — Certified state reductions (`goldbach_21`, `zf_380`, `riemann_95`, `erdos_ternary_14`) and end-to-end Lean 4 mathematical semantics proofs (`Halts M ↔ ...`) for **Goldbach's Conjecture**, **ZF Set Theory Consistency**, the **Riemann Hypothesis**, **Erdős's ternary conjecture**, and **Brocard's problem** (`brocard_28`, a new 28-state machine). 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, the Riemann Hypothesis, and Erdős's ternary conjecture | Certified state reductions (`25 → 21`, `393 → 380`, `120 → 104 → 95`, `15 → 14`) and end-to-end halting equivalences (`Halts M ↔ ¬ GoldbachConjecture`, `ZFInconsistent`, `¬ RiemannHypothesis`, `¬ ErdosTernaryConjecture`) | [`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, Erdős's ternary conjecture, and Brocard's problem | Certified state reductions (`25 → 21`, `393 → 380`, `120 → 104 → 95`, `15 → 14`), a new 28-state Brocard machine, and end-to-end halting equivalences (`Halts M ↔ ¬ GoldbachConjecture`, `ZFInconsistent`, `¬ RiemannHypothesis`, `¬ ErdosTernaryConjecture`, `¬ BrocardConjecture`) | [`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) (54 closed-pattern/reflective holdouts + 35 [`Accelerations/`](BusyBeaver/BB6/Accelerations/README.md) + 180 resolved [`Halt/`](BusyBeaver/BB6/Halt/) and [`NonHalt/`](BusyBeaver/BB6/NonHalt/) proofs, plus halting equivalences and hardness evidence) and [`BusyBeaver/BB33/`](BusyBeaver/BB33/README.md) (6 machines) | [`BusyBeaver/README.md`](BusyBeaver/README.md), [`BusyBeaver/BB6/README.md`](BusyBeaver/BB6/README.md), [`BusyBeaver/BB6/Accelerations/README.md`](BusyBeaver/BB6/Accelerations/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)), the `erdos_ternary_14` reduction ([`ErdosTernary14.lean`](Cryptids/ErdosTernary14.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_ternary_15` and `erdos_ternary_14` equivalences with `ErdosTernaryConjecture` (`Nat.digits`, and Markov's Principle for `¬ ErdosTernaryConjecture`), 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_ternary_14` reduction ([`ErdosTernary14.lean`](Cryptids/ErdosTernary14.lean)), the `brocard_28` equivalence `Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n! + 1)` ([`Brocard28.lean`](Cryptids/Brocard28.lean), [`Semantics/Brocard28.lean`](Cryptids/Semantics/Brocard28.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_ternary_15` and `erdos_ternary_14` equivalences with `ErdosTernaryConjecture` (`Nat.digits`, and Markov's Principle for `¬ ErdosTernaryConjecture`), the `brocard_28` equivalence with `¬ BrocardConjecture` (Markov's Principle), 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), [`riemann_95`](artifacts/riemann_95/README.md), and [`erdos_ternary_14`](artifacts/erdos_ternary_14/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), [`erdos_ternary_14`](artifacts/erdos_ternary_14/README.md), and [`brocard_28`](artifacts/brocard_28/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. diff --git a/RELATED_WORK.md b/RELATED_WORK.md index 2b524999..1baa17e3 100644 --- a/RELATED_WORK.md +++ b/RELATED_WORK.md @@ -21,6 +21,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 ternary conjecture (`erdos_ternary_15`, `erdos_ternary_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. +- **Brocard's problem (`brocard_28`):** a new 28-state machine (Nov 2026) with Lean 4 semantics proofs, after Charlie Reams's 61-state machine (Nov 2026) and a 43-state table without a machine-checked proof (May 2026). ### 1. Goldbach's Conjecture (`goldbach`) @@ -66,3 +67,13 @@ Enumerates positive integers $n$ and tests an elementary arithmetic inequality e | :--- | :--- | :--- | :--- | :--- | | 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/ErdosTernary15.lean`](Cryptids/ErdosTernary15.lean), [`Cryptids/Semantics/ErdosTernary15.lean`](Cryptids/Semantics/ErdosTernary15.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/ErdosTernary14.lean`](Cryptids/ErdosTernary14.lean), [`Cryptids/Semantics/ErdosTernary14.lean`](Cryptids/Semantics/ErdosTernary14.lean)) | + +### 5. Brocard's Problem (`brocard`) + +Enumerates `n = 8, 9, …` and halts if and only if `n! + 1` is a perfect square for some such `n`, i.e. if Brocard's problem (Brocard 1876, 1885; Ramanujan 1913) has a solution beyond `n = 4, 5, 7`. Erdős conjectured that there is none; none exists for `n ≤ 10^12` (Matson 2017). `brocard_28` keeps `n! / 8` in unary, since `n! + 1 = m^2` forces `m = 2k + 1` and `n! / 8 = k (k + 1) / 2`, and tests it for triangularity by subtracting `1, 2, 3, …`. William Gasarch's SIGACT News Open Problems Column ([vol. 57, no. 3, Sept 2026](https://doi.org/10.1145/3848065.3848068), Open Problem 6.2) asks to improve the 43-state count and reports Jonathan Brown's conjecture that about 30 states may suffice; `brocard_28` improves the count to 28. + +| Year | Authors / Source | States (`(Q, 2)`) | Construction / Reduction Method | Formal Proof | +| :--- | :--- | :--- | :--- | :--- | +| 2026 | Gurpreet Tandi, Josue Gonzalez-Hendrix & Jonathan Brown ([`arXiv:2605.20215`](https://arxiv.org/abs/2605.20215), May 2026) | `≤ 43` (claimed) | Unary factorial, square test by subtracting odd numbers; the state count is an upper bound obtained by merging states, with the table in the appendix | None | +| 2026 | Charlie Reams ([`calr3/tinycryptids`](https://github.com/calr3/tinycryptids) `brocard/`, Nov 2026) | `61` | 98-state hand design (unary factorial by copying, odd-number square test, 7-round warm-up) merged to 61 states by exact SAT | Lean 4 proof in `tinycryptids` (`TM.Brocard.M61.halts_iff`, core Lean) | +| 2026 | Daniel Veljjanoski, with Claude (Anthropic) as assistant (`brocard_28`) | `28` | Triangularity test of `n! / 8` with a free `+1` per wrap (the blank beyond the chunk block acts as its hole), in-place multiply with the counter grown by one cell at each round start, a residue gate (`n! / 8 ≡ 0 (mod 4)` exactly for `n ≥ 8`) as the warm-up gate, and a one-state start through the loop's never-read cells | Lean 4 proofs ([`Cryptids/Brocard28.lean`](Cryptids/Brocard28.lean), [`Cryptids/Semantics/Brocard28.lean`](Cryptids/Semantics/Brocard28.lean)) | diff --git a/artifacts/brocard_28/README.md b/artifacts/brocard_28/README.md new file mode 100644 index 00000000..df57b38e --- /dev/null +++ b/artifacts/brocard_28/README.md @@ -0,0 +1,66 @@ +# 28-state Brocard machine + +This binary Turing machine has **28 states** and 55 defined transitions. It halts only in state +`23` (`M0`) reading `0`, its one undefined cell. It starts in state `0` (`GO`) on the blank tape. +Lean proves that it halts if and only if Brocard's problem `n! + 1 = m^2` has a solution with +`n > 7`, i.e. beyond the three known solutions `n = 4, 5, 7` (Brocard 1876, Ramanujan 1913; +Erdős conjectured there are no others; none exist for `n ≤ 10^12`). + +The machine was designed by Daniel Veljjanoski, with Claude (Anthropic) as assistant. Earlier +machines for the same problem: Charlie Reams's 61-state machine with a Lean proof +([`calr3/tinycryptids`](https://github.com/calr3/tinycryptids), November 2026) and a 43-state table +without a machine-checked proof in Tandi, Gonzalez-Hendrix and Brown, *Measuring Decidability as Related to Busy +Beaver Numbers* ([arXiv:2605.20215](https://arxiv.org/abs/2605.20215)). Improving that 43-state count is +Open Problem 6.2 of William Gasarch's SIGACT News Open Problems Column ([vol. 57, no. 3, September +2026](https://doi.org/10.1145/3848065.3848068)), which reports Jonathan Brown's conjecture that about +30 states may suffice; this machine has 28. + +## How it works + +Everything is in unary. The tape holds a block `N` of `n` cells, a separator, and a block `B` +that holds `n!/8` cells between rounds (`3` at `n = 4`). `n! + 1` is a square if and only if +`n!/8` is a triangular number `1 + 2 + ... + k` (`m = 2k + 1`), so a round multiplies `B` by +`n + 1`, grows `N` by one cell, and tests `B` by subtracting `1, 2, 3, ...`: + +* **Multiply** (states `2`–`11`): a hole walks through `N`; for each cell the template `B` is + copied once to the right end, cell by cell with a cursor hole. The merge leaves one extra cell. +* **Test** (states `1`, `12`–`19`): a hole walks right through `B`; a block `S` right of `B` holds + the current chunk size with a hole walking left, and the blank beyond `S` acts as its hole, so + `S` grows by one cell per wrap for free. At each wrap the machine checks whether `B` is + exhausted. +* **Fail** (states `20`–`22`): `S` is erased and the last cell of `B` with it, which cancels the + merge's extra cell. +* **Gate** (states `23`–`27`): a success walks left over `B` counting its ones modulo `4`. + Residue `0` halts at the separator; residues `2` and `3` return to the next round. Since + `32` divides `n!` for `n ≥ 8`, every success with `n ≥ 8` has residue `0`, while the known + solutions have `7!/8 = 630 ≡ 2` and `5!/8 = 15 ≡ 3 (mod 4)` (`n = 6` fails the test). +* **Start**: the machine starts in `GO` (state `0`) on the blank tape. `GO` and the two cells + that no run of the loop reads (`TLx` and `M1` reading `0`) steer the loop's own states to + write `1111 0 111` in 46 steps and enter the loop in `LN1` on the blank left of `N`, the + configuration every round passes through. This start was found by an exhaustive search over + one-state starts; no start without a new state exists. Earlier versions with 41 and 34 + states, whose gate counted the cells of `N`, are in the history of the pull request. + +As a one-line table in the style of the bbchallenge standard format, with the states `0`–`25` +written `A`–`Z` and `26`–`27` written `a`–`b` (the standard format itself covers only 26 states, +and the bbchallenge.org viewer ignores case, so this string is for reading, not for that viewer): + +``` +1LK1RD_0LK0RN_0LD1LC_1RE1LD_0RL0RF_0RK1RF_0RH1RG_1LI1RH_0LJ1LI_1RK1LJ_0LC0RG_1RM1RL_0RB1LM_0RO1RN_1LP1RO_0LQ0LR_0LX1RN_0LS1LR_1RT1LS_0RU0RN_0RV0RU_0LW0RV_0LW0LC_---1LY_1RA1LZ_0Rb1La_0Rb1LX_1RU1Rb +``` + +## Review entry points + +- [`Brocard28.lean`](../../Cryptids/Brocard28.lean): the machine (loaded from `machine.txt`), the + routine lemmas, and `halts_brocard28_iff_exists_tri`. +- [`Semantics/Brocard28.lean`](../../Cryptids/Semantics/Brocard28.lean): + `halts_brocard28_iff_exists_square` and `halts_brocard28_iff_not_brocard`. + +## Verification + +`python3 verify.py` simulates the machine on the blank tape, checks that the 46-step start +produces `1111 0 111`, and checks the tape at every test against `n!/8 + 1` (`n = 5, 6` at the +default `--steps 250000`; the tests for `n = 7` and `n = 8` start after about 360,000 and +23,000,000 steps). It also checks that from a prepared tape a planted triangular number of cells +with residue `0` halts in state `23` while a non-triangular one goes on to the next test with +the expected tape. diff --git a/artifacts/brocard_28/machine.txt b/artifacts/brocard_28/machine.txt new file mode 100644 index 00000000..90eb293d --- /dev/null +++ b/artifacts/brocard_28/machine.txt @@ -0,0 +1,28 @@ +1L10 1R3 +0L10 0R13 +0L3 1L2 +1R4 1L3 +0R11 0R5 +0R10 1R5 +0R7 1R6 +1L8 1R7 +0L9 1L8 +1R10 1L9 +0L2 0R6 +1R12 1R11 +0R1 1L12 +0R14 1R13 +1L15 1R14 +0L16 0L17 +0L23 1R13 +0L18 1L17 +1R19 1L18 +0R20 0R13 +0R21 0R20 +0L22 0R21 +0L22 0L2 +--- 1L24 +1R0 1L25 +0R27 1L26 +0R27 1L23 +1R20 1R27 diff --git a/comparator/README.md b/comparator/README.md index f5a903c6..31cc4ddd 100644 --- a/comparator/README.md +++ b/comparator/README.md @@ -11,7 +11,7 @@ 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`, `ErdosTernaryConjecture`, etc.), and states all 34 target + `paZFInconsistent`, `ErdosTernaryConjecture`, etc.), and states all 36 target state-reduction, equivalence, `PA` metatheory & internalized `ZF` provability, and semantics theorems with `sorry`. - [`BusyBeaverChallenge.lean`](../BusyBeaverChallenge.lean) imports **only** Mathlib and Lean core @@ -43,8 +43,9 @@ 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`), the `ErdosTernary14` reduction, and all five `candidate_fewer_states` - theorems (15 theorems total). + `Zf380`, `Riemann104`), the `ErdosTernary14` reduction, all five `candidate_fewer_states` + theorems, and the `brocard_28` equivalence `Brocard28.halts_brocard28_iff_exists_square` + (16 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 @@ -53,15 +54,15 @@ that: [`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`, - `erdos_ternary_15.json`, `erdos_ternary_14.json`). + `erdos_ternary_15.json`, `erdos_ternary_14.json`, `brocard_28.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 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 `ErdosTernary14` 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 | +| [`constructive.json`](./constructive.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound` | All 16 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 `ErdosTernary14` reduction, and `Brocard28.halts_brocard28_iff_exists_square` | +| [`all.json`](./all.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound`, `Classical.choice` | All 36 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 506 `BB(6)` and `BB(3, 3)` holdout Level A, Level B, equivalence, A6 `is_not_halt`, and hardness-evidence theorems (`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`, `is_not_halt`, `isHalt_HHH1LC_iff_HHH0LA`, `HardnessEvidence.*`) | | [`a6.json`](./a6.json) | `BusyBeaverChallenge` | `BusyBeaver.BB6.M_1RB0LF_1RC0RA_1LD0RB_0LE0LC_0LA0LC_0LBHHH` | `propext`, `Quot.sound`, `Classical.choice` | A6 `is_not_halt` | @@ -76,6 +77,7 @@ that: | [`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_ternary_15.json`](./erdos_ternary_15.json) | `Challenge` | `Cryptids.Semantics.ErdosTernary15` | `propext`, `Quot.sound`, `Classical.choice` | `halts_erdosTernary15_iff_exists_counterexample`, `halts_erdosTernary15_iff_not_erdosTernary` | | [`erdos_ternary_14.json`](./erdos_ternary_14.json) | `Challenge` | `Cryptids.Semantics.ErdosTernary14` | `propext`, `Quot.sound`, `Classical.choice` | `candidate_fewer_states`, `candidate_equivalent`, `halts_candidate_iff_not_erdosTernary` | +| [`brocard_28.json`](./brocard_28.json) | `Challenge` | `Cryptids.Semantics.Brocard28` | `propext`, `Quot.sound`, `Classical.choice` | `halts_brocard28_iff_exists_square`, `halts_brocard28_iff_not_brocard` | 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 45857bbc..bd8b7a1c 100644 --- a/comparator/all.json +++ b/comparator/all.json @@ -35,7 +35,9 @@ "ConjectureMachines.ErdosTernary15.halts_erdosTernary15_iff_not_erdosTernary", "ConjectureMachines.ErdosTernary14.candidate_fewer_states", "ConjectureMachines.ErdosTernary14.candidate_equivalent", - "ConjectureMachines.ErdosTernary14.Semantics.halts_candidate_iff_not_erdosTernary" + "ConjectureMachines.ErdosTernary14.Semantics.halts_candidate_iff_not_erdosTernary", + "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square", + "ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard" ], "permitted_axioms": [ "propext", diff --git a/comparator/brocard_28.json b/comparator/brocard_28.json new file mode 100644 index 00000000..29a8682a --- /dev/null +++ b/comparator/brocard_28.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Cryptids.Semantics.Brocard28", + "theorem_names": [ + "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square", + "ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ] +} diff --git a/comparator/constructive.json b/comparator/constructive.json index 043f3a3c..2d917499 100644 --- a/comparator/constructive.json +++ b/comparator/constructive.json @@ -16,7 +16,8 @@ "ConjectureMachines.Riemann104.candidate_equivalent", "ConjectureMachines.Riemann95.candidate_fewer_states", "ConjectureMachines.ErdosTernary14.candidate_fewer_states", - "ConjectureMachines.ErdosTernary14.candidate_equivalent" + "ConjectureMachines.ErdosTernary14.candidate_equivalent", + "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square" ], "permitted_axioms": [ "propext", diff --git a/formalization.yaml b/formalization.yaml index eb6409e1..3f8a0fd5 100644 --- a/formalization.yaml +++ b/formalization.yaml @@ -12,7 +12,8 @@ project: the 2016 744-state machine riemann_744), and Erdős's ternary conjecture (15 -> 14 states: Tristan Stérin and Damien Woods's 2021 15-state machine erdos_ternary_15 and Tristan Stérin's October 2026 14-state machine - erdos_ternary_14), + erdos_ternary_14), and Brocard's problem (a new 28-state machine brocard_28, + November 2026), proving halting equivalences and connecting every machine's blank-tape halting behavior to the corresponding statement in Mathlib. authors: @@ -165,6 +166,49 @@ sources: First Lean 4 proof that erdos_ternary_14 halts iff erdos_ternary_15 halts, and hence iff Erdős's ternary conjecture is false (Cryptids/ErdosTernary14.lean, Cryptids/Semantics/ErdosTernary14.lean). + - title: "A Turing machine for Brocard's problem (tinycryptids, brocard_61)" + authors: + - "Charlie Reams" + id: "https://github.com/calr3/tinycryptids" + type: "web post" + relationship: "background" + author_endorsement: "not-contacted" + note: >- + A 61-state, 2-symbol machine (a 98-state design merged by exact SAT) with a + Lean proof TM.Brocard.M61.halts_iff in core Lean, published in November 2026; + an earlier machine for the problem, with a Lean proof. Not used by brocard_28. + - title: "Measuring Decidability as Related to Busy Beaver Numbers" + authors: + - "Gurpreet Tandi" + - "Josue Gonzalez-Hendrix" + - "Jonathan Brown" + id: "https://arxiv.org/abs/2605.20215" + type: "article" + relationship: "background" + author_endorsement: "not-contacted" + note: >- + Describes a Turing machine for Brocard's problem with an upper bound of 43 + states (May 2026), without a machine-checked proof. + - title: "Relationships Between the Busy Beaver Function and Mathematics II: Small Turing Machines and Open Problems (SIGACT News Open Problems Column)" + authors: + - "William Gasarch" + id: "https://doi.org/10.1145/3848065.3848068" + type: "article" + relationship: "background" + author_endorsement: "not-contacted" + note: >- + SIGACT News 57(3), September 2026. Open Problem 6.2 asks to improve the + 43-state count for Brocard's problem and reports Jonathan Brown's conjecture + that about 30 states may suffice. brocard_28 improves the count to 28. + - title: "A 28-state Turing machine for Brocard's problem with Lean 4 proofs (brocard_28)" + authors: + - "Daniel Veljjanoski" + type: "original-proof" + relationship: "other" + note: >- + New machine (artifacts/brocard_28/machine.txt) and first Lean 4 proofs that it halts + iff n! + 1 is a perfect square for some n > 7 (Cryptids/Brocard28.lean, + Cryptids/Semantics/Brocard28.lean). related_formalizations: - id: "https://github.com/lengyijun/goldbach_tm" @@ -213,7 +257,11 @@ status: machine erdos_ternary_14 satisfies Halts erdosTernary14 <-> ∃ n, 8 < n ∧ 2 ∉ pw n and hence Halts candidate <-> Halts reference against erdos_ternary_15 constructively (Cryptids/ErdosTernary14.lean), and Halts candidate <-> ¬ - ErdosTernaryConjecture (Cryptids/Semantics/ErdosTernary14.lean). + ErdosTernaryConjecture (Cryptids/Semantics/ErdosTernary14.lean). The 28-state + machine brocard_28 satisfies Halts brocard28 <-> ∃ n, 8 ≤ n ∧ IsTri (n! / 8) and + Halts brocard28 <-> ∃ n, 7 < n ∧ IsSquare (n! + 1) constructively + (Cryptids/Brocard28.lean, Cryptids/Semantics/Brocard28.lean), and + Halts brocard28 <-> ¬ BrocardConjecture with Markov's Principle. sorry_count: 0 sorry_in_definitions: 0 axioms: @@ -356,6 +404,16 @@ status: sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator/erdos_ternary_14.json" + - declaration: "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square" + file: "Cryptids/Semantics/Brocard28.lean" + sorry_count: 0 + axioms: ["propext", "Quot.sound"] + comparator_config: "comparator/constructive.json" + - declaration: "ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard" + file: "Cryptids/Semantics/Brocard28.lean" + sorry_count: 0 + axioms: ["propext", "Classical.choice", "Quot.sound"] + comparator_config: "comparator/brocard_28.json" automation: methods: @@ -377,15 +435,18 @@ automation: prompting_notes: >- Used as assistant for the erdos_ternary_15 and erdos_ternary_14 proofs (Cryptids/ErdosTernary15.lean, Cryptids/Semantics/ErdosTernary15.lean, - Cryptids/ErdosTernary14.lean, Cryptids/Semantics/ErdosTernary14.lean). + Cryptids/ErdosTernary14.lean, Cryptids/Semantics/ErdosTernary14.lean) and for + the design, simulation checks and proofs of brocard_28 + (Cryptids/Brocard28.lean, Cryptids/Semantics/Brocard28.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. The erdos_ternary_15 machine is by Tristan Stérin and Damien Woods and the erdos_ternary_14 - machine by Tristan Stérin; the erdos_ternary_15 and erdos_ternary_14 proofs were written - by Daniel Veljjanoski with Claude (Anthropic) as assistant. + machine by Tristan Stérin; the erdos_ternary_15 and erdos_ternary_14 proofs, and the + brocard_28 machine and proofs, were written by Daniel Veljjanoski with Claude + (Anthropic) as assistant. fidelity: divergences: >- @@ -517,6 +578,18 @@ alignment: lean: "ConjectureMachines.ErdosTernary14.Semantics.halts_candidate_iff_not_erdosTernary" module: "Cryptids.Semantics.ErdosTernary14" status: "proved" + - source: "brocard_28 <-> ∃ n ≥ 8, n! / 8 triangular" + lean: "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_tri" + module: "Cryptids.Brocard28" + status: "proved" + - source: "brocard_28 <-> ∃ n > 7, IsSquare (n! + 1)" + lean: "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square" + module: "Cryptids.Semantics.Brocard28" + status: "proved" + - source: "brocard_28 <-> ¬ BrocardConjecture" + lean: "ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard" + module: "Cryptids.Semantics.Brocard28" + status: "proved" acknowledgements: >- We thank Eric Wieser for careful review, the Busy Beaver Challenge community, diff --git a/verify.py b/verify.py index 5ace947b..b508d87a 100755 --- a/verify.py +++ b/verify.py @@ -47,6 +47,10 @@ `2^k` and the count of powers without a digit 2 (`Cryptids/ErdosTernary15.lean`). - Erdos (14 states): at every entry to the division state `D` the tape is the configuration predicted by `Cryptids/ErdosTernary14.lean`. + - Brocard (28 states): the 46-step start writes `1111 0 111`, then at every entry to the + test state `TLx` the tape holds `n` cells of `N` and `n!/8 + 1` cells of `B` + (`Cryptids/Brocard28.lean`), and from a prepared tape a triangular `B` with a + multiple of `4` cells halts in `M0`. """ from __future__ import annotations @@ -257,6 +261,25 @@ ] +# A new machine with no reference: checked like a candidate (table, SHA-256, Lean +# definitions in `Machines.lean` and `Challenge.lean`) plus its own stage simulation. +BROCARD_28 = { + "id": "brocard_28", + "path": "artifacts/brocard_28", + "lean_file": "Cryptids/Machines.lean", + "lean_def": "brocard28", + "proof_path": "Cryptids/Brocard28.lean", + "challenge_path": "Challenge.lean", + "states": 28, + "machine_sha256": ( + "957e52ef4b8f40da12c9d840ea4a28369f76cbf10c384fb65012f121edc03d39" + ), + "table_file_sha256": ( + "957e52ef4b8f40da12c9d840ea4a28369f76cbf10c384fb65012f121edc03d39" + ), +} + + @dataclasses.dataclass(frozen=True) class Transition: write: int @@ -887,6 +910,95 @@ def expected_entries(): } +def verify_brocard_28(machine: Machine, steps: int) -> dict[str, object]: + """Checks the round layout of `Cryptids/Brocard28.lean`. + + On the blank tape, the first 46 steps (the start, which passes through the test state + twice) write `1111 0 111` and end in state 3 (`LN1`) on the blank left of `N`. After + that, every time `brocard_28` enters state 1 (`TLx`, the start of a test) the head is + on cell `p` with `B = n!/8 + 1` ones on cells `p, ..., p+B-1`, a `0` on `p-1`, the `n` + cells of `N` on `p-n-1, ..., p-2`, and nothing else; the first entry is at step 318 + with `n = 5`. Then, from a prepared tape with eight cells of `N` and `1 + T_8 = 37` + cells of `B` in state 1 (`36 = T_8` is triangular and a multiple of `4`), the machine + halts in state 23 (`M0`); with `2 + T_8` cells it reaches the next test with `9` cells + of `N` and `9 * 37 + 1` cells of `B`. + """ + proof_text = (ROOT / "Cryptids/Brocard28.lean").read_text(encoding="utf-8") + assert "theorem halts_brocard28_iff_exists_tri" in proof_text + halting = [ + (q, sym) + for q, row in enumerate(machine.table) + for sym, tr in enumerate(row) + if tr is None + ] + # Only `M0` (state 23) on `0` halts. + assert halting == [(23, 0)], f"brocard_28 halting entries: {halting}" + + def run(ones: set[int], head: int, state: int, limit: int, stop_state: int | None): + """Runs until `stop_state` is entered (after a step), a halt, or `limit` steps.""" + for t in range(limit): + tr = machine.table[state][int(head in ones)] + if tr is None: + return "halt", state, head, t + if tr.write: + ones.add(head) + else: + ones.discard(head) + head += tr.direction + state = tr.next_state + if state == stop_state: + return "stop", state, head, t + 1 + return "limit", state, head, limit + + def factorial(n: int) -> int: + f = 1 + for i in range(2, n + 1): + f *= i + return f + + # The start: 46 steps, no stop. + ones: set[int] = set() + status, state, head, total = run(ones, 0, 0, 46, None) + assert status == "limit" and state == 3, f"brocard_28 start: {status} in state {state}" + seed = {head + 1 + i for i in range(4)} | {head + 6 + i for i in range(3)} + assert ones == seed, "brocard_28 start: tape is not 1111 0 111" + + # Blank-tape rounds: n = 5, 6, ... as far as `steps` allows. + n, tests = 4, 0 + while True: + status, state, head, t = run(ones, head, state, steps - total, 1) + total += t + if status != "stop": + assert status == "limit", f"brocard_28 halted at step {total}" + break + n += 1 + b = factorial(n) // 8 + 1 + expected = {head + i for i in range(b)} | {head - 2 - i for i in range(n)} + assert ones == expected, f"brocard_28 test n={n}: tape mismatch at step {total}" + tests += 1 + if tests == 1: + assert total == 318, f"brocard_28 first test at step {total}" + if steps >= 8_000: + assert tests >= 2, f"brocard_28: only {tests} tests in {steps} steps" + + # Planted tests at a live round (eight cells of N): T_8 = 36 = 4 * 9. + def planted(b: int): + cells = {i for i in range(b)} | {-2 - i for i in range(8)} + return run(cells, 0, 1, 3_000_000, 1), cells + + (status, state, _, _), _ = planted(1 + 36) + assert (status, state) == ("halt", 23), f"brocard_28 planted square: {status} in {state}" + (status, state, head, _), cells = planted(2 + 36) + assert status == "stop", f"brocard_28 planted non-square: {status}" + expected = {head + i for i in range(9 * 37 + 1)} | {head - 2 - i for i in range(9)} + assert cells == expected, "brocard_28 planted non-square: wrong next tape" + return { + "steps_simulated": total, + "tests_verified": tests, + "last_n": n, + "planted_square_halts": True, + } + def extract_goldbach_chk0( machine: Machine, steps: int, is_candidate: bool ) -> dict[str, object]: @@ -1196,6 +1308,43 @@ def run_verification( f" up to the start of stage n = {erdosTernary14_sim['last_stage']}" ) + # Brocard: table, SHA-256, Lean definitions, and simulation. + bspec = BROCARD_28 + b_text = (ROOT / str(bspec["path"]) / "machine.txt").read_text(encoding="utf-8") + assert sha256_bytes(b_text.encode("utf-8")) == bspec["table_file_sha256"], ( + "brocard_28 table file SHA-256 mismatch" + ) + bm = parse_canonical_machine(b_text) + assert bm.states == bspec["states"], f"brocard_28 state count mismatch: {bm.states}" + assert bm.sha256 == bspec["machine_sha256"], ( + f"brocard_28 machine SHA-256 mismatch: {bm.sha256}" + ) + for lean_path in (bspec["lean_file"], bspec["challenge_path"]): + assert ( + parse_lean_machine_def( + (ROOT / str(lean_path)).read_text(encoding="utf-8"), + str(bspec["lean_def"]), + expected_table_path=f"{bspec['path']}/machine.txt", + ).table + == bm.table + ), f"{lean_path} brocard_28 table mismatch" + assert "theorem halts_brocard28_iff_exists_square" in ( + ROOT / "Challenge.lean" + ).read_text(encoding="utf-8") + brocard_sim = verify_brocard_28(bm, steps) + report["candidates"]["brocard_28"] = { + "states": bm.states, + "machine_sha256": bm.sha256, + } + report["simulations"]["brocard_28"] = brocard_sim + if verbose: + print( + f"[PASS] Brocard 28 ({bm.states} states, SHA-256 {bm.sha256[:16]}...):" + f" {brocard_sim['tests_verified']} tests verified on the blank tape" + f" ({brocard_sim['steps_simulated']:,} steps, up to n = {brocard_sim['last_n']});" + " planted square halts in M0" + ) + # 5. Concrete blank-tape lockstep simulations gb_ref_sim = extract_goldbach_chk0( baseline_machines["goldbach"], steps, is_candidate=False