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 interval $\tfrac{1}{2}\log 2 < L < \tfrac{1}{2}\log 3$, the first-prime window where only the prime $n = 2$ contributes to the explicit formula. Our main technical contribution () 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 $\mathbb{Q}[\tau]$ and are computable without numerical quadrature. We also prove a pure-rational absorption certificate (): $V + P_{2,7/20} \ge \tfrac{69}{100}V \ge 0$, with the key step $87^{16}\cdot 68^5 < 1701^5\cdot 32^{16}$ verified in Lean 4/Mathlib (integer comparisons via native_decide; transcendental bounds $\log 2 < 7/10$ and $\sqrt{2} > 7/5$ via Real.sum_le_exp_of_nonneg and Real.sqrt_lt_sqrt; the Arb-certified integral in is independent of the Lean formalisation). We give an exact spectral description of $C_{b,L}$ (), falsify Path A by explicit certified negative witnesses (), and identify the spectral mechanism: the Weil constant $c_L \approx 1.36527$ acts as a global negative diagonal shift that Path A cannot overcome, whereas without it the $\{P_0,P_2\}$ subspace is positive definite (). We also correct an error in an earlier draft that attributed the obstruction to an edge-mass asymptotic: the companion formula $\langle K_LP_0,P_2\rangle \sim c_2/\kappa_e(L)$ fails by a factor of $40$ inside the first-prime window, invalidating the proposed flip-point formula $\theta_0 = 1 - c_2/\kappa_e$ (). We prove the Path B Schur criterion () with the same certified Weil constant (derived from Suzuki \cite{Suzuki2026} equation (4.5); see (ii)). Finally, gives the finite-dimensional Schur reduction needed for FP-0.35 and records the numerical margins produced by the public Arb computation. In the present audit-safe revision, the repository's historical "residual = 0" accumulator is not treated as a rigorous interval-norm certificate: a strict outward upper bound (or an interval $LDL^{\mathsf T}$/Cholesky inertia certificate) is still required before the computational step can be promoted to an unconditional proof of FP-0.35. This paper therefore does not claim that the Riemann Hypothesis, or even positivity beyond the certified algebraic reductions, follows from the recorded pilot output.