diff --git a/Challenge.lean b/Challenge.lean index 60991aec..56af86b3 100644 --- a/Challenge.lean +++ b/Challenge.lean @@ -28,7 +28,8 @@ Self-contained specification module audited against `Cryptids` by `leanprover/co `Semantics.Zf.halts_zf432_iff_wadeZFInconsistent`), and first-order Peano Arithmetic (`PA`) consistency and $\Sigma_1^0$ standard-model adequacy (`Semantics.PA.not_paProvable_false`, `Semantics.PA.paHalts_holds_iff_halts`, `Semantics.PA.paZFInconsistent_holds_iff_zfInconsistent`), - and the `brocard_28` equivalence `Brocard28.halts_brocard28_iff_exists_square` + the `brocard_28` equivalence `Brocard28.halts_brocard28_iff_exists_square`, and the + `legendre_21` equivalence `Legendre21.halts_legendre21_iff_exists_gap` are verified **without `Classical.choice`** (`ListBlank` uses primitive `Quot` rather than `Quotient` so `Halts` is choice-free). Because `Zf/Soundness.lean` proves `not_zfInconsistent` via `ZFSet.{0}` (`Classical.choice`)—and `CIC + EM` proves `Con(ZF)` without choice @@ -37,13 +38,13 @@ Self-contained specification module audited against `Cryptids` by `leanprover/co metatheory that cannot prove `Con(PA)` or `Con(ZF)` (see `Cryptids/Semantics/README.md`). - **Full gate (`comparator/all.json`; `permitted_axioms = ["propext", "Quot.sound", "Classical.choice"]`):** - Audits all 36 theorems, including `Riemann95.candidate_equivalent` (which uses `Classical.choice` + Audits all 38 theorems, including `Riemann95.candidate_equivalent` (which uses `Classical.choice` via `Nat.Prime`), classical `PA` and `ZFSet.{0}` soundness/non-halting, negated-`Π₁⁰` Goldbach (`¬ GoldbachConjecture`, which uses Markov's Principle), analytic `RiemannHypothesis` equivalences, and the `erdos_ternary_15` and `erdos_ternary_14` equivalences with `ErdosTernaryConjecture` (`Nat.digits` uses `Classical.choice`; `¬ ErdosTernaryConjecture` also - uses Markov's Principle), and the `brocard_28` equivalence with `¬ BrocardConjecture` (Markov's - Principle). + uses Markov's Principle), and the `brocard_28` and `legendre_21` equivalences with + `¬ BrocardConjecture` and `¬ LegendreConjecture` (Markov's Principle). -/ meta section @@ -263,6 +264,11 @@ def brocard28Rows : List (List (Option (Fin 2 × Dir × Fin 28))) := load_machine_rows% "artifacts/brocard_28/machine.txt" /-- 28-state Brocard machine. -/ def brocard28 : Machine 28 2 := Machine.ofRows brocard28Rows +/-- Rows of `legendre21`. -/ +def legendre21Rows : List (List (Option (Fin 2 × Dir × Fin 21))) := + load_machine_rows% "artifacts/legendre_21/machine.txt" +/-- 21-state Legendre machine. -/ +def legendre21 : Machine 21 2 := Machine.ofRows legendre21Rows end Machines /-- **Goldbach's Conjecture**: every even integer greater than 2 is the sum of two primes. -/ @@ -760,6 +766,11 @@ solutions; none exist for `n ≤ 10 ^ 12` (Matson 2017). -/ def BrocardConjecture : Prop := ∀ n : ℕ, 7 < n → ¬ IsSquare (n.factorial + 1) +/-- **Legendre's conjecture** (one of Landau's four problems, 1912): for every `n ≥ 1` there is +a prime `p` with `n ^ 2 < p < (n + 1) ^ 2`. -/ +def LegendreConjecture : Prop := + ∀ n : ℕ, 1 ≤ n → ∃ p : ℕ, p.Prime ∧ n ^ 2 < p ∧ p < (n + 1) ^ 2 + namespace Goldbach21 /-- 25-state Goldbach reference machine (`goldbach_25`, Yao & Leng 2024). -/ abbrev reference : BundledMachine 2 := Machines.goldbach25.bundle @@ -890,4 +901,14 @@ theorem halts_brocard28_iff_not_brocard : ConjectureMachines.Halts brocard28 ↔ ¬ BrocardConjecture := by sorry end Brocard28 +namespace Legendre21 +/-- 21-state Legendre machine (`legendre_21`, Veljjanoski 2026). -/ +abbrev legendre21 : Machine 21 2 := Machines.legendre21 +theorem halts_legendre21_iff_exists_gap : + ConjectureMachines.Halts legendre21 ↔ + ∃ n : ℕ, 1 ≤ n ∧ ∀ p : ℕ, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2) := by sorry +theorem halts_legendre21_iff_not_legendre : + ConjectureMachines.Halts legendre21 ↔ ¬ LegendreConjecture := by sorry +end Legendre21 + end ConjectureMachines diff --git a/Cryptids.lean b/Cryptids.lean index 7a1d5979..8afe01f7 100644 --- a/Cryptids.lean +++ b/Cryptids.lean @@ -25,6 +25,8 @@ public import Cryptids.ErdosTernary14 public import Cryptids.Semantics.ErdosTernary14 public import Cryptids.Brocard28 public import Cryptids.Semantics.Brocard28 +public import Cryptids.Legendre21 +public import Cryptids.Semantics.Legendre21 /-! # Certified State Reductions & Formalized Conjecture-Checking Turing Machines @@ -32,7 +34,8 @@ public import Cryptids.Semantics.Brocard28 This library formalizes record smaller 2-symbol Turing machines for **Goldbach's Conjecture** (`25 → 21` states), **ZF Set Theory Consistency** (`393 → 380` states), the **Riemann Hypothesis** (`120 → 104 → 95` states), and **Erdős's ternary conjecture** (`15 → 14` -states), a 28-state machine for **Brocard's problem** (`brocard_28`), as well as complete +states), a 28-state machine for **Brocard's problem** (`brocard_28`), a 21-state machine for +**Legendre's conjecture** (`legendre_21`), as well as complete Lean 4 formalizations of all publicly known baseline machines (`goldbach_25`, `zf_432`, `zf_393`, `riemann_744`, `riemann_120`, `erdos_ternary_15`), @@ -81,6 +84,12 @@ linking every machine's blank-tape halting problem to Mathlib's statements: (`V n = n! / 8`) and `ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square` (`Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n! + 1)`), and `ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard`. +- `Cryptids.Legendre21`, `Cryptids.Semantics.Legendre21` — A 21-state machine for Legendre's + conjecture (`legendre21`), built on the primality test of `goldbach_21`, with constructive + proofs of `Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ EmptyInterval n` and + `ConjectureMachines.Legendre21.halts_legendre21_iff_exists_gap` + (`Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ ∀ p, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2)`), and + `ConjectureMachines.Legendre21.halts_legendre21_iff_not_legendre`. - `Cryptids.Semantics.Goldbach`, `Cryptids.Semantics.Zf`, `Cryptids.Semantics.Riemann` — End-to-end proofs linking halting from the blank tape to the corresponding mathematical conjectures across all baseline machines (`goldbach25`, `zf432`, `riemann744`). diff --git a/Cryptids/Legendre21.lean b/Cryptids/Legendre21.lean new file mode 100644 index 00000000..38a3b53f --- /dev/null +++ b/Cryptids/Legendre21.lean @@ -0,0 +1,1060 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.Goldbach21 + +/-! +# Legendre21 + +The 21-state Turing machine `legendre_21` halts on the blank tape if and only if Legendre's +conjecture fails: some `n ≥ 1` has no prime strictly between `n ^ 2` and `(n + 1) ^ 2`. + +## Provenance and Attribution + +The machine and the proofs are by Daniel Veljjanoski, with Claude (Anthropic) as assistant +(November 2026). The primality test is the one of the Goldbach machines: the anonymous 2016 +machine, Andrew Yao and Yijun Leng's `goldbach_25` (2024), and `goldbach_21` of Maxence Faldor +and Moritz Firsching (2026), whose lemmas in `Cryptids/Goldbach21.lean` this file uses. An +earlier machine for the same conjecture is Charlie Reams's 44-state machine with a Lean proof +(`calr3/tinycryptids`, November 2026). + +## Machine Layout + +States `0`–`20` of the table are `q14, q0, q3, q4, q6, q7, q9, q11, q12, q13, q15, q16, q20, q22, +q23, q24, A1, B, C, Z1, X`; `q0`–`q24` are the numbers of the same states in +`Goldbach21.edited`. The tape holds, left to right, a block of ones for the number under test, +a separator `0`, a flag cell, and a walker area of ones with one hole. The tape left of the +block stays blank; the block grows to the left. + +* Test (the sixteen `q` states): `q16` reading the blank left of a block of `t` ones writes a + `1` (the block now has `t + 1` cells) and enters the trial division of `t`. A prime leaves + `q6` on the separator; a composite leaves `q6` on the flag cell, through `A1`. The block is + restored in both cases. +* Walker (`B`, `C`, `Z1`): after each test `B` runs right to the hole and fills it, `C` opens a + hole one cell further left, `Z1` runs back, and `q3`, `q4`, `q16` return to the left end of + the block, where the next number is tested. +* Interval `n` is `n ^ 2, …, n ^ 2 + 2 n`. It starts with the flag clear and `2 n` ones in the + walker area (the blank beyond them is the hole). The first prime of the interval sets the + flag, moves the separator one cell left, and is tested once more. When the hole reaches the + left end with the flag set, it moves into the flag cell: the flag is clear again and the + walker area has `2 n + 2` ones, the start of interval `n + 1`. When the hole reaches the left + end with the flag clear after a composite, `C` reads the flag, `X` reads the separator, and + the machine halts: `X` reading `0` is the one undefined cell. +* Start: `q14` (state `0`) on the blank tape. After `17` steps the machine is at the test of `1` + with the walker area `1 0 1`. No state is used for the start only. + +## Proof Outline + +`leg25` is the machine in the 25-state numbering of `Goldbach21.edited` (`A1, B, C, Z1, X` +take the numbers `1, 2, 5, 8, 10`, which are free in our table), so the step and scan lemmas +and the machine-generic pass lemmas of `Cryptids/Goldbach21.lean` apply unchanged; the lemmas +stated there for `edited` only are proved again for `leg25`. +-/ + +@[expose] public section + +namespace ConjectureMachines.Legendre21 + +open Turing (Dir) +open StateTransition +open Goldbach21 + +/-- 21-state Legendre machine (`legendre_21`). -/ +abbrev legendre21 : Machine 21 2 := Machines.legendre21 + +/-- `legendre21` in the 25-state numbering of `Goldbach21.edited`: row `i` is state +`0` = `q0`, `1` = `A1`, `2` = `B`, `3` = `q3`, `4` = `q4`, `5` = `C`, `6` = `q6`, `7` = `q7`, +`8` = `Z1`, `9` = `q9`, `10` = `X`, `11` = `q11`, `12` = `q12`, `13` = `q13`, `14` = `q14`, `15` += `q15`, `16` = `q16`, `20` = `q20`, `22` = `q22`, `23` = `q23`, `24` = `q24`; +rows `17, 18, 19, 21` are unused. -/ +def leg25 : Machine 25 2 := Machine.ofRows [ + [some (0, .right, 11), some (1, .left, 22)], + [some (0, .right, 6), some (1, .right, 1)], + [some (1, .left, 5), some (1, .right, 2)], + [some (0, .left, 16), some (1, .right, 4)], + [some (0, .left, 16), some (1, .right, 6)], + [some (1, .left, 10), some (0, .left, 8)], + [some (0, .right, 2), some (0, .left, 7)], + [some (1, .right, 5), some (1, .left, 22)], + [some (0, .left, 3), some (1, .left, 8)], + [some (1, .right, 0), some (0, .left, 9)], + [none, some (0, .right, 2)], + [some (1, .right, 11), some (0, .right, 12)], + [some (1, .right, 13), some (1, .right, 12)], + [some (0, .left, 14), some (0, .left, 20)], + [some (1, .left, 15), some (1, .left, 14)], + [some (1, .left, 1), some (0, .left, 23)], + [some (1, .right, 3), some (1, .left, 16)], + [none, none], + [none, none], + [none, none], + [some (1, .left, 9), some (1, .left, 20)], + [none, none], + [some (0, .right, 0), some (0, .left, 22)], + [some (1, .right, 24), some (1, .left, 23)], + [some (1, .right, 3), some (1, .right, 24)] +] + +/-- State `i` of `legendre21` is state `embed25 i` of `leg25`. -/ +def embed25 (q : Fin 21) : Fin 25 := + ([14, 0, 3, 4, 6, 7, 9, 11, 12, 13, 15, 16, 20, 22, 23, 24, 1, 2, 5, 8, 10] : + List (Fin 25)).getD q.val 0 + +theorem transition_embed25 (q : Fin 21) (a : Fin 2) : + leg25.transition (embed25 q) a = + (legendre21.transition q a).map fun t => (t.1, t.2.1, embed25 t.2.2) := by + revert q a; decide + +theorem step_embed25 (q : Fin 21) (T : Tape (Fin 2)) : + step leg25 ⟨embed25 q, T⟩ = + (step legendre21 ⟨q, T⟩).map fun c => ⟨embed25 c.state, c.tape⟩ := by + simp only [step, transition_embed25, Option.map_map] + rcases legendre21.transition q T.head with _ | ⟨a, d, q'⟩ <;> rfl + +theorem respects_embed25 : + Respects (step legendre21) (step leg25) + fun c₁ c₂ => c₂ = ⟨embed25 c₁.state, c₁.tape⟩ := by + intro c₁ c₂ h + subst h + obtain ⟨q, T⟩ := c₁ + rcases e : step legendre21 ⟨q, T⟩ with _ | c + · simpa [step_embed25] using e + · exact ⟨⟨embed25 c.state, c.tape⟩, rfl, + Relation.TransGen.single (by simp [step_embed25, e])⟩ + +/-- Halting of `legendre21` is halting of `leg25` from state `14` (`q14`, the start state). -/ +theorem halts_iff_leg25 : + ConjectureMachines.Halts legendre21 ↔ (eval (step leg25) ⟨14, default⟩).Dom := + (tr_eval_dom' respects_embed25 rfl).symm + +/-! +## The primality test in `leg25` + +The test is the one of `Goldbach21.edited`. Inside the test three things differ: +* `q21` is merged into `q9`: `(q20, 0) = 1 L q9`, and `q9` reading `0` reaches `q22` through + `(q0, 1) = 1 L q22` (three steps instead of one, same tape); +* the entry is `(q16, 0) = 1 R q3` instead of `(q0, 1) = 1 R q3`; +* the composite exit is `(q15, 0) = 1 L A1`: `A1` runs right over the restored block and + `(A1, 0) = 0 R q6` leaves `q6` on the cell right of the separator. + +Three more cells of the test states differ from `edited`, `(q3, 0)`, `(q6, 0)` and `(q7, 0)`; +they are read only at the exits of the test and by the interval logic. + +Used unchanged from `Goldbach21`: the step and scan lemmas and the machine-generic pass lemmas +`nSteps_pass_11_to_13` and `nSteps_pass_13_zero_to_15`. The other lemmas of this section +follow the `_edit`, `cfg6E` and `cfg11E` lemmas of `Goldbach21` line by line (`pass_15_bsucc_to_6` +and `sim6_accept` word for word), stated for `leg25` and for arbitrary tape on both sides of the +block. +-/ + +theorem pass_13_one_to_9 (m : ℕ) (L R : ListBlank (Fin 2)) : + nSteps leg25 (1 + ((m + 1) + 1)) + ⟨13, Tape.mk' (ListBlank.append (List.replicate (m + 1) 1) (L.cons 0)) (R.cons 1)⟩ = + some ⟨9, Tape.mkL L ((ListBlank.append (List.replicate (m + 1) 1) (R.cons 0)).cons 1)⟩ := by + refine nSteps_bind_eq (step_one (step_mk'_left (b := 0) (q' := 20) rfl _ _)) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 20) (a := 1) (b := 1) rfl (m + 1) _ _) ?_ + exact step_one (step_mkL_left (b := 1) (q' := 9) rfl _ _) + +theorem pass_9_b0_to_11 (A : ℕ) (L_base R : ListBlank (Fin 2)) : + nSteps leg25 (3 + (A + (2 + A))) + ⟨9, Tape.mkL (counterTape A 0 L_base) (R.cons 1)⟩ = + some ⟨11, Tape.mk' (counterTape 0 A L_base) (R.cons 1)⟩ := by + unfold counterTape + simp only [List.replicate_zero, ListBlank.append] + refine nSteps_bind_eq + (step_nSteps (step_mkL_right (b := 1) (q' := 0) rfl _ _) + (step_nSteps (step_mk'_left (b := 1) (q' := 22) rfl _ _) + (step_one (step_mkL_left (b := 0) (q' := 22) rfl _ _)))) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 22) (a := 1) (b := 0) rfl A _ _) ?_ + rw [append_replicate_cons] + refine nSteps_bind_eq + (step_nSteps (step_mkL_right (b := 0) (q' := 0) rfl _ _) + (step_one (by + rw [List.replicate_succ, ListBlank.append] + exact step_mk'_right (b := 0) (q' := 11) rfl _ _))) ?_ + exact nSteps_mk'_right_scan (q := 11) (a := 0) (b := 1) rfl A _ _ + +theorem pass_9_bsucc_to_11 (A b : ℕ) (L_base R : ListBlank (Fin 2)) : + nSteps leg25 (1 + (b + (2 + b))) + ⟨9, Tape.mkL (counterTape A (b + 1) L_base) R⟩ = + some ⟨11, Tape.mk' (counterTape (A + 1) b L_base) R⟩ := by + unfold counterTape + rw [List.replicate_succ, ListBlank.append] + refine nSteps_bind_eq (step_one (step_mkL_left (b := 0) (q' := 9) rfl _ _)) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 9) (a := 1) (b := 0) rfl b _ _) ?_ + rw [append_replicate_cons] + refine nSteps_bind_eq + (step_nSteps (step_mkL_right (b := 1) (q' := 0) rfl _ _) + (step_one (by + rw [List.replicate_succ, ListBlank.append] + exact step_mk'_right (b := 0) (q' := 11) rfl _ _))) ?_ + exact nSteps_mk'_right_scan (q := 11) (a := 0) (b := 1) rfl b _ _ + +theorem pass_11_b0 (A m : ℕ) (L_base R : ListBlank (Fin 2)) : + nSteps leg25 ((1 + (m + 1)) + ((1 + ((m + 1) + 1)) + (3 + (A + (2 + A))))) + ⟨11, Tape.mk' (counterTape A 0 L_base) + ((ListBlank.append (List.replicate m 1) ((R.cons 1).cons 0)).cons 1)⟩ = + some ⟨11, Tape.mk' (counterTape 0 A L_base) + ((ListBlank.append (List.replicate (m + 1) 1) (R.cons 0)).cons 1)⟩ := + nSteps_bind_eq (nSteps_pass_11_to_13 rfl rfl rfl m _ _) + (nSteps_bind_eq (pass_13_one_to_9 m _ _) + (pass_9_b0_to_11 A _ _)) + +theorem pass_11_bsucc (A b m : ℕ) (L_base R : ListBlank (Fin 2)) : + nSteps leg25 ((1 + (m + 1)) + ((1 + ((m + 1) + 1)) + (1 + (b + (2 + b))))) + ⟨11, Tape.mk' (counterTape A (b + 1) L_base) + ((ListBlank.append (List.replicate m 1) ((R.cons 1).cons 0)).cons 1)⟩ = + some ⟨11, Tape.mk' (counterTape (A + 1) b L_base) + ((ListBlank.append (List.replicate (m + 1) 1) (R.cons 0)).cons 1)⟩ := + nSteps_bind_eq (nSteps_pass_11_to_13 rfl rfl rfl m _ _) + (nSteps_bind_eq (pass_13_one_to_9 m _ _) + (pass_9_bsucc_to_11 A b _ _)) + +theorem pass_15_bsucc_to_6 (A b : ℕ) (L_base R : ListBlank (Fin 2)) : + nSteps leg25 (1 + (b + (1 + (b + 3)))) + ⟨15, Tape.mkL (counterTape A (b + 1) L_base) ((R.cons 1).cons 1)⟩ = + some ⟨6, Tape.mk' + ((ListBlank.append (List.replicate (A + b + 3) 1) (L_base.cons 0)).cons 1) R⟩ := by + unfold counterTape + rw [List.replicate_succ, ListBlank.append] + refine nSteps_bind_eq (step_one (step_mkL_left (b := 0) (q' := 23) rfl _ _)) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 23) (a := 1) (b := 1) rfl b _ _) ?_ + refine nSteps_bind_eq (step_one (step_mkL_right (b := 1) (q' := 24) rfl _ _)) ?_ + refine nSteps_bind_eq (nSteps_mk'_right_scan (q := 24) (a := 1) (b := 1) rfl b _ _) ?_ + have h_cnt : ListBlank.append (List.replicate b 1) + ((ListBlank.append (List.replicate A 1) (L_base.cons 0)).cons 1) = + ListBlank.append (List.replicate (A + b + 1) 1) (L_base.cons 0) := by + rw [append_replicate_cons, append_replicate_add] + have : b + 1 + A = A + b + 1 := by omega + rw [this] + rw [h_cnt] + refine step_nSteps (step_mk'_right (b := 1) (q' := 3) rfl _ _) ?_ + refine step_nSteps (step_mk'_right (b := 1) (q' := 4) rfl _ _) ?_ + exact step_one (step_mk'_right (b := 1) (q' := 6) rfl _ _) + +theorem pass_11_to_6 (A b m : ℕ) (L_base R_end : ListBlank (Fin 2)) : + nSteps leg25 ((1 + (m + 1)) + ((1 + ((m + 1) + 1)) + (1 + (b + (1 + (b + 3)))))) + ⟨11, Tape.mk' (counterTape A (b + 1) L_base) + ((ListBlank.append (List.replicate m 1) ((R_end.cons 0).cons 0)).cons 1)⟩ = + some ⟨6, Tape.mk' ((ListBlank.append (List.replicate (A + b + 3) 1) (L_base.cons 0)).cons 1) + (ListBlank.append (List.replicate m 1) (R_end.cons 0))⟩ := + nSteps_bind_eq (nSteps_pass_11_to_13 rfl rfl rfl m _ _) + (nSteps_bind_eq (nSteps_pass_13_zero_to_15 rfl rfl rfl m _ _) + (pass_15_bsucc_to_6 A b _ _)) + +/-- Composite exit. `q15` reads the `0` of the counter with `A + 1 ≥ 1` ones of the block on +its left, so `A1` starts on a `1`; it leaves `q6` on the first cell right of the separator. -/ +theorem pass_15_b0_to_exit (A m : ℕ) (L_base R_end : ListBlank (Fin 2)) : + nSteps leg25 (2 + ((m + 3) + 1)) + ⟨15, Tape.mkL (counterTape (A + 1) 0 L_base) + ((ListBlank.append (List.replicate (m + 1) 1) (R_end.cons 0)).cons 1)⟩ = + some ⟨6, Tape.mk' + ((ListBlank.append (List.replicate (A + m + 4) 1) (L_base.cons 0)).cons 0) R_end⟩ := by + unfold counterTape + simp only [List.replicate_zero, ListBlank.append] + have h1 : ListBlank.append (List.replicate (A + 1) 1) (L_base.cons 0) = + (ListBlank.append (List.replicate A 1) (L_base.cons 0)).cons 1 := rfl + rw [h1] + refine nSteps_bind_eq + (step_nSteps (step_mkL_left (b := 1) (q' := 1) rfl _ _) + (step_one (step_mkL_right (b := 1) (q' := 1) rfl _ _))) ?_ + have h2 : ((ListBlank.append (List.replicate (m + 1) 1) (R_end.cons 0)).cons 1).cons 1 = + ListBlank.append (List.replicate (m + 3) 1) (R_end.cons 0) := rfl + rw [h2] + refine nSteps_bind_eq (nSteps_mk'_right_scan (q := 1) (a := 1) (b := 1) rfl (m + 3) _ _) ?_ + have h3 : ListBlank.append (List.replicate (m + 3) 1) + ((ListBlank.append (List.replicate A 1) (L_base.cons 0)).cons 1) = + ListBlank.append (List.replicate (A + m + 4) 1) (L_base.cons 0) := by + rw [append_replicate_cons, append_replicate_add] + have : m + 3 + 1 + A = A + m + 4 := by omega + rw [this] + rw [h3] + exact step_one (step_mk'_right (b := 0) (q' := 6) rfl _ _) + +theorem pass_11_to_exit (A m : ℕ) (L_base R_end : ListBlank (Fin 2)) : + nSteps leg25 ((1 + (m + 1)) + ((1 + ((m + 1) + 1)) + (2 + ((m + 3) + 1)))) + ⟨11, Tape.mk' (counterTape (A + 1) 0 L_base) + ((ListBlank.append (List.replicate m 1) ((R_end.cons 0).cons 0)).cons 1)⟩ = + some ⟨6, Tape.mk' + ((ListBlank.append (List.replicate (A + m + 4) 1) (L_base.cons 0)).cons 0) R_end⟩ := + nSteps_bind_eq (nSteps_pass_11_to_13 rfl rfl rfl m _ _) + (nSteps_bind_eq (nSteps_pass_13_zero_to_15 rfl rfl rfl m _ _) + (pass_15_b0_to_exit A m _ _)) + +theorem sim6_d (k : ℕ) (L_base R_rest : ListBlank (Fin 2)) : + let L_cnt := ListBlank.append (List.replicate (k + 2) 1) (L_base.cons 0) + let R_mid := R_rest.cons 0 + nSteps leg25 (2 + ((k + 2) + (2 + ((k + 1) + (6 + (k + 1)))))) + ⟨6, Tape.mk' (L_cnt.cons 1) ((R_rest.cons 1).cons 1)⟩ = + some ⟨0, Tape.mk' ((L_base.cons 0).cons 1) + (ListBlank.append (0 :: (List.replicate k 0 ++ [1])) (R_mid.cons 1))⟩ := by + dsimp only + refine nSteps_bind_eq + (step_nSteps (step_mk'_left (b := 0) (q' := 7) rfl _ _) + (step_one (step_mkL_left (b := 1) (q' := 22) rfl _ _))) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 22) (a := 1) (b := 0) rfl (k + 2) _ _) ?_ + rw [List.replicate_succ, ListBlank.append] + refine nSteps_bind_eq + (step_nSteps (step_mkL_right (b := 0) (q' := 0) rfl _ _) + (step_one (step_mk'_right (b := 0) (q' := 11) rfl _ _))) ?_ + refine nSteps_bind_eq (nSteps_mk'_right_scan (q := 11) (a := 0) (b := 1) rfl (k + 1) _ _) ?_ + rw [List.replicate_succ, ListBlank.append] + refine nSteps_bind_eq + (step_nSteps (step_mk'_right (b := 0) (q' := 12) rfl _ _) + (step_nSteps (step_mk'_right (b := 1) (q' := 13) rfl _ _) + (step_nSteps (step_mk'_left (b := 0) (q' := 20) rfl _ _) + (step_nSteps (step_mkL_left (b := 1) (q' := 20) rfl _ _) + (step_nSteps (step_mkL_left (b := 1) (q' := 9) rfl _ _) + (step_one (step_mkL_left (b := 0) (q' := 9) rfl _ _))))))) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 9) (a := 1) (b := 0) rfl k _ _) ?_ + rw [append_replicate_cons, List.replicate_succ, ListBlank.append] + apply step_one + simpa [ListBlank.append_assoc] using + step_mkL_right (M := leg25) (q := 9) (q' := 0) (a := 0) (b := 1) rfl + (L_base.cons 0) (ListBlank.append (0 :: List.replicate k 0) (((R_rest.cons 0).cons 1).cons 1)) + +theorem sim6_accept (k : ℕ) (L_base R_end : ListBlank (Fin 2)) : + let L_cnt := ListBlank.append (List.replicate (k + 2) 1) (L_base.cons 0) + nSteps leg25 (2 + ((k + 2) + (2 + ((k + 1) + (6 + (k + (1 + (k + 3)))))))) + ⟨6, Tape.mk' (L_cnt.cons 1) ((R_end.cons 0).cons 1)⟩ = + some ⟨6, Tape.mk' ((L_cnt.cons 1).cons 1) (R_end.cons 0)⟩ := by + dsimp only + refine nSteps_bind_eq + (step_nSteps (step_mk'_left (b := 0) (q' := 7) rfl _ _) + (step_one (step_mkL_left (b := 1) (q' := 22) rfl _ _))) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 22) (a := 1) (b := 0) rfl (k + 2) _ _) ?_ + rw [List.replicate_succ, ListBlank.append] + refine nSteps_bind_eq + (step_nSteps (step_mkL_right (b := 0) (q' := 0) rfl _ _) + (step_one (step_mk'_right (b := 0) (q' := 11) rfl _ _))) ?_ + refine nSteps_bind_eq (nSteps_mk'_right_scan (q := 11) (a := 0) (b := 1) rfl (k + 1) _ _) ?_ + rw [List.replicate_succ, ListBlank.append] + refine nSteps_bind_eq + (step_nSteps (step_mk'_right (b := 0) (q' := 12) rfl _ _) + (step_nSteps (step_mk'_right (b := 1) (q' := 13) rfl _ _) + (step_nSteps (step_mk'_left (b := 0) (q' := 14) rfl _ _) + (step_nSteps (step_mkL_left (b := 1) (q' := 14) rfl _ _) + (step_nSteps (step_mkL_left (b := 1) (q' := 15) rfl _ _) + (step_one (step_mkL_left (b := 0) (q' := 23) rfl _ _))))))) ?_ + refine nSteps_bind_eq (nSteps_mkL_left_scan (q := 23) (a := 1) (b := 1) rfl k _ _) ?_ + refine nSteps_bind_eq (step_one (step_mkL_right (b := 1) (q' := 24) rfl _ _)) ?_ + refine nSteps_bind_eq (nSteps_mk'_right_scan (q := 24) (a := 1) (b := 1) rfl k _ _) ?_ + rw [append_replicate_cons] + refine step_nSteps (step_mk'_right (b := 1) (q' := 3) rfl _ _) ?_ + refine step_nSteps (step_mk'_right (b := 1) (q' := 4) rfl _ _) ?_ + exact step_one (step_mk'_right (b := 1) (q' := 6) rfl _ _) + +/-- Inside the test of `k + 3 + r`: `q6` on the block, `k + 2` is the next divisor to try, +`r + 1` cells of the block are right of the head. `L.cons 0` is the tape left of the block, +`R.cons 0` the tape right of it. -/ +def tcfg6 (L R : ListBlank (Fin 2)) (k r : ℕ) : Cfg 25 2 := + ⟨6, Tape.mk' ((ListBlank.append (List.replicate (k + 2) 1) (L.cons 0)).cons 1) + (ListBlank.append (List.replicate (r + 1) 1) (R.cons 0))⟩ + +def tcfg11 (L R : ListBlank (Fin 2)) (A B m r : ℕ) : Cfg 25 2 := + ⟨11, Tape.mk' (counterTape A B L) + ((ListBlank.append (List.replicate (m + 1) 1) + ((ListBlank.append (List.replicate r 1) (R.cons 0)).cons 0)).cons 1)⟩ + +/-- Exit of the test of `p` (a block of `p + 1` ones, restored). Prime: `q6` on the separator. +Composite: `q6` on the first cell right of the separator. -/ +def testExit (L R : ListBlank (Fin 2)) (is_prime : Bool) (p : ℕ) : Cfg 25 2 := + if is_prime then + ⟨6, Tape.mk' (ListBlank.append (List.replicate (p + 1) 1) (L.cons 0)) (R.cons 0)⟩ + else + ⟨6, Tape.mk' ((ListBlank.append (List.replicate (p + 1) 1) (L.cons 0)).cons 0) R⟩ + +theorem tcfg11_step_b0 (L R : ListBlank (Fin 2)) (A m r' : ℕ) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (tcfg11 L R A 0 m (r' + 1)) = some (tcfg11 L R 0 A (m + 1) r') := by + have h_rep : ListBlank.append (List.replicate (r' + 1) 1) (R.cons 0) = + (ListBlank.append (List.replicate r' 1) (R.cons 0)).cons 1 := rfl + unfold tcfg11 + rw [h_rep] + have h := pass_11_b0 A (m + 1) L (ListBlank.append (List.replicate r' 1) (R.cons 0)) + exact ⟨_, by omega, h⟩ + +theorem tcfg11_step_bsucc (L R : ListBlank (Fin 2)) (A b m r' : ℕ) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (tcfg11 L R A (b + 1) m (r' + 1)) = + some (tcfg11 L R (A + 1) b (m + 1) r') := by + have h_rep : ListBlank.append (List.replicate (r' + 1) 1) (R.cons 0) = + (ListBlank.append (List.replicate r' 1) (R.cons 0)).cons 1 := rfl + unfold tcfg11 + rw [h_rep] + have h := pass_11_bsucc A b (m + 1) L (ListBlank.append (List.replicate r' 1) (R.cons 0)) + exact ⟨_, by omega, h⟩ + +theorem tcfg11_drain (L R : ListBlank (Fin 2)) (k r A B m : ℕ) + (hAB : A + B = k + 1) (hdvd : (k + 2) ∣ B + m + 2) : + ∃ A' B', A' + B' = k + 1 ∧ (k + 2) ∣ B' + (m + r) + 2 ∧ + ∃ s, nSteps leg25 s (tcfg11 L R A B m r) = some (tcfg11 L R A' B' (m + r) 0) := by + induction r generalizing A B m with + | zero => + exact ⟨A, B, hAB, by simpa using hdvd, 0, rfl⟩ + | succ r' ih => + cases B with + | zero => + obtain ⟨s₁, _, hs₁⟩ := tcfg11_step_b0 L R A m r' + have hdvd' : (k + 2) ∣ A + (m + 1) + 2 := by + have h_eq : A + (m + 1) + 2 = (0 + m + 2) + (k + 2) := by omega + rw [h_eq] + exact Nat.dvd_add_self_right.mpr hdvd + obtain ⟨A', B', hAB', hdvd'', s₂, hs₂⟩ := ih 0 A (m + 1) (by omega) hdvd' + have h_mr : m + 1 + r' = m + (r' + 1) := by omega + rw [h_mr] at hdvd'' hs₂ + exact ⟨A', B', hAB', hdvd'', s₁ + s₂, nSteps_bind_eq hs₁ hs₂⟩ + | succ b => + obtain ⟨s₁, _, hs₁⟩ := tcfg11_step_bsucc L R A b m r' + have hdvd' : (k + 2) ∣ b + (m + 1) + 2 := by + have h_eq : b + (m + 1) + 2 = b + 1 + m + 2 := by omega + rwa [h_eq] + obtain ⟨A', B', hAB', hdvd'', s₂, hs₂⟩ := ih (A + 1) b (m + 1) (by omega) hdvd' + have h_mr : m + 1 + r' = m + (r' + 1) := by omega + rw [h_mr] at hdvd'' hs₂ + exact ⟨A', B', hAB', hdvd'', s₁ + s₂, nSteps_bind_eq hs₁ hs₂⟩ + +theorem tcfg6_step_enter (L R : ListBlank (Fin 2)) (k r' : ℕ) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (tcfg6 L R k (r' + 1)) = some (tcfg11 L R 1 k 0 r') := by + have h_rep : ListBlank.append (List.replicate (r' + 1 + 1) 1) (R.cons 0) = + ((ListBlank.append (List.replicate r' 1) (R.cons 0)).cons 1).cons 1 := rfl + unfold tcfg6 tcfg11 + rw [h_rep] + have h1 := sim6_d k L (ListBlank.append (List.replicate r' 1) (R.cons 0)) + have h0_to_11 (L_b R_m : ListBlank (Fin 2)) : + nSteps leg25 (1 + k) + ⟨0, Tape.mk' ((L_b.cons 0).cons 1) + (ListBlank.append (0 :: (List.replicate k 0 ++ [1])) R_m)⟩ = + some ⟨11, Tape.mk' (counterTape 1 k L_b) (R_m.cons 1)⟩ := by + rw [ListBlank.append, ListBlank.append_assoc, ListBlank.append, ListBlank.append] + refine nSteps_bind_eq (step_one + (step_mk'_right (M := leg25) (q := 0) (q' := 11) (a := 0) (b := 0) rfl _ _)) ?_ + exact nSteps_mk'_right_scan (M := leg25) (q := 11) (a := 0) (b := 1) rfl k _ _ + have h := nSteps_bind_eq h1 (h0_to_11 L _) + exact ⟨_, by omega, h⟩ + +theorem tcfg6_pass_succ_dvd (L R : ListBlank (Fin 2)) (k r' : ℕ) + (hdvd : (k + 2) ∣ (k + 4 + r')) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (tcfg6 L R k (r' + 1)) = some (testExit L R false (k + 4 + r')) := by + obtain ⟨s₀, _, hs₀⟩ := tcfg6_step_enter L R k r' + obtain ⟨A', B', hAB', hdvd', s₁, hs₁⟩ := + tcfg11_drain L R k r' 1 k 0 (by omega) (by simp) + simp only [Nat.zero_add] at hdvd' hs₁ + have hB0 : B' = 0 := by + have h_eq1 : k + 4 + r' = (r' + 2) + (k + 2) := by omega + have h_eq2 : B' + r' + 2 = B' + (r' + 2) := by omega + rw [h_eq1, Nat.dvd_add_self_right] at hdvd + rw [h_eq2] at hdvd' + exact Nat.eq_zero_of_dvd_of_lt ((Nat.dvd_add_iff_left hdvd).mpr hdvd') (by omega) + subst hB0 + have hA : A' = k + 1 := by omega + subst hA + have h_fin := pass_11_to_exit k (r' + 1) L R + have h_p : k + (r' + 1) + 4 = (k + 4 + r') + 1 := by omega + have h_fin' : + nSteps leg25 ((1 + (r' + 1 + 1)) + ((1 + ((r' + 1 + 1) + 1)) + (2 + ((r' + 1 + 3) + 1)))) + (tcfg11 L R (k + 1) 0 r' 0) = some (testExit L R false (k + 4 + r')) := by + unfold tcfg11 testExit + simpa [List.replicate_zero, ListBlank.append, h_p] using h_fin + exact ⟨_, by omega, nSteps_bind_eq hs₀ (nSteps_bind_eq hs₁ h_fin')⟩ + +theorem tcfg6_pass_succ_not_dvd (L R : ListBlank (Fin 2)) (k r' : ℕ) + (hdvd : ¬ (k + 2) ∣ (k + 4 + r')) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (tcfg6 L R k (r' + 1)) = some (tcfg6 L R (k + 1) r') := by + obtain ⟨s₀, _, hs₀⟩ := tcfg6_step_enter L R k r' + obtain ⟨A', B', hAB', hdvd', s₁, hs₁⟩ := + tcfg11_drain L R k r' 1 k 0 (by omega) (by simp) + simp only [Nat.zero_add] at hdvd' hs₁ + cases B' with + | zero => + exfalso + apply hdvd + have h_eq1 : k + 4 + r' = (r' + 2) + (k + 2) := by omega + rw [h_eq1, Nat.dvd_add_self_right] + simpa using hdvd' + | succ b => + have h_fin := pass_11_to_6 A' b (r' + 1) L R + have h_k : A' + b + 3 = (k + 1) + 2 := by omega + have h_fin' : + nSteps leg25 ((1 + (r' + 1 + 1)) + ((1 + ((r' + 1 + 1) + 1)) + (1 + (b + (1 + (b + 3)))))) + (tcfg11 L R A' (b + 1) r' 0) = some (tcfg6 L R (k + 1) r') := by + unfold tcfg11 tcfg6 + simpa [List.replicate_zero, ListBlank.append, h_k] using h_fin + exact ⟨_, by omega, nSteps_bind_eq hs₀ (nSteps_bind_eq hs₁ h_fin')⟩ + +theorem tcfg6_eval (L R : ListBlank (Fin 2)) (k r : ℕ) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (tcfg6 L R k r) = + some (testExit L R (decide (NoFactorFrom k (k + 3 + r))) (k + 3 + r)) := by + induction r generalizing k with + | zero => + have h_nf : NoFactorFrom k (k + 3 + 0) := by + intro d hd1 hd2 hdvd + have hd_eq : d = k + 2 := by omega + subst hd_eq + have h1 : (k + 2) ∣ 1 := by + have h_add : (k + 2) ∣ (k + 2) + 1 := hdvd + exact (Nat.dvd_add_right (Nat.dvd_refl (k + 2))).mp h_add + have := Nat.le_of_dvd (by omega) h1 + omega + rw [decide_eq_true h_nf] + have h1 := sim6_accept k L R + have h_cnt : + ((ListBlank.append (List.replicate (k + 2) 1) (L.cons 0)).cons 1).cons 1 = + ListBlank.append (List.replicate (k + 3 + 1) 1) (L.cons 0) := rfl + refine ⟨2 + ((k + 2) + (2 + ((k + 1) + (6 + (k + (1 + (k + 3))))))), by omega, ?_⟩ + unfold tcfg6 testExit + simpa [Nat.add_zero, List.replicate_zero, ListBlank.append, h_cnt] using h1 + | succ r' ih => + have h_arith : k + 3 + (r' + 1) = k + 4 + r' := by omega + rw [h_arith] + by_cases hdvd : (k + 2) ∣ (k + 4 + r') + · have h_nf : ¬ NoFactorFrom k (k + 4 + r') := fun h => h (k + 2) (by omega) (by omega) hdvd + rw [decide_eq_false h_nf] + exact tcfg6_pass_succ_dvd L R k r' hdvd + · obtain ⟨s₁, _, hs₁⟩ := tcfg6_pass_succ_not_dvd L R k r' hdvd + obtain ⟨s₂, _, hs₂⟩ := ih (k + 1) + have h_arith2 : k + 1 + 3 + r' = k + 4 + r' := by omega + rw [h_arith2] at hs₂ + have h_iff : NoFactorFrom k (k + 4 + r') ↔ NoFactorFrom (k + 1) (k + 4 + r') := by + constructor + · intro h d hd1 hd2 + exact h d (by omega) hd2 + · intro h d hd1 hd2 + rcases Nat.eq_or_lt_of_le hd1 with rfl | hd_gt + · exact hdvd + · exact h d (by omega) hd2 + have h_dec : decide (NoFactorFrom k (k + 4 + r')) = + decide (NoFactorFrom (k + 1) (k + 4 + r')) := by + simp [h_iff] + rw [h_dec] + exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + +/-- The test event: `q16` reading the `0` left of a block of `t` ones. `(q16, 0) = 1 R q3` +makes the block `t + 1` long and enters the test of `t`. -/ +def testCfg (L R : ListBlank (Fin 2)) (t : ℕ) : Cfg 25 2 := + ⟨16, Tape.mkL ((L.cons 0).cons 0) (ListBlank.append (List.replicate t 1) (R.cons 0))⟩ + +theorem enter_two (L R : ListBlank (Fin 2)) : + nSteps leg25 3 ⟨16, Tape.mkL (L.cons 0) (((R.cons 0).cons 1).cons 1)⟩ = + some ⟨6, Tape.mk' (((L.cons 1).cons 1).cons 1) (R.cons 0)⟩ := + step_nSteps (step_mkL_right (b := 1) (q' := 3) rfl L (((R.cons 0).cons 1).cons 1)) + (step_nSteps (step_mk'_right (b := 1) (q' := 4) rfl (L.cons 1) ((R.cons 0).cons 1)) + (step_one (step_mk'_right (b := 1) (q' := 6) rfl ((L.cons 1).cons 1) (R.cons 0)))) + +theorem enter_ge3 (L R : ListBlank (Fin 2)) : + nSteps leg25 3 ⟨16, Tape.mkL (L.cons 0) (((R.cons 1).cons 1).cons 1)⟩ = + some ⟨6, Tape.mk' (((L.cons 1).cons 1).cons 1) (R.cons 1)⟩ := + step_nSteps (step_mkL_right (b := 1) (q' := 3) rfl L (((R.cons 1).cons 1).cons 1)) + (step_nSteps (step_mk'_right (b := 1) (q' := 4) rfl (L.cons 1) ((R.cons 1).cons 1)) + (step_one (step_mk'_right (b := 1) (q' := 6) rfl ((L.cons 1).cons 1) (R.cons 1)))) + +/-- **The test.** From the test event of `t ≥ 2` the machine reaches the exit that says +whether `t` is prime, with the block (now `t + 1` ones) restored and `L`, `R` untouched. -/ +theorem test_eval (L R : ListBlank (Fin 2)) (t : ℕ) (ht : 2 ≤ t) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (testCfg L R t) = some (testExit L R (decide (IsPrime t)) t) := by + rcases Nat.eq_or_lt_of_le ht with rfl | ht3 + · rw [decide_eq_true isPrime_two] + have h2 := enter_two (L.cons 0) R + refine ⟨3, by omega, ?_⟩ + unfold testCfg testExit + exact h2 + · obtain ⟨r0, rfl⟩ : ∃ r0, t = r0 + 3 := ⟨t - 3, by omega⟩ + have h_enter : nSteps leg25 3 (testCfg L R (r0 + 3)) = some (tcfg6 L R 0 r0) := + enter_ge3 (L.cons 0) (ListBlank.append (List.replicate r0 1) (R.cons 0)) + obtain ⟨s₂, _, hs₂⟩ := tcfg6_eval L R 0 r0 + have h_prime_iff : IsPrime (r0 + 3) ↔ NoFactorFrom 0 (0 + 3 + r0) := by + unfold IsPrime + have h_eq : 0 + 3 + r0 = r0 + 3 := by omega + rw [h_eq] + exact ⟨fun h => h.2, fun h => ⟨by omega, h⟩⟩ + have h_dec : decide (IsPrime (r0 + 3)) = decide (NoFactorFrom 0 (0 + 3 + r0)) := by + simp [h_prime_iff] + have h_eq : 0 + 3 + r0 = r0 + 3 := by omega + rw [h_dec] + rw [h_eq] at hs₂ ⊢ + exact ⟨3 + s₂, by omega, nSteps_bind_eq h_enter hs₂⟩ + +/-! +## Interval logic + +Right of the block: the separator `0`, the flag cell `f`, and the walker area `walkerTape h r` +(`h` ones, a hole, `r` ones; the blank beyond `walkerTape h 0` is the hole). After a test `B` runs +right to the hole and fills it, `C` opens a hole one cell further left, `Z1` runs back. + +* composite, flag clear, hole not at the left end: next number; +* composite, flag clear, hole at the left end: `C` reads the clear flag, `X` reads the + separator: **halt**; +* prime, flag clear: `B` sets the flag, `C` and `X` move the separator one cell left (the block + loses a cell, the walker area gains one), and the same number is tested once more; +* flag set (prime or composite; a composite makes the four-step detour `q6 q7 C X` first): + next number; when the hole is at the left end it moves into the flag cell, which clears the + flag and leaves the walker area full: the next interval starts. +-/ + +local notation:max "ones(" n ", " L ")" => ListBlank.append (List.replicate n (1 : Fin 2)) L + +theorem step_mkL_none {M : Machine 25 2} {q : Fin 25} {a : Fin 2} + (h : M.transition q a = none) (L R : ListBlank (Fin 2)) : + step M ⟨q, Tape.mkL (L.cons a) R⟩ = none := by + simp [step, h, Tape.mkL] + +/-- `B` runs right over `h + 1` ones and fills the hole, `C` opens a hole one cell to the left, +`Z1` runs back over the ones and stops on the cell left of them. -/ +theorem walkB (h : ℕ) (Lf Rr : ListBlank (Fin 2)) : + nSteps leg25 ((h + 1) + (2 + h)) ⟨2, Tape.mk' Lf ones(h + 1, Rr.cons 0)⟩ = + some ⟨8, Tape.mkL Lf ones(h, (Rr.cons 1).cons 0)⟩ := by + have h1 : nSteps leg25 (h + 1) ⟨2, Tape.mk' Lf ones(h + 1, Rr.cons 0)⟩ = + some ⟨2, Tape.mk' ones(h + 1, Lf) (Rr.cons 0)⟩ := + nSteps_mk'_right_scan (q := 2) (a := 1) (b := 1) rfl (h + 1) Lf (Rr.cons 0) + have h2 : nSteps leg25 2 ⟨2, Tape.mk' (ones(h, Lf).cons 1) (Rr.cons 0)⟩ = + some ⟨8, Tape.mkL ones(h, Lf) ((Rr.cons 1).cons 0)⟩ := + step_nSteps (step_mk'_left (b := 1) (q' := 5) rfl _ _) + (step_one (step_mkL_left (b := 0) (q' := 8) rfl _ _)) + have h3 : nSteps leg25 h ⟨8, Tape.mkL ones(h, Lf) ((Rr.cons 1).cons 0)⟩ = + some ⟨8, Tape.mkL Lf ones(h, (Rr.cons 1).cons 0)⟩ := + nSteps_mkL_left_scan (q := 8) (a := 1) (b := 1) rfl h Lf ((Rr.cons 1).cons 0) + exact nSteps_bind_eq h1 (nSteps_bind_eq h2 h3) + +/-- Way back when `Z1` stops on the separator: `q3` reads the last cell of the block, `q4` the +separator, `q16` runs left over the block of `n + 1` ones. -/ +theorem ret_q4 (n : ℕ) (L X : ListBlank (Fin 2)) : + nSteps leg25 (3 + (n + 1)) ⟨8, Tape.mkL (ones(n + 1, L.cons 0).cons 0) X⟩ = + some ⟨16, Tape.mkL (L.cons 0) ones(n + 1, X.cons 0)⟩ := by + have h1 : nSteps leg25 3 ⟨8, Tape.mkL ((ones(n, L.cons 0).cons 1).cons 0) X⟩ = + some ⟨16, Tape.mkL (ones(n, L.cons 0).cons 1) (X.cons 0)⟩ := + step_nSteps (step_mkL_left (b := 0) (q' := 3) rfl _ _) + (step_nSteps (step_mkL_right (b := 1) (q' := 4) rfl _ _) + (step_one (step_mk'_left (b := 0) (q' := 16) rfl _ _))) + have h2 : nSteps leg25 (n + 1) ⟨16, Tape.mkL ones(n + 1, L.cons 0) (X.cons 0)⟩ = + some ⟨16, Tape.mkL (L.cons 0) ones(n + 1, X.cons 0)⟩ := + nSteps_mkL_left_scan (q := 16) (a := 1) (b := 1) rfl (n + 1) (L.cons 0) (X.cons 0) + exact nSteps_bind_eq h1 h2 + +/-- Way back when `Z1` stops on the clear flag: `q3` reads the separator, `q16` runs left over +the block of `m` ones. -/ +theorem ret_q3 (m : ℕ) (Lz X : ListBlank (Fin 2)) : + nSteps leg25 (2 + m) ⟨8, Tape.mkL ((ones(m, Lz).cons 0).cons 0) X⟩ = + some ⟨16, Tape.mkL Lz ones(m, (X.cons 0).cons 0)⟩ := by + have h1 : nSteps leg25 2 ⟨8, Tape.mkL ((ones(m, Lz).cons 0).cons 0) X⟩ = + some ⟨16, Tape.mkL ones(m, Lz) ((X.cons 0).cons 0)⟩ := + step_nSteps (step_mkL_left (b := 0) (q' := 3) rfl _ _) + (step_one (step_mkL_left (b := 0) (q' := 16) rfl _ _)) + exact nSteps_bind_eq h1 + (nSteps_mkL_left_scan (q := 16) (a := 1) (b := 1) rfl m Lz ((X.cons 0).cons 0)) + +/-- The detour of a composite exit with the flag set: `q6` clears the flag, `q7` marks the +separator, `C` and `X` put both back; `B` is then on the set flag. -/ +theorem detour (Lm Y : ListBlank (Fin 2)) : + nSteps leg25 4 ⟨6, Tape.mk' (Lm.cons 0) (Y.cons 1)⟩ = + some ⟨2, Tape.mk' (Lm.cons 0) (Y.cons 1)⟩ := + step_nSteps (step_mk'_left (b := 0) (q' := 7) rfl _ _) + (step_nSteps (step_mkL_right (b := 1) (q' := 5) rfl _ _) + (step_nSteps (step_mk'_left (b := 1) (q' := 10) rfl _ _) + (step_one (step_mkL_right (b := 0) (q' := 2) rfl _ _)))) + +/-- The walker area: `h` ones, a hole, `r` ones, then blank. -/ +def walkerTape (h r : ℕ) : ListBlank (Fin 2) := ones(h, ones(r, B0).cons 0) + +theorem walkerTape_zero (h : ℕ) : walkerTape h 0 = ones(h, B0) := + congrArg (fun l : ListBlank (Fin 2) => ones(h, l)) B0_cons_zero + +theorem comp_f0_succ (L : ListBlank (Fin 2)) (t h r : ℕ) : + nSteps leg25 (1 + (((h + 1) + (2 + h)) + (2 + (t + 1)))) + (testExit L ((walkerTape (h + 1) r).cons 0) false t) = + some ⟨16, Tape.mkL (L.cons 0) ones(t + 1, ((walkerTape h (r + 1)).cons 0).cons 0)⟩ := by + have h1 : nSteps leg25 1 + ⟨6, Tape.mk' (ones(t + 1, L.cons 0).cons 0) ((walkerTape (h + 1) r).cons 0)⟩ = + some ⟨2, Tape.mk' ((ones(t + 1, L.cons 0).cons 0).cons 0) (walkerTape (h + 1) r)⟩ := + step_one (step_mk'_right (b := 0) (q' := 2) rfl _ _) + have h2 := walkB h ((ones(t + 1, L.cons 0).cons 0).cons 0) ones(r, B0) + have h3 := ret_q3 (t + 1) (L.cons 0) ones(h, (ones(r, B0).cons 1).cons 0) + unfold testExit + exact nSteps_bind_eq h1 (nSteps_bind_eq h2 h3) + +theorem comp_f0_zero (L : ListBlank (Fin 2)) (t r : ℕ) : + ∃ c, nSteps leg25 3 (testExit L ((walkerTape 0 r).cons 0) false t) = some c ∧ + step leg25 c = none := by + have h1 : nSteps leg25 3 + ⟨6, Tape.mk' (ones(t + 1, L.cons 0).cons 0) ((ones(r, B0).cons 0).cons 0)⟩ = + some ⟨10, Tape.mkL (ones(t + 1, L.cons 0).cons 0) ((ones(r, B0).cons 1).cons 1)⟩ := + step_nSteps (step_mk'_right (b := 0) (q' := 2) rfl _ _) + (step_nSteps (step_mk'_left (b := 1) (q' := 5) rfl _ _) + (step_one (step_mkL_left (b := 1) (q' := 10) rfl _ _))) + unfold testExit + exact ⟨_, h1, step_mkL_none rfl _ _⟩ + +/-- `B` on the set flag, the separator on its left: one walker step and back to `q16`. -/ +theorem flag1_pass (L : ListBlank (Fin 2)) (t h r : ℕ) : + nSteps leg25 (((h + 1) + (2 + h)) + (3 + (t + 1))) + ⟨2, Tape.mk' (ones(t + 1, L.cons 0).cons 0) ((walkerTape h r).cons 1)⟩ = + some ⟨16, Tape.mkL (L.cons 0) ones(t + 1, ones(h, ones(r + 1, B0).cons 0).cons 0)⟩ := by + have h2 := walkB h (ones(t + 1, L.cons 0).cons 0) ones(r, B0) + have h3 := ret_q4 t L ones(h, (ones(r, B0).cons 1).cons 0) + exact nSteps_bind_eq h2 h3 + +theorem comp_f1 (L : ListBlank (Fin 2)) (t h r : ℕ) : + nSteps leg25 (4 + (((h + 1) + (2 + h)) + (3 + (t + 1)))) + (testExit L ((walkerTape h r).cons 1) false t) = + some ⟨16, Tape.mkL (L.cons 0) ones(t + 1, ones(h, ones(r + 1, B0).cons 0).cons 0)⟩ := by + have h1 := detour ones(t + 1, L.cons 0) (walkerTape h r) + unfold testExit + exact nSteps_bind_eq h1 (flag1_pass L t h r) + +theorem prime_f1 (L : ListBlank (Fin 2)) (t h r : ℕ) : + nSteps leg25 (1 + (((h + 1) + (2 + h)) + (3 + (t + 1)))) + (testExit L ((walkerTape h r).cons 1) true t) = + some ⟨16, Tape.mkL (L.cons 0) ones(t + 1, ones(h, ones(r + 1, B0).cons 0).cons 0)⟩ := by + have h1 : nSteps leg25 1 + ⟨6, Tape.mk' ones(t + 1, L.cons 0) (((walkerTape h r).cons 1).cons 0)⟩ = + some ⟨2, Tape.mk' (ones(t + 1, L.cons 0).cons 0) ((walkerTape h r).cons 1)⟩ := + step_one (step_mk'_right (b := 0) (q' := 2) rfl _ _) + unfold testExit + exact nSteps_bind_eq h1 (flag1_pass L t h r) + +/-- First prime of an interval (flag clear): the flag is set, the separator moves one cell +left, and the machine is back at the test event of the same number `n + 1`. -/ +theorem prime_f0 (L : ListBlank (Fin 2)) (n h r : ℕ) : + nSteps leg25 (4 + (((h + 1 + 1) + (2 + (h + 1))) + (3 + (n + 1)))) + (testExit L ((walkerTape h r).cons 0) true (n + 1)) = + some ⟨16, Tape.mkL (L.cons 0) ones(n + 1, ((walkerTape h (r + 1)).cons 1).cons 0)⟩ := by + have h1 : nSteps leg25 4 + ⟨6, Tape.mk' (ones(n + 1, L.cons 0).cons 1) (((walkerTape h r).cons 0).cons 0)⟩ = + some ⟨2, Tape.mk' (ones(n + 1, L.cons 0).cons 0) (((walkerTape h r).cons 1).cons 1)⟩ := + step_nSteps (step_mk'_right (b := 0) (q' := 2) rfl _ _) + (step_nSteps (step_mk'_left (b := 1) (q' := 5) rfl _ _) + (step_nSteps (step_mkL_left (b := 1) (q' := 10) rfl _ _) + (step_one (step_mkL_right (b := 0) (q' := 2) rfl _ _)))) + have h2 := walkB (h + 1) (ones(n + 1, L.cons 0).cons 0) ones(r, B0) + have h3 := ret_q4 n L ones(h + 1, (ones(r, B0).cons 1).cons 0) + unfold testExit + exact nSteps_bind_eq h1 (nSteps_bind_eq h2 h3) + +/-- The number `1`: `q3` and `q4` send `q16` straight back; nothing right of the block moves. -/ +theorem testCfg_one (L R : ListBlank (Fin 2)) : + nSteps leg25 5 (testCfg L R 1) = some ⟨16, Tape.mkL (L.cons 0) ones(2, R.cons 0)⟩ := by + have h1 : nSteps leg25 3 ⟨16, Tape.mkL ((L.cons 0).cons 0) ((R.cons 0).cons 1)⟩ = + some ⟨16, Tape.mkL (((L.cons 0).cons 1).cons 1) (R.cons 0)⟩ := + step_nSteps (step_mkL_right (b := 1) (q' := 3) rfl _ _) + (step_nSteps (step_mk'_right (b := 1) (q' := 4) rfl _ _) + (step_one (step_mk'_left (b := 0) (q' := 16) rfl _ _))) + have h2 : nSteps leg25 2 ⟨16, Tape.mkL ones(2, L.cons 0) (R.cons 0)⟩ = + some ⟨16, Tape.mkL (L.cons 0) ones(2, R.cons 0)⟩ := + nSteps_mkL_left_scan (q := 16) (a := 1) (b := 1) rfl 2 (L.cons 0) (R.cons 0) + unfold testCfg + exact nSteps_bind_eq h1 h2 + +/-! +## Events + +`evCfg t f h r`: `q16` on the blank left of a block of `t` ones, nothing but blanks further left; +right of the block the separator, the flag `f`, and the walker area `walkerTape h r`. +-/ + +def evCfg (t : ℕ) (f : Fin 2) (h r : ℕ) : Cfg 25 2 := + ⟨16, Tape.mkL (B0.cons 0) ones(t, ((walkerTape h r).cons f).cons 0)⟩ + +theorem ev_congr {t t' : ℕ} (f : Fin 2) {h h' r r' : ℕ} + (ht : t = t') (hh : h = h') (hr : r = r') : evCfg t f h r = evCfg t' f h' r' := by + subst ht hh hr; rfl + +theorem testCfg_B0 (R : ListBlank (Fin 2)) (t : ℕ) : + testCfg B0 R t = ⟨16, Tape.mkL (B0.cons 0) ones(t, R.cons 0)⟩ := + congrArg (fun l : ListBlank (Fin 2) => + (⟨16, Tape.mkL (l.cons 0) ones(t, R.cons 0)⟩ : Cfg 25 2)) B0_cons_zero + +theorem ev_test (t : ℕ) (f : Fin 2) (h r : ℕ) (ht : 2 ≤ t) : + ∃ s, 1 ≤ s ∧ + nSteps leg25 s (evCfg t f h r) = + some (testExit B0 ((walkerTape h r).cons f) (decide (IsPrime t)) t) := by + have h0 := test_eval B0 ((walkerTape h r).cons f) t ht + rw [testCfg_B0] at h0 + exact h0 + +theorem ev_one (f : Fin 2) (h r : ℕ) : nSteps leg25 5 (evCfg 1 f h r) = some (evCfg 2 f h r) := by + have h0 := testCfg_one B0 ((walkerTape h r).cons f) + rw [testCfg_B0] at h0 + exact h0 + +theorem ev_comp_f0_succ (t h r : ℕ) (ht : 2 ≤ t) (hp : ¬ IsPrime t) : + ∃ s, 1 ≤ s ∧ nSteps leg25 s (evCfg t 0 (h + 1) r) = some (evCfg (t + 1) 0 h (r + 1)) := by + obtain ⟨s, _, hs⟩ := ev_test t 0 (h + 1) r ht + rw [decide_eq_false hp] at hs + exact ⟨_, by omega, nSteps_bind_eq hs (comp_f0_succ B0 t h r)⟩ + +theorem ev_comp_f0_zero (t r : ℕ) (ht : 2 ≤ t) (hp : ¬ IsPrime t) : + ∃ s c, nSteps leg25 s (evCfg t 0 0 r) = some c ∧ step leg25 c = none := by + obtain ⟨s, _, hs⟩ := ev_test t 0 0 r ht + rw [decide_eq_false hp] at hs + obtain ⟨c, hc, hn⟩ := comp_f0_zero B0 t r + exact ⟨_, c, nSteps_bind_eq hs hc, hn⟩ + +theorem ev_f1 (t h r : ℕ) (ht : 2 ≤ t) : + ∃ s, 1 ≤ s ∧ nSteps leg25 s (evCfg t 1 h r) = + some ⟨16, Tape.mkL (B0.cons 0) ones(t + 1, ones(h, ones(r + 1, B0).cons 0).cons 0)⟩ := by + obtain ⟨s, _, hs⟩ := ev_test t 1 h r ht + by_cases hp : IsPrime t + · rw [decide_eq_true hp] at hs + exact ⟨_, by omega, nSteps_bind_eq hs (prime_f1 B0 t h r)⟩ + · rw [decide_eq_false hp] at hs + exact ⟨_, by omega, nSteps_bind_eq hs (comp_f1 B0 t h r)⟩ + +theorem ev_f1_succ (t h r : ℕ) (ht : 2 ≤ t) : + ∃ s, 1 ≤ s ∧ nSteps leg25 s (evCfg t 1 (h + 1) r) = some (evCfg (t + 1) 1 h (r + 1)) := + ev_f1 t (h + 1) r ht + +theorem ev_f1_zero (t r : ℕ) (ht : 2 ≤ t) : + ∃ s, 1 ≤ s ∧ nSteps leg25 s (evCfg t 1 0 r) = some (evCfg (t + 1) 0 (r + 1) 0) := by + obtain ⟨s, hs1, hs⟩ := ev_f1 t 0 r ht + refine ⟨s, hs1, ?_⟩ + have e : evCfg (t + 1) 0 (r + 1) 0 = + ⟨16, Tape.mkL (B0.cons 0) ones(t + 1, (ones(r + 1, B0).cons 0).cons 0)⟩ := by + unfold evCfg + rw [walkerTape_zero] + rw [e] + exact hs + +theorem ev_prime_f0 (t h r : ℕ) (ht : 2 ≤ t) (hp : IsPrime t) : + ∃ s, 1 ≤ s ∧ nSteps leg25 s (evCfg t 0 h r) = some (evCfg t 1 h (r + 1)) := by + obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩ + obtain ⟨s, _, hs⟩ := ev_test (n + 1) 0 h r ht + rw [decide_eq_true hp] at hs + exact ⟨_, by omega, nSteps_bind_eq hs (prime_f0 B0 n h r)⟩ + +/-! +## Intervals + +Interval `n` is `n ^ 2, …, n ^ 2 + 2 n`. It starts at the event `evCfg (n * n) 0 (2 * n) 0`: +flag clear, walker area `2 n` ones. Every test moves the hole one cell left, except the first +test of the first prime: it sets the flag and adds a cell to the walker area instead, and the +same prime is then tested again. With a prime, the hole reaches the left end with the flag +set at the last number and the next interval starts with `2 n + 2` ones. Without a prime the +hole reaches the left end with the flag clear at the last number, a composite: the machine halts. +-/ + +theorem not_isPrime_sq (n : ℕ) (hn : 2 ≤ n) : ¬ IsPrime (n * n) := by + intro ⟨_, hnf⟩ + have h2 : n * 2 ≤ n * n := Nat.mul_le_mul_left n hn + exact hnf n (by omega) (by omega) (Dvd.intro n rfl) + +theorem sq_succ (n : ℕ) : (n + 1) * (n + 1) = n * n + 2 * n + 1 := by + rw [Nat.add_mul, Nat.mul_add]; omega + +/-- `j` composites in a row with the flag clear: the hole moves `j` cells left. -/ +theorem walk0 (h j : ℕ) : ∀ (t r : ℕ), 2 ≤ t → (∀ i, i < j → ¬ IsPrime (t + i)) → + ∃ s, j ≤ s ∧ nSteps leg25 s (evCfg t 0 (h + j) r) = some (evCfg (t + j) 0 h (r + j)) := by + induction j with + | zero => intro t r _ _; exact ⟨0, le_rfl, rfl⟩ + | succ j ih => + intro t r ht hnp + obtain ⟨s₁, h1, hs₁⟩ := ev_comp_f0_succ t (h + j) r ht (hnp 0 (Nat.succ_pos j)) + obtain ⟨s₂, h2, hs₂⟩ := ih (t + 1) (r + 1) (by omega) (fun i hi => by + have h' := hnp (i + 1) (by omega) + have e : t + 1 + i = t + (i + 1) := by omega + rw [e]; exact h') + refine ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ ?_⟩ + rw [hs₂] + exact congrArg some (ev_congr 0 (by omega) rfl (by omega)) + +/-- `j` numbers in a row with the flag set: the hole moves `j` cells left. -/ +theorem walk1 (h j : ℕ) : ∀ (t r : ℕ), 2 ≤ t → + ∃ s, j ≤ s ∧ nSteps leg25 s (evCfg t 1 (h + j) r) = some (evCfg (t + j) 1 h (r + j)) := by + induction j with + | zero => intro t r _; exact ⟨0, le_rfl, rfl⟩ + | succ j ih => + intro t r ht + obtain ⟨s₁, h1, hs₁⟩ := ev_f1_succ t (h + j) r ht + obtain ⟨s₂, h2, hs₂⟩ := ih (t + 1) (r + 1) (by omega) + refine ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ ?_⟩ + rw [hs₂] + exact congrArg some (ev_congr 1 (by omega) rfl (by omega)) + +/-- Interval `n` has a prime. -/ +def HasPrime (n : ℕ) : Prop := ∃ x, x < (n + 1) * (n + 1) ∧ n * n < x ∧ IsPrime x + +instance instDecidableHasPrime (n : ℕ) : Decidable (HasPrime n) := + inferInstanceAs (Decidable (∃ x, x < (n + 1) * (n + 1) ∧ n * n < x ∧ IsPrime x)) + +/-- An interval with a prime: from the start of interval `n` to the start of interval `n + 1`. -/ +theorem cycle_adv (n : ℕ) (hn : 2 ≤ n) (hp : HasPrime n) : + ∃ s, 1 ≤ s ∧ nSteps leg25 s (evCfg (n * n) 0 (2 * n) 0) = + some (evCfg ((n + 1) * (n + 1)) 0 (2 * (n + 1)) 0) := by + have hsq := sq_succ n + have h4 : 2 * 2 ≤ n * n := Nat.mul_le_mul hn hn + have hex : ∃ j, IsPrime (n * n + j) := by + obtain ⟨x, _, hx2, hx3⟩ := hp + have e : n * n + (x - n * n) = x := by omega + exact ⟨x - n * n, by rw [e]; exact hx3⟩ + obtain ⟨j0, hj0, hmin⟩ : + ∃ j0, IsPrime (n * n + j0) ∧ ∀ i, i < j0 → ¬ IsPrime (n * n + i) := + ⟨Nat.find hex, Nat.find_spec hex, fun i hi => Nat.find_min hex hi⟩ + have hj0_pos : 1 ≤ j0 := by + rcases Nat.eq_zero_or_pos j0 with hz | hpos + · subst hz; exact absurd hj0 (not_isPrime_sq n hn) + · exact hpos + have hj0_le : j0 ≤ 2 * n := by + obtain ⟨x, hx1, hx2, hx3⟩ := hp + have hle : j0 ≤ x - n * n := Nat.le_of_not_lt (fun hlt => hmin (x - n * n) hlt (by + have e : n * n + (x - n * n) = x := by omega + rw [e]; exact hx3)) + omega + obtain ⟨h0, hh0⟩ : ∃ h0, 2 * n = h0 + j0 := ⟨2 * n - j0, by omega⟩ + obtain ⟨s₁, _, hs₁⟩ := walk0 h0 j0 (n * n) 0 (by omega) hmin + obtain ⟨s₂, hs2, hs₂⟩ := ev_prime_f0 (n * n + j0) h0 (0 + j0) (by omega) hj0 + obtain ⟨s₃, _, hs₃⟩ := walk1 0 h0 (n * n + j0) (0 + j0 + 1) (by omega) + obtain ⟨s₄, _, hs₄⟩ := ev_f1_zero (n * n + j0 + h0) (0 + j0 + 1 + h0) (by omega) + refine ⟨s₁ + (s₂ + (s₃ + s₄)), by omega, ?_⟩ + have e1 : evCfg (n * n) 0 (2 * n) 0 = evCfg (n * n) 0 (h0 + j0) 0 := ev_congr 0 rfl hh0 rfl + have e3 : evCfg (n * n + j0) 1 h0 (0 + j0 + 1) = evCfg (n * n + j0) 1 (0 + h0) (0 + j0 + 1) := + ev_congr 1 rfl (by omega) rfl + have e4 : evCfg (n * n + j0 + h0 + 1) 0 (0 + j0 + 1 + h0 + 1) 0 = + evCfg ((n + 1) * (n + 1)) 0 (2 * (n + 1)) 0 := ev_congr 0 (by omega) (by omega) rfl + rw [e1] + rw [e3] at hs₂ + rw [e4] at hs₄ + exact nSteps_bind_eq hs₁ (nSteps_bind_eq hs₂ (nSteps_bind_eq hs₃ hs₄)) + +/-- An interval without a prime: the machine halts. -/ +theorem cycle_halt (n : ℕ) (hn : 2 ≤ n) (hnp : ¬ HasPrime n) : + ∃ s c, nSteps leg25 s (evCfg (n * n) 0 (2 * n) 0) = some c ∧ step leg25 c = none := by + have hsq := sq_succ n + have h4 : 2 * 2 ≤ n * n := Nat.mul_le_mul hn hn + have hno : ∀ i, i < 2 * n + 1 → ¬ IsPrime (n * n + i) := by + intro i hi hpi + rcases Nat.eq_zero_or_pos i with hz | hpos + · subst hz; exact not_isPrime_sq n hn hpi + · exact hnp ⟨n * n + i, by omega, by omega, hpi⟩ + obtain ⟨s₁, _, hs₁⟩ := walk0 0 (2 * n) (n * n) 0 (by omega) (fun i hi => hno i (by omega)) + obtain ⟨s₂, c, hs₂, hc⟩ := + ev_comp_f0_zero (n * n + 2 * n) (0 + 2 * n) (by omega) (hno (2 * n) (by omega)) + have e1 : evCfg (n * n) 0 (2 * n) 0 = evCfg (n * n) 0 (0 + 2 * n) 0 := + ev_congr 0 rfl (by omega) rfl + rw [e1] + exact ⟨s₁ + s₂, c, nSteps_bind_eq hs₁ hs₂, hc⟩ + +/-! +## Start and main theorem +-/ + +/-- Start of interval `w + 2`. -/ +def intervalCfg (w : ℕ) : Cfg 25 2 := evCfg ((w + 2) * (w + 2)) 0 (2 * (w + 2)) 0 + +theorem interval_advance (w : ℕ) (h : HasPrime (w + 2)) : + ∃ s, 1 ≤ s ∧ nSteps leg25 s (intervalCfg w) = some (intervalCfg (w + 1)) := by + obtain ⟨s, hs1, hs⟩ := cycle_adv (w + 2) (by omega) h + exact ⟨s, hs1, hs⟩ + +theorem interval_halt (w : ℕ) (h : ¬ HasPrime (w + 2)) : + ∃ s c, nSteps leg25 s (intervalCfg w) = some c ∧ step leg25 c = none := + cycle_halt (w + 2) (by omega) h + +theorem boot_17 : + nSteps leg25 17 ⟨14, default⟩ = + some ⟨16, ⟨0, ListBlank.mk [], ListBlank.mk [1, 0, 0, 1, 0, 1]⟩⟩ := rfl + +/-- From the blank tape the machine reaches the test event of `1` in `17` steps, with the +walker area `1 0 1`. The number `1` does not move the hole (`ev_one`), so the hole starts one +cell further left than at the start of a later interval. -/ +theorem boot_ev : nSteps leg25 17 ⟨14, default⟩ = some (evCfg 1 0 1 1) := boot_17 + +/-- Interval `1` (`1, 2, 2, 3`) by the general lemmas: the machine reaches the start of +interval `2`. -/ +theorem boot_interval : ∃ s, nSteps leg25 s ⟨14, default⟩ = some (intervalCfg 0) := by + have h1 := ev_one 0 1 1 + obtain ⟨s₂, _, hs₂⟩ := ev_prime_f0 2 1 1 (by omega) isPrime_two + obtain ⟨s₃, _, hs₃⟩ := ev_f1_succ 2 0 2 (by omega) + obtain ⟨s₄, _, hs₄⟩ := ev_f1_zero 3 3 (by omega) + exact ⟨_, nSteps_bind_eq boot_ev + (nSteps_bind_eq h1 (nSteps_bind_eq hs₂ (nSteps_bind_eq hs₃ hs₄)))⟩ + +theorem empty_or_all (N : ℕ) : + (∃ w, ¬ HasPrime (w + 2)) ∨ ∀ w, w < N → HasPrime (w + 2) := by + induction N with + | zero => exact Or.inr (fun w hw => absurd hw (Nat.not_lt_zero w)) + | succ N ih => + rcases ih with hce | hall + · exact Or.inl hce + · by_cases hN : HasPrime (N + 2) + · refine Or.inr (fun w hw => ?_) + rcases Nat.lt_succ_iff_lt_or_eq.mp hw with h | h + · exact hall w h + · subst h; exact hN + · exact Or.inl ⟨N, hN⟩ + +theorem interval_iter_bounded (N : ℕ) (hall : ∀ w, w < N → HasPrime (w + 2)) : + ∃ s, N ≤ s ∧ nSteps leg25 s (intervalCfg 0) = some (intervalCfg N) := by + induction N with + | zero => exact ⟨0, le_rfl, rfl⟩ + | succ N ih => + obtain ⟨s₁, _, hs₁⟩ := ih (fun w hw => hall w (Nat.lt_succ_of_lt hw)) + obtain ⟨s₂, _, hs₂⟩ := interval_advance N (hall N (Nat.lt_succ_self N)) + exact ⟨s₁ + s₂, by omega, nSteps_bind_eq hs₁ hs₂⟩ + +theorem interval_reach_or_halt (w : ℕ) : + (∃ s, nSteps leg25 s (intervalCfg 0) = some (intervalCfg w)) ∨ + (∃ s c, nSteps leg25 s (intervalCfg 0) = some c ∧ step leg25 c = none) := by + induction w with + | zero => exact Or.inl ⟨0, rfl⟩ + | succ w ih => + rcases ih with ⟨s₁, hs₁⟩ | hhalt + · by_cases hw : HasPrime (w + 2) + · obtain ⟨s₂, _, hs₂⟩ := interval_advance w hw + exact Or.inl ⟨s₁ + s₂, nSteps_bind_eq hs₁ hs₂⟩ + · obtain ⟨s₂, c, hs₂, hnone⟩ := interval_halt w hw + exact Or.inr ⟨s₁ + s₂, c, nSteps_bind_eq hs₁ hs₂, hnone⟩ + · exact Or.inr hhalt + +theorem halts_leg25_iff : + (eval (step leg25) ⟨14, default⟩).Dom ↔ ∃ w : ℕ, ¬ HasPrime (w + 2) := by + obtain ⟨s0, hboot⟩ := boot_interval + rw [nSteps_eval_dom hboot] + 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 empty_or_all (k + 1) with hce | hall + · exact hce + · obtain ⟨s, hks, hs⟩ := interval_iter_bounded (k + 1) hall + have h_eq_none := nSteps_eq_none_of_step_none s hk hnone (by omega) + rw [h_eq_none] at hs + cases hs + · rintro ⟨w, hw⟩ + have h_halt : ∃ s c, nSteps leg25 s (intervalCfg 0) = some c ∧ step leg25 c = none := by + rcases interval_reach_or_halt w with ⟨s₁, hs₁⟩ | hhalt + · obtain ⟨s₂, c, hs₂, hnone⟩ := interval_halt w hw + exact ⟨s₁ + s₂, c, nSteps_bind_eq hs₁ hs₂, hnone⟩ + · exact hhalt + obtain ⟨s, c, hs, hnone⟩ := h_halt + rw [Part.dom_iff_mem] + exact ⟨c, mem_eval'.mpr ⟨nSteps_reaches hs, hnone⟩⟩ + +/-- No prime strictly between `n ^ 2` and `(n + 1) ^ 2`. -/ +def EmptyInterval (n : ℕ) : Prop := ∀ x, n * n < x → x < (n + 1) * (n + 1) → ¬ IsPrime x + +/-- **Main theorem.** The 21-state machine halts on the blank tape if and only if some +`n ≥ 1` has no prime strictly between `n ^ 2` and `(n + 1) ^ 2`. -/ +theorem halts_legendre21_iff : + ConjectureMachines.Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ EmptyInterval n := by + rw [halts_iff_leg25, halts_leg25_iff] + constructor + · rintro ⟨w, hw⟩ + exact ⟨w + 2, by omega, fun x hx1 hx2 hx3 => hw ⟨x, hx2, hx1, hx3⟩⟩ + · rintro ⟨n, hn, hE⟩ + have hn2 : 2 ≤ n := by + rcases Nat.eq_or_lt_of_le hn with h | h + · subst h; exact absurd isPrime_two (hE 2 (by omega) (by omega)) + · exact h + obtain ⟨w, rfl⟩ : ∃ w, n = w + 2 := ⟨n - 2, by omega⟩ + exact ⟨w, fun ⟨x, hx1, hx2, hx3⟩ => hE x hx2 hx1 hx3⟩ + +end ConjectureMachines.Legendre21 diff --git a/Cryptids/Machines.lean b/Cryptids/Machines.lean index 345a59a2..c4ca77d4 100644 --- a/Cryptids/Machines.lean +++ b/Cryptids/Machines.lean @@ -240,6 +240,11 @@ def brocard28Rows : List (List (Option (Fin 2 × Dir × Fin 28))) := load_machine_rows% "artifacts/brocard_28/machine.txt" /-- 28-state Brocard machine. -/ def brocard28 : Machine 28 2 := Machine.ofRows brocard28Rows +/-- Rows of `legendre21`. -/ +def legendre21Rows : List (List (Option (Fin 2 × Dir × Fin 21))) := + load_machine_rows% "artifacts/legendre_21/machine.txt" +/-- 21-state Legendre machine. -/ +def legendre21 : Machine 21 2 := Machine.ofRows legendre21Rows end Machines 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 1a27139c..09f968fa 100644 --- a/Cryptids/Propositions.lean +++ b/Cryptids/Propositions.lean @@ -40,6 +40,8 @@ constructions and halting proofs: 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`). +6. **Legendre's Conjecture** (`LegendreConjecture`): + For every `n ≥ 1` there is a prime strictly between `n ^ 2` and `(n + 1) ^ 2` (`legendre_21`). -/ @[expose] public section @@ -716,4 +718,11 @@ solutions; none exist for `n ≤ 10 ^ 12` (Matson 2017). -/ def BrocardConjecture : Prop := ∀ n : ℕ, 7 < n → ¬ IsSquare (n.factorial + 1) +/-! ## 7. Legendre's Conjecture -/ + +/-- **Legendre's conjecture** (one of Landau's four problems, 1912): for every `n ≥ 1` there is +a prime `p` with `n ^ 2 < p < (n + 1) ^ 2`. -/ +def LegendreConjecture : Prop := + ∀ n : ℕ, 1 ≤ n → ∃ p : ℕ, p.Prime ∧ n ^ 2 < p ∧ p < (n + 1) ^ 2 + end ConjectureMachines diff --git a/Cryptids/README.md b/Cryptids/README.md index 3702997a..035872c3 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) and the `brocard_28` machine and proofs (Brocard's problem) 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), the `brocard_28` machine and proofs (Brocard's problem), and the `legendre_21` machine and proofs (Legendre's conjecture) are by Daniel Veljjanoski, with Claude (Anthropic) as assistant. ## Formalized Machines @@ -16,6 +16,7 @@ This library contains formally verified 2-symbol Turing machines and Lean 4 sema | 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) | +| Legendre's conjecture | `legendre_21` | `21` | Daniel Veljjanoski (Nov 2026), with the primality test of `goldbach_21`; earlier: Charlie Reams's 44-state machine ([`calr3/tinycryptids`](https://github.com/calr3/tinycryptids), Nov 2026) | `¬ LegendreConjecture` | [`Legendre21.lean`](./Legendre21.lean), [`Semantics/Legendre21.lean`](./Semantics/Legendre21.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. @@ -31,6 +32,7 @@ All proofs in [`Cryptids/`](./) are checked by the Lean 4 kernel (`v4.35.0-rc4`) - **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`. + - **Legendre's conjecture (`legendre_21`):** The machine tests `1, 2, 3, …` with the trial-division test of `goldbach_21` and keeps a walker area of `2n` ones for the interval `n^2, …, n^2 + 2n`, whose hole moves one cell per number; it constructively satisfies `Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ ∀ p, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2)` without `Classical.choice` ([`Legendre21.lean`](./Legendre21.lean), [`Semantics/Legendre21.lean`](./Semantics/Legendre21.lean)), and with Markov's Principle `Halts legendre21 ↔ ¬ LegendreConjecture`. - **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/Legendre21.lean b/Cryptids/Semantics/Legendre21.lean new file mode 100644 index 00000000..07860419 --- /dev/null +++ b/Cryptids/Semantics/Legendre21.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Google LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Cryptids.Legendre21 +public import Cryptids.Propositions +public import Cryptids.Semantics.Goldbach + +/-! +# Semantics of `legendre_21` + +`Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ ∀ p, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2)`: the statement +of `Cryptids/Legendre21.lean` with Mathlib's `Nat.Prime` (through `isPrime_iff_prime` of +`Cryptids/Semantics/Goldbach.lean`) and `n ^ 2` for `n * n`. Hence +`Halts legendre21 ↔ ¬ LegendreConjecture`. +-/ + +@[expose] public section + +namespace ConjectureMachines.Legendre21 + +/-- The 21-state machine halts on the blank tape if and only if some `n ≥ 1` has no prime +strictly between `n ^ 2` and `(n + 1) ^ 2`. -/ +theorem halts_legendre21_iff_exists_gap : + ConjectureMachines.Halts legendre21 ↔ + ∃ n : ℕ, 1 ≤ n ∧ ∀ p : ℕ, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2) := by + rw [halts_legendre21_iff] + constructor + · rintro ⟨n, hn, hE⟩ + refine ⟨n, hn, fun p hp ⟨h1, h2⟩ => + hE p ?_ ?_ ((Goldbach21.Semantics.isPrime_iff_prime p).mpr hp)⟩ + · rwa [Nat.pow_two] at h1 + · rwa [Nat.pow_two] at h2 + · rintro ⟨n, hn, hE⟩ + refine ⟨n, hn, fun x h1 h2 hx => + hE x ((Goldbach21.Semantics.isPrime_iff_prime x).mp hx) ⟨?_, ?_⟩⟩ + · rwa [Nat.pow_two] + · rwa [Nat.pow_two] + +/-- The 21-state machine halts on the blank tape if and only if Legendre's conjecture is +false. -/ +theorem halts_legendre21_iff_not_legendre : + ConjectureMachines.Halts legendre21 ↔ ¬ LegendreConjecture := by + rw [halts_legendre21_iff_exists_gap] + constructor + · rintro ⟨n, hn, hE⟩ hL + obtain ⟨p, hp, h⟩ := hL n hn + exact hE p hp h + · intro h + by_contra hne + exact h fun n hn => by + by_contra hnp + exact hne ⟨n, hn, fun p hp hlt => hnp ⟨p, hp, hlt⟩⟩ + +end ConjectureMachines.Legendre21 diff --git a/Cryptids/Semantics/README.md b/Cryptids/Semantics/README.md index dab7e202..f75290e4 100644 --- a/Cryptids/Semantics/README.md +++ b/Cryptids/Semantics/README.md @@ -679,3 +679,42 @@ with `V n = n.factorial / 8` and `IsTri x ↔ ∃ k, x = 1 + 2 + ⋯ + k`. 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). + +## 10. A 21-State Legendre Machine ([`Legendre21.lean`](./Legendre21.lean)) + +In [`Cryptids/Legendre21.lean`](../Legendre21.lean) and [`Cryptids/Semantics/Legendre21.lean`](./Legendre21.lean), +we formalize a new 21-state binary Turing machine for Legendre's conjecture (`legendre_21`, Daniel Veljjanoski with +Claude (Anthropic) as assistant, November 2026): + +```lean +theorem halts_legendre21_iff : + ConjectureMachines.Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ EmptyInterval n + +theorem halts_legendre21_iff_exists_gap : + ConjectureMachines.Halts legendre21 ↔ + ∃ n : ℕ, 1 ≤ n ∧ ∀ p : ℕ, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2) + +theorem halts_legendre21_iff_not_legendre : + ConjectureMachines.Halts legendre21 ↔ ¬ LegendreConjecture +``` + +with `EmptyInterval n ↔ ∀ x, n * n < x → x < (n + 1) * (n + 1) → ¬ IsPrime x` and `IsPrime` the +predicate of `Cryptids/Goldbach21.lean`. + +1. **Machine (`Legendre21.lean`)**: The tape holds the number under test in unary, a separator, a + flag cell and a walker area. The primality test is the one of `goldbach_21`; sixteen of the 21 + states are its states. The machine is embedded into the 25-state numbering of + `Goldbach21.edited` (`leg25`), so the step and scan lemmas and the machine-generic pass lemmas + of `Goldbach21.lean` apply unchanged, and the lemmas stated there for `edited` only are proved + again; `test_eval` says that from a test event the machine reaches the exit that decides + `IsPrime t` with the block restored. After each test the hole of the walker area moves one cell + left. Interval `n` (`n ^ 2, …, n ^ 2 + 2 n`) starts with `2 n` ones in the walker area; its + first prime sets the flag and is tested twice; the hole reaches the left end at the last + number, with the flag set (`cycle_adv`: the next interval starts with `2 n + 2` ones) or clear + (`cycle_halt`: the machine halts). The first `17` steps are run concretely, and interval `1` + follows from the general lemmas. This gives `halts_legendre21_iff` with `propext` and + `Quot.sound` only. +2. **Semantics (`Semantics/Legendre21.lean`)**: `isPrime_iff_prime` (`Semantics/Goldbach.lean`) and + `Nat.pow_two` + give `halts_legendre21_iff_exists_gap` without `Classical.choice`; + `halts_legendre21_iff_not_legendre` uses Markov's Principle via `by_contra` (as in Section 9). diff --git a/README.md b/README.md index 8430e160..f98372bb 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**, **Erdős's ternary conjecture**, and **Brocard's problem** (`brocard_28`, a new 28-state machine). +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**, **Brocard's problem** (`brocard_28`, a new 28-state machine), and **Legendre's conjecture** (`legendre_21`, a new 21-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, 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) | +| [`Cryptids/`](Cryptids/) | `(Q, 2)` Turing machines for Goldbach, ZF consistency, the Riemann Hypothesis, Erdős's ternary conjecture, Brocard's problem, and Legendre's conjecture | Certified state reductions (`25 → 21`, `393 → 380`, `120 → 104 → 95`, `15 → 14`), a new 28-state Brocard machine, a new 21-state Legendre machine, and end-to-end halting equivalences (`Halts M ↔ ¬ GoldbachConjecture`, `ZFInconsistent`, `¬ RiemannHypothesis`, `¬ ErdosTernaryConjecture`, `¬ BrocardConjecture`, `¬ LegendreConjecture`) | [`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)), 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). +- **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)), the `legendre_21` equivalence `Halts legendre21 ↔ ∃ n, 1 ≤ n ∧ ∀ p, p.Prime → ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2)` ([`Legendre21.lean`](Cryptids/Legendre21.lean), [`Semantics/Legendre21.lean`](Cryptids/Semantics/Legendre21.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` and `legendre_21` equivalences with `¬ BrocardConjecture` and `¬ LegendreConjecture` (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), [`erdos_ternary_14`](artifacts/erdos_ternary_14/README.md), and [`brocard_28`](artifacts/brocard_28/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), [`brocard_28`](artifacts/brocard_28/README.md), and [`legendre_21`](artifacts/legendre_21/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 1baa17e3..ce92ba0c 100644 --- a/RELATED_WORK.md +++ b/RELATED_WORK.md @@ -22,6 +22,7 @@ Community records for conjecture-checking and ZFC-independent Turing machines ar - **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). +- **Legendre's conjecture (`legendre_21`):** a new 21-state machine (Nov 2026) with Lean 4 semantics proofs, built on the primality test of `goldbach_21`, after Charlie Reams's 44-state machine (Nov 2026). ### 1. Goldbach's Conjecture (`goldbach`) @@ -77,3 +78,12 @@ Enumerates `n = 8, 9, …` and halts if and only if `n! + 1` is a perfect square | 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)) | + +### 6. Legendre's Conjecture (`legendre`) + +Tests `1, 2, 3, …` for primality in the intervals `n^2, …, n^2 + 2n` and halts if and only if some interval with `n ≥ 1` holds no prime, i.e. if Legendre's conjecture (one of Landau's four problems, 1912) is false: some `n ≥ 1` has no prime strictly between `n^2` and `(n + 1)^2`. + +| Year | Authors / Source | States (`(Q, 2)`) | Construction / Reduction Method | Formal Proof | +| :--- | :--- | :--- | :--- | :--- | +| 2026 | Charlie Reams ([`calr3/tinycryptids`](https://github.com/calr3/tinycryptids/tree/main/legendre) `legendre/`, Nov 2026; a sieve variant `legendre-sieve/` has 45 states) | `44` | 71-state hand design reduced to 44 states: trial division by a mod walk with two holes, an interval register of `2n + 3` cells with a hole marking the position, a flag set by a prime | Lean 4 proof in `tinycryptids` (`TM.Legendre.M44.halts_iff`) | +| 2026 | Daniel Veljjanoski, with Claude (Anthropic) as assistant (`legendre_21`) | `21` | The trial-division test of `goldbach_21` (16 of its states, 7 cells changed) and five more states: a walker area of `2n` ones whose hole moves one cell per number, a flag set by the first prime of the interval (which is tested twice, moving the separator one cell), a halt when the hole reaches the left end with the flag clear; the start runs through the loop's own states | Lean 4 proofs ([`Cryptids/Legendre21.lean`](Cryptids/Legendre21.lean), [`Cryptids/Semantics/Legendre21.lean`](Cryptids/Semantics/Legendre21.lean)) | diff --git a/artifacts/legendre_21/README.md b/artifacts/legendre_21/README.md new file mode 100644 index 00000000..d7b64aba --- /dev/null +++ b/artifacts/legendre_21/README.md @@ -0,0 +1,73 @@ +# 21-state Legendre machine + +This binary Turing machine has **21 states** and 41 defined transitions. It halts only in state +`20` (`X`) reading `0`, its one undefined cell. It starts in state `0` (`q14`) on the blank tape. +Lean proves that it halts if and only if Legendre's conjecture is false, i.e. if some `n ≥ 1` has +no prime strictly between `n^2` and `(n + 1)^2` (one of Landau's four problems, 1912). + +The machine was designed by Daniel Veljjanoski, with Claude (Anthropic) as assistant. Its +primality test is the one of the Goldbach machines: the anonymous 2016 machine, Andrew Yao and +Yijun Leng's `goldbach_25`, and [`goldbach_21`](../goldbach_21/README.md) by Maxence Faldor and Moritz +Firsching. Sixteen of the 21 states are states of that test, with seven of their cells changed, +and the Lean proof uses the lemmas of [`Goldbach21.lean`](../../Cryptids/Goldbach21.lean). An +earlier machine for the same conjecture is Charlie Reams's 44-state machine with a Lean proof of +an equivalent statement ([`calr3/tinycryptids`](https://github.com/calr3/tinycryptids/tree/main/legendre), +November 2026). That machine also tracks the interval with a register of cells with a hole and a +flag set by a prime; here the register needs no rebuild between intervals, and the primality +test is a different one. + +## How it works + +Everything is in unary. The tape holds, left to right, a block of ones for the number under +test, a separator `0`, a flag cell, and a walker area of ones with one hole. The tape left of +the block stays blank; the block grows to the left. States `0`–`20` are +`q14, q0, q3, q4, q6, q7, q9, q11, q12, q13, q15, q16, q20, q22, q23, q24, A1, B, C, Z1, X`, +where `q0`–`q24` are the names of the same states in the Lean proof of `goldbach_21`. + +* **Test** (the sixteen `q` states): `q16` reading the blank left of a block of `t` ones writes + a `1` and enters the trial division of `t` by `2, 3, …`. A prime leaves `q6` on the + separator; a composite leaves `q6` on the flag cell, through `A1`. The block is restored. +* **Walker** (`B`, `C`, `Z1`): after each test `B` runs right to the hole and fills it, `C` opens + a hole one cell further left, `Z1` runs back, and `q3`, `q4`, `q16` return to the left end of + the block, where the next number is tested. +* **Intervals**: interval `n` is `n^2, …, n^2 + 2n` (`n^2` is never prime, so it holds the same + primes as the open interval of the conjecture). It starts with the flag clear and `2n` ones in + the walker area; the blank beyond them is the hole. The first prime of the interval sets the + flag, moves the separator one cell left, and is tested once more. When the hole reaches the + left end with the flag set, it moves into the flag cell: the flag is clear again and the + walker area has `2n + 2` ones, the start of interval `n + 1`. +* **Halt**: when the hole reaches the left end with the flag clear after a composite, no prime + was seen in the interval; `C` reads the flag, `X` reads the separator, and `X` reading `0` is + undefined. +* **Start**: `q14` on the blank tape. After 17 steps the machine is at the test of `1` with the + walker area `1 0 1`; the number `1` does not move the hole, so interval `1` (`1, 2, 2, 3`) + ends as every later interval does. No state is used for the start only. + +The machine began as a 25-state hand design (the test and eight more states) and was reduced to +21 states by computer searches over merged states, changed cells and start states; the +survivors of each search were then checked against a simulator written from the definition. +Searches that merge one state of the 21-state machine and change up to two cells, for every +start state, and a partial search with three changed cells found no 20-state machine. + +In the bbchallenge standard text format (states `0`–`20` written `A`–`U`): + +``` +1LK1LA_0RH1LN_0LL1RD_0LL1RE_0RR0LF_1RS1LN_1RB0LG_1RH0RI_1RJ1RI_0LA0LM_1LQ0LO_1RC1LL_1LG1LM_0RB0LN_1RP1LO_1RC1RP_0RE1RQ_1LS1RR_1LU0LT_0LC1LT_---0RR +``` + +## Review entry points + +- [`Legendre21.lean`](../../Cryptids/Legendre21.lean): the machine (loaded from `machine.txt`), + its embedding into the state numbering of `Goldbach21.edited`, the test (`test_eval`), the + interval lemmas, and `halts_legendre21_iff`. +- [`Semantics/Legendre21.lean`](../../Cryptids/Semantics/Legendre21.lean): + `halts_legendre21_iff_exists_gap` and `halts_legendre21_iff_not_legendre`. + +## Verification + +`python3 verify.py` simulates the machine on the blank tape and checks the whole tape at every +test event (`q16` reading `0`) against the block, separator, flag and walker area of the proof; +the first events are at steps 14 and 17, and the default `--steps 250000` covers 50 test +events, up to the number 43. It also checks that from a prepared tape at the end of an interval +in which no prime was seen the machine halts in state `20`, while with the flag set it goes on +to the next interval with the expected tape. diff --git a/artifacts/legendre_21/machine.txt b/artifacts/legendre_21/machine.txt new file mode 100644 index 00000000..7a4daebc --- /dev/null +++ b/artifacts/legendre_21/machine.txt @@ -0,0 +1,21 @@ +1L10 1L0 +0R7 1L13 +0L11 1R3 +0L11 1R4 +0R17 0L5 +1R18 1L13 +1R1 0L6 +1R7 0R8 +1R9 1R8 +0L0 0L12 +1L16 0L14 +1R2 1L11 +1L6 1L12 +0R1 0L13 +1R15 1L14 +1R2 1R15 +0R4 1R16 +1L18 1R17 +1L20 0L19 +0L2 1L19 +--- 0R17 diff --git a/comparator/README.md b/comparator/README.md index 31cc4ddd..a9de5904 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 36 target + `paZFInconsistent`, `ErdosTernaryConjecture`, etc.), and states all 38 target state-reduction, equivalence, `PA` metatheory & internalized `ZF` provability, and semantics theorems with `sorry`. - [`BusyBeaverChallenge.lean`](../BusyBeaverChallenge.lean) imports **only** Mathlib and Lean core @@ -44,8 +44,8 @@ that: adequacy (`not_paProvable_false`, `paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`), the direct simulation reductions (`Goldbach21`, `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). + theorems, the `brocard_28` equivalence `Brocard28.halts_brocard28_iff_exists_square`, and the + `legendre_21` equivalence `Legendre21.halts_legendre21_iff_exists_gap` (17 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 @@ -54,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`, `brocard_28.json`). + `erdos_ternary_15.json`, `erdos_ternary_14.json`, `brocard_28.json`, `legendre_21.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 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 | +| [`constructive.json`](./constructive.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound` | All 17 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`, the `ErdosTernary14` reduction, `Brocard28.halts_brocard28_iff_exists_square`, and `Legendre21.halts_legendre21_iff_exists_gap` | +| [`all.json`](./all.json) | `Challenge` | `Cryptids` | `propext`, `Quot.sound`, `Classical.choice` | All 38 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` | @@ -78,6 +78,7 @@ that: | [`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` | +| [`legendre_21.json`](./legendre_21.json) | `Challenge` | `Cryptids.Semantics.Legendre21` | `propext`, `Quot.sound`, `Classical.choice` | `halts_legendre21_iff_exists_gap`, `halts_legendre21_iff_not_legendre` | 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 bd8b7a1c..8cd3a5ea 100644 --- a/comparator/all.json +++ b/comparator/all.json @@ -37,7 +37,9 @@ "ConjectureMachines.ErdosTernary14.candidate_equivalent", "ConjectureMachines.ErdosTernary14.Semantics.halts_candidate_iff_not_erdosTernary", "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square", - "ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard" + "ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard", + "ConjectureMachines.Legendre21.halts_legendre21_iff_exists_gap", + "ConjectureMachines.Legendre21.halts_legendre21_iff_not_legendre" ], "permitted_axioms": [ "propext", diff --git a/comparator/constructive.json b/comparator/constructive.json index 2d917499..0d664b59 100644 --- a/comparator/constructive.json +++ b/comparator/constructive.json @@ -17,7 +17,8 @@ "ConjectureMachines.Riemann95.candidate_fewer_states", "ConjectureMachines.ErdosTernary14.candidate_fewer_states", "ConjectureMachines.ErdosTernary14.candidate_equivalent", - "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square" + "ConjectureMachines.Brocard28.halts_brocard28_iff_exists_square", + "ConjectureMachines.Legendre21.halts_legendre21_iff_exists_gap" ], "permitted_axioms": [ "propext", diff --git a/comparator/legendre_21.json b/comparator/legendre_21.json new file mode 100644 index 00000000..03d04466 --- /dev/null +++ b/comparator/legendre_21.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Cryptids.Semantics.Legendre21", + "theorem_names": [ + "ConjectureMachines.Legendre21.halts_legendre21_iff_exists_gap", + "ConjectureMachines.Legendre21.halts_legendre21_iff_not_legendre" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ] +} diff --git a/formalization.yaml b/formalization.yaml index 3f8a0fd5..333c23dc 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), and Brocard's problem (a new 28-state machine brocard_28, + erdos_ternary_14), Brocard's problem (a new 28-state machine brocard_28, + November 2026), and Legendre's conjecture (a new 21-state machine legendre_21, November 2026), proving halting equivalences and connecting every machine's blank-tape halting behavior to the corresponding statement in Mathlib. @@ -209,6 +210,28 @@ sources: 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). + - title: "A Turing machine for Legendre's conjecture (tinycryptids, legendre_44)" + authors: + - "Charlie Reams" + id: "https://github.com/calr3/tinycryptids/tree/main/legendre" + type: "web post" + relationship: "background" + author_endorsement: "not-contacted" + note: >- + A 44-state, 2-symbol machine (reduced from a 71-state design) with a Lean proof + TM.Legendre.M44.halts_iff of an equivalent statement, published in November 2026; + an earlier machine for the conjecture. Not used by legendre_21. + - title: "A 21-state Turing machine for Legendre's conjecture with Lean 4 proofs (legendre_21)" + authors: + - "Daniel Veljjanoski" + type: "original-proof" + relationship: "other" + note: >- + New machine (artifacts/legendre_21/machine.txt) built on the primality test of + goldbach_21, and first Lean 4 proofs that it halts iff some n >= 1 has no prime + strictly between n^2 and (n+1)^2 (Cryptids/Legendre21.lean, + Cryptids/Semantics/Legendre21.lean). The proof uses the lemmas of + Cryptids/Goldbach21.lean for the test. related_formalizations: - id: "https://github.com/lengyijun/goldbach_tm" @@ -261,7 +284,11 @@ status: 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. + Halts brocard28 <-> ¬ BrocardConjecture with Markov's Principle. The 21-state + machine legendre_21 satisfies Halts legendre21 <-> ∃ n, 1 ≤ n ∧ ∀ p, p.Prime -> + ¬ (n ^ 2 < p ∧ p < (n + 1) ^ 2) constructively (Cryptids/Legendre21.lean, + Cryptids/Semantics/Legendre21.lean), and Halts legendre21 <-> ¬ LegendreConjecture + with Markov's Principle. sorry_count: 0 sorry_in_definitions: 0 axioms: @@ -414,6 +441,16 @@ status: sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator/brocard_28.json" + - declaration: "ConjectureMachines.Legendre21.halts_legendre21_iff_exists_gap" + file: "Cryptids/Semantics/Legendre21.lean" + sorry_count: 0 + axioms: ["propext", "Quot.sound"] + comparator_config: "comparator/constructive.json" + - declaration: "ConjectureMachines.Legendre21.halts_legendre21_iff_not_legendre" + file: "Cryptids/Semantics/Legendre21.lean" + sorry_count: 0 + axioms: ["propext", "Classical.choice", "Quot.sound"] + comparator_config: "comparator/legendre_21.json" automation: methods: @@ -437,7 +474,8 @@ automation: (Cryptids/ErdosTernary15.lean, Cryptids/Semantics/ErdosTernary15.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). + (Cryptids/Brocard28.lean, Cryptids/Semantics/Brocard28.lean) and of legendre_21 + (Cryptids/Legendre21.lean, Cryptids/Semantics/Legendre21.lean). spend_usd: "" notes: >- Candidate state reductions and halting-equivalence proofs were discovered @@ -445,7 +483,7 @@ automation: 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, and the - brocard_28 machine and proofs, were written by Daniel Veljjanoski with Claude + brocard_28 and legendre_21 machines and proofs, were written by Daniel Veljjanoski with Claude (Anthropic) as assistant. fidelity: @@ -590,6 +628,18 @@ alignment: lean: "ConjectureMachines.Brocard28.halts_brocard28_iff_not_brocard" module: "Cryptids.Semantics.Brocard28" status: "proved" + - source: "legendre_21 <-> ∃ n ≥ 1, no IsPrime x with n * n < x < (n + 1) * (n + 1)" + lean: "ConjectureMachines.Legendre21.halts_legendre21_iff" + module: "Cryptids.Legendre21" + status: "proved" + - source: "legendre_21 <-> ∃ n ≥ 1, no prime p with n ^ 2 < p < (n + 1) ^ 2" + lean: "ConjectureMachines.Legendre21.halts_legendre21_iff_exists_gap" + module: "Cryptids.Semantics.Legendre21" + status: "proved" + - source: "legendre_21 <-> ¬ LegendreConjecture" + lean: "ConjectureMachines.Legendre21.halts_legendre21_iff_not_legendre" + module: "Cryptids.Semantics.Legendre21" + status: "proved" acknowledgements: >- We thank Eric Wieser for careful review, the Busy Beaver Challenge community, diff --git a/verify.py b/verify.py index b508d87a..5f87546e 100755 --- a/verify.py +++ b/verify.py @@ -51,6 +51,10 @@ 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`. + - Legendre (21 states): the first test events are at steps 14 and 17, and at every test + event (`q16` reading `0`) the tape is the block, separator, flag and walker area of + `Cryptids/Legendre21.lean`; from a prepared tape an interval in which no prime was + seen halts in `X`. """ from __future__ import annotations @@ -280,6 +284,24 @@ } +# A new machine with no reference, checked like `brocard_28`. +LEGENDRE_21 = { + "id": "legendre_21", + "path": "artifacts/legendre_21", + "lean_file": "Cryptids/Machines.lean", + "lean_def": "legendre21", + "proof_path": "Cryptids/Legendre21.lean", + "challenge_path": "Challenge.lean", + "states": 21, + "machine_sha256": ( + "5366c36eb3032c5bd10775874aeac0a4182a817eeaf51ad945b523099929c2f9" + ), + "table_file_sha256": ( + "5366c36eb3032c5bd10775874aeac0a4182a817eeaf51ad945b523099929c2f9" + ), +} + + @dataclasses.dataclass(frozen=True) class Transition: write: int @@ -999,6 +1021,118 @@ def planted(b: int): "planted_square_halts": True, } + +def verify_legendre_21(machine: Machine, steps: int) -> dict[str, object]: + """Checks the interval layout of `Cryptids/Legendre21.lean`. + + State numbers are those of `machine.txt`: `11` is `q16` and `20` is `X`. A test event is + `q16` reading `0`. At a test event with the head on cell `p` the tape holds a block of + `t` ones on `p+1, ..., p+t` (the number under test), a `0` on `p+t+1` (the separator), + the flag `f` on `p+t+2`, and the walker area from `p+t+3` on: `h` ones, a hole, `r` ones; + nothing else. On the blank tape the events follow the model of the Lean proof: `t < 2` + goes to `t + 1`; the first prime of an interval (`f = 0`) is tested again with `f = 1` + and `r + 1`; otherwise the hole moves one cell left (`h - 1`, `r + 1`) and `t` grows by + one, and with `h = 0` and `f = 1` the next interval starts with `f = 0`, `h = r + 1`, + `r = 0`. The first events are at steps 14 (`t = 0`) and 17 (`t = 1`), both with the + walker area `1 0 1`. Then, from a prepared event tape with `t = 8`, `f = 0`, `h = 0`, + `r = 4` (the end of an interval in which no prime was seen), the machine halts in state + `20` (`X`); with `f = 1`, `r = 5` (the tape the blank-tape run has at `8`) it reaches + the test of `9` with the flag clear and six ones in the walker area. + """ + proof_text = (ROOT / "Cryptids/Legendre21.lean").read_text(encoding="utf-8") + assert "theorem halts_legendre21_iff" in proof_text + halting = [ + (q, sym) + for q, row in enumerate(machine.table) + for sym, tr in enumerate(row) + if tr is None + ] + # Only `X` (state 20) on `0` halts. + assert halting == [(20, 0)], f"legendre_21 halting entries: {halting}" + q16 = 11 + + def is_prime(x: int) -> bool: + return x >= 2 and all(x % d for d in range(2, int(x**0.5) + 1)) + + def layout(p: int, t: int, f: int, h: int, r: int) -> set[int]: + a = p + t + 3 + cells = {p + 1 + i for i in range(t)} + cells |= {a + i for i in range(h)} | {a + h + 1 + i for i in range(r)} + if f: + cells.add(p + t + 2) + return cells + + def advance(t: int, f: int, h: int, r: int): + """The next test event by the model, or `None` for a halt.""" + if t < 2: + return (t + 1, f, h, r) + if is_prime(t) and f == 0: + return (t, 1, h, r + 1) + if h > 0: + return (t + 1, f, h - 1, r + 1) + if f == 1: + return (t + 1, 0, r + 1, 0) + return None + + def run(ones: set[int], head: int, state: int, limit: int): + """Runs until the next test event (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 == q16 and head not in ones: + return "event", state, head, t + 1 + return "limit", state, head, limit + + # Blank tape: every test event as far as `steps` allows. + ones: set[int] = set() + head, state, total, events = 0, 0, 0, 0 + model = (0, 0, 1, 1) + last = 0 + while True: + status, state, head, t = run(ones, head, state, steps - total) + total += t + if model is None: + # The model says the interval had no prime: the machine must halt, not go on. + assert status != "event", "legendre_21: the model halts, the machine goes on" + break + if status != "event": + assert status == "limit", f"legendre_21 halted at step {total}" + break + assert ones == layout(head, *model), ( + f"legendre_21 test event {events} (number {model[0]}): tape mismatch" + f" at step {total}" + ) + if events < 2: + assert total == (14, 17)[events], f"legendre_21 event {events} at step {total}" + last = model[0] + events += 1 + model = advance(*model) + if steps >= 250_000: + assert events >= 40, f"legendre_21: only {events} test events in {steps} steps" + + # Planted: the end of interval 2 (the number 8) with and without a prime seen. + cells = layout(0, 8, 0, 0, 4) + status, state, _, _ = run(cells, 0, q16, 100_000) + assert (status, state) == ("halt", 20), f"legendre_21 planted gap: {status} in {state}" + cells = layout(0, 8, 1, 0, 5) + status, state, head, _ = run(cells, 0, q16, 100_000) + assert status == "event", f"legendre_21 planted interval end: {status}" + assert cells == layout(head, 9, 0, 6, 0), "legendre_21 planted interval end: wrong tape" + return { + "steps_simulated": total, + "events_verified": events, + "last_number": last, + "planted_gap_halts": True, + } + + def extract_goldbach_chk0( machine: Machine, steps: int, is_candidate: bool ) -> dict[str, object]: @@ -1345,6 +1479,43 @@ def run_verification( " planted square halts in M0" ) + # Legendre: table, SHA-256, Lean definitions, and simulation. + lspec = LEGENDRE_21 + l_text = (ROOT / str(lspec["path"]) / "machine.txt").read_text(encoding="utf-8") + assert sha256_bytes(l_text.encode("utf-8")) == lspec["table_file_sha256"], ( + "legendre_21 table file SHA-256 mismatch" + ) + lm = parse_canonical_machine(l_text) + assert lm.states == lspec["states"], f"legendre_21 state count mismatch: {lm.states}" + assert lm.sha256 == lspec["machine_sha256"], ( + f"legendre_21 machine SHA-256 mismatch: {lm.sha256}" + ) + for lean_path in (lspec["lean_file"], lspec["challenge_path"]): + assert ( + parse_lean_machine_def( + (ROOT / str(lean_path)).read_text(encoding="utf-8"), + str(lspec["lean_def"]), + expected_table_path=f"{lspec['path']}/machine.txt", + ).table + == lm.table + ), f"{lean_path} legendre_21 table mismatch" + assert "theorem halts_legendre21_iff_exists_gap" in ( + ROOT / "Challenge.lean" + ).read_text(encoding="utf-8") + legendre_sim = verify_legendre_21(lm, steps) + report["candidates"]["legendre_21"] = { + "states": lm.states, + "machine_sha256": lm.sha256, + } + report["simulations"]["legendre_21"] = legendre_sim + if verbose: + print( + f"[PASS] Legendre 21 ({lm.states} states, SHA-256 {lm.sha256[:16]}...):" + f" {legendre_sim['events_verified']} test events verified on the blank tape" + f" ({legendre_sim['steps_simulated']:,} steps, up to the number" + f" {legendre_sim['last_number']}); planted gap halts in X" + ) + # 5. Concrete blank-tape lockstep simulations gb_ref_sim = extract_goldbach_chk0( baseline_machines["goldbach"], steps, is_candidate=False