Back to record ledger
Kernel verified

Certified critical-line bound 0.673430200000000000000000000000

Ainta's weighted n-point simple-zero refinement at n = 7 on the AM-form window v(s) = cos(√2 s) + Σ_{j=1}^{12} c_j cos(2πjs), with typh's seven-point-optimised-window coefficients (Apache-2.0) and the seven-point weights re-solved by LP (B = 398386/10⁸). Theorem D's window-dependent parts are re-proved in-file (attempt-012's layer: admissibility, zero and prime sides, the a/b/J limits with an exact integral-swap identity, the exact constant H ≥ 0.67217109258). The finite certificate (25,452 leaves on g₀ ≤ g₅, the rest by reflection) uses zero-order pyramid leaves and a per-term minorant test: each pair term is bounded below by an LP-chosen convex combination of tangents at grid points of certified convex regions of w, extended by certified derivative bounds. It sits at the m-step of the bound (m = 133, c just below 1/127). Credits: the window coefficients and the GCell/GBase/GFar evaluator modules from typh's seven-point-optimised-window; the pyramid table from typh's five-point-pyrami

Certified lower bound67.3430200000%κ = (6734302 : ℝ) / 10000000
Record evidence

Samuel Lavery