What this does NOT prove: the lower bound. That stays White's published μ ≥ 0.379005 (a preprint reports a certified 0.37912). I also retracted my own informal μ ≥ 0.380827 claim — solver-optimal ≠…