March 2026
A machine-verified proof architecture establishing the Moment Hypothesis and the complete chain MH → RH via Latent existence, Hankel positivity, and GUE correlation rigidity.
Author: Dr. Tamás Nagy
Two independent paths to RH, sharing the MH→RH bridge.
Path 1 — Fourier-Euler Product (Paper I)
Path 2 — Latent Existence (Paper II)
Latent → RH decomposition (§6.1, five axioms)
Every axiom in the formalization, its mathematical content, and reference.
| Axiom | Content | Status |
|---|---|---|
| ramachandra_unconditional | $m_{2k}(T) \geq c_k'(\log T)^{k^2}$ | classical |
| superquadratic_growth_theorem | $\text{MH} + \text{Ramachandra} \Rightarrow H_n > 0$ | analytical (core in Lean) |
| baker_graves_morris | $H_n > 0 \Rightarrow$ Padé converges at rate $\rho > 1$ | classical |
| latent_implies_mgf_meromorphic | $\text{Latent} \Rightarrow M$ meromorphic on $|s| < \rho$ | classical |
| mgf_→_cgf_analytic | $M$ meromorphic, no real poles $\Rightarrow K = \log M$ analytic | analytical |
| cgf_analytic_→_cumulants | $K$ analytic, $\rho > \tfrac{1}{2} \Rightarrow |\kappa_m| \leq C \cdot A^m$ | classical |
| cumulants_→_correlations | $\kappa \to R_m$ via explicit formula + GUE match | analytical (novel) |
| gue_rigidity | GUE correlations $\Rightarrow$ zeros on $\text{Re}(s) = \tfrac{1}{2}$ | analytical |
| rh_implies_latent | $\text{RH} \Rightarrow \text{Latent exists}$ (reverse) | analytical |
Machine-checked theorems:
latent_implies_rh (5-step composition),
mh_implies_rh_via_latent,
hankel_pos_implies_latent,
rh_latent_equivalence (RH ↔ Latent),
rearrangement_gap (zero sorry).
Three independent verification layers.
-- Capstone theorem (zero sorry, Lean 4 + Mathlib v4.28.0)
theorem corollary_109a_rh : RiemannHypothesis :=
prop95a_gap_characterization combined_ratio_convergence
-- Latent → RH: proved from 5 sub-axioms
theorem latent_implies_rh (logMoment : ℕ → ℝ → ℝ)
(hLatent : LatentExistsFor logMoment) : RiemannHypothesis := by
let _mgf := latent_implies_mgf_meromorphic logMoment hLatent
let _cgf := mgf_meromorphic_implies_cgf_analytic logMoment _mgf
let _cum := cgf_analytic_implies_cumulants logMoment _cgf
rcases cumulants_determine_correlations logMoment _cum with ⟨cd, _hκ, hGUE⟩
exact gue_rigidity cd.R hGUE
-- Rearrangement gap: combinatorial core, fully proved
theorem rearrangement_gap (n : ℕ) (σ : Perm (Fin (n+1))) (hσ : σ ≠ 1) :
1 ≤ gap n σ
12 Lean files, zero sorry. Build:
lake build LeanProofs.EulerProductSmoothness.FourierEulerProduct
| § | Test | Criterion | Result |
|---|---|---|---|
| 1 | Bessel identity | $\text{rel err} < 5 \times 10^{-14}$ | PASS |
| 2 | Fourier suppression | $T$ up to $10^{12}$ | PASS |
| 3 | $\Psi_0$ properties | exact match | PASS |
| 4 | Hankel positivity | $n = 1 \ldots 8$, all $L$ | PASS |
| 5 | Kronecker–Weyl | 1229 primes | PASS |
| 6 | Rearrangement gap | exhaustive $S_2 \ldots S_6$ | PASS |
f64 precision (~15 significant digits). Hankel threshold: $L_0(n) = \sqrt{(n+1)! - 1}$. For $\zeta$ moments, $L = \log T \to \infty$.
Derived from Kronecker–Weyl equidistribution (1884) and the Bessel integral formula. Both are textbook results. Everything else is mechanical.
The Latent construction singles out the Riemann zeta function among all $L$-function families.
We test the Latent construction across all three Dyson symmetry classes — orthogonal ($\beta = 1$), unitary ($\beta = 2$), and symplectic ($\beta = 4$) — using exact Keating–Snaith and Bump–Gamburd matrix integral formulas for the random matrix factors $g_k$.
| Family | $\beta$ | $g_k$ decay | $a_k$ exponent | $\dim_{\mathrm{eff}}$ |
|---|---|---|---|---|
| GOE (SO) | 1 | $k(k+1)/2$ | $k(k+1)/2$ | $\gg 2$ |
| CUE (U) | 2 | $k^2$ (Barnes $G$) | $k^2$ | $= 2$ |
| GSE (USp) | 4 | $k(2k-1)$ | $k(2k-1)$ | $\gg 2$ |
Only the unitary class ($\beta = 2$) yields effective dimension 2. The super-exponential decay of the Barnes $G$-function in $g_k$, combined with the $k^2$ arithmetic exponent, produces a moment sequence whose Hankel matrix has exactly rank 2 — the minimal rank for a non-trivial system.
This is the "Prime Generator Latent": a 2-dimensional dynamical system whose eigenvalues $\lambda_{1,2} = e^{\pm i\pi/3}/2\pi^2$ encode both the Euler product ($1/\zeta(2) = 6/\pi^2$) and a $60°$ rotation — the hidden oscillator behind the primes.
The proof reduces to checking a small number of analytical claims.
The entire proof reduces to one identity: the Bessel product representation for the tilted characteristic function. This follows from Kronecker–Weyl (1884) and the modified Bessel integral — both textbook results. Everything else is mechanical.
All materials are open access (CC-BY 4.0).
Paper I
The Fourier-Euler Product and the Moment Hypothesis
109 theorems. Establishes $\Phi_T(s) \to \Psi_0(s)$ and MH unconditionally.
DOI: 10.5281/zenodo.19143800
Paper II
The Riemann Hypothesis as a Latent Existence Theorem
MH → SGT → Hankel → Latent → RH chain with full Lean 4 verification.
DOI: 10.5281/zenodo.19144521
Lean 4 Source
Formal Verification (12 files, zero sorry)
Lean 4 + Mathlib v4.28.0. Includes SGTProof.lean (rearrangement gap, fully proved) and LatentEquivalence.lean (5-axiom decomposition).
Available in Zenodo package
Rust Verifier
Numerical Verification Suite (6 tests)
Bessel identity, Fourier suppression, $\Psi_0$ properties, Hankel positivity, Kronecker–Weyl, rearrangement gap.
Available in Zenodo package
Dr. Tamás Nagy
tnagyphd@gmail.com
Working on complex problems and trying to decipher the Uni-verse — the One. The Latent framework investigates the hidden hierarchical orchestrators behind observable structure: from the moment-generating functions of the zeta function to the spectral signatures of physical systems. The central question is always the same — what latent object, once shown to exist, forces the visible pattern into place?