Formalizing Weil's Explicit Formula and Positivity Criterion for the Riemann Hypothesis in Lean

We present a Lean formalization of Weil’s explicit formula and positivity criterion for the Riemann hypothesis on a specified class of complex-valued functions with finitely many exceptional points and exponential decay. The zero functional is an unconditional sum over distinct zeros of the completed xi-function, with analytic multiplicities included once. The arithmetic functional is defined independently through pole, prime-power, and compensated archimedean terms. We establish the necessary integrability and summability results and transfer the explicit formula along one smooth, compactly supported approximation sequence. Uniform weighted derivative bounds include jump contributions and require no convergence of derivatives. For the converse criterion, a polynomial–Gaussian construction realizes a negative witness in the original test class whenever an off-critical-line zero exists. A summable majorant is fixed before the Gaussian width is chosen, so that an explicit finite parameter makes the negative main term dominate the entire zero sum. Alignment with Mathlib’s original Riemann hypothesis and a final value-identity bridge yield an arithmetic-side positivity criterion. We give source correspondence and distinguish the scopes of Lean compilation, separate-implementation checking, and model-assisted review. The result formalizes a classical equivalence; it establishes neither universal positivity of the functional nor the Riemann hypothesis itself. This record contains the preprint, Online Resource 1 (ESM_1.pdf), and the source and evidence collection (ESM_2.zip). Author-owned manuscript and documentation materials are licensed under CC BY 4.0. Author-owned original code is licensed under Apache-2.0. Third-party materials retain their original licenses and notices. The file-level scope is specified in LICENSE_SCOPE.txt and LICENSE_SCOPE.json. The source collection supports inspection and correspondence with the accepted artifacts; it is not presented as a newly tested turnkey build.