Back to record ledger
Kernel verified

Certified critical-line bound 0.673429810000000000000000000000

Seven-point weighted refinement with a jointly optimised window: v(s) = cos(sqrt2 s) + sum_{j=1}^{12} c_j cos(2 pi j s), the c_j chosen together with the seven-point weights to maximise (H_W - B mu)/(1 - c mu) (typh). H_W >= 0.6721710925, B = 398386/10^8, c = 787320/10^8 within 0.01% of the minimum, m = 133. Theorem D for the window and the AM kernel evaluator are attempt-012's, the six-gap engine instance attempt-010's (Samuel Lavery, Apache-2.0), re-proved for the new coefficients, with a kernel-cheaper evaluator (same values) and faster soundness proofs; the certificate data (pyramid, derivative and point tables, convex regions, basins, walk: 72455 leaves) regenerated by typh. Proved constant >= 0.6734298129, candidate 67342981/10^8.

Certified lower bound67.3429810000%κ = (67342981 : ℝ) / 100000000
Record evidence

typh