Cryptids.Semantics.Riemann

Imports

/-
Copyright (c) 2026 Google LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
module

public import Cryptids.Semantics.Riemann.Gadgets
public import Cryptids.Semantics.Riemann.Dispatcher
public import Cryptids.Semantics.Riemann.RegisterMachine
public import Cryptids.Semantics.Riemann.Analytic

Semantics of the 744-State Riemann Hypothesis Turing Machine (`riemann_744`)

This file formalizes the semantics of the 744-state baseline Turing machine Machines.riemann744 (riemann_744), connecting its halting problem on the blank tape to the negation of Mathlib's RiemannHypothesis.

Provenance and Attribution

744-state Riemann Hypothesis Turing machine (riemann_744, 2016): Designed by Yuri Matiyasevich, Scott Aaronson, and Stefan O'Rear in sorear/metamath-turing-machines (machines/2016-riemann-matiyasevich-aaronson-744/riemann.nql), encoding an elementary counterexample search for the Riemann Hypothesis via harmonic numbers and $\operatorname{lcm}(1, \dots, x)$ building on Schoenfeld's (1976) explicit bound for $|\psi(x) - x|$ and Lagarias's (2002) elementary reformulation.

This formalization (Cryptids.Semantics.Riemann & submodules): Formalized in Lean 4 by Maxence Faldor and Moritz Firsching (using Gemini Argon).

Architecture

The equivalence is factored through the elementary integer predicate MatiyasevichRiemannCounterexample (x : ℕ) : Prop directly computed by riemann.nql:

Part I (halts_riemann744_iff_exists_counterexample, 0 sorrys): ConjectureMachines.Halts Machines.riemann744 ↔ ∃ x : ℕ, MatiyasevichRiemannCounterexample x

Layer 1 (Cryptids.Semantics.Riemann.Gadgets): Canonical tape layout (entryCfg, postPcCfg), return scan loops, 11-bit ripple-carry PC adder, and primitive unary register operations (reg_init_eval, reg_incr_eval, reg_decr_eval).

Layer 2 (Cryptids.Semantics.Riemann.Dispatcher): Bounded-window symbolic evaluator (WinState), complete 2,048-entry BDD instruction decoder (program : ℕ → Instr), reachable invariant (RegInv), and halting simulation (halts_reference_iff_regHalts).

Layer 3 (Cryptids.Semantics.Riemann.RegisterMachine): Complete verification of the 16-register NQL counter machine (regHalts_iff_exists_counterexample).

Part II (Cryptids.Semantics.Riemann.Analytic): (∃ x : ℕ, MatiyasevichRiemannCounterexample x) ↔ ¬ RiemannHypothesis Proves the identity $\psi(x) = \log \operatorname{lcm}(1, \dots, x)$, the Euler–Mascheroni harmonic bounds, and the reduction to Schoenfeld's (1976) explicit bound and Schmidt's (1903) oscillation theorem.

@[expose] public sectionnamespace ConjectureMachines.Semantics.Riemannopen Turing StateTransition

Unconditional halting equivalence between the 744-state Turing machine Machines.riemann744 and the 16-register NQL counter machine RegHalts, combining Layer 1 and Layer 2.

theorem halts_reference_iff_regHalts_unconditional :
    ConjectureMachines.Halts Machines.riemann744 ↔ RegHalts := by⊢ ConjectureMachines.Halts Machines.riemann744 ↔ RegHalts
  apply halts_reference_iff_regHalts Layer1.entryCfg_zero_nilhInit⊢ ∀ (pc : ℕ) (regs : List ℕ),
  pc + 1 < 2048 → ∃ s, 1 ≤ s ∧ nSteps refM s (postPcCfg 32 pc regs) = some (entryCfg (pc + 1) (regs ++ [0]))hIncr⊢ ∀ (k : Fin 16) (pc : ℕ) (regs : List ℕ),
  ↑k < regs.length →
    pc + 1 < 2048 →
      ∃ s,
        1 ≤ s ∧
          nSteps refM s (postPcCfg (regIncrState ↑k) pc regs) =
            some (entryCfg (pc + 1) (regs.set (↑k) (regs.getD (↑k) 0 + 1)))hDecr⊢ ∀ (k : Fin 16) (pc : ℕ) (regs : List ℕ),
  ↑k < regs.length →
    pc + 2 < 2048 →
      ∃ s,
        1 ≤ s ∧
          nSteps refM s (postPcCfg (regDecrState ↑k) pc regs) =
            some
              (if (regs.getD (↑k) 0 == 0) = true then entryCfg (pc + 1) regs
              else entryCfg (pc + 2) (regs.set (↑k) (regs.getD (↑k) 0 - 1)))
  ·hInit⊢ ∀ (pc : ℕ) (regs : List ℕ),
  pc + 1 < 2048 → ∃ s, 1 ≤ s ∧ nSteps refM s (postPcCfg 32 pc regs) = some (entryCfg (pc + 1) (regs ++ [0])) intro pc regs _hInitpc:ℕregs:List ℕa✝:pc + 1 < 2048⊢ ∃ s, 1 ≤ s ∧ nSteps refM s (postPcCfg 32 pc regs) = some (entryCfg (pc + 1) (regs ++ [0]))
    exact Layer1.reg_init_eval pc regsAll goals completed! 🐙
  ·hIncr⊢ ∀ (k : Fin 16) (pc : ℕ) (regs : List ℕ),
  ↑k < regs.length →
    pc + 1 < 2048 →
      ∃ s,
        1 ≤ s ∧
          nSteps refM s (postPcCfg (regIncrState ↑k) pc regs) =
            some (entryCfg (pc + 1) (regs.set (↑k) (regs.getD (↑k) 0 + 1))) intro k pc regs hk _hIncrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 1 < 2048⊢ ∃ s,
  1 ≤ s ∧
    nSteps refM s (postPcCfg (regIncrState ↑k) pc regs) =
      some (entryCfg (pc + 1) (regs.set (↑k) (regs.getD (↑k) 0 + 1)))
    simpa [List.getElem?_eq_getElem hk] using Layer1.reg_incr_eval k.val k.isLt pc regs hkAll goals completed! 🐙
  ·hDecr⊢ ∀ (k : Fin 16) (pc : ℕ) (regs : List ℕ),
  ↑k < regs.length →
    pc + 2 < 2048 →
      ∃ s,
        1 ≤ s ∧
          nSteps refM s (postPcCfg (regDecrState ↑k) pc regs) =
            some
              (if (regs.getD (↑k) 0 == 0) = true then entryCfg (pc + 1) regs
              else entryCfg (pc + 2) (regs.set (↑k) (regs.getD (↑k) 0 - 1))) intro k pc regs hk _hDecrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048⊢ ∃ s,
  1 ≤ s ∧
    nSteps refM s (postPcCfg (regDecrState ↑k) pc regs) =
      some
        (if (regs.getD (↑k) 0 == 0) = true then entryCfg (pc + 1) regs
        else entryCfg (pc + 2) (regs.set (↑k) (regs.getD (↑k) 0 - 1)))
    obtain ⟨s, hs, heval⟩ := Layer1.reg_decr_eval k.val k.isLt pc regs hkhDecrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))⊢ ∃ s,
  1 ≤ s ∧
    nSteps refM s (postPcCfg (regDecrState ↑k) pc regs) =
      some
        (if (regs.getD (↑k) 0 == 0) = true then entryCfg (pc + 1) regs
        else entryCfg (pc + 2) (regs.set (↑k) (regs.getD (↑k) 0 - 1)))
    simp only [List.getD, List.getElem?_eq_getElem hk, Option.getD_some]hDecrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))⊢ ∃ s,
  1 ≤ s ∧
    nSteps refM s (postPcCfg (regDecrState ↑k) pc regs) =
      some (if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))
    refine ⟨s, hs, ?_⟩hDecrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))⊢ nSteps refM s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))
    rw [hevalhDecrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))⊢ some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  some (if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))]hDecrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))⊢ some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  some (if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))
    congr 1hDecrk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))⊢ (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))
    by_cases hz : regs[k.val] = 0posk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))hz:regs[↑k] = 0⊢ (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))negk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))hz:¬regs[↑k] = 0⊢ (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))
    ·posk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))hz:regs[↑k] = 0⊢ (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)) simp [hz]All goals completed! 🐙
    ·negk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))hz:¬regs[↑k] = 0⊢ (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)) have hbeq : (regs[k.val] == 0) = false := beq_eq_false_iff_ne.mpr hznegk:Fin 16pc:ℕregs:List ℕhk:↑k < regs.lengtha✝:pc + 2 < 2048s:ℕhs:1 ≤ sheval:nSteps Layer1.reference s (postPcCfg (regDecrState ↑k) pc regs) =
  some (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1)))hz:¬regs[↑k] = 0hbeq:(regs[↑k] == 0) = false⊢ (if regs[↑k] = 0 then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))) =
  if (regs[↑k] == 0) = true then entryCfg (pc + 1) regs else entryCfg (pc + 2) (regs.set (↑k) (regs[↑k] - 1))
      simp [hz, hbeq]All goals completed! 🐙

2. Two-Part Decomposition of the Main Equivalence

Part I (Turing Machine ↔ Elementary Counterexample): The 744-state baseline machine riemann_744 (Machines.riemann744) halts on the blank tape if and only if there exists an integer x satisfying MatiyasevichRiemannCounterexample x.

theorem halts_riemann744_iff_exists_counterexample :
    ConjectureMachines.Halts Machines.riemann744 ↔ ∃ x : ℕ, MatiyasevichRiemannCounterexample x :=
  halts_reference_iff_regHalts_unconditional.trans regHalts_iff_exists_counterexample

The 744-state baseline machine riemann_744 (Machines.riemann744) halts on the blank tape if and only if the Riemann Hypothesis is false.

theorem halts_riemann744_iff_not_riemannHypothesis :
    ConjectureMachines.Halts Machines.riemann744 ↔ ¬ RiemannHypothesis :=
  halts_riemann744_iff_exists_counterexample.trans exists_counterexample_iff_not_riemannHypothesis

end ConjectureMachines.Semantics.Riemann

Semantics of the 744-State Riemann Hypothesis Turing Machine (riemann_744)

Provenance and Attribution

Architecture

2. Two-Part Decomposition of the Main Equivalence

Semantics of the 744-State Riemann Hypothesis Turing Machine (`riemann_744`)