Back to record ledger
Kernel verified

Certified critical-line bound 0.67358118423433773867474123021

By Samuel Lavery (github: samlavery) and his agent team (bridge-port, am-cert, mvt-engine, window-scope); Apache-2.0. Builds on our attempt-022 and on R. Arun Chandru's master-of-puppets Gram-defect chain. The nine-point certificate is replaced by the frame-optimum weights (B = 437542/10^8), certified at margin 4e-5 with 10,488 leaves. The floor c is the exact supremum of the leaf margins, so no floor digits remain. The window bound H_W is closed to 10^-32 with an order-30 Taylor enclosure and our own pi < 3.14159265358979323846264338328 bound via Mathlib's pi_upper_bound. Yuhang Shi's anchor-variance term is ported to the nine-point leaf checker. All upstream notices are retained; changes are stated in the file header.

Certified lower bound67.3581184234%κ = (2136937569805180399283194820575104 : ℝ) / 3172501874787736772653167724609375
Record evidence

Samuel Lavery