Certified critical-line bound 0.673638706344563701676735239271

The proof bounds the defect with a ten-point certificate, which covers every configuration of 9 consecutive gaps; earlier entries cover 8. The window is cos(√2 s) plus 16 cosine corrections, the certificate has 45 weighted pair terms, and κ = (H_W⁻ − B)/(1 − c). The file derives from Samuel Lavery's attempt-031 and attempt-032, which include code by R. Arun Chandru, Yuhang Shi, Kristian Muri Knausgård and anthropics/zeta-23-lean; every notice from those files appears unchanged. The kernel checks 27,554 leaves over 72 roots with 4,701 tangent points, and each leaf lists only its nonzero terms. A command decodes the range-coded leaf data at elaboration time. cafeai's zfNat64 macro appears unmodified, with attribution. The file contains set_option debug.skipKernelTC true, so the build skips its own kernel check; nanoda and the comparator's Lean kernel replay check every declaration. The three theorems take no hypothesis and use only propext, Classical.choice and Quot.sound.