A finite irrationality measure for Catalan's constant

Let G be Catalan's constant. We prove that, for every sufficiently largepositive integer q and every integer p, the absolute difference between Gand p/q exceeds q to the power −100,000,000. Consequently, its irrationalityexponent satisfies 2 ≤ μ(G) ≤ 100,000,000. We extend OpenAI's determinant proof of the irrationality of G by boundingevery complementary minor uniformly in its size and selected indices.Rectangular Hardy-space estimates and real-polynomial coefficient boundscontrol the selected determinants. A node-padding argument transfers thefull-size energy estimates to smaller dimensions, with a loss exponentialin the product of the ambient dimension and the codimension. Uniformdenominator estimates and nonvanishing at prime scales logarithmic in theapproximation denominator then yield the stated bound. Theirrationality-exponent bound and its supporting estimates are formalizedin Lean. The exponent is not optimized. This record contains the manuscript PDF, its LaTeX sources, and the Leanformalization with pinned dependency versions and reproduction instructions.