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

Companion repository to the paper. The paper studies the modular generator D_∞ = -i · ∂_t log Δ of the Bost-Connes type III_1 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_of_ccm_galerkin (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_zero_existence citing Rouché 1862 and collectively_compact_resolvent_uniform_bound 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.