What question did this study set out to answer?

The research aims to study the Bost-Connes modular generator as a candidate for a Hilbert-Pólya operator and explore its implications regarding the Riemann Hypothesis.

June 28, 2026Open Access

The Bost-Connes Modular Generator as a candidate Hilbert-Pólya Operator, formalized in Lean 4

Key Points

The research aims to study the Bost-Connes modular generator as a candidate for a Hilbert-Pólya operator and explore its implications regarding the Riemann Hypothesis.
Constructed a Galerkin approximation chain to approximate the spectra of the modular generator D∞.
Developed a structured type, CCMGalerkinSpectralData, recorded in Lean 4 to package Galerkin-side ingredients.
Verified the relationship between inhabiting CCMGalerkinSpectralData and the Riemann Hypothesis through a computer-verified terminal process.
Demonstrated that inhabiting CCMGalerkinSpectralData is equivalent to the Riemann Hypothesis.
Establish a Galerkin-side chain that specifies necessary conditions without constructing CCMGalerkinSpectralData terms.
Provided literature-based full per-axiom disclosure in support of the research findings.

Abstract

Companion repository to the paper. The paper studies the modular generator D_∞ = -i · ∂ₜ log Δ of the Bost-Connes type III₁ factor at the critical KMS state (β = 1), acting on the GNS Hilbert space, as a candidate Hilbert-Pólya operator. We construct a Galerkin approximation chain whose spectra approximate that of D_∞ in the sense made precise by Bögli-Siegl-Tretter spectral exactness, and package the resulting Galerkin-side ingredients into a single named structured type, CCMGalerkinSpectralData, recorded in Lean 4 against a pinned Mathlib revision. The principal result is a transparent conditional reduction: inhabiting CCMGalerkinSpectralData is equivalent to the Riemann Hypothesis. This work does not claim a closure of the Riemann Hypothesis — no term of CCMGalerkinSpectralData is constructed in the formalization; the Galerkin-side ingredients required for inhabitation are explicitly named in the gate's type-level fields. The chain's canonical terminal HilbertPolyaBostConnes. rhₒfccmgalerkin (g: CCMGalerkinSpectralData): RiemannHypothesis is computer-verified against Mathlib's formal statement of the Riemann Hypothesis. The named-axiom budget is closed against literature: 8 CCM-substrate-own atomic axioms (of which 2 — roucheᵦeroₑxistence citing Rouché 1862 and collectivelycompactᵣesolventᵤniformbound citing Anselone 1971 + Stummel 1970 — appear in the canonical terminal's #print axioms closure; 6 are off-terminal background substrate) plus 6 TT-upstream-inherited axioms via Lake-dep on the companion Tomita-Takesaki substrate. Each axiom carries a literature citation whose published proof does not invoke the Riemann Hypothesis; full per-axiom disclosure is in the companion axioms-disclosure. md document, with the bibliography in references. tex. Companion Lean 4 formalization: localparty/hilbert-polya-bost-connes-lean (v0. 1 release, commit 6d29ee6; Mathlib SHA 5e932f97dd25535344f80f9dd8da3aab83df0fe6; Lake-dep on tt-bost-connes-lean v0. 2, Zenodo DOI 10. 5281/zenodo. 20674891). During the preparation of this work, the author used Claude Opus 4. 7. The author reviewed all content and takes full responsibility for the paper.

Read Full Paperexternally

Ask AI

Helpful

Bookmark

View Full Paper