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

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 + P2,7/20 >= (69/100)*V >= 0, machine-verified in Lean 4/Mathlib. We give an exact spectral description of Cb,L (Theorem 3.1), falsify Path A by explicit certified negative witnesses (Theorem 6.1), and identify the spectral mechanism: the Weil constant c_L ≈ 1.36527 acts as a global negative diagonal shift that Path A cannot overcome, while without it the {P_0, P_2} subspace is positive definite (Remark 6.2). We also correct an error in an earlier draft: the companion asymptotic for the off-diagonal entry K_L fails by a factor of 40 at L=7/20, invalidating the proposed flip-point formula theta_0 = 1 - c_2/kappa_edge inside the first-prime window (Remark 6.3). We prove the Path B Schur criterion (Theorem 5.3) and establish FP-0.35 (Theorem 7.3): lambda(7/20) > 0, using 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). These results do not imply the Riemann Hypothesis. Supporting code and 124 automated tests at https://github.com/telleroutlook/weil-first-prime v1.8 (2026-08-15): Lean 4 formalisation extended. Seven new machine-verified theorems added to WeilFirstPrime/Theorem3.lean (total 20): (1) log3_gt_seven_tenths: 7/10 < Real.log 3, via Real.exp_one_lt_three. (2) first_prime_window_check: Real.log 2 / 2 < 7/20 < Real.log 3 / 2, machine-verifying L=7/20 lies in the first-prime window. (3-5) tau2_pos, tau2_lt_one, tau2_bounds: 0 < tau_2 < 1 where tau_2 = (log 2)*(10/7) is the prime-2 shift at L=7/20. (6) tau3_gt_one: tau_3 = (log 3)*(10/7) > 1. (7) single_active_prime: tau_2 < 1 < tau_3, machine-verifying that p=2 is the ONLY active prime at L=7/20 (justifying the "first-prime window" label). Build: 3107 Lean jobs, zero errors. No overfull hbox warnings in LaTeX (5 fixed). No change to any theorem, certificate, or mathematical conclusion.