1. Cryptids
  2. Semantics
  3. Riemann120
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.Riemann104 public import Cryptids.Semantics.Riemann120.VonMangoldt public import Cryptids.Semantics.Riemann120.Bridge

Halting Equivalence for riemann120 and riemann104

This module connects all layers of the formalization of Joseph M. Shunia's 120-state, 2-symbol Turing machine (riemann120, arXiv:2609.30306, September 2026) and its 104-state reduction (riemann104) into the complete end-to-end equivalences:

    Halts riemann120 ↔ ¬ RiemannHypothesis

    Halts ConjectureMachines.Riemann104.candidate ↔ ¬ RiemannHypothesis.

@[expose] public sectionnamespace ConjectureMachines.Riemann120open Turing ConjectureMachinestheorem quarterClock_eq_quarterClockStep : ∀ z : ℕ, VonMangoldt.quarterClock z = Riemann120Analytic.quarterClockStep z ⊢ VonMangoldt.quarterClock 0 = Riemann120Analytic.quarterClockStep 0 ⊢ VonMangoldt.quarterClock 0 = Riemann120Analytic.quarterClockStep 0 All goals completed! 🐙 z:ℕ⊢ VonMangoldt.quarterClock (z + 1) = Riemann120Analytic.quarterClockStep (z + 1) z:ℕ⊢ VonMangoldt.quarterClock (z + 1) = Riemann120Analytic.quarterClockStep (z + 1) z:ℕ⊢ 1 + VonMangoldt.quarterClock (z / 4) = 1 + Riemann120Analytic.quarterClockStep (z / 4) All goals completed! 🐙theorem halts_riemann120_iff_not_riemannHypothesis : Halts riemann120 ↔ ¬ RiemannHypothesis := ⊢ ConjectureMachines.Halts riemann120 ↔ ¬RiemannHypothesis ⊢ RiemannHypothesis → ∀ (n : ℕ), 21845 < n → ↑n - Chebyshev.theta ↑n ≤ (↑(Riemann120Analytic.quarterClockStep (n - 1)) + 1) * 2 ^ Riemann120Analytic.quarterClockStep (n - 1) * Real.log ↑n hRH:RiemannHypothesisn:ℕhn:21845 < n⊢ ↑n - Chebyshev.theta ↑n ≤ (↑(Riemann120Analytic.quarterClockStep (n - 1)) + 1) * 2 ^ Riemann120Analytic.quarterClockStep (n - 1) * Real.log ↑n hRH:RiemannHypothesisn:ℕhn:21845 < nhlt:↑n - Chebyshev.theta ↑n < (↑(VonMangoldt.quarterClock (n - 1)) + 1) * 2 ^ VonMangoldt.quarterClock (n - 1) * Real.log ↑n⊢ ↑n - Chebyshev.theta ↑n ≤ (↑(Riemann120Analytic.quarterClockStep (n - 1)) + 1) * 2 ^ Riemann120Analytic.quarterClockStep (n - 1) * Real.log ↑n hRH:RiemannHypothesisn:ℕhn:21845 < nhlt:↑n - Chebyshev.theta ↑n < (↑(Riemann120Analytic.quarterClockStep (n - 1)) + 1) * 2 ^ Riemann120Analytic.quarterClockStep (n - 1) * Real.log ↑n⊢ ↑n - Chebyshev.theta ↑n ≤ (↑(Riemann120Analytic.quarterClockStep (n - 1)) + 1) * 2 ^ Riemann120Analytic.quarterClockStep (n - 1) * Real.log ↑n All goals completed! 🐙end ConjectureMachines.Riemann120namespace ConjectureMachines.Riemann104.Semanticsopen ConjectureMachines

The 104-state record machine riemann_104 (ConjectureMachines.Riemann104.candidate) halts on the blank tape if and only if Mathlib's RiemannHypothesis is false.

theorem halts_candidate_iff_not_riemannHypothesis : Halts ConjectureMachines.Riemann104.candidate ↔ ¬ RiemannHypothesis := ConjectureMachines.Riemann104.candidate_equivalent.trans ConjectureMachines.Riemann120.halts_riemann120_iff_not_riemannHypothesisend ConjectureMachines.Riemann104.Semanticsend