Sturm–Liouville Eigenvalue Simplicity and a Spectral Assumption Interface in Lean 4: The Messina Nullification Framework

This deposit contains the AFM submission for "Sturm–Liouville EigenvalueSimplicity and a Spectral Assumption Interface in Lean 4: The MessinaNullification Framework" (Joseph Messina, 2026), submitted to the Annalsof Formalized Mathematics. The paper presents two Lean 4 / Mathlib contributions: 1. A standalone formalization of Sturm–Liouville eigenvalue simplicity for confining potentials, proved via a Wronskian / L²-decay argument. The capstone theorem `sturmₗiouvilleₛimpleₑigenvalues` is independent of any number-theoretic application and is offered as a reusable Mathlib infrastructure contribution. 2. A modular spectral-assumption interface for the Riemann Hypothesis and Simple Zeros Conjecture. Building on the Loeffler–Stoll formalization of the Riemann zeta function, the paper expresses RH and Simple Zeros as conditional consequences of two explicitly named hypotheses (a spectral gap on the shifted zero spectrum, and a multiplicity bound). All classical analytic ingredients are supplied by Mathlib. The single remaining open identification step — the Hilbert–Pólya correspondence — is isolated as a named context structure HPContext, separating object identification from operator identification, so that future Mathlib developments can discharge each component independently. A constructive mechanism, the leveling trick, demonstrates that aspectral gap at Δ = 1/2 forces every nontrivial zero of ζ onto thecritical line via an algebraic squeeze: the deviation Re (ρ) − 1/2 liesin a set with the gap property and is bounded in absolute value by 1/2from the critical strip, so it must equal zero. INDEPENDENT KERNEL VERIFICATION The load-bearing algebraic content of every paper section has beenindependently kernel-verified by AXLE (Axiom Lean Engine, https: //axle. axiommath. ai), in the lean-4. 28. 0 environment. VerificationIDs: Section 2. 1 (masterₑnforcement) e0755420-c907-4578-8f2f-ab59d002ed52 Section 4 (sturmₗiouvilleₛimpleₑigenvalues, architecture) da53f7a2-78f9-446d-9dda-a130631e6994 Section 5 (levelingₜheorem, levelingᵢmpliesᵣeₕalf) 376a6860-4bb2-4d3d-a461-cce659917ee6 Section 6 (resolutionfromₜhreeₐxioms and corollaries) 5ac337c1-6c9d-4390-bcaa-42c626f75582 Earlier audit batch (AXLE): 22abc227, 572b70d1, c133ead0, 3de41f1f, f854b8e9, 01ae8bf9 The four STATEMENT/CONTENT pairs that were submitted to AXLE areincluded in this deposit (axleₚairs/) so reviewers can re-run theverifications independently via the AXLE web console. CONTENTS messinaₙullificationAFMᵥ7. pdf Main paper (21 pages) messinaₙullificationAFMᵥ7. tex LaTeX source messinaAFMₛubmissionₚackage. tar. gz Full code artifact: - leanfiles/ (14 Lean files, the corpus referenced by the paper) - axleₚairs/ (8 AXLE-ready Lean files + verification guide) - experimentalcompanion/ (IBM circuits + replication guide for §B) - lakefile. lean, lean-toolchain (pinned environment) - preₛubmissioncheck. sh (build verification script) - README. md (file-to-section map) PINNED ENVIRONMENT Lean: leanprover/lean4: v4. 24. 0 Mathlib commit: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 COMPANION DEPOSITS Volume 1 — Core Operator Library: 10. 5281/zenodo. 18902403 Volume 2 — RH and Analytic Number Theory: 10. 5281/zenodo. 18902325 CODE ARCHIVE Software Heritage ID: swh: 1: dir: bccceead57529b29b6c04136107654357e9da11f;origin=https: //github. com/Joeyxyxyz/MessinaNullificationFrameworkRHAFM;visit=swh: 1: snp: 8acb06dea0b7d5d30e18da780871dfe707907c38;anchor=swh: 1: rev: 3c9ed2bf4465d3d1d85706d917a9202bc209cd3b GitHub: https: //github. com/Joeyxyxyz/MessinaNullificationFrameworkRHAFM