Certified State Reductions & Formalized Conjecture-Checking Turing Machines

This library formalizes record smaller 2-symbol Turing machines for Goldbach's Conjecture (25 → 21 states), ZF Set Theory Consistency (393 → 380 states), and the Riemann Hypothesis (120 → 104 states), as well as complete Lean 4 formalizations of all publicly known baseline machines (goldbach_25, zf_432, zf_393, riemann_744, riemann_120), linking every machine's blank-tape halting problem to Mathlib's statements:

Cryptids.Propositions — Shared definitions of GoldbachConjecture, MatiyasevichRiemannCounterexample, ZFInconsistent, and WadeZFInconsistent.

Cryptids.Machines — Turing machine execution model, bundled machines (BundledMachine), and machine table definitions (ConjectureMachines.Machines.*).

Cryptids.Goldbach21, Cryptids.Zf380, Cryptids.Riemann104 — Proofs of candidate.states < reference.states and Halts candidate ↔ Halts reference.

Cryptids.Zf393, Cryptids.Semantics.Zf393 — Wade's 393-state ZF machine (zf393), our 380-state reduction (zf380), and end-to-end proofs of ConjectureMachines.Zf393.halts_zf393_iff_zfInconsistent, ConjectureMachines.Zf393.not_halts_zf393, ConjectureMachines.Zf380.Semantics.halts_candidate_iff_zfInconsistent, and ConjectureMachines.Zf380.Semantics.not_halts_candidate.

Cryptids.Riemann120, Cryptids.Semantics.Riemann120 — Shunia's 120-state Riemann Hypothesis machine (riemann120), our 104-state reduction (riemann104), and end-to-end proofs of ConjectureMachines.Riemann120.halts_riemann120_iff_not_riemannHypothesis and ConjectureMachines.Riemann104.Semantics.halts_candidate_iff_not_riemannHypothesis.

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).