Certified critical-line bound 0.673638842664358872953956820071
Kristian Muri Knausgård's contribution: improves the terminal H_W lower bound of 贝奕 (Bei Yi)'s beiyi-ten-strongcover-t014 (2026-11-01). Extends AMW.taylorN_F using Complex.exp_bound (n := 36; cosine/sine degrees 34/35). Tightens rational bounds for sqrt(2)/2, cos(sqrt(2)/2), sin(sqrt(2)/2), and H_W from denominator 10^42 to 10^50; propagates the floor through dyadic and cumulative counts. Window coefficients, certificate data, tree and checker are unchanged. κ gain over predecessor: ~5.04e-42.
Builds on Rishi Khan (TEN), Samuel Lavery/team (OpethN; am-cert/bridge-port), R. Arun Chandru (master-of-puppets), Yuhang Shi, AMTOPA, Zeta Lab, Anthropic (Zeta23), ajp88, typh and cafeai/Zero Forge.
Also reuses Knausgård's Lean work for arXiv:2610.08965 (github.com/kristianmk/839): card_near_le/Simple673, Distinct839 matching labels, the real-form eigenvalue lemma, and adapted Poisson/sum-of-squares steps. All upstream notices retained.