Per-zero exclusion bounds free of assumptions on the zeros above the band, sharpened by a formally verified zero-free half-plane

A positive value λ of the Weil quadratic form, truncated to the window [−h,h], h=½log13, evaluated at its pole-conditioned minimiser and computed on the geometric side independently of the zeros, is converted into a bound |Re ρ_k − ½| ≤ δ*_k for individual zeros of ζ(s), with no assumption on the location of the infinitely many zeros above the band; the other in-band zeros enter at their on-line ordinates (Platt–Trudgian). We feed into the envelope of the explicit formula the zero-free half-plane Re s > 7/8 of OpenAI (2026), whose Lean formalisation we compiled independently from a fresh clone and audited (7 061 modules; axioms propext, Classical.choice, Quot.sound only; negative control detected). The admissible width drops from 1/2 to 3/8, the envelope factor from 13.21 to 6.04, and every bound tightens by the factor 1.501. In the cell q=13, Ω=75.55, d=21: |Re ρ₁ − ½| ≤ 3.50×10⁻¹⁹, |Re ρ₅ − ½| ≤ 9.93×10⁻¹⁵, |Re ρ₁₀ − ½| ≤ 4.31×10⁻¹⁰, |Re ρ₁₈ − ½| ≤ 5.74×10⁻³, under two explicitly stated computational hypotheses (A) and (E); condition (C2) is computed at 120 digits. The cost of independence from the zeros above the band falls from 4.36 to 2.90. To our knowledge this is the first use of a formally verified zero-free region as an input to a finite positivity certificate. Files: English version (kosulsuz_v04_en.pdf) and Turkish version (kosulsuz_v04_tr.pdf), identical content.