Structural Lemmas for the First-Prime Window of the Weil Quadratic Form

Abstract

We prove six structural results for the local Weil quadratic form Q_W^L on L^2(-L,L) in the first-prime window (half*log2 < L < half*log3), the minimal interval where only the prime n=2 contributes to the Weil explicit formula. Our main technical contribution (Theorem 5.1) is an algebraisation showing that the matrices J_ij(tau) and E_ij(tau) lie in Q[tau] and are computable without numerical quadrature. We also prove a pure-rational absorption certificate (Theorem 4.3): V + P_{2,7/20} >= (69/100)*V >= 0, machine-verified in Lean 4/Mathlib. We give an exact spectral description of C_{b,L} (Theorem 3.1), falsify Path A by explicit certified negative witnesses (Theorem 6.1), and prove the Path B Schur criterion (Theorem 5.3). In v2 (2026-08-06), we additionally establish FP-0.35 (Theorem 7.3): lambda(7/20) > 0. The proof uses the certified Weil constant c_L(7/20) = log(2*pi*7/20) + gamma_E (from Suzuki arXiv:2606.09096 equation (4.5), Arb 256-bit certified), and a mixed-precision residual certification verifying ||I - C_inv * C_arb||_inf = 0 for both parity sectors (even N=8, odd N=6). These results do not imply the Riemann Hypothesis. Supporting code and 124 automated tests at https://github.com/telleroutlook/weil-first-prime Version 1.5: Corrected the Schur-complement residual to use the complete second moment $S^{(0)} = S_{VV} + S_{VK} + S_{KV} + S_{KK}$ (v1.3–v1.4 inadvertently used $S_{KK}$ alone). The positive-definiteness conclusion is unchanged; the reported minimum eigenvalues are revised to $9.5\times10^{-4}$ (even) and $5.0\times10^{-2}$ (odd), with the even-sector margin now correctly shown to be small but strictly positive.