A Numerical Test of the Quadratic Estimate in arXiv:2609.04176v1

Bilar, Daniyel Yaacov · 2026-09-18 · publication/preprint · cc-by-4.0

Version of record (canonical): https://doi.org/10.5281/zenodo.22830611
Concept DOI (always latest PDF): https://doi.org/10.5281/zenodo.22830610
Download PDF (Zenodo): open
Companion software: 10.5281/zenodo.22830201 (catalog)
OSF mirror: osf.io/yhf8t
Sketchnote for PAPER1 v1.4.0: Sun arXiv:2609.04176v1 Theorem 9.1 chain through (3.5), (5.13), (5.24); measured B-squared coefficient about +1.85 versus required at most -0.0097; two gaps including v2(F_B) log 2 and Remark 9.3 constant 221 times too small; companion Lean software DOI

Sketchnote for v1.4.0 (CC BY 4.0). Full-size PNG.

Abstract

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. Evaluating the preprint's own chain through equations (3.5), (5.13) and (5.24) at B = 200, 400, 800, 1000, 1200 yields a positive B2 coefficient converging near +1.85, where the chain needs a value below −0.0097. Because (5.24) bounds the height from above, this refutes the proof route rather than the rationality assertion. Companion Lean 4 formalization of structural lemmas from Sections 2–5: 10.5281/zenodo.22830201. Source: github.com/chokmah-me/catalan-sun-lean. This record is the paper PDF only.

Keywords

Catalan's constant · irrationality · numerical verification · arXiv:2609.04176 · quadratic estimate · Lean 4 companion

← All research