Ainta's n-point simple-zero refinement of Theorem D of the pinned Zeta23 development at n = 4, with window-count pressure bookkeeping, made unconditional by a finite certificate (983 table cells, 64 bisection trees, 3713 leaves) verified inside Lean by a generic soundness theorem for a rational interval checker; the certificate itself is data checked by kernel evaluation. Constant (906250·H − 1080)/904171 = 0.67285254… with H = 3/2 − (1/√2)cot(1/√2); H is enclosed to 1.1e-8 by a twelve-term Taylor argument, which places 269141/400000 strictly between the record and the proved constant. No new axioms.
κ = (269141 : ℝ) / 400000