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), encoding the coupling between the prime-2 layer and the Legendre basis, 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, with the key step 87^16 * 68^5 < 1701^5 * 32^16 (41-digit integers) machine-verified in Lean 4/Mathlib via native_decide and Real.sum_le_exp_of_nonneg. We give an exact spectral description of the truncated shift operator C_{b,L} (Theorem 3.1), falsify Path A by explicit certified negative witnesses (Theorem 6.1), and provide a conditional Path B Schur criterion (Theorem 5.3). All results are independent of the main conjecture FP-0.35 (lambda(7/20) > 0) and do not imply the Riemann Hypothesis. Supporting code, Lean 4 formalisation, and 123 automated tests are available at https://github.com/telleroutlook/weil-first-prime Version 1.1: typesetting corrections (abstract/maketitle ordering fix; hyperref link color update). No mathematical content changed.