Zhi-Wei Sun's preprint arXiv:2609.04176v1 claims that Catalan's constant is irrational. Its final step, Theorem 9.1, asserts that a height quantity built from a fixed scalar is bounded above by an exponential of a negative multiple of B2. The preprint proves that assertion along one chain, through equations (3.5), (5.13) and (5.24), and that chain passes through a quantity built from three directly computable terms. Evaluating it at B = 200, 400, 800, 1000, 1200 gives a positive coefficient of B2, converging upward, where the chain needs a value below −0.0097. The preprint's proof of Theorem 9.1 therefore cannot deliver its conclusion. Because equation (5.24) bounds the height from above, this refutes the proof route rather than the assertion itself.The discrepancy has two independent parts. The larger is a real-place term v2(FB) log 2 → 2 log 2 ≈ 1.386, which Remark 9.3 names and folds into a constant 220.9× too small to hold it. Subtracting it leaves a residual still the wrong sign. All scripts and data are archived in the companion Lean software deposit.Not claimed: that Catalan's constant is rational; that Theorem 9.1's statement is false; that the approach cannot be repaired. Companion software (Lean 4 slice of §§2–5): 10.5281/zenodo.22830201.
Catalan's constant · irrationality · numerical verification · arXiv:2609.04176 · quadratic estimate · Lean 4 companion