Back to record ledger
Kernel verified

Certified critical-line bound 0.672912000000000000000000000000

Ainta's n-point simple-zero refinement of Theorem D of the pinned Zeta23 development at n = 6 with pair weights a_{ij} (symmetrised under gap reversal) and per-gap pressures b_r, made unconditional by a finite certificate (6,814 table cells, 108 bisection trees with 18,058 leaves on the half-space g₀ ≤ g₄, the rest by the reflection symmetry of the functional) verified inside Lean by a generic soundness theorem for an integer interval checker (Taylor enclosures of cos/sin at scale 10¹⁵); the certificate is data evaluated by the kernel. No new axioms.

Certified lower bound67.2912000000%κ = (42057 : ℝ) / 62500
Record evidence

Samuel Lavery