A Lean 4 Formalization of Theta-Hankel Spectral Theory: Complex-Scale Exclusion and Quadratic Jensen Hyperbolicity

This paper presents a Lean 4 formalization built from the differential theta kernel of the Riemann xi function. First, a certified Rayleigh estimate yields a quantitative spectral obstruction: the spectral product of a theta-Hankel adjoint square cannot equal normalized xi under any constant complex rescaling. Second, certified moment bounds establish M₀M₄ < 3M₂² and factor the degree-two, zero-shift Jensen polynomial J2,0 into two distinct real linear factors. A partition into 1600 rational cells, explicit exponential bounds, and analytic tail estimates proves the quantitative gap 3M₂² − M₀M₄ ≥ 4287/10⁸. The complexified polynomial has exactly these two real roots. The development also establishes an entire theta-Jensen generating function and formalizes the equivalence between exclusion of its non-real zeros and Mathlib’s RiemannHypothesis. This is a formal reduction, not a proof of RH; global non-real-zero exclusion remains unproved. The final theorem dependency audits report only propext, Classical.choice, and Quot.sound, with no sorryAx. All three release audit workflows passed on Linux and Windows, including final theorem dependency and tracked-source checks. The Lean sources are archived as release v1.0.0 at https://doi.org/10.5281/zenodo.23287564, corresponding to commit dbb6bd2447296cab184d7bb457054c6efec6207d.