\documentclass[11pt]{amsart}
\IfFileExists{lmodern.sty}%
  {\usepackage[T1]{fontenc}\usepackage{lmodern}\usepackage{microtype}}%
  {\usepackage[expansion=false]{microtype}}
\usepackage{amssymb,mathtools}
\usepackage{booktabs,array}
\usepackage{enumitem}
\emergencystretch=2.5em
\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}

% ---------------------------------------------------------------------------
% Location of the Lean formalization.
\newcommand{\FormalizationURL}{https://github.com/slitsey/catalan-irrationality-measure}
\newcommand{\FormalizationLink}{\url{\FormalizationURL}}
% ---------------------------------------------------------------------------

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\numberwithin{equation}{section}

\newcommand{\Z}{\mathbb Z}
\newcommand{\Q}{\mathbb Q}
\newcommand{\R}{\mathbb R}
\newcommand{\N}{\mathbb N}
\newcommand{\cV}{\mathcal V}
\newcommand{\cR}{\mathcal R}
\newcommand{\cA}{\mathcal A}
\newcommand{\cI}{\mathcal I}
\newcommand{\cJ}{\mathcal J}
\newcommand{\lean}[1]{\texttt{#1}}

\begin{document}

\title{An irrationality measure for Catalan's constant}

\author{Sean Litsey}
\email{sean.litsey.math@gmail.com}

\date{October 16, 2026}

\subjclass[2020]{Primary 11J82; Secondary 11J72, 68V20}

\keywords{Catalan's constant, irrationality measure, irrationality exponent, determinants,
Andr\'eief identity, formal verification, Lean}

\begin{abstract}
Building on OpenAI's proof that Catalan's constant
$G=\sum_{j\ge0}(-1)^j/(2j+1)^2$ is irrational, we prove
$|G-a/b|>b^{-740}$ for every integer $a$ and every sufficiently large
integer $b$. Thus $\mu(G)\le740$. Using Chebyshev's estimates for final
prime selection gives $2\,220$; denominator and content asymptotics still use PNT.
The earlier bounds $759$, $2\,276$, $878$ and $2\,632$ remain proved.
We change the determinant parameters, obtaining a $20N$ matrix and a
polynomial of degree at most $18N$. Uniform physical prime-column pools and
sparse residue relations sharpen its common denominator. Exact energy
certificates and separate treatment of free, fixed and marked populations
give a uniform mixed-integrand bound. Stronger supplied energy trials,
central-gap quadrature and jointly paid atom weights control the same
determinant polynomial on $|x-G|\le e^{-(519037/5000)N}$.
An explicit uniform residue-kernel construction supplies additional common
coefficient content of quadratic logarithmic rate $16/63$. A further
lemma (Lemma~U3, derived by Claude with the author) adds content of
rate $1/3$ at the primes in $(8N,9N)$, and a column-block lemma (Lemma~U6,
derived by Claude with the author) adds content of rate $1/16$ at the primes
in $(4N,9N/2)$.
Coefficient divisibility recycles denominator prime squares; selecting the
largest prime with $p^2\nmid b$ completes the improved measure criterion.
We retain the earlier $48N$ construction and its $1\,981$ bound to explain
the methods. Every ingredient of the new global theorem is formalized in
Lean~4 with only the standard axioms and no unproved steps.
\end{abstract}

\maketitle

\section{Introduction}\label{sec:intro}

OpenAI \cite{OpenAI2026} recently proved that Catalan's constant
\[
 G=\sum_{j=0}^\infty\frac{(-1)^j}{(2j+1)^2}=0.91596\,55941\ldots
\]
is irrational, and formalized the proof in Lean. (An earlier claimed proof
\cite{Sun2026} was found to contain a gap \cite{Wachs2026}.) The argument is by contradiction:
under the hypothesis $G\in\Q$ an explicit determinant $\Delta_N$ of size $n=48N$ is a
nonzero rational number whose denominator is controlled prime by prime, so that
$\log|\Delta_N|\ge-(\mathsf A+o(1))n^2$; on the other hand a real-variable estimate gives
$\log|\Delta_N|\le-(\mathsf U-o(1))n^2$ with $\mathsf U>\mathsf A$. The margin is small:
$\mathsf U-\mathsf A\approx1.3\cdot10^{-4}$.
As OpenAI remarks, the argument proves qualitative irrationality; an irrationality measure
requires additional control of rational approximations.

Recall that the \emph{irrationality exponent} $\mu(\xi)$ of a real number $\xi$ is the
infimum of the $\mu$ such that $|\xi-a/b|>b^{-\mu}$ for all integers $a$ and all
sufficiently large $b$.

\begin{theorem}\label{thm:main}
For every integer $a$ and every sufficiently large integer $b$,
\[
 \left|G-\frac ab\right|>b^{-740}.
\]
In particular $\mu(G)\le740$. Using Chebyshev's bounds for final prime
selection gives the additional statement $|G-a/b|>b^{-2\,220}$.
The denominator and coefficient-content asymptotics still use PNT.
The earlier statements with exponents $759$ and $2\,276$ (Section~\ref{sec:u3}) and
$878$ and $2\,632$ (Section~\ref{ssec:gap878}) remain proved.
\end{theorem}

Theorem~\ref{thm:main}, together with every result in this paper, has been verified in the
Lean~4 proof assistant on top of OpenAI's formalization, with no unproved steps and only the
standard axioms; see Section~\ref{sec:formal}. The formalization is available at \FormalizationLink. The use of AI in this work is disclosed at the end of the paper.

\subsection{Previous results}
The first finite irrationality measure for $G$ was obtained by Jha \cite{Jha2026}, who proved
$\mu(G)\le10^8$, also with a Lean formalization built on OpenAI's. The present work was
carried out independently; we found Jha's preprint in a literature search after our proof was
complete. Both arguments have the shape that OpenAI's proof suggests: one replaces the
determinant by a polynomial in the constant, clears denominators, and needs a perturbation
estimate near $G$. They differ in the perturbation estimate. Jha bounds the complementary
minors of OpenAI's matrix in every dimension, by an energy estimate with node padding, with a
codimension loss of the form $\exp(1000\,n(n-m))$. Here the perturbation of the matrix is
written, by a quadrature formula, as a combination of point evaluations of OpenAI's row
polynomials. The selected parameter family first gave perturbation exponent
$\rho=538/5$; the supplied trials and central-gap quadrature below sharpen
it to $\rho=519037/5000$ (Section~\ref{ssec:gap878}). The improvement also uses actual local arithmetic
and certified energy fields for that family. For other recent work on rational approximations to $G$ see Eskandari
\cite{Eskandari2026}; for earlier work on the arithmetic of $G$ and related values see
\cite{RivoalZudilin2003,Zudilin2003}; for an effective approach to linear independence of
related $L$-values see Calegari, Dimitrov and Tang \cite{CDT2024}.

Marcos Costa Santos Carreira \cite[Sections~2--6]{Carreira2026} studies five-parameter determinant designs and
reports $\mu(G)<2715$ for the design $(96,15,6,8,5)$, using partial-population
energy estimates and sharper row and column determinant bounds. His work
also develops a two-measure equilibrium formulation. Our selected design
is $(20,3,1,2,1)$. His general-design analysis and two-measure equilibrium
formulation provide related structural viewpoints. The estimates proved
here use full-interval marked polynomial atoms, coefficientwise prime-square
recycling and the explicit secondary coefficient-content construction below.

\subsection{Outline of the proof}
Sections~\ref{sec:setup}--\ref{sec:proof} develop the $48N$ determinant and
the earlier $1981$ bound. Section~\ref{sec:twenty} changes the parameters and
proves the current result. The steps for the new family are:
\begin{enumerate}[label=(\roman*)]
\item Its determinant polynomial has degree at most $18N$. Actual prime
valuations supply a common denominator of normalized growth
$8795/4800+(21/200)\log2$. Multiplication by $(18N)!$ gives an integer
polynomial, nonzero at $a/b$ for large prime indices $p$ with $p^2\nmid b$.
\item Four certified endpoint trials and a uniform interpolation between free
and fixed populations give physical real-place constant
$2.256085-\tfrac12\log2$. Full-interval marked-sheet bounds and joint
quadrature weights give perturbation exponent $538/5$; the arithmetic gap
permits decay rate $\eta=1.7755$ after normalization.
\item Coefficientwise divisibility strengthens the integer evaluation bound.
The largest-good-prime refinement initially gives exponent $1091$.
\item A uniform full-row residue kernel gives a secondary prime-content tent
of area $16/63$. Dividing by this common coefficient content preserves
recycling and increases the available normalized gap to $2.029$.
With $d=18$ and $\rho=538/5$, the same criterion gives the retained
$955/2864$ checkpoint.
\item Supplied $40$-mode and $160$-mode trials improve the dual target to
$2.2563367$. Interpolation nodes avoiding a central physical gap jointly
improve the marked field and actual coefficient-functional price. With
$\rho=519037/5000$ and $\eta=425979/200000$, the criterion gives
$878$; final Chebyshev selection gives $2632$. The historical $3662$
statement remains available.
\item A third residue-kernel lemma (Lemma~U3, Section~\ref{sec:u3}) gives
coefficient content at the primes $8N<p<9N$ of area $1/3$. Dividing by it
raises the usable decay to $\eta=492599/200000$, and the same criterion
gives $759$; final Chebyshev selection gives $2276$.
\item A fourth lemma (Lemma~U6, Section~\ref{sec:u6}), a rank bound for a block of
columns at the primes $4N<p<9N/2$, gives coefficient content of area $1/16$.
Dividing by it raises the usable decay to $\eta=505079/200000$, and the same criterion
gives $740$; final Chebyshev selection gives $2220$.
\end{enumerate}

\subsection{Notation and conventions}
We use the notation of OpenAI's paper \cite{OpenAI2026} and refer to it for the constructions; we
restate only what we use. Citations of the form \cite[Prop.~2.1]{OpenAI2026} point to
numbered statements, sections and equations of OpenAI's paper. We write $\log$ for the natural
logarithm.

\section{OpenAI's construction and the facts we use}\label{sec:setup}

For a positive integer $N$ put \cite[(2)]{OpenAI2026}
\begin{gather*}
 n=48N,\qquad b=7N,\qquad q=g=4N,\qquad h=2N,\\
 L=59N,\qquad C=63N,\qquad H=65N,\qquad A=19N,
\end{gather*}
and $D_*=n-1-2g=40N-1$. (The letter $A$ for $19N$ is OpenAI's; the constant $\mathsf A$ below
is different.) The row polynomials $P_r,D_r\in\Z[t]$ ($0\le r<n$) are those of
\cite[(3)]{OpenAI2026}; we only need that
\begin{equation}\label{eq:rows}
 P_r(t)=(1-t)^ht^{C-1}T_{|r-g|}(1/t),\qquad \deg P_r<H,
\end{equation}
where $T_d$ is the Chebyshev polynomial. In particular $P_r$ depends only on $|r-g|$. Let
$f(t)=\sqrt{1-t^2}$, $d\mu(t)=|t|\,dt/f(t)$ on $(-1,1)$ (a measure of mass $2$),
\[
 A_r(t)=P_r(t)-\frac32\,\mathbf 1_{\{t>0\}}\frac{f(t)}{t}D_r(t),\qquad
 \psi_k(s)=s^{b+k}(1-s)^q ,
\]
and let $\cA_N$ be the real $n\times n$ matrix
\begin{equation}\label{eq:matrix}
 \cA_N(r,k)=\int_{-1}^1\int_0^1 A_r(t)\,\frac{\psi_k(s)}{1-ts}\,ds\,d\mu(t)
 \qquad(0\le r,k<n),
\end{equation}
so that OpenAI's determinant is $\det\cA_N$ \cite[(7) and \S5.1]{OpenAI2026}. Put
$c_l=4^{-l}\binom{2l}{l}$ for integers $l\ge0$ and $c_z=0$ otherwise.

\begin{proposition}[OpenAI]\label{prop:openai}
\leavevmode
\begin{enumerate}[label=(\alph*)]
\item \emph{(Rational structure \cite[Prop.~2.1 and (20)]{OpenAI2026}.)} There are rational
 matrices $\cA^0_N,\mathcal L_N\in\Q^{n\times n}$ with $\cA_N=\cA^0_N+G\,\mathcal L_N$ and
 \begin{equation}\label{eq:L}
  \mathcal L_N(r,k)=\sum_{v=0}^{q}(-1)^v\binom qv\sum_{i}[t^i]P_r\cdot4\,c_{(i-b-k-v)/2}.
 \end{equation}
\item \emph{(Real place \cite[Prop.~7.1]{OpenAI2026}.)} With
 $\mathsf U_{\mathrm{OAI}}=2.290939875-\tfrac12\log2$,
 \[
  \limsup_{N\to\infty}\frac{\log|\det\cA_N|}{n^2}\le-\mathsf U_{\mathrm{OAI}} .
 \]
\item \emph{(Local estimates \cite[Prop.~2.2, \S3, Prop.~3.4]{OpenAI2026}.)} For every rational
 $z$ OpenAI bounds $v_\ell(\det(\cA^0_N+z\mathcal L_N))$ from below at every prime $\ell$, by
 quantities depending on $\ell$, $N$ and the denominator of $z$. The sum of these bounds, weighted by
 $\log\ell$, is at most $(\mathsf A+o(1))n^2$, where
 \[
  \mathsf A=\frac{8609}{4608}+\frac{505}{4608}\log2 .
 \]
\item \emph{(Nonvanishing \cite[Prop.~4.1]{OpenAI2026}.)} There is an absolute constant
 $P_*\ge260$ such that, for every prime $p>P_*$ and every $z\in\Q$ whose denominator is not
 divisible by $p$, $v_p\bigl(\det(\cA^0_p+z\mathcal L_p)\bigr)=-96p$; in particular this
 determinant is nonzero.
\end{enumerate}
\end{proposition}

Two remarks on (c) and (d). OpenAI states them under the hypothesis $G=z\in\Q$, but the proofs only use the arithmetic of the rational matrix $\cA^0_N+z\mathcal L_N$. In (d) OpenAI assumes $p>\max(P_*,\operatorname{den}z)$, but the proof only uses $p\nmid\operatorname{den}z$;
this uniformity in $z$ is essential for an irrationality measure, and is how we use the
result.

We also use OpenAI's real-place machinery: the double integral, the two sheet estimates
\cite[Props.~5.2, 5.3]{OpenAI2026}, and the certified energy dual \cite[Prop.~6.1, \S7]{OpenAI2026}.
They are recalled where needed in Section~\ref{sec:perturbation}.

OpenAI's irrationality proof is the inequality $\mathsf U_{\mathrm{OAI}}>\mathsf A$, and
$\mathsf U_{\mathrm{OAI}}-\mathsf A=1.3031\ldots\cdot10^{-4}$. With a new certificate for one case
of OpenAI's energy dual, Proposition~\ref{prop:dual} below shows that (b) holds with
\[
 \mathsf U=2.29180925-\tfrac12\log2
\]
in place of $\mathsf U_{\mathrm{OAI}}$. We use this constant throughout.

\begin{definition}
$\Delta_N(X)=\det(\cA^0_N+X\mathcal L_N)\in\Q[X]$. Thus $\Delta_N(G)=\det\cA_N$, and
$\Delta_N(z)$ for $z\in\Q$ is the rational determinant OpenAI studies under the hypothesis
$G=z$. We write $\gamma_0=\mathsf U-\mathsf A$.
\end{definition}

Numerically $\mathsf U=1.9452356\ldots$, $\mathsf A=1.9442359\ldots$ and
\begin{equation}\label{eq:gap}
 9.996945\cdot10^{-4}<\gamma_0=9.996948\ldots\cdot10^{-4}.
\end{equation}

\section{Arithmetic of \texorpdfstring{$\Delta_N(X)$}{Delta\_N(X)}}\label{sec:arith}

\begin{lemma}[Degree]\label{lem:degree}
$\deg\Delta_N\le44N$.
\end{lemma}

\begin{proof}
By \eqref{eq:L} row $r$ of $\mathcal L_N$ depends only on $P_r$, hence only on $|r-g|$ by
\eqref{eq:rows}. So rows $r$ and $2g-r$ of $\mathcal L_N$ agree for $0\le r<g$. Subtracting
row $r$ from row $2g-r$ for each $r<g$ is a unipotent change of rows, which does not change the
determinant, and it makes the $g$ rows of index in $(g,2g]$ of the new $X$-coefficient
vanish. A determinant $\det(B+XL')$ in which $L'$ has only $n-g$ nonzero rows has degree at
most $n-g=44N$ in $X$.
\end{proof}

\begin{proposition}[Common denominator]\label{prop:denominators}
There are positive integers $D_N$ such that $D_N\Delta_N(i)\in\Z$ for every $i\in\N$, and for
every $\varepsilon>0$, $\log D_N\le(\mathsf A+\varepsilon)n^2$ for all large $N$.
\end{proposition}

\begin{proof}
At an integer $z=i$ the denominator of $z$ is $1$, and OpenAI's local lower bounds for
$v_\ell(\Delta_N(i))$ become independent of $i$: at odd primes they depend only on $\ell$ and
$N$ (and vanish for $\ell>H$), and at $\ell=2$ they depend on $z$ only through a quantity that,
over the integers, is largest at $z=0$. Let $e_\ell(N)\ge0$ be the resulting bound, and put
$D_N=\prod_{\ell\le H}\ell^{e_\ell(N)}$. Then $v_\ell(D_N\Delta_N(i))\ge0$ for every prime $\ell$,
and summing the bounds $e_\ell(N)\log\ell$ exactly as in OpenAI's proof of its finite-place bound
\cite[Prop.~3.4]{OpenAI2026} gives $\log D_N\le(\mathsf A+o(1))n^2$. 
\end{proof}


\begin{proposition}[Sparse prime-row dependencies]\label{prop:sparse-rows}
Let $N\ge1$ and let $p$ be a sufficiently large prime such that
$58N\le3p$, $p\le21N$ and $65N<p^2$. Put
$e=\min(4N,63N-3p)$. For any rational $z$ such that $pz$ has denominator coprime to $p$,
\[
 v_p(\Delta_N(z))\ge-96N+e
\]
when $\Delta_N(z)\ne0$. The corresponding lower bound with the usual formal convention
$v_p(0)=0$ also holds at zero.
\end{proposition}

\begin{proof}
Work over $\mathbb F_p$ and put $W=(1-X^2)^{(p-1)/2}$. For $1\le d\le e$, let
$\delta_kP=P_{g+kp+d}-P_{g+kp-d}$ and define $\delta_kD$ similarly, for $k=0,1,2$.
Chebyshev's identities in characteristic $p$ give
$T_p(Y)=Y^p$ and $U_{p-1}(Y)=(Y^2-1)^{(p-1)/2}$. With
\[
 Q_d=2(1-X)^hX^{C-p-1}U_{d-1}(X^{-1}),\qquad Q_d^{\mathrm{lo}}=X^{-p}Q_d,
\]
both expressions are polynomials, and direct substitution gives
\begin{align*}
 \delta_0D&=X^pQ_d,& \delta_1D&=Q_d,&
 \delta_2D&=2Q_d^{\mathrm{lo}}-X^pQ_d,\\
 XW\delta_0P&=0,& XW\delta_1P&=(1-X^{2p})Q_d,&
 XW\delta_2P&=2(1-X^{2p})Q_d^{\mathrm{lo}}.
\end{align*}
There is no parity sign: substituting $Y=X^{-1}$ in $U_{p-1}$ cancels the sign
that arises from reversal. The support of $Q_d$ is contained in
$[C-p-d,H-p-1]\subseteq[2p,3p)$, and $Q_d=X^pQ_d^{\mathrm{lo}}$.

The leading residues of $p^2$ times a raw matrix entry are obtained by grouping
the coefficients of $XWP_r$ and $D_r$ by their base-$p$ digit. At a raw column
$b\le j<L$, a nonzero coefficient $(Q_d)_{2p+j\bmod p}$ can contribute only when
$j/p$ (integer division) is $1$ or $2$. Indeed, $3p\ge H-b$ excludes quotient zero,
and $d\le g$ excludes quotient three. Write $k=\lfloor j/p\rfloor$ and let
$M_{u,k}$ and $Z_{u,k}$ denote OpenAI's rational moment and zeta coefficients.
The three row differences have the common coefficient $(Q_d)_{2p+j\bmod p}$ times,
respectively,
\begin{align*}
 A_k&=-\tfrac32Z_{3,k},\\
 B_k&=M_{1,k}-M_{3,k}-\tfrac32Z_{2,k},\\
 C_k&=2(M_{0,k}-M_{2,k})-3Z_{1,k}+\tfrac32Z_{3,k}.
\end{align*}
For $k=1,2$, the exact rational identity
\[
 C_k=\frac{292}{59}B_k-\frac{3281}{177}A_k
\]
is checked directly from the moment formulas. Its reduction modulo $p$ proves the
same identity for the leading row residues. The column filter is an integer linear
combination of raw columns in $[b,L)$, so the identity persists after filtering.

For each $d$, replace row $g+2p+d$ by
$\delta_2-\frac{292}{59}\delta_1+\frac{3281}{177}\delta_0$.
Every source row is strictly below this target. The resulting row transformation
is lower triangular with diagonal one and therefore preserves the determinant.
There are exactly $e$ distinct target rows, all below $48N$.
All entries of the scaled matrix have denominator coprime to $p$, and each target row
now has residue zero. Dividing these $e$ rows by $p$ preserves that denominator property,
so $v_p(p^{96N}\Delta_N(z))\ge e$. This proves the claim. A fixed cutoff
$p\ge10^6$ suffices for the finite rational denominator checks used in the formal proof.
\end{proof}

\begin{proposition}[An earlier residue window]\label{prop:early-rows}
Let $N\ge1$ and let $p\ge10^6$ be prime, with $18N\le p$, $3p\le58N$
and $65N<p^2$. For any rational $z$ whose product $pz$ has denominator coprime to $p$,
\[
 v_p(\Delta_N(z))\ge-96N+(3p-54N).
\]
The same formal convention at zero applies.
\end{proposition}

\begin{proof}
Use all $g=4N$ modes from the preceding proof. Each $Q_d$ is still supported in
$[2p,3p)$: $3p+g\le C$ and $H\le4p$. The obstruction to the digit identity
is now quotient zero, contributed by coefficients in $[2p+b,H-p)$.
For $c\in\mathbb F_p^{g}$ put $Q_c=\sum_{d=1}^{g}c_dQ_d$ and let
\[
 B:\mathbb F_p^{g}\longrightarrow\mathbb F_p^{r},\qquad
 r=H-3p-b=58N-3p,
\]
record precisely these coefficients of $Q_c$. Rank--nullity gives
$\dim\ker B\ge g-r=3p-54N$. When $c\in\ker B$, its combined polynomial has
support below $2p+b$ and above $L-p$, so only column quotients one and two
contribute. The same rational digit identity therefore makes
\[
 J(c)=\sum_{d=1}^{g}c_d
 \left(\delta_2-\frac{292}{59}\delta_1+\frac{3281}{177}\delta_0\right)
\]
a left null vector of the leading residue matrix. The map $J$ is injective:
its coefficient at the distinct target row $g+2p+d$ is exactly $c_d$, and all
source rows lie below $g+2p$ since $g<p$.
Consequently the residue rank is at most $n-(3p-54N)$.

For completeness, the rank-to-valuation step does not require a particular
basis of $\ker B$. If a rational matrix $A$ has entries with denominator coprime
to $p$, and its reduction has rank at most $n-e$, factor that reduction through
$\mathbb F_p^{n-e}$ and lift the factors to rational matrices with integer entries.
Write $A=UV+pE$, with $E$ also having denominators coprime to $p$.
Multilinearity of the determinant kills every term with more than $n-e$ columns
from $UV$; all remaining terms contain at least $e$ factors $p$. Thus
$v_p(\det A)\ge e$. Apply this to $A=p^2M$ and $e=3p-54N$.
\end{proof}

\begin{proposition}[Refined common denominator]\label{prop:sparse-denominators}
There are positive integers $D_N^*$ such that $D_N^*\Delta_N(i)\in\mathbb Z$ for every
$i\in\mathbb N$ and, for every $\varepsilon>0$ and all sufficiently large $N$,
\[
 \log D_N^*\le(\mathsf A_*+\varepsilon)n^2,\qquad
 \mathsf A_* = \mathsf A-\frac{5}{1728}.
\]
\end{proposition}

\begin{proof}
Take the minimum of the old denominator exponent and the new bounds
from Propositions~\ref{prop:sparse-rows} and~\ref{prop:early-rows} wherever each applies.
This defines $D_N^*$ and proves integrality at all integer points.
For large $N$ the old exponent is exactly $96N$ throughout these windows.
The resulting continuous saving is
\[
 f(x)=3(x-18)_+-3(x-58/3)_+-3(x-59/3)_++3(x-21)_+,
\]
where $y_+=\max(y,0)$. It rises from zero to four on $[18,58/3]$,
is constant on $[58/3,59/3]$, then decreases to zero at $21$.
It is nonnegative, supported in $[18,21]$, and
$\int_1^{65}f(x)\,dx=20/3$. The weighted prime number theorem gives
\[
 \frac{N}{n^2}\sum_{p\le65N}f(p/N)\log p\longrightarrow\frac{5}{1728}.
\]
Subtract this saving from Proposition~\ref{prop:denominators} to obtain the result.
\end{proof}

\begin{lemma}[Integer-valued polynomials]\label{lem:intvalued}
If $f\in\Q[X]$ has degree at most $d$ and $f(\N)\subseteq\Z$, then $d!\,f\in\Z[X]$.
\end{lemma}

\begin{proof}
The $d$-th forward difference of $f$ is $d!$ times its coefficient of $X^d$, and it is an
integer combination of $f(0),\ldots,f(d)$. Subtract that coefficient times the integer-valued
polynomial $X(X-1)\cdots(X-d+1)$ and induct on $d$.
\end{proof}


\begin{proposition}[Square-denominator nonvanishing]\label{prop:square-nonvanishing}
For every prime $p>P_*$ and rational $z$ such that $pz$ has denominator coprime to $p$,
$\Delta_p(z)\ne0$. In particular, $\Delta_p(a/b)\ne0$ if $a\in\Z$, $b\ge1$ and $p^2\nmid b$.
\end{proposition}

\begin{proof}
The scaled residue matrix in OpenAI's nonvanishing proof is obtained from the rational matrix
by multiplying each entry by $p^2$ and permuting its rows and columns. Each filtered entry is
affine in $z$, so its change from the entry at zero is $p^2z\mathcal L_p(r,k)$.
The central-binomial coefficients $c_l$ have denominators that are powers of $2$, and the
filter coefficients are integers. Thus the denominator of $\mathcal L_p(r,k)$ is coprime to
the odd prime $p$. If $pz$ also has denominator coprime to $p$, the change
$p(pz)\mathcal L_p(r,k)$ has denominator coprime to $p$ and residue zero. The scaled residue
matrix is therefore exactly the matrix at $z=0$. OpenAI's proof shows that this matrix has
nonzero determinant for $p>P_*$, proving $\Delta_p(z)\ne0$.

If $p\nmid b$, then $p(a/b)$ has denominator coprime to $p$. Otherwise write $b=pc$;
$p^2\nmid b$ implies $p\nmid c$, and $p(a/b)=a/c$ again has denominator coprime to $p$.
\end{proof}

\begin{corollary}\label{cor:Q}
$Q_N=(44N)!\,D_N^*\,\Delta_N(X)$ lies in $\Z[X]$ and has degree at most $44N$. If $p>P_*$ is
prime, $a\in\Z$, $b\ge1$ and $p^2\nmid b$, then $Q_p(a/b)\ne0$ and hence $b^{44p}|Q_p(a/b)|\ge1$.
\end{corollary}

\begin{proof}
The first claims follow from Lemmas~\ref{lem:degree} and~\ref{lem:intvalued} and
Proposition~\ref{prop:sparse-denominators}. Proposition~\ref{prop:square-nonvanishing} gives $\Delta_p(a/b)\ne0$. Finally $b^{44p}Q_p(a/b)$ is a
nonzero integer.
\end{proof}

\section{The irrationality-measure criterion}\label{sec:criterion}

\begin{proposition}\label{prop:criterion}
Let $\xi\in\R$, $d\in\N$ and $\eta,\rho>0$. Let $Q_p\in\Z[X]$ be defined for primes $p$ and
suppose that, for all primes $p\ge P_0$:
\begin{enumerate}[label=(\roman*)]
\item $\deg Q_p\le dp$;
\item $Q_p(a/b)\ne0$ for all $a\in\Z$ and $b\ge1$ with $p\nmid b$;
\item $|Q_p(x)|\le e^{-\eta p^2}$ whenever $|x-\xi|\le e^{-\rho p}$.
\end{enumerate}
Put $\kappa=\max(d/\eta,4)$. Then $|\xi-a/b|>b^{-3\rho\kappa}$ for all $a\in\Z$ and all
sufficiently large $b$. Assuming the prime number theorem, for every $\varepsilon>0$ and every $c>1$ the same holds with the exponent $(1+\varepsilon)\rho\max(d/\eta,c/\varepsilon)$. If (ii) holds whenever $p^2\nmid b$, this PNT exponent improves to $(1+\varepsilon)\rho\max(d/\eta,c/(2\varepsilon))$.
\end{proposition}

\begin{proof}
Suppose $|\xi-a/b|\le b^{-3\rho\kappa}$ with $b$ large, and put $X=\kappa\log b$. If every
prime in $(X,3X]$ divided $b$, then $\vartheta(3X)-\vartheta(X)\le\log b\le X/4$, where
$\vartheta$ is Chebyshev's function. But Chebyshev's bounds $\vartheta(x)\le x\log4$ and
$\vartheta(x)\ge(x-1)\log2-O(\sqrt x\log x)$ give $\vartheta(3X)-\vartheta(X)\ge X\log2-o(X)$.
Hence for large $b$ there is a prime $p\in(X,3X]$ with $p\nmid b$, and $p\ge P_0$. Since
$\rho p\le3\rho\kappa\log b$, we get $|a/b-\xi|\le e^{-\rho p}$, so by (iii)
$|Q_p(a/b)|\le e^{-\eta p^2}$. By (i) and (ii), $b^{dp}Q_p(a/b)$ is a nonzero integer, so
$e^{-\eta p^2}\ge b^{-dp}$, that is $p\le(d/\eta)\log b\le X$. This contradicts $p>X$.

For the second statement use the window $(X,(1+\varepsilon)X]$ with
$X=\max(d/\eta,c/\varepsilon)\log b$. Then $\log b\le\varepsilon X/c$, while the prime number theorem gives $\vartheta((1+\varepsilon)X)-\vartheta(X)=\varepsilon X+o(X)$, which exceeds $\varepsilon X/c$ for large $X$.

For the stronger nonvanishing condition, put $X=\max(d/\eta,c/(2\varepsilon))\log b$.
If every prime in $(X,(1+\varepsilon)X]$ had its square dividing $b$, their distinct prime
squares would have product dividing $b$. Taking logarithms gives
$2(\vartheta((1+\varepsilon)X)-\vartheta(X))\le\log b\le2\varepsilon X/c$.
The PNT contradicts this for large $X$. There is therefore a prime with $p^2\nmid b$ in the
window, and the polynomial argument proceeds unchanged.

\end{proof}

The factor $3$ in the first version, or $1+\varepsilon$ in the second, is the price of
finding a prime $p\nmid b$ in a window of the right size.

\section{The perturbation estimate}\label{sec:perturbation}

This section proves the main new ingredient. Recall
$\mathsf U=2.29180925-\frac12\log2$.

\begin{theorem}[Perturbation estimate]\label{thm:perturbation}
Let $\rho=366.3$. For every $\varepsilon>0$ there is $N_0$ such that for all $N\ge N_0$ and all
real $x$ with $|x-G|\le e^{-\rho N}$,
\[
 |\Delta_N(x)-\Delta_N(G)|\le\exp\bigl(n^2(-\mathsf U+\varepsilon)\bigr).
\]
\end{theorem}

Let $\delta=x-G$, so that $\Delta_N(x)=\det(\cA_N+\delta\mathcal L_N)$. The plan: write
$\mathcal L_N=\Phi\beta$, where the columns of $\Phi$ are values of OpenAI's row functions
$A_r$ at fixed nodes (\S\ref{ssec:quadrature}); expand the determinant column by column
(\S\ref{ssec:expansion}); write each resulting mixed determinant as an integral
(\S\ref{ssec:andreief}); and bound the integrand by OpenAI's method
(\S\S\ref{ssec:vandermonde}--\ref{ssec:energy}). Throughout, $J=H=65N$.

\subsection{A quadrature formula for \texorpdfstring{$\mathcal L_N$}{L\_N}}\label{ssec:quadrature}

Let $x_a=\cos\bigl((2a+1)\pi/(2J)\bigr)$ for $0\le a<J$ be the roots of the Chebyshev
polynomial $T_J$, let $\tau_a=(x_a-1)/2\in(-1,0)$, and let
$\ell_a(t)=\prod_{c\ne a}(t-\tau_c)/(\tau_a-\tau_c)$ be the Lagrange basis.

\begin{lemma}\label{lem:quadrature}
For $0\le r,k<n$,
\[
 \mathcal L_N(r,k)=\sum_{a<J}A_r(\tau_a)\,\beta_{a,k},\qquad
 \beta_{a,k}=\sum_{v=0}^q(-1)^v\binom qv\sum_{i<H}[t^i]\ell_a\cdot4\,c_{(i-b-k-v)/2},
\]
and $|\beta_{a,k}|\le B:=8J^2K^N$, where $K=95\cdot10^{46}$.
\end{lemma}

\begin{proof}
Since $\deg P_r<H=J$, Lagrange interpolation gives $[t^i]P_r=\sum_aP_r(\tau_a)[t^i]\ell_a$.
Substitute this into \eqref{eq:L} and use $A_r(\tau)=P_r(\tau)$ for $\tau\le0$.

For the bound, put $g_a(t)=\ell_a(t)(t-1)^q$. Since $[t^i]\ell_a=0$ for $i\ge H$ and
$c_z=0$ unless $z\ge0$, the substitution $i=b+k+v+e$ and
$\sum_v(-1)^v\binom qv[t^{j+v}]\ell_a=[t^{j+q}]g_a$ give
\[
 \beta_{a,k}=4\sum_{0\le e<H}c_{e/2}\,[t^{b+k+e+q}]g_a .
\]
Every coefficient of a polynomial is bounded by its maximum modulus on the unit circle
(average $g(\omega^j)\omega^{-jm}$ over the $M$-th roots of unity $\omega^j$, $M>\deg g$). Since
$|c_z|\le1$, it suffices to show $|g_a(t)|\le2J\,K^N$ for $|t|=1$.

We have $T_J=2^{J-1}\prod_c(X-x_c)$, so $\prod_c(t-\tau_c)=T_J(2t+1)/(2^J\,2^{J-1})$. For
the denominator of $\ell_a$, $\prod_{c\ne a}|\tau_a-\tau_c|=2^{1-J}\prod_{c\ne a}|x_a-x_c|$
and $\prod_{c\ne a}(x_a-x_c)=2^{1-J}T_J'(x_a)=2^{1-J}J\,U_{J-1}(x_a)$. Since
$U_{J-1}(\cos\theta)\sin\theta=\sin(J\theta)$ and $\sin(J\theta_a)=\pm1$ at
$\theta_a=(2a+1)\pi/(2J)$, we get $|U_{J-1}(x_a)|\ge1$, so the denominator is at least
$J\,2^{2-2J}$. Finally, for $|t|=1$,
$|t-\tau_a|\ge1+\tau_a=(1+x_a)/2\ge\sin^2(\pi/(4J))\ge1/(4J^2)$. Hence
\[
 |\ell_a(t)|\le\frac{|T_J(2t+1)|}{2^{2J-1}}\cdot\frac{2^{2J-2}}J\cdot4J^2=2J\,|T_J(2t+1)| .
\]
Writing $\zeta=\cosh w$, one has $T_J(\zeta)=\cosh(Jw)$, $|\zeta-1|+|\zeta+1|=2\cosh\operatorname{Re}w$
and $|\cosh(Jw)|\le e^{J|\operatorname{Re}w|}$, so
\[
 |T_J(\zeta)|\le\bigl(S+\sqrt{S^2-1}\bigr)^J,\qquad S=\tfrac12\bigl(|\zeta-1|+|\zeta+1|\bigr).
\]
For $\zeta=2t+1$ with $|t|=1$, let $s=|t+1|\in[0,2]$. Then $|\zeta-1|=2$, $|\zeta+1|=2s$,
$S=1+s$, and $|t-1|^2=4-s^2$ by the parallelogram law. With $J=65N$ and $q=4N$,
\[
 |g_a(t)|\le2J\,\Bigl(\bigl(1+s+\sqrt{s^2+2s}\bigr)^{65}(4-s^2)^2\Bigr)^N\le2J\,K^N,
\]
where the last inequality holds for all $s\in[0,2]$. (The function
$(1+s+\sqrt{s^2+2s})^{65}(4-s^2)^2$ is largest near $s=1.917$, where its logarithm is
$110.394\ldots$, while $\log K=110.4728\ldots$. We check it by
splitting $[0,2]$ into $21$ intervals; on each, the first factor is increasing and the second
decreasing in $s$, so it suffices to compare rational upper bounds at the endpoints with $K$.)
\end{proof}

\begin{remark}
The cruder bound $\sum_i|[t^i]\ell_a|\le\prod_{c\ne a}(1-\tau_c)/\prod_{c\ne a}|\tau_a-\tau_c|\le(3+2\sqrt2)^J$,
together with $\sum_v\binom qv=2^q$, gives $|\beta_{a,k}|\le2^{q+2}(3+2\sqrt2)^J$, whose
logarithm is $(4\log2+65\log(3+2\sqrt2))N\approx117.35N$ instead of $\log K\cdot N\approx110.47N$.
The unit circle captures the cancellation in $(t-1)^q$ between $t=1$, where $|T_J(2t+1)|$ is
largest, and $t=-1$, where it is smallest.
\end{remark}

Let $\Phi$ be the $n\times J$ matrix $\Phi(r,a)=A_r(\tau_a)$. Then
$\Delta_N(x)=\det\bigl(\cA_N+\delta\,\Phi\beta\bigr)$.

\subsection{Column expansion}\label{ssec:expansion}

For a map $f\colon\{0,\ldots,n-1\}\to\{\varnothing\}\cup\{0,\ldots,J-1\}$ let $M_f$ be the
matrix whose column $k$ is column $k$ of $\cA_N$ if $f(k)=\varnothing$ and the column
$\Phi(\cdot,f(k))$ otherwise, and let $m(f)=\#\{k:f(k)\ne\varnothing\}$.

\begin{lemma}\label{lem:expansion}
If $|\beta_{a,k}|\le B$ and $|\det M_f|\le M c^{m(f)}$ for every $f$, with $M,c\ge0$, then
\[
 \bigl|\det(\cA_N+\delta\Phi\beta)-\det\cA_N\bigr|\le M\bigl((1+J|\delta|Bc)^n-1\bigr).
\]
\end{lemma}

\begin{proof}
Column $k$ of $\cA_N+\delta\Phi\beta$ is $\cA_N(\cdot,k)+\sum_a\delta\beta_{a,k}\Phi(\cdot,a)$.
Multilinearity gives
$\det(\cA_N+\delta\Phi\beta)=\sum_f\prod_{k:f(k)\ne\varnothing}\delta\beta_{f(k),k}\det M_f$.
The term $f\equiv\varnothing$ is $\det\cA_N$, and the others sum in absolute value to at most
$M\sum_{f\not\equiv\varnothing}(|\delta|Bc)^{m(f)}=M((1+J|\delta|Bc)^n-1)$.
\end{proof}

\subsection{A mixed Andr\'eief identity}\label{ssec:andreief}

Fix $f$, and let $p=n-m(f)$. Permuting columns (which only changes the sign of the
determinant), $M_f$ has $p$ integral columns $\cA_N(\cdot,E_i)$, $0\le E_1<\cdots<E_p<n$,
followed by $m=n-p$ point columns $(A_r(\tau'_j))_r$, where $\tau'_j=\tau_{f(k_j)}\in(-1,0)$.

\begin{lemma}\label{lem:andreief}
Let $\mu,\nu$ be finite measures, $F_r$ ($r<p+m$), $G_i$ ($i<p$) and $K$ functions with the
required integrability, and $B$ the $(p+m)\times(p+m)$ matrix with
$B(r,i)=\iint F_r(t)K(t,s)G_i(s)\,d\mu(t)\,d\nu(s)$ for $i<p$ and $B(r,p+j)=F_r(\tau'_j)$.
Then
\begin{multline*}
 (p!)^2\det B=\int\!\!\int\det\bigl[F_r((t\mathbin\Vert\tau')_c)\bigr]_{r,c}\\
 \times\det[K(t_i,s_j)]_{i,j<p}\,\det[G_i(s_j)]_{j,i<p}\;d\mu^p(t)\,d\nu^p(s),
\end{multline*}
where $t\mathbin\Vert\tau'$ is the concatenated list of length $p+m$. Consequently $|\det B|$
is at most $(p!)^{-2}$ times the total mass of $\mu^p\otimes\nu^p$ times the supremum of the
absolute value of the integrand.
\end{lemma}

\begin{proof}
For $m=0$ this is Andr\'eief's identity applied twice \cite{Forrester2018Andreief}, as used by
OpenAI for \cite[(62)]{OpenAI2026}. In general expand $\det B$ by multilinearity in the first
$p$ columns, which integrates $t$ and $s$ variables column by column, and then antisymmetrize
first in the $t$ variables and then in the $s$ variables; the last $m$ columns are constant
throughout.
\end{proof}

We apply this with $F_r=A_r$, $G_i=\psi_{E_i}$, $K(t,s)=1/(1-ts)$, $\mu$ as in
\S\ref{sec:setup} and $\nu$ Lebesgue measure on $(0,1)$; the integrability is OpenAI's
\cite[\S5.1]{OpenAI2026}. The mass of $\mu^p\otimes\nu^p$ is $2^p\le2^n$, so
\begin{equation}\label{eq:detMf}
 |\det M_f|\le2^n\sup_{t,s}\Bigl|\det[A_r((t\mathbin\Vert\tau')_c)]\cdot
 \det\Bigl[\frac1{1-t_is_j}\Bigr]\cdot\det[\psi_{E_i}(s_j)]\Bigr|,
\end{equation}
the supremum over $t\in(-1,1)^p$ and $s\in(0,1)^p$ with distinct nonzero coordinates (a set of
full measure). We have bounded the factor $(p!)^{-2}$ by $1$.

\subsection{A generalized Vandermonde bound}\label{ssec:vandermonde}

The column determinant is
$\det[\psi_{E_i}(s_j)]=\prod_js_j^b(1-s_j)^q\cdot\det[s_j^{E_i}]$. Write
$V(y)=\prod_{i<j}(y_j-y_i)$ and $\cV(y)=|V(y)|$.

\begin{lemma}\label{lem:genvandermonde}
Let $s_0,\ldots,s_{p-1}\in[0,1]$ and let $E_1,\ldots,E_p<n$ be distinct. Then
\[
 \bigl|\det[s_j^{E_i}]\bigr|\le\Bigl(\prod_j(1+s_j)\Bigr)^{n-p}\cV(s)\le2^{p(n-p)}\,\cV(s).
\]
\end{lemma}

\begin{proof}
Let $m=n-p$, let $k_1,\ldots,k_m$ be the integers in $[0,n)$ that are not among the $E_i$,
and let $P(X)=\prod_j(X-s_j)$, a monic polynomial of degree $p$. Consider two $n\times n$
matrices. The rows of $\Omega$ are the linear functionals $f\mapsto f(s_j)$ ($j<p$) and
$f\mapsto[X^{k_l}]f$ ($l\le m$), evaluated on the monomials $X^a$, $a<n$. The columns of
$\Gamma$ are the coefficient vectors of the polynomials $X^b$ ($b<p$) and $X^iP$ ($i<m$), all
of degree less than $n$.
\begin{itemize}
\item Ordering the columns of $\Omega$ as $E_1,\ldots,E_p,k_1,\ldots,k_m$ makes it block
 triangular, with diagonal blocks $[s_j^{E_i}]$ and the identity. So
 $|\det\Omega|=|\det[s_j^{E_i}]|$.
\item In the natural order of the monomials, $\Gamma$ is block triangular with diagonal blocks
 the identity and the matrix $\bigl([X^{p+l}]X^iP\bigr)_{l,i}$, which is unitriangular because
 $P$ is monic of degree $p$. So $|\det\Gamma|=1$.
\item The entries of $\Omega\Gamma$ are the values of the functionals on the polynomials. Since
 $P(s_j)=0$, the block of evaluations on the $X^iP$ vanishes, so $\Omega\Gamma$ is block
 triangular with diagonal blocks the Vandermonde matrix $[s_j^b]_{j,b<p}$ and
 $Q=\bigl([X^{k_l}]X^iP\bigr)_{l,i}$.
\end{itemize}
Hence $|\det[s_j^{E_i}]|=\cV(s)\,|\det Q|$. A determinant is bounded by the product of the
$\ell^1$ norms of its columns, and each column of $Q$ consists of distinct coefficients of
$X^iP$. Its $\ell^1$ norm is therefore at most the sum of the absolute values of the
coefficients of $P$, which is $\prod_j(1+s_j)\le2^p$.
\end{proof}

\begin{remark}
The bound is close to optimal. The ratio $\det[s_j^{E_i}]/V(s)$ is a Schur polynomial with
nonnegative coefficients, and its value at $s=(1,\ldots,1)$, for a single missing exponent
$k$, is $\binom{n-1}k$, of size $2^{n-1}$ up to a polynomial factor.
\end{remark}

\subsection{The integrand}\label{ssec:integrand}

Use OpenAI's coordinate $t=2x/(1+x^2)$, $x\in(-1,1)$ \cite[(64)]{OpenAI2026}, write $x_i$ for
the coordinates of the free nodes $t_i$ and $y_j\in(-1,0)$ for those of the fixed nodes
$\tau'_j$, and $z=x\mathbin\Vert y\in(-1,1)^n$. For a list $z$ of $n$ distinct nonzero numbers
in $(-1,1)$ OpenAI's column factorization \cite[\S5.1, before (65)]{OpenAI2026} reads
\begin{equation}\label{eq:sheet}
 \det[A_r(t_c)]_{r,c}=\cR_n(z)\prod_c t_c^{C-1}(1-t_c)^h ,
\end{equation}
where $\cR_n$ is OpenAI's sheet determinant. OpenAI proves two bounds for it
\cite[Props.~5.2, 5.3]{OpenAI2026}, with $K_0=10e^{12}$:
\begin{align}
 |\cR_n(z)|&\le(1+K_0n)^n\,\cV(1/z)\prod_c|z_c|^g
 &&\text{if }\textstyle\sum_c\frac{1-z_c^2}{1+z_c^2}\le D_*,\label{eq:sheet2}\\
 |\cR_n(z)|&\le(3/2)^nn^{n/2}2^{-\binom n2}\prod_c(1+z_c^2)^{\frac{n-1}2}|z_c|^{g-(n-1)}
 &&\text{always}.\label{eq:sheet1}
\end{align}
Following OpenAI, $\kappa=2$ refers to \eqref{eq:sheet2} and $\kappa=1$ to \eqref{eq:sheet1}.
Let $w(x)=|t|^{C-1}(1-t)^h=2^{C-1}|x|^{C-1}(1-x)^{2h}(1+x^2)^{-(C-1+h)}$.

\subsubsection*{The $p$-node majorants and their energy}
For $x\in(-1,1)^p$ and $s\in(0,1)^p$ with distinct nonzero entries, put $t_i=2x_i/(1+x_i^2)$
and
\begin{align*}
 \cJ^{(p)}(x,s)&=\prod_iw(x_i)\cdot\frac{\cV(t)\cV(s)^2}{\prod_{i,j}(1-t_is_j)}
   \prod_js_j^b(1-s_j)^q,\\
 \cI^{(p)}_2(x,s)&=\cJ^{(p)}(x,s)\,\cV(1/x)\prod_i|x_i|^{g-(n-p)},\\
 \cI^{(p)}_1(x,s)&=\cJ^{(p)}(x,s)\prod_i(1+x_i^2)^{\frac{n-1}2}|x_i|^{g-(n-1)}.
\end{align*}
For $p=n$ these are OpenAI's majorants $\cI_{2,n}$ and $2^{\binom n2}\cI_{1,n}$
\cite[(74)]{OpenAI2026}. Let OpenAI's one-point fields be \cite[(76)]{OpenAI2026}
\begin{gather*}
 W_\kappa(x)=\tfrac{19}{48}\log|x|+\tfrac1{12}\log(1-x)-\bigl(\tfrac\kappa2+\tfrac{17}{48}\bigr)\log(1+x^2),\\
 W_s(s)=\tfrac7{48}\log s+\tfrac1{12}\log(1-s),\qquad
 D(x)=\tfrac16-\tfrac{2x^2}{1+x^2},
\end{gather*}
and define the normalized energy
\begin{align*}
 E^{(p)}_\kappa(x,s)={}&\Bigl(\frac Cn+\frac{\kappa-2}2-\frac{\kappa+1}{2n}\Bigr)\log2
 +\frac1n\sum_jW_s(s_j)\\
 &+\frac1n\sum_{i}\Bigl(W_\kappa(x_i)+\frac{\kappa+2}{2n}\log(1+x_i^2)\Bigr)\\
 &+\frac1{n^2}\Bigl(\kappa\sum_{i<j}\log|x_i-x_j|+\sum_{i<j}\log(1-x_ix_j)\Bigr)\\
 &+\frac2{n^2}\sum_{i<j}\log|s_i-s_j|-\frac1{n^2}\sum_{i,j}\log(1-2x_is_j+x_i^2),
\end{align*}
all sums over indices $<p$; note the normalization by $n$, not $p$. For $p=n$ this is the
normalized logarithm $n^{-2}\log\cI_{\kappa,n}-\frac12\log 2$ of OpenAI's energy argument.
Expanding the coordinate change $t=2x/(1+x^2)$ gives, for every
$p\le n$,
\begin{equation}\label{eq:energy-identity}
 \log\cI^{(p)}_\kappa(x,s)=n^2\Bigl(E^{(p)}_\kappa(x,s)+\tfrac12\log2\Bigr)+e_\kappa(p)\log2,
\end{equation}
with $e_1(p)=p(C-1)+\binom p2-n(C-1)$ and $e_2(p)=e_1(p)-\binom n2$.

Retain the product in Lemma~\ref{lem:genvandermonde}, rather than replacing
each factor by $2$. For $a\in[0,1]$, put
\[
 E^{(p)}_{\kappa,a}=E^{(p)}_\kappa+\frac an\sum_{j<p}\log(1+s_j),
 \qquad t=\frac mn.
\]
The retained product contributes exactly $n^2(E^{(p)}_{\kappa,t}-E^{(p)}_\kappa)$
to the logarithm of the majorant.

\begin{proposition}[Pointwise bound]\label{prop:pointwise}
In the setting of \eqref{eq:detMf}, let $K_n=\max\{(1+K_0n)^n,(3/2)^nn^{n/2}\}$, and let
$\kappa=2$ if $\sum_c\frac{1-z_c^2}{1+z_c^2}\le D_*$ and $\kappa=1$ otherwise. Then the
integrand in \eqref{eq:detMf} is at most
\[
 K_n\,2^{-\omega_\kappa Nm}\exp\Bigl(n^2\bigl(E^{(p)}_{\kappa,t}(x,s)+\tfrac12\log2\bigr)\Bigr),\qquad \omega_1=28,\quad\omega_2=36.
\]
Moreover, if $\kappa=1$ then $\sum_{i<p}\frac{1-x_i^2}{1+x_i^2}>D_*-m$.
\end{proposition}

\begin{proof}
By \eqref{eq:sheet}, Cauchy's evaluation
\[
 \det\Bigl[\frac1{1-t_is_j}\Bigr]=\frac{V(t)V(s)}{\prod_{i,j}(1-t_is_j)}
\]
\cite[(63)]{OpenAI2026} and
Lemma~\ref{lem:genvandermonde}, the integrand is at most
\[
 \Bigl(\prod_j(1+s_j)\Bigr)^m|\cR_n(z)|\prod_jw(y_j)\cdot\cJ^{(p)}(x,s).
\]
For a fixed node $-1<y<0$, put $u=|y|$ and
\[
 R(u)=\frac{u^{19}(1+u)^4}{(1+u^2)^{40}}.
\]
The identity
\[
 27(1+u^2)^4-256u^2=(3u^2-1)^2(3u^4+14u^2+27)
\]
gives $u^2/(1+u^2)^4\le27/256$. Also $(1+u)^4\le4(1+u^2)^2$
and $2u\le(1+u^2)^2$, so
\[
 R(u)\le2(27/256)^9\le2^{-28}.
\]
The fixed-node numerator has powers $A=19N$ and $2h=4N$. The weaker of the two
denominator exponents below is $C-1+h-(n-1)/2=41N-1/2\ge40N$ for $N\ge1$.
For the second case, put $S(u)=u^{19}(1+u)^4/(1+u^2)^{64}$; its denominator exponent is $C-1+h=65N-1\ge64N$. Consequently
\begin{equation}\label{eq:fixed-node}
\begin{aligned}
 w(y)(1+y^2)^{\frac{n-1}2}|y|^{g-(n-1)}&\le2^{C-1}R(u)^N\le2^{C-1}2^{-28N},\\
 w(y)|y|^{g-(n-1)}&\le2^{C-1}S(u)^N\le2^{C-1}2^{-36N}.
\end{aligned}
\end{equation}
The stronger bound for $S$ follows from two positive-polynomial identities. With $v=1+u^2$,
\begin{align*}
3125v^6-46656u^2&=(5u^2-1)^2(125u^8+800u^6+2190u^4+3344u^2+3125),\\
v^{10}-2u(1+u)^4&=(1-u)^2+u^2(1-6u)^2+u^4(1-u)^2\\
&\quad+119u^6+\sum_{j=4}^{10}\binom{10}{j}u^{2j}.
\end{align*}
Thus $u^2/v^6\le3125/46656$ and $u(1+u)^4/v^{10}\le1/2$, giving
$S(u)\le\tfrac12(3125/46656)^9\le2^{-36}$.

We use $\binom n2=\binom p2+pm+\binom m2$ repeatedly.

\emph{Case $\kappa=1$.} By \eqref{eq:sheet1}, the first inequality in \eqref{eq:fixed-node}
and \eqref{eq:energy-identity}, the integrand is at most
\[
 K_n2^{-28Nm}\exp\bigl(n^2(E^{(p)}_{1,t}+\tfrac12\log2)\bigr)\cdot
 2^{-\binom n2+m(C-1)+e_1(p)} ,
\]
and $-\binom n2+m(C-1)+e_1(p)=\binom p2-\binom n2\le0$. The case condition fails for $z$ and
each fixed node contributes at most $1$ to its sum, which gives the last assertion.

\emph{Case $\kappa=2$.} By \eqref{eq:sheet2} we must bound $\cV(1/z)\prod_c|z_c|^g$. Split
$\cV(1/z)=\cV(1/x)\prod_{i,j}|1/y_j-1/x_i|\,\cV(1/y)$. Since $|1/y-1/x|=|x-y|/|xy|\le2/|xy|$
and $\cV(1/y)=\cV(y)\prod_j|y_j|^{-(m-1)}\le\prod_j|y_j|^{-(m-1)}$,
\[
 \cV(1/z)\prod_c|z_c|^g\le2^{pm}\,\cV(1/x)\prod_i|x_i|^{g-m}\prod_j|y_j|^{g-(n-1)}.
\]
With the second inequality in \eqref{eq:fixed-node} and \eqref{eq:energy-identity}, the
integrand is at most
$K_n2^{-36Nm}\exp\bigl(n^2(E^{(p)}_{2,t}+\tfrac12\log2)\bigr)\cdot2^{pm+m(C-1)+e_2(p)}$,
and $pm+m(C-1)+e_2(p)=-\binom m2\le0$.
\end{proof}

\begin{remark}
Each fixed node brings a factor $2^{C-1}$, exactly compensated by the difference
between the $n$-node and $p$-node normalizations. The remaining factors are $2^{-28N}$ and $2^{-36N}$ in the two cases.
Retaining the numerator and denominator together saves $32N\log2$ per fixed node
compared with the earlier separate bound $2^{2h}=2^{4N}$.
\end{remark}

\subsection{The energy bound for \texorpdfstring{$p\le n$}{p<=n} nodes}\label{ssec:energy}

OpenAI's certificate \cite[\S7]{OpenAI2026} supplies, for $\kappa=1,2$, a parameter
$\lambda_\kappa\ge0$ ($\lambda_2=0$, $\lambda_1=2.47405979$), trial sequences
$u^{(\kappa)},v^{(\kappa)}$ (OpenAI's $p,v$), and rational upper bounds
\begin{equation}\label{eq:Bfields}
\begin{gathered}
 \sup_{-1\le x<1,\,x\ne0}\bigl\{W_\kappa+\lambda_\kappa D-2\kappa T(u^{(\kappa)},\cdot)-S(v^{(\kappa)},\cdot)\bigr\}\le B^\kappa_x,\\
 \sup_{0<s<1}\bigl\{W_s+2T(v^{(\kappa)},\cdot)\bigr\}\le B^\kappa_s,
\end{gathered}
\end{equation}
in the notation of \cite[(77)--(78)]{OpenAI2026}. For $\kappa=1$ we use OpenAI's
certificate, which gives $B^1_x=-1.324376$ and $B^1_s=-1.427976$. For $\kappa=2$ we use the
trial sequences of Proposition~\ref{prop:dual} in place of OpenAI's, with
\[
 B^2_x=-0.98572217,\qquad B^2_s=-1.60942387 .
\]
With these, the dual value
\[
 U_\kappa=-\tfrac{11}{16}\log2+\kappa\|u^{(\kappa)}\|_*^2+\tfrac12\|v^{(\kappa)}\|_*^2+B^\kappa_x+B^\kappa_s
\]
satisfies $U_1<-2.296789875$ \cite[Prop.~7.1]{OpenAI2026} and $U_2<-2.29180925$
(Proposition~\ref{prop:dual}). Put
\[
 c_\kappa=(\kappa+2)\log2+|B^\kappa_x|+|B^\kappa_s|+\lambda_\kappa/6,
\]
so that $c_1=5.24413\ldots$ and $c_2=5.36773\ldots$,
and $c^*=53678/10000>\max(c_1,c_2)$.

\begin{proposition}[Energy bound with missing points]\label{prop:energy}
For every $d>0$ there is $N_0$ such that for all $N\ge N_0$, all $p\le n$ (with $m=n-p$) and
all $x\in(-1,1)^p$, $s\in(0,1)^p$ with distinct nonzero coordinates,
\[
 E^{(p)}_\kappa(x,s)\le U_\kappa+d+\frac mn\,c_\kappa ,
\]
for $\kappa=2$ unconditionally and for $\kappa=1$ under
$\sum_{i<p}\frac{1-x_i^2}{1+x_i^2}>D_*-m$.
\end{proposition}

\begin{proof}
OpenAI's proof of \cite[Prop.~6.1]{OpenAI2026} 
regularizes the logarithmic interactions by matched damping, controls the diagonal and endpoint
corrections, and completes two squares with the trial sequences. All of these steps are
estimates for sums over the points, normalized by $n$, and they remain valid, with the same
error terms, uniformly for any number $p\le n$ of points. The quadratic terms are bounded by
$\kappa\|u\|_*^2+\frac12\|v\|_*^2$ as before. Only three places change.
\begin{enumerate}[label=(\arabic*)]
\item The constant term. For $p=n$ the powers of $2$ combine to $-\frac{11}{16}\log2$. For
 $p<n$ the same computation gives $-\frac{11}{16}\log2+(\frac\kappa2+1)(1-p^2/n^2)\log2$, and
 $1-p^2/n^2\le2m/n$.
\item The one-point terms. They are $\frac1n\sum_{i<p}X(x_i)\le\frac pnB_x=B_x+\frac mn|B_x|$,
 since $B_x<0$, and likewise for the column field with $B_s$.
\item The case field ($\kappa=1$ only). OpenAI uses $\lambda\,\frac1n\sum_iD(x_i)\ge-\lambda/n$
 when \eqref{eq:sheet2}'s condition fails. Since $D(x)=\frac{1-x^2}{1+x^2}-\frac56$ and
 $D_*=\frac56n-1$, the shifted condition gives $\sum_{i<p}D(x_i)>-1-\frac m6$, which costs
 $\lambda(1+m/6)/n$.
\end{enumerate}
The damping parameter is chosen in terms of $d$ alone, and the remaining errors are
$O_d(1/n)$, uniformly in $p$ and the configuration. 
\end{proof}

\subsection{A new certificate for the second case of the energy dual}\label{ssec:dual}

For a finite list $c_1,\dots,c_K$ of reals and finitely many pairs $(z_j,r_j)$ of complex numbers
with $|z_j|<1$, consider the trial sequence
\begin{equation}\label{eq:trial}
 u_k=c_k+\operatorname{Re}\sum_j r_jz_j^k\qquad(k\ge1;\ c_k=0\text{ for }k>K).
\end{equation}
This is the form of OpenAI's trial sequences \cite[\S7]{OpenAI2026}.

\begin{proposition}\label{prop:dual}
There are trial sequences $u,v$ of the form \eqref{eq:trial}, with $K=40$, coefficients $c_k$
in $10^{-8}\Z$, twelve pairs $(z_j,r_j)$ for $u$ and fifteen for $v$, all $z_j$ and $r_j$ in
$\Q+\Q i$ (they are listed in the file \lean{Dual/Data.lean} of the formalization), such that
\eqref{eq:Bfields} holds for $\kappa=2$ with $B^2_x=-0.98572217$ and $B^2_s=-1.60942387$, and
$\|u\|_*^2\le0.066723974$, $\|v\|_*^2\le1.292855037$. Hence
\begin{align*}
 U_2&\le-\tfrac{11}{16}\log2+2\cdot0.066723974+\tfrac12\cdot1.292855037\\
 &\qquad-0.98572217-1.60942387<-2.29180925 ,
\end{align*}
and Proposition~\ref{prop:openai}(b) holds with $\mathsf U=2.29180925-\frac12\log2$ in place of
$\mathsf U_{\mathrm{OAI}}$.
\end{proposition}

The sequences were found numerically, by maximizing the dual value $-U_2$ over sequences of
the form \eqref{eq:trial} with prescribed bases $z_j$ (OpenAI's, together with
$\pm0.9$, $\pm0.97$, $0.96$, $\pm0.99$ and a few others) by a cutting-plane method, and then
rounded. At the optimum the two fields of \eqref{eq:Bfields} nearly equioscillate, with about
fifty and thirty local maxima.

\begin{proof}
All computations below are in exact integer and rational arithmetic and are carried out by Lean's kernel.
We follow the structure of OpenAI's certificate, but make each step a decidable check of
general lemmas.

\emph{Closed forms.} For $|x|\le1$, OpenAI's formulas give
\[
 T(u,x)=\sum_{k\le K}\frac{c_kT_k(x)}k-\frac12\operatorname{Re}\sum_jr_j\log(1-2xz_j+z_j^2)
\]
and
$S(u,x)=\sum_{k\le K}c_kx^k/k-\operatorname{Re}\sum_jr_j\log(1-xz_j)$. Expanding the squares and
using $\sum_{k\ge1}w^k/k=-\log(1-w)$,
\begin{multline*}
 \|u\|_*^2=\sum_{k\le K}\frac{c_k^2+2c_kt_k}k
 -\frac12\operatorname{Re}\sum_{j,l}\bigl(r_jr_l\log(1-z_jz_l)
 +r_j\bar r_l\log(1-z_j\bar z_l)\bigr),\\ t_k=\operatorname{Re}\sum_jr_jz_j^k .
\end{multline*}
So the norms and the values of the fields at rational points are rational numbers plus finite
sums of terms $\operatorname{Re}((c+di)\log w)$ with $c,d,w$ rational. Each such term is
approximated to $10^{-12}$ by OpenAI's rational approximations of the logarithm and the
arctangent \cite[\S7]{OpenAI2026}; the reduction of $w$ to the range of these approximations is
computed and checked rationally.

\emph{Stationary points.} The derivative of each field $F$ is a sum of rational functions with
rational coefficients, hence $F'=A/Q$ with explicit $A,Q\in\Q[x]$ (of degrees $78$ and $39$ for
the row field, $60$ and $21$ for the column field), where $Q$ does not vanish on the domain. The
domain is cut into $154$ (respectively $94$) intervals. On $104$ (respectively $63$) of them
$A$ has no root: after the substitution $x=a+(b-a)/(1+y)$, all coefficients of
$(1+y)^{\deg A}A(x)$ have the same sign, so that $A$ has no root in $(a,b)$ (the case of
Descartes's rule of signs without sign changes). The remaining $50$ (respectively $31$)
intervals have length $2\cdot10^{-7}$ and contain the roots of $A$; a breakpoint between two
intervals of the first kind is not a root of $A$.

\emph{Brackets.} On a bracket $[l,l+w]$ write $A(l+wt)=\sum a_it^i$ and $Q(l+wt)=\sum q_it^i$.
For $0\le t\le1$, $|F'|\le\sum|a_i|/(|q_0|-\sum_{i\ge1}|q_i|)$; since $A$ has a root in the
bracket, $a_0$ and $a_1$ are small, and this gives $|F(x)-F(l)|\le10^{-8}$ on the bracket. The
value $F(l)$ is computed as above.

\emph{Conclusion.} The fields tend to $-\infty$ at $0$ and $1$ (the row field at $0^\pm$ and
$1^-$), so their suprema are attained at stationary points or at $x=-1$, and every stationary
point lies in a bracket. Comparing the certified values with $B^2_x$ and $B^2_s$ proves
\eqref{eq:Bfields}. The bound for $U_2$ follows, with $\log2>0.6931471803$. OpenAI's proof of
\cite[Prop.~7.1]{OpenAI2026} applies to any trial sequences in its two cases and gives
$\limsup_N\log|\det\cA_N|/n^2\le\max(U_1,U_2)+\frac12\log2$, and $U_1<-2.296789875$.
\end{proof}

For efficient replay, the implementation clears polynomial denominators once and performs
the root-cover and bracket substitutions over $\Z$, retaining rational arithmetic for the
final scalar ratio and field approximations. Lean proves the coefficient conversions and
the soundness of both substitutions. This changes the computation of the certificates,
while preserving their trial sequences, covers and certified bounds.

\begin{remark}
OpenAI's own certificate for $\kappa=2$ records its bounds to five digits, as
$B^2_x\le-0.98399+2.4\cdot10^{-5}$, $B^2_s\le-1.60890+2.4\cdot10^{-5}$ and a norm term at most
$0.77844$, while its computations show that the largest bracket values of its two fields are
$-0.98403338\ldots$ and $-1.60894641\ldots$ and its norm term is at most $0.778423472$. Read
to seven digits, OpenAI's certificate already gives $U_2<-2.2910468$, and hence the exponent
$34\,000$ by the argument of Section~\ref{sec:proof}. This is also formalized
(\lean{SharpBarrier}).
\end{remark}

\subsection{A weighted endpoint certificate}\label{ssec:weighted}

For each fixed $a\in\{0,1\}$, repeat the proof of Proposition~\ref{prop:energy}
with the column field $W_s+2T(v,\cdot)+a\log(1+s)$, retaining the quadratic
mass correction instead of using $1-p^2/n^2\le2m/n$. Write
$K_a=\kappa\|u_a\|_*^2+\frac12\|v_a\|_*^2$ and
$b_a=B_{x,a}+B_{s,a}$. The resulting bound, uniform in the same configurations, is
\[
 E^{(p)}_{\kappa,a}\le-\tfrac{11}{16}\log2+K_a+(1-t)b_a
 +(\tfrac\kappa2+1)(2t-t^2)\log2+\lambda_a t/6+d.
\]
Its error is uniform because $0\le a\le1$ and the added field is bounded and smooth
at the damping endpoint. One may weaken it before damping at a cost
$a\log2/n$, which tends uniformly to zero.
Since $E^{(p)}_{\kappa,t}=(1-t)E^{(p)}_{\kappa,0}+tE^{(p)}_{\kappa,1}$,
the two fixed endpoint inequalities give
\begin{equation}\label{eq:weighted-quadratic}
 E^{(p)}_{\kappa,t}\le V_0+tC+t^2Q+d,
\end{equation}
where
\begin{align*}
 V_0&=-\tfrac{11}{16}\log2+K_0+b_0,\\
 C&=K_1-K_0+b_1-2b_0+(\kappa+2)\log2+\lambda_0/6,\\
 Q&=b_0-b_1-(\tfrac\kappa2+1)\log2+(\lambda_1-\lambda_0)/6.
\end{align*}
Thus only two fixed trials need certification; no interpolated family of norms is assumed.

For $\kappa=2$, the $a=0$ endpoint is Proposition~\ref{prop:dual}.
A second rational trial, listed in \lean{WeightedDualTwo/Data.lean}, certifies
\begin{gather*}
 B_{x,1}=-0.9498627,\qquad B_{s,1}=-1.2145624,\\
 \|u_1\|_*^2\le0.0713397,\qquad \|v_1\|_*^2\le1.3114478,
 \qquad\lambda_0=\lambda_1=0.
\end{gather*}
Here $B_{s,1}$ bounds the column field including $\log(1+s)$.
The same exact rational checks used in Proposition~\ref{prop:dual} apply:
the derivative numerators have degrees $81$ and $62$, and the covers have
$159$ and $93$ pieces, including $51$ and $31$ stationary-point brackets.
These caps give $C\le5.817$, $Q\le0$, and $V_0<-2.29180925$.

For $\kappa=1$, keep OpenAI's original trial at both endpoints, with
$K_0=K_1=0.9321$ as a common norm cap and $\lambda_0=\lambda_1=2.47405979$.
The new column check is
\[
 W_s+2T(v^{(1)},s)+\log(1+s)\le-0.7586255.
\]
Its derivative is rational with numerator degree $9$ and denominator degree $3$;
a cover of five pieces has one stationary-point bracket. Combined with the old caps,
it gives $C\le5.913488$, $Q\le-1.70907$, and
$V_0\le-2.29180925-0.004980625$. The extra constant margin absorbs the
larger linear coefficient: for $t\ge0$,
\[
 0.183488t-1.70907t^2\le\frac{0.183488^2}{4\cdot1.70907}<0.004980625.
\]
Consequently the two cases give
\begin{equation}\label{eq:weighted-energy}
 E^{(p)}_{1,t}\le-2.29180925+d+5.73t,\qquad
 E^{(p)}_{2,t}\le-2.29180925+d+5.817t.
\end{equation}
All the new field, norm, cover and algebraic inequalities are checked by Lean's kernel.

The additional case-two decay absorbs its larger energy cost: since
$8\log2>48(5.817-5.73)$ and $n=48N$, its product of fixed-node and energy factors is bounded by the common factor
$2^{-28Nm}\exp(nm\cdot5.73)$. This uses the two cases together and does not change their trial sequences.

\subsection{Completion of the proof}\label{ssec:assembly}

\begin{proof}[Proof of Theorem~\ref{thm:perturbation}]
Fix $d>0$ and let $N$ be large. By \eqref{eq:detMf}, Proposition~\ref{prop:pointwise},
\eqref{eq:weighted-energy}, with $c^*=5.73$ and $-2.29180925=-\mathsf U-\frac12\log 2$, every $f$
with $m=m(f)$ satisfies
\[
 |\det M_f|\le2^nK_n\,2^{-28Nm}\exp\bigl(n^2(-\mathsf U+d)+nm\,c^*\bigr)=Mc^m,
\]
with
\[
 M=2^nK_n\,e^{n^2(-\mathsf U+d)},\qquad c=2^{-28N}\,e^{nc^*}.
\]
(The degenerate configurations, such as two fixed nodes being equal or a vanishing coordinate,
have measure zero or make the determinant vanish.) By Lemma~\ref{lem:quadrature},
$|\beta_{a,k}|\le B=8J^2K^N$. Now
\begin{align*}
 \log(nJBc)&=\log(8nJ^3)-28N\log2+N\log K+nc^*\\ &= -28N\log2+N\log K+48Nc^*+\log(8\cdot48\cdot65^3N^4),
\end{align*}
and $-28\log2+\log K+48c^*<366.107$; so $nJBc\le e^{366.3N}$ for $N\ge4000$. If $|\delta|\le e^{-366.3N}$ then $J|\delta|Bc\le1/n$ and $(1+J|\delta|Bc)^n-1\le e-1<2$.
Lemma~\ref{lem:expansion} gives
\[
 |\Delta_N(x)-\Delta_N(G)|\le2M=2^{n+1}K_n\,e^{n^2(-\mathsf U+d)} .
\]
Since $\log K_n=O(n\log n)$, taking $d=\varepsilon/2$ proves the theorem.
\end{proof}

\begin{remark}[The value of $\rho$]
Per unit of $N$, the quadrature weights contribute $\log K<110.475$, the
fixed nodes contribute $-28\log2$, and the weighted energy contributes
$48\cdot5.73=275.04$. The polynomial prefactor is absorbed by the remaining
margin to $\rho=366.3$. Retaining the Vandermonde product replaces the former
combined charge $48\log2+48\cdot5.3678$ by the weighted energy charge, then the separate fixed-node caps and the quadratic margin lower it to $48\cdot5.73$.
\end{remark}

\section{The $48N$ bound}\label{sec:proof}

\begin{proof}[The earlier $1981$ bound]
Let $\gamma_*=\mathsf U-\mathsf A_* = \gamma_0+5/1728$ and $\eta=8969/1000$.
The certified old margin \eqref{eq:gap} implies
$2304\gamma_*>2304\cdot9.996945\cdot10^{-4}+20/3>8.969$.
For sufficiently small $\varepsilon>0$ and large primes $p$, the real bound and perturbation
estimate give $|\Delta_p(x)|\le2e^{n^2(-\mathsf U+\varepsilon)}$ on
$|x-G|\le e^{-366.3p}$. The factorial and the factor two are $e^{o(n^2)}$, while
Proposition~\ref{prop:sparse-denominators} bounds $D_p^*$ by
$e^{n^2(\mathsf A_*+\varepsilon)}$. Thus
$Q_p=(44p)!D_p^*\Delta_p$ satisfies $|Q_p(x)|\le e^{-\eta p^2}$ for large $p$.
Corollary~\ref{cor:Q} gives its degree and square-denominator nonvanishing.

Apply Proposition~\ref{prop:criterion} with $d=44$, $\rho=366.3$ and
$R=d/\eta=44000/8969$. Choose $c=10001/10000$ and
$\varepsilon=c/(2R)=89698969/880000000$. The PNT exponent is
\[
 (1+\varepsilon)\rho R=366.3\left(\frac{44000}{8969}+\frac{10001}{20000}\right)
 =1980.157945\ldots<1981.
\]
With the Chebyshev window the exponent is
$3\rho R=5390.968892\ldots<5391$.
\end{proof}

\begin{remark}[Further reductions]\label{rem:limits}
The sparse-row mechanism raises the denominator gap without changing the determinant's
degree or the perturbation estimate. Further improvements can come from additional residue
dependencies in other prime windows, more efficient determinant parameters, or a smaller
perturbation exponent. Coefficient recycling below removes the overhead of
the earlier square-prime selection step. The remaining analytic and arithmetic
constants still give a bound far above two; the present proof does not
establish an irrationality exponent near two.
\end{remark}

\section{A twenty-row parameter family}\label{sec:twenty}

The preceding sections explain the $48N$ construction and its $1981$ bound.
We now change the determinant parameters, first derive the $1281$ checkpoint,
then refine quadrature and prime selection to prove Theorem~\ref{thm:main}.
This change requires new arithmetic and real-place
estimates; substituting parameters into the earlier numerical constants would
not suffice.

\subsection{The determinant and its arithmetic}
Use the same moment and contact construction with
\[
 \begin{gathered}
 n=20N,\quad b=3N,\quad q=N,\quad g=2N,\quad h=N,\\
 L=24N,\quad C=26N,\quad H=27N,\quad A=8N.
 \end{gathered}
\]
In the definitions of the row polynomials, replace the previous parameter values
by these values: the offset is $r-2N$, the reversal length is $26N$, and the common
row factor is $(1-t)^N$. The filtered columns are
$t^{3N+k}(1-t)^N$. Write $\Delta_N^{(20)}(X)$ for the resulting determinant
polynomial. Row reflection gives
\[
 \deg\Delta_N^{(20)}\le18N.
\]
The three $20\times20$ base matrices corresponding to signs $0,1,-1$ are
invertible. Exact inverse certificates modulo $1009$ prove their rational
nonvanishing. The prime-index reduction then proves uniformly, outside a fixed
finite set of primes,
\[
 \Delta_p^{(20)}(a/b)\ne0\qquad\text{if }p^2\nmid b.
\]
The finite inverse computations certify the base matrices; the deduction for
all large primes is a separate theorem, not an extrapolation from those
computations.

For large odd primes with $27N<p^2$, the actual filtered determinant satisfies
$v_p(\Delta_N^{(20)}(z))\ge-N f(p/N)$ whenever $z$ has $p$-unit denominator.
The physical column pools and their rational inverse maps give
\[
 f(x)=\begin{cases}
 40&0\le x\le10,\\
 60-2x&10\le x\le12,\\
 36&12\le x\le27/2,\\
 63-2x&27/2\le x\le14,\\
 91-4x&14\le x\le16,\\
 75-3x&16\le x\le24,\\
 27-x&24\le x\le27,\\
 0&27\le x.
 \end{cases}
\]
Each bound applies to the actual determinant: the pool reconstruction retains
the integer filter, and the upper-range central remainders are proved
$p$-integral. The exact integral is $\int_0^{27} f=2937/4$.
The proved sparse row relations add the saving
\[
 g(x)=3(x-22/3)_+-6(x-8)_++3(x-26/3)_+.
\]
It is supported on $[22/3,26/3]$, where $f=40$, and has integral $4/3$.
Thus $f-g\ge0$, and
\[
 \frac1{400}\int_0^{27}(f-g)(x)\,dx=\frac{8795}{4800}.
\]
The continuous weighted prime-number theorem proves that this integral is the
normalized limiting odd-prime cost. The finitely many excluded primes and
primes at most $2\sqrt{65N}$ contribute $o(N^2)$, using the already proved
logarithmic entry bounds. Primes above $27N$ are locally integral.

The $2$-adic smoothing and exceptional-column expansion also survives the
parameter change. Nonzero coefficient minors have distinct coefficient
indices within each exceptional family, and their raw column indices are
distinct. If $m$ and $\ell$ are the two exceptional populations, the quadratic
part of the selector exponent is
\[
 \tfrac32m^2+\tfrac12\ell^2-50Nm-26N\ell+520N^2\ge-42N^2,
 \qquad m,\ell\ge0,\quad m+\ell\le20N.
\]
Indeed, adding $42N^2$ to the left side gives
\[
 2(m-11N)^2+(20N-m-\ell)(6N+m)+\tfrac12(20N-m-\ell)^2.
\]
The full minor expansion, not just this quadratic inequality, yields
\[
 \|\Delta_N^{(20)}(z)\|_2
 \le\bigl(8F(z)(27N)^2\bigr)^{20N}2^{42N^2+40N}.
\]
At integer points $F(z)\le F(0)$. Consequently a common denominator
$D_N^{(20)}$ clears every integer value and, for every $\epsilon>0$, eventually
\[
 \log D_N^{(20)}\le
 \left(\frac{8795}{4800}+\frac{21}{200}\log2+\epsilon\right)(20N)^2.
\]
The formal construction uses a harmless eventual threshold $N\ge10^{12}$ to
absorb all finite prime cutoffs. No effective threshold for the final rational
denominator is asserted.

\subsection{Free and fixed populations}
Recompute both sheet duals for the new parameters. Four rational trial
certificates cover the two sheet cases at the two endpoints of the missing
population. Their global field bounds, derivatives, norms and finite diagonal
corrections are checked by the kernel. The certified dual target is
\[
 U_{20}=\frac{2256085}{1000000}.
\]
The physical determinant energy retains the correction $+\tfrac12\log2$.
Fixed-node fields include the common-factor cancellation in the quadrature
weights; their costs are not replaced by the free-node fields. The finite
population interpolation gives, uniformly in every missing mass $m$,
an energy loss at most $4.3\,m/(20N)$, in addition to an arbitrarily small
regularization error. Damping is chosen before taking $N$ large, so this is a
uniform bound rather than a numerical cutoff near the endpoints.

Use $18N$ Chebyshev nodes for the residual row polynomials, and a circle of
radius $1001/1000$. The exact circle certificate gives $K\le e^{33}$.
The joint common-factor and quadrature-weight bound is $54000N K^N$ per atom.
Combining it with the population estimate gives the actual mixed integrand,
multiplied by all its atom weights, the bound
\[
 S_N(54000N)^m
 \exp\!\left((20N)^2\left(-U_{20}+\tfrac12\log2+\delta\right)+119Nm\right),
\]
where
\[
 S_N=(3/2)^{20N}(20N)^{10N}
       +(1+10e^{12}(20N))^{20N},\qquad \log S_N=o(N^2).
\]
This estimate covers both sheets. Zero nodes and repeated nodes give zero
determinants and are included separately.

The mixed Andr\'eief identity can retain the product of the atom weights on
both sides of the integral. The determinant column expansion then uses their
joint bound, with atom cost $54000N e^{119N}$. Since
\[
 (20N)(18N)(54000N)e^{119N}\le e^{120N}
\]
eventually, for every $\epsilon>0$ the actual determinant polynomial satisfies
\begin{align*}
 |\Delta_N^{(20)}(G)|&\le
 e^{(20N)^2(-U_{20}+\frac12\log2+\epsilon)},\\
 |\Delta_N^{(20)}(x)-\Delta_N^{(20)}(G)|&\le
 e^{(20N)^2(-U_{20}+\frac12\log2+\epsilon)}
 \quad\text{if }|x-G|\le e^{-120N}.
\end{align*}

\subsection{The $1281$ checkpoint}
Set
\[
 A_{20}=\frac{8795}{4800}+\frac{21}{200}\log2,
 \qquad\gamma_{20}=U_{20}-\tfrac12\log2-A_{20}.
\]
The certified rational budget gives $400\gamma_{20}>177/100$.
The integer-valued polynomial argument supplies
$Q_N^{(20)}=(18N)!D_N^{(20)}\Delta_N^{(20)}\in\Z[X]$ for all sufficiently
large $N$; smaller indices can be assigned the zero polynomial. Factorial
growth is $o(N^2)$, so the criterion applies with
\[
 d=18,\qquad\eta=177/100,\qquad\rho=120.
\]
Choose $\varepsilon=247/5000$ and $c=1001/1000$ in the square-denominator
prime window. Its exponent is
\[
 (1+\varepsilon)120\max\left(\frac{18}{177/100},
           \frac{1001/1000}{2(247/5000)}\right)
 =\frac{377784}{295}<1281.
\]
The Chebyshev criterion gives $216000/59<3662$. These prove the earlier
$1281$ bound and the retained historical Chebyshev bound.
The corresponding Lean statements are in \lean{Parametric/TwentyMain}.
They have suffixes \lean{1281} and \lean{3662}. We next improve the first bound.

\subsection{Full-interval marked atoms and the critical radius}
Keep the same integer polynomial $Q_N^{(20)}$, and let $J=18N$.
Take $\tau_1,\ldots,\tau_J$ to be all roots of $T_J$ in $(-1,1)$.
Since $J$ is even none is zero. Exact coefficient quadrature now gives
\begin{gather*}
 (\mathcal L_N)_{rk}=\sum_{a=1}^J P_r(\tau_a)\beta_{ak},
 \qquad \kappa_N(t)=t^{8N}(1-t)^N,\\
 |\kappa_N(\tau_a)\beta_{ak}|\le108000N e^{18N}.
\end{gather*}
The fixed vectors are values of the original $P_r$, including at positive
nodes; they are not values of the physical amplitude $A_r$ there.

For $p$ free and $m$ fixed columns, $p+m=20N$, the marked first-sheet
Hadamard bound has the same prefactor $(3/2)^{20N}(20N)^{10N}$ as before.
The full first-case energy certificate gives loss $(448/5)Nm$. Here its scalar budget is sharpened from
$27/5$ to $269/50$: the difference is bounded above by
\[
 -\frac8{125}+\frac{593}{1000}a-\frac{693}{500}a^2
 =-\frac{693}{500}\left(a-\frac{593}{2772}\right)^2
   -\frac{3167}{5544000}<0.
\]
Removing the quadrature term $(9/10)a$ leaves coefficient $112/25$;
multiplication by $20Nm$ gives the stated loss.
In the second case expand only positive marked nodes into actual and near
sheets, using the exact identity $P=-2A+3A_{\rm near}$ after removal of
the common row weight. The grouped energy certificate retains separate
Vandermonde factors for actual and near nodes; its loss is $89Nm$.
The expansion costs at most $5^m$. Both estimates include a uniform
arbitrarily small quadratic-scale error. Combining them with the joint
weight bound gives
\begin{equation}\label{eq:full-marked-bound}
 S_N(540000N)^m
 \exp\!\left((20N)^2\left(-U_{20}+\tfrac12\log2+\epsilon\right)+(538/5)Nm\right).
\end{equation}
Here $S_N$ is the same prefactor as above. In the second case the sharper
$107Nm$ can be increased to $(538/5)Nm$.

The mixed Andr\'eief bound allows arbitrary fixed column vectors.
Formally, modify the integrated row functions at finitely many distinct
auxiliary points; the atomless measure makes this change invisible to
the integrals. Repeated fixed atoms give identical columns and determinant
zero. Free/free and free/fixed collisions are excluded on null sets.
No equality of a positive marked $P$ column and an actual free column is
assumed. These arguments also cover $p=0$ and $m=0$.

After integration, put
\[
 M_N=2^{20N}S_N
 e^{(20N)^2(-U_{20}+\frac12\log2+\epsilon)},\qquad
 c_N=540000N e^{(538/5)N}.
\]
The exact joint column expansion gives
\[
 |\Delta_N^{(20)}(G+\delta)-\Delta_N^{(20)}(G)|
 \le M_N\bigl((1+J|\delta|c_N)^{20N}-1\bigr).
\]
If $|\delta|\le e^{-(538/5)N}$ the binomial factor is at most
$(1+9720000N^2)^{20N}=e^{O(N\log N)}$. Its logarithm is $o(N^2)$;
there is no need to bound the factor by an absolute constant.
Absorb it and the factorial normalization into the regularization error.
For all sufficiently large $N$,
\begin{equation}\label{eq:rho1076}
 |Q_N^{(20)}(x)|\le e^{-(177/100)N^2}
 \quad\text{whenever }|x-G|\le e^{-(538/5)N}.
\end{equation}

\subsection{Coefficient recycling and the final prime choice}
Write $Q_N=Q_N^{(20)}=\sum_j c_{Nj}X^j$ and $D=18N$.
For every sufficiently large $N$ and every prime $N<q\le2N$,
\begin{equation}\label{eq:coefficient-recycling}
 q^{2j}\mid c_{Nj}\qquad(j\ge0).
\end{equation}
Indeed $q^2\mathcal A_N^0$ and $\mathcal L_N$ are $q$-integral, while
$q^{40N}\mid D_N^{(20)}$. The $20N$ determinant therefore shows that
\[
 Q_N(X/q^2)=(18N)!\frac{D_N^{(20)}}{q^{40N}}
       \det(q^2\mathcal A_N^0+X\mathcal L_N)
\]
is coefficientwise $q$-integral. Its $j$th coefficient is $c_{Nj}/q^{2j}$,
which proves \eqref{eq:coefficient-recycling}. This conclusion uses
coefficientwise local integrality, not integer-valued specialization.

If $B$ is a product of distinct prime squares $q^2\mid b$ with $N<q\le2N$,
then $B\mid b$ and $B^j\mid c_{Nj}$. Each summand in
$b^D Q_N(a/b)=\sum_{j=0}^D c_{Nj}a^j b^{D-j}$ is divisible by $B^D$.
Thus, whenever $Q_N(a/b)\ne0$,
\begin{equation}\label{eq:recycled-integer-lower}
 1\le(b/B)^D|Q_N(a/b)|.
\end{equation}
No coprimality of $a,b$ is required.

The same certified gap used above satisfies the sharper rational bound
\[
 400\gamma_{20}
 =400\left(\frac{2256085}{1000000}\right)-\frac{8795}{12}-242\log2
 >\frac{17755}{10000}.
\]
Indeed the already verified bound $\log2<0.693147181$ suffices.
The interval estimate \eqref{eq:rho1076}, including normalization, therefore
holds with every $\eta<400\gamma_{20}$, in particular this sharper choice.
Set $\eta=17755/10000$, $d=18$, $\rho=538/5$, $k=5455/538$ and
$\delta_0=1/1000000$. For large $b$, put $L_b=\log b$,
$U=kL_b$, $V=(k-1)L_b$. The prime number theorem supplies, simultaneously
for every sufficiently large real $t$,
\[
 (1-\delta_0)t\le\theta(t)\le(1+\delta_0)t.
\]
If every prime in $(V,U]$ had its square dividing $b$, then
$2(\theta(U)-\theta(V))\le L_b$. The displayed PNT bounds contradict this,
since $2(1-\delta_0(2k-1))>1$.
Choose the \emph{largest} prime $p\in(V,U]$ for which $p^2\nmid b$.
Every prime $q\in(p,U]$ has $q^2\mid b$, and $U<2V<2p$.
Take $B$ to be the product of their squares and put
$T=\theta(U)-\theta(p)$, so $\log B=2T$.

Suppose $|G-a/b|\le b^{-1091}$. Since $\rho p\le\rho U=1091L_b$,
\eqref{eq:rho1076} applies at $a/b$. Prime-index nonvanishing and
\eqref{eq:recycled-integer-lower} give
\[
 \eta p\le d(L_b-2T).
\]
But the PNT bounds imply $T\ge U-p-2\delta_0U$.
Using $p\le U$ and $2d-\eta>0$ now yields
\[
 \eta k\le d+4d\delta_0 k,
 \qquad
 \eta k-d-4d\delta_0k=\frac{47987}{26900000}>0,
\]
a contradiction. This proves the retained $1091$ bound.

The combined Lean theorem in namespace \lean{CatalanMeasure.Parametric} is
\lean{catalan\_irrationalityMeasure\_1091}.
It is proved in \lean{Parametric/}\allowbreak\lean{TwentyCostMain}.
Its public series version is in \lean{Solution.lean}.
The earlier $1095$ theorem remains in \lean{Parametric/}\allowbreak\lean{TwentySharperMain};
the $1099$ theorem remains in \lean{Parametric/}\allowbreak\lean{TwentyRecycledMain}.
The sharper gap and marked-column cost give the limiting exponent
$3873600/3551\approx1090.848$; the strong eventual statement above
uses the integer exponent $1091$. The following arithmetic refinement gives the $955$ checkpoint;
Section~\ref{ssec:gap878} then sharpens its real estimate to the $878$
bound, Section~\ref{sec:u3} to the $759$ bound, and Section~\ref{sec:u6} to the current statement of Theorem~\ref{thm:main}.

\subsection{A uniform secondary coefficient-content tent}\label{ssec:secondary-tent}

Write $\mathcal A_{N,p}$ for the reduction of $p^2$ times the actual
filtered base matrix. For all sufficiently large $N$ and primes
$52N/9<p<44N/7$, we prove
\begin{equation}\label{eq:tent-rank}
 \begin{gathered}
 \operatorname{rank}\mathcal A_{N,p}\le20N-e_N(p),\\
 e_N(p)=\max\left(0,\min\left(\left\lfloor\frac{9p-52N}{2}\right\rfloor,
                  \left\lfloor\frac{44N-7p}{2}\right\rfloor\right)\right).
 \end{gathered}
\end{equation}
The finitely many primes dividing
$B_*=6310886697782126553600$ may be excluded. Every assertion in this
subsection concerns the full canonical row range, including its endpoints.

Here is an explicit construction and its dimension count. Work over
$\mathbf F_p$, set $n=(p-1)/2$, $g=27N-4p$, $a=p-g$, $b=p-3N$, and use
\[
 x=(z+z^{-1})/2,\quad s=(z-z^{-1})/2,\quad
 h=\frac{z^{26N}(z-1)^{2N}}{(1+z^2)^{27N}},\quad
 b_0=\frac{z^4(z-1)}{(1+z^2)^4}.
\]
In terms of the signed moments $M_{u,J}$ and $Z_{u,J}$ from OpenAI's
entry formulas \cite{OpenAI2026}, put
\[
 A_J(x)=\sum_{v=0}^5M_{v-1,J}x^v,\qquad
 B_J(x)=\frac32\sum_{v=0}^4Z_{v,J}x^v,\qquad
 a_J=B_J-sA_J/x.
\]
In particular the signed boundary moment $M_{-1,J}$ is retained.
The raw source for column $j=Jp+e$, $0\le e<p$, is the Laurent jump of
$2^{26N-1}h x^e a_J^p$; this follows directly by grouping the literal
entry coefficients into base-$p$ digits.

Use the six ordinary differentials
$dz/z,dz,z\,dz,dz/(z-1),dz/(1+z^2),z\,dz/(1+z^2)$, followed by
the boundary differential $dz/z^2$. For a coefficient vector
$c=(\alpha_0,\alpha_1,\alpha_2,\beta,\gamma,\zeta,\omega)$ define
\begin{align*}
 P_c&=\gamma+(2\alpha_0-2\alpha_2+\beta+\zeta)x
             +(2\alpha_1+2\omega)x^2+4\alpha_2x^3,\\
 Q_c&=-\zeta+(-2\alpha_1+\beta+\zeta+2\omega)x
             +(2\alpha_1-4\alpha_2-2\omega)x^2+4\alpha_2x^3.
\end{align*}
Thus the differential is $(U_c+sV_c)dz/z$, where
$P_c=2xU_c$ and $Q_c=2x(x-1)V_c$. Its macro response is the coefficient
of $x^5$ in
\begin{equation}\label{eq:tent-trace}
 H_{J,c}=\bigl((xB_J-(x-1)A_J)P_c+
                  (xB_J-(x+1)A_J)Q_c\bigr)/16.
\end{equation}
This identity follows by adding the two expressions related by $z\mapsto z^{-1}$.

For reproducibility the complete fixed response matrix, multiplied by
$4608$, is
\[
 \begin{pmatrix}
 976&64&4640&-48&25&551&80\\
 -984&3768&-3336&-792&764&-532&1704\\
 2208&-1680&-6384&1440&-354&1602&-1632\\
 -2008&-1768&2104&-600&1196&-1028&-344\\
 -1320&288&16&-552&-935&-1025&1752
 \end{pmatrix}.
\]
Rows are $J=0,\ldots,4$. The first four ordinary columns in the first
four rows have determinant $46085/1769472$ before this scaling.
Consequently there are ordinary seeds $\eta_0,\eta_1,\eta_2,\eta_E$
whose first four responses are respectively
$(1,1,1,1)$, $(0,0,0,0)$, $(0,0,0,0)$ and $(1,0,0,0)$.
Choose their $(\gamma,\zeta)$ coordinates to be
$(0,0),(1,0),(0,1),(0,0)$, respectively; the first four coordinates
are then uniquely determined by the displayed invertible matrix.
The fifth seed is explicitly
\[
 \eta_B=\frac{dz}{z^2}+\frac{20981}{91559}\frac{dz}{z}
             -\frac{40734}{91559}dz-\frac{5430}{91559}z\,dz.
\]
Its first four responses are $(0,0,0,-22627/732472)$, and its
$\beta,\gamma,\zeta$ coordinates vanish. These five seeds are independent:
the boundary pole distinguishes the fifth, the two free coordinates
distinguish the kernel seeds, and the two remaining response vectors
are independent. Multiplication of all seeds by
$D=747824613120$ makes their coefficients integral. All reductions and
independence certificates are valid away from $B_*$.

For five inputs $I_i$ of degree $<p$, form
\[
 H_U=\sum_iP_i^p I_i,\quad H_V=\sum_iQ_i^p I_i,\quad
 K=(z-1)^p\mathcal T_{4p-1}H_U+(z+1)^p\mathcal T_{4p-1}H_V,
\]
where $\mathcal T_d I=(2z)^d I((1+z^2)/(2z))$ and the seeds now include
the common factor $D$. Impose the flags
\begin{gather*}
 x^a\mid H_U,H_V,\qquad (x-1)^N\mid H_U,\qquad
 (x+1)^n\mid H_U,\qquad (x-1)^{N+n}\mid H_V,\\
 \deg\sum_i\alpha_{2,i}I_i<2p-8N-1.
\end{gather*}
The last condition is one shared top-degree cap. Together with the lower
endpoint condition described below, these imply
\[
 T=z^{24N-2p}(1+z^2)^a(z-1)^{p+2N-1}(z+1)^{p-1}\mid K,
 \qquad \deg K+8N+3\le10p.
\]
Thus $R=K/T$ has degree $<20N$, and $u=z^{-2N}R$ is an actual full
row packet. The map from the five inputs to this row is injective:
the involution separates the two natural channels, and Frobenius
interleaving separates each input coefficient and the independent seeds.
Both division and extraction of the $20N$ row coefficients preserve this
injection under the displayed flags.

The literal raw response of this row is
\begin{equation}\label{eq:tent-raw-response}
 -8\,2^{26N-1}\sum_i[x^5]H_{J,i}\,[x^{p-1-e}]I_i.
\end{equation}
One elementary way to verify the jump calculation is the finite Laurent
identity $\operatorname{CT}_{z=0}(sL(x(z)))=-[x^{-1}]L$.
Combining it with \eqref{eq:tent-trace} and
\[
 [x^{6p-1-e}](H(x)^pI(x))=[x^5]H\,[x^{p-1-e}]I
 \quad(\deg I<p)
\]
proves \eqref{eq:tent-raw-response} directly. Hence no generic
surjectivity of the raw matrix or of its polynomial responses is needed.

Take $I_0=F$ with $(x-1)^{p-N}\mid F$ and $\deg F<p$.
It has $N$ parameters, and $[x^{p-1-e}]F=f(e)$ for a polynomial
$f$ of degree $<N$. Explicitly, the basis $(x-1)^{p-1-k}$,
$0\le k<N$, corresponds to the Newton basis $\binom{e}{k}$.
Set $I_1=x^af_1$, $I_2=x^af_2$, $\deg f_i<g$, and
$I_E=x^bh_E$, $\deg h_E<3N$. These choices pay the $x=0$ flags.
For $p=6N+\delta$, $\delta>0$, allow $\deg I_B<4\delta$;
for $p+d=6N$, set $I_B=0$.
The remaining constraint costs are
\[
\begin{array}{c|c|c}
 &p=6N+\delta&p+d=6N\\\hline
 \text{parameter dimension}&N+2g+3N+4\delta&N+2g+3N\\
 \text{small beta flag}&3N&g\\
 \text{two }H_U\text{ branch flags}&N+n&N+n\\
 \text{shared top cap}&8N-p+1&8N-p+1\\
 \text{extra endpoint/response flags}&0&4d+4d
\end{array}
\]
For the beta flag use $Q_i(1)=\beta_i$ and
$(x-1)^p\mid Q_i^p-Q_i(1)$; its small polynomial vanishes after
the indicated number of coefficient constraints. Since
$N+n\le p-N$, this pays the entire $H_V$ branch flag.
On the upper side the boundary input degree pays the lower endpoint
$z^{24N-2p}\mid K$. On the lower side it is paid by the first $4d$
coefficients after the automatic $z^{2p}$ factor; impose another $4d$
literal raw-response conditions on the available $J=4$ columns.

The $E$ response is confined to the unavailable $J=0$, $e<3N$ block.
On the upper side the $B$ response is confined to unavailable $J=3$
columns, because every available such column has $e<p-4\delta$.
Thus every available raw response is the same nonzero scalar times
$f(e)$, including the lower side's explicitly constrained $J=4$ block.
The $N$th column difference annihilates it. Subtracting the displayed
costs gives nullity at least
$N-(7\delta+1)/2$ on the upper side and $N-(9d+1)/2$ on the lower side,
with integer quotients; these are exactly \eqref{eq:tent-rank}.

The actual canonical normalization pays the flat $p^{40N}$ denominator,
and the scaled perturbation matrix vanishes modulo $p$ in this window.
The rank bound therefore puts $p^{e_N(p)}$ in \emph{every coefficient}
of $Q_N$, rather than just its integer values. Let
\[
 c_N=\prod_{52N/9<p<44N/7}p^{e_N(p)}
\]
for sufficiently large $N$, taking $c_N=1$ at the finitely many earlier
indices. Weighted PNT summation \cite{PNTPlus} gives
\[
 \log c_N=(16/63+o(1))N^2,\qquad
 \frac{16}{63}=\frac19+\frac17.
\]
These new primes exceed $2N$ and have no overlap with the already counted
gain in this window. The integral polynomial $\widetilde Q_N=Q_N/c_N$
retains the degree bound, rational nonvanishing and all recycled prime
squares. Its uniform decay is available with
\[
 \eta=\frac{3551}{2000}+\frac{507}{2000}=\frac{2029}{1000},
 \qquad \frac{507}{2000}<\frac{16}{63}.
\]
Apply the preceding largest-good-prime argument to $\widetilde Q_N$ with
$k=4775/538$, $\rho=538/5$, $d=18$ and $\delta_0=10^{-6}$.
Then $\rho k=955$ and the exact remaining margin is
\[
 \eta k-d-4d\delta_0k=\frac{1291}{168125}>0.
\]
This proves the retained $955$ checkpoint. Its Lean theorem is
\begin{center}
\lean{catalan\_irrationalityMeasure\_955}
\end{center}
in
\lean{Parametric/}\allowbreak\lean{SecondaryTentMain}. The limiting exponent using the full
tent area is $244036800/255713\approx954.339$.

Alternatively, apply the Chebyshev final prime-selection criterion of
Proposition~\ref{prop:criterion} to the same $\widetilde Q_N$. Its degree
is still at most $18N$. Since $p\nmid b$ implies $p^2\nmid b$, the same
rational nonvanishing theorem applies. The exact criterion exponent is
\[
 3\frac{538}{5}\max\left(\frac{18}{2029/1000},4\right)
 =\frac{5810400}{2029}<2864.
\]
For $b\ge2$, weakening the exponent gives $b^{-2864}<|G-a/b|$. This proves
the retained $2864$ checkpoint, formalized as
\lean{catalan\_}\allowbreak\lean{irrationality}\allowbreak\lean{Measure\_2864} in
\lean{Parametric/}\allowbreak\lean{SecondaryTentChebyshev}.
Only final prime selection uses Chebyshev here: the denominator asymptotics
and the secondary coefficient-content rate remain PNT-backed, as the
denominator asymptotics already were for the historical $3662$ theorem.


\subsection{Supplied trials and central-gap interpolation}\label{ssec:gap878}

We now retain the same canonical determinant polynomial, degree bound,
integer normalization, own-prime nonvanishing and coefficient-content
divisor, and improve its real estimates. This changes neither the local
arithmetic nor the polynomial's rational zeros. The preceding $955/2864$
proofs remain available as separate checkpoints.

\paragraph{The supplied trial contracts.}
Set
\[
 \begin{gathered}
 U_* =2.2563367,\quad c_1=4.21,\quad c_2=4.29472,\\
 g=\frac{401}{2500},\quad
 a=\frac{2g}{1+g^2}=\frac{2005000}{6410801}.
 \end{gathered}
\]
The first-population trial has $40$ finite modes and its saved geometric
tails. The second has $160$ finite modes and its saved real and complex
tails. Their coefficients are exact rationals in
\lean{FirstStrongTrial/Data} and \lean{StrongTrial/Data}; the certificate
generation records fix their input hashes. The effective first sequence
is $p=2P$, so its norm contribution is $4\|P\|^2+\|V\|^2/2$;
the second uses $2\|P\|^2+\|V\|^2/2$. These conventions are part of
the supplied-field contracts, rather than an identification of the two
trial norms. The certified caps are
\[
\begin{array}{c|ccc}
 &\text{weighted norm}&\text{row plus column cap}&\lambda\\ \hline
 \text{first}&.67761&-2.47913&1.68493357\\
 \text{second}&.77424975&-2.54538346&0 .
\end{array}
\]
The second sequence also satisfies $p_1\ge .18$. Its marked residual
satisfies the stronger, restricted bound
\begin{equation}\label{eq:gap878-residual}
 -\frac9{10}\log(1+x^2)-2T(P,x)\le -.0524
 \quad(g\le |x|\le1).
\end{equation}
The near-field bound remains global: for $0<y<1$,
\[
 -\frac9{10}\log(1+y^2)
 +\frac{16N-1}{20N}\log y-p_1y\le-\frac34
 \qquad(N\ge1).
\]
The coefficient $(16N-1)/(20N)\ge3/4$, and $\log y<0$,
reduce this to the certified one-variable inequality with $p_1\ge .18$.
All row, column and restricted residual caps cover their entire domains,
including endpoint neighborhoods; sampled maxima are not proof inputs.

For the second trial, Descartes' rule gives distinct-root budgets
$59,22,23,50$ on the four dyadic subintervals of $(-1,1)$ split at
$-1/2$, $0$ and $1/2$. The column derivative has budget $87$ on $(0,1)$.
The $241$ rational brackets have strictly opposite endpoint signs.
The intermediate value theorem supplies a distinct root in each bracket;
exhausting each budget therefore covers every critical point. Values at
$\pm1/2$ are nonzero, and zero is excluded from the logarithmic domains.
Point and derivative bounds on these brackets, the endpoint bounds, and
the separate closed-interval residual certificates prove the displayed
suprema. These are ordinary Lean proofs of exact rational checks.

For clarity, the second grouped population budget has
$0\le\tau\le\alpha\le1$ and difference
\[
 \begin{aligned}
 &h_0+\bigl(2.6\log2-F+R-c_2\bigr)\alpha-2\log2\,\alpha^2\\
 &\qquad +(\log2-R-.75)\tau-\log2\,\tau^2,
 \end{aligned}
\]
where $h_0=.77424975+F+U_*-.7\log2$,
$F=-2.54538346$ and $R=-.0524$.
The constant is negative; the $\tau$ coefficient is negative; and
completing the $\alpha$ square gives a strictly negative upper.
For example, using $.693147180<\log2<.693147181$, the latter
square has positive margin at least
\[
 \frac{4948963197}{46209812000000000000}.
\]
The analogous first-population square, with the supplied first trial and
$\lambda=1.68493357$, gives $c_1=4.21$. Thus the two actual marked row
prices are $84.2Nm$ and $85.8944Nm$. The domain restriction in
\eqref{eq:gap878-residual} is applied only to selected marked atoms;
the integrated free variables retain their full original domains.

\paragraph{Exact nodes and their jointly paid weights.}
Use the $18N$ roots of
\[
 P_N(t)=T_{9N}\!\left(\frac{2t^2-(1+a^2)}{1-a^2}\right).
\]
They are distinct, lie in $(-1,-a)\cup(a,1)$, and have the explicit form
\[
 t_{j,\pm}=\pm\sqrt{a^2+(1-a^2)(1+s_j)/2},
 \qquad T_{9N}(s_j)=0.
\]
The physical inverse satisfies $t=2x/(1+x^2)$; hence every selected
marked point has $|x|>g$. This property survives the second-sheet
grouping because its marked coordinates are selections of these points.
Polynomial interpolation is exact at these nodes, so the same residual
coefficient functional and common-factor cancellation apply.

At a root, the Chebyshev derivative identity gives
\[
 |P_N'(t_{j,\pm})|\ge\frac{36Na}{1-a^2}.
\]
Fix $r=1001/1000$ and write $s=|\operatorname{Re}z|$ on $|z|=r$.
For $w=(2z^2-(1+a^2))/(1-a^2)$, its exact ellipse half-sum is
\[
 H(s)=\frac{\sqrt{(r^2+1)^2-4s^2}
                +\sqrt{(r^2+a^2)^2-4a^2s^2}}{1-a^2}.
\]
It decreases with $s$, whereas $|1-z|^2\le r^2+1+2s$ increases.
A contiguous cover of $[0,r]$ by $55$ rational intervals, with upward
square-root bounds and certified logarithms, proves
\[
 9\log\bigl(H(s)+\sqrt{H(s)^2-1}\bigr)
       +\log(r^2+1+2s)<17.913.
\]
Since $|z-t_{j,\pm}|\ge1/1000$ and $(1-a^2)/(36a)\le1$,
the same coefficient-functional argument as before yields the actual
joint bound
\[
 \bigl|\Phi_{N,k}(C_N L_{j,\pm})\bigr|
       \le108000N\exp(17.913N).
\]
Here $L_{j,\pm}$ is the cardinal polynomial of the new nodes and $C_N$
is the existing common factor. The residual cap and this increased nodal
price are paid together. A smaller field cap without its changed weights
would not give this conclusion.

\paragraph{The completed ledger.}
The larger marked row price is $20c_2=85.8944$. Adding the actual weight
price gives
\[
 \rho=20c_2+17.913=\frac{519037}{5000}=103.8074.
\]
The exact unperturbed gap is
$400U_*-8795/12-242\log2>375279/200000$;
dividing by the unchanged content divisor adds
$507/2000$. Thus the integer polynomial has the same degree bound
$dN=18N$, with usable decay
\[
 \eta=\frac{375279}{200000}+\frac{507}{2000}
       =\frac{425979}{200000}=2.129895.
\]
Apply the largest-good-prime criterion with
\[
 k=\frac{4390000}{519037},\qquad \delta_0=10^{-7}.
\]
Its window and integer-payment margins are respectively
\[
 \frac{2595176739037}{2595185000000}>0,
 \qquad
 \eta k-18-72\delta_0k=\frac{3770721}{259518500}>0.
\]
Since $\rho k=878$, this proves the $878$ bound
(the first statement of the previous version of Theorem~\ref{thm:main}). The limiting exponent of this paid ledger is
\[
 \frac{18\rho}{\eta}=\frac{41522960}{47331}
          =877.288880\ldots<878.
\]
For final Chebyshev selection the same integer polynomial and its
nonvanishing theorem give
\[
 3\rho\max\left(\frac{18}{\eta},4\right)
      =\frac{41522960}{15777}<2632.
\]
Weakening this exponent for $b\ge2$ proves the second statement.
Denominator growth and secondary content still use PNT in both results.
The two theorems of this subsection are
\lean{catalan\_irrationalityMeasure\_878} and
\lean{catalan\_irrationalityMeasure\_2632} in
\lean{Parametric/GapMain}.

\section{The third-band content: Lemma U3}\label{sec:u3}

The secondary tent of Section~\ref{ssec:secondary-tent} lives at primes
$p\approx6N$. A second residue-kernel family sits at the primes
$8N<p<9N$. Its rank bound was derived by Claude (Anthropic) working with the
author; the proof below is the one formalized in Lean. Throughout, the design is
$(20,3,1,2,1)$, so the matrix has size $20N$ and the base matrix is
$A_N$ (the filtered matrix at the Catalan parameter $0$). Rows are indexed by
$0\le r<20N$ with signed offset $m=r-2N\in[-2N,18N-1]$, and the raw
columns are $j\in[3N,24N)$. For a prime $p$ write $h=(p+1)/2$ and work in $\mathbb F_p[X]$.

\begin{theorem}[Lemma U3]\label{thm:u3}
Let $N\ge1$ and let $p$ be a prime with $8N<p<9N$. Then
$\operatorname{rank}_{\mathbb F_p}\operatorname{red}(p^2A_N)\le 20N-(18N-2p-1)$,
that is, the nullity of the reduced scaled base matrix is at least $18N-2p-1$.
\end{theorem}

The raw row polynomials of the design are
$P_r=(1-X)^N\,\mathrm{rev}(T_{|m|})$ and $D_r=\operatorname{sgn}(m)(1-X)^N\,\mathrm{rev}(U_{|m|-1})$,
where $T_k,U_k$ are Chebyshev polynomials and $\mathrm{rev}$ reverses coefficients
inside degree $26N-1$. The Lean-proved digit formula (the existing
\lean{rawEntry\_primeDigitPair}) says that for a column $j=Jp+\ell$ ($0\le\ell<p$)
the residue of $p^2\cdot$(raw entry) is a fixed linear function of the digits
$(X W P_r)[vp+\ell]$ and $D_r[vp+\ell]$, $v\ge0$, with $W=(1-X^2)^{(p-1)/2}$,
and the filtered matrix is the raw matrix on $[3N,24N)$ multiplied by the
alternating binomial filter $\Delta$ of order $N$. For a coefficient vector
$c\in\mathbb F_p^{20N}$ put $P_c=\sum c_rP_r$ and $D_c=\sum c_rD_r$. Every
$c$ whose raw response vanishes on $[3N,24N)$ lies in the left kernel of
$\operatorname{red}(p^2A_N)$; the proof counts linear conditions that force this.

\begin{lemma}[Chebyshev Frobenius reflection]\label{lem:u3-reflect}
Let $p$ be an odd prime. In $\mathbb F_p[X]$, for every integer $m$,
\[
 T_{p-m}=X^pT_m-(X^2-1)^{h}\,U_{m-1}.
\]
\end{lemma}
\begin{proof}
Both sides satisfy the three-term Chebyshev recurrence in $m$, so it suffices to check
$m=0,1$. This needs $T_p=X^p$ (Dickson) and $U_{p-1}=(X^2-1)^{(p-1)/2}$. The latter follows
from the Pell identity $T_n^2-(X^2-1)U_{n-1}^2=1$ at $n=p$,
$(X^2-1)^p=X^{2p}-1$, cancellation of $X^2-1$, and comparison of leading
coefficients to fix the sign. For $m=1$ use $T_{p+1}=XT_p+(X^2-1)U_{p-1}$ and $T_{p-1}=2XT_p-T_{p+1}$.
\end{proof}

\paragraph{Step 1: identity K.}
Reflecting the identity of Lemma~\ref{lem:u3-reflect} at degree $p+26N$ gives, for
each row,
\[
 (1-X^2)^h\,\mathrm{rev}(U_{m-1})-X\,\mathrm{rev}(T_m)
   =-X^{p+1}\,\mathrm{rev}(T_{p-m}),
\]
and $\mathrm{rev}(T_{p-m})$ is divisible by $X^{26N-1-|p-m|}$ with $|p-m|\le p+2N$ because
$m\ge-2N$ and $8N<p$. Hence $X^{24N}\mid(1-X^2)^hD_c-XP_c$ for \emph{every} $c$. This is the
form in which the formalization proves identity K (the analytic proof by the substitution
$x=(z+z^{-1})/2$ and $s^p=x^p-z^{-p}$ is equivalent).

\paragraph{Step 2: the flag subspace.}
Let $V$ be the set of $c$ with $(1-X^2)^h\mid P_c$. Since $(1-X)^N\mid P_r$ always, the
condition consists of $h-N$ Taylor-coefficient equations at $X=1$ and $h$ at $X=-1$, that
is $p+1-N$ linear equations. For $c\in V$ write $P_c=(1-X^2)^hY$ and
$\widetilde Q=XY$. Because $(1-X^2)^p=1-X^{2p}$ in characteristic $p$,
\[
 XWP_c=(1-X^{2p})\,\widetilde Q .
\]
Moreover $P_c$ has no coefficients below $X^{8N}$ and none from $X^{27N}$ on,
so $\widetilde Q$ is supported in degrees $[8N+1,\,27N-p-1]$. Dividing the
congruence of Step~1 by the unit $(1-X^2)^h$ modulo $X^{24N}$ gives
\[
 D_c[k]=\widetilde Q[k]\qquad(k<24N).
\]

\paragraph{Step 3: rank-one columns.}
Let $27N-3p\le\ell<24N-2p$. Then the digits of $XWP_c$ at residue $\ell$ are
$(0,q,0,-q,0,\dots)$ with $q=\widetilde Q[p+\ell]$ (the digits of
$\widetilde Q$ at this residue vanish except for $v=1$, by the support, and
$X^{2p}\widetilde Q$ shifts the digit sequence by two places), and the digits of $D_c$ are
$(0,q,0,0,\dots)$ (by identity K for $v\le2$ and degree for $v\ge3$, since $3p+\ell\ge27N$).
Therefore the response at every column $j=Jp+\ell$ equals
$q\,\kappa_J$ with $\kappa_J$ independent of $c$: the columns of this residue
class have rank at most one on $V$.

\paragraph{Step 4: counting.}
For $p\in(8N,9N)$ the columns $j\in[3N,24N)$ with residue $\ell$ are:
$J\in\{1,2\}$ if $\ell<27N-3p$ (two columns), $J\in\{0,1,2\}$ for
$27N-3p\le\ell<24N-2p$ (rank one), and $J\in\{0,1\}$ for $24N-2p\le\ell<p$ (two columns). The
number of linear functionals needed to kill the response on $V$ is therefore
\[
 2(27N-3p)+(p-3N)+2(3p-24N)=3N+p .
\]
Adding the $p+1-N$ flag equations, the kernel of all $2p+2N+1$ conditions has dimension at least
$20N-(2p+2N+1)=18N-2p-1$ and lies in the left kernel of $\operatorname{red}(p^2A_N)$.
This proves Theorem~\ref{thm:u3}. The formal statement is
\lean{u3\_canonical\_rank}; the exact numerical checks (identity K, $\dim V=21N-p-1$, and rank $3N+p$ on $V$ at
$(N,p)=(7,59),(7,61),(13,107),(13,113),(19,157),(19,167)$) agree with the proof.

\paragraph{From nullity to coefficient content.}
For $8N<p<9N$ and $N\ge10^{12}$ the actual normalizer has $p$-exponent
\[
 40N-(26N-3p)^+,
\]
because the odd-loss function equals $40$ on $[0,10]$ and the prime gain is $26-3x$ on
$[8,26/3]$ and $0$ beyond. Rescaling the determinant polynomial by $X\mapsto X/p^2$ then shows
that $p^{2i-(26N-3p)^+}$ divides the $i$-th coefficient of $Q_N$. A nullity of at least
$18N-2p-1$ gives $v_p\det(A_N+zB_N)\ge-(22N+2p+1)$ for rational $z$ with $p\nmid\operatorname{den}z$, hence
$p^{e}\mid Q_N(z)$ for every integer $z$ with
\[
 e=e_N(p)=\min\bigl(p-8N-1,\;18N-2p-1\bigr)^+ ,
\]
which equals $18N-2p-1-\max(26N-3p,0)$. Since $e\le2p-(26N-3p)^+$ for the tail
$i\ge p$, the integer-valued criterion with a $p^e$-divisible tail gives
$p^{e}\mid\operatorname{coeff}_i(Q_N)$ for all $i$ (formalized as
\lean{twentyMeasure}\allowbreak\lean{IntPoly\_third\_coeff\_dvd}). The exponent satisfies
$N\theta(p/N)-1\le e\le N\theta(p/N)$ for the tent $\theta(x)=\max(0,\min(x-8,18-2x))$
of area $1/3$ on $[8,9]$. These primes exceed $2N$ and are disjoint from the primes
of Section~\ref{ssec:secondary-tent}, so the combined content
$c_N=\prod p^{e_N(p)}\cdot\prod_{52N/9<p<44N/7}p^{e'_N(p)}$ keeps all recycled prime
squares. Weighted PNT summation gives $\log c_N^{\mathrm{new}}\ge(\tfrac13-o(1))N^2\ge\tfrac{3331}{10000}N^2$
eventually, so the total content rate used is
\[
 \chi=\frac{507}{2000}+\frac{3331}{10000}.
\]

\paragraph{The 759 ledger.}
With the unchanged real-place gap $375279/200000$ the usable decay is
\[
 \eta=\frac{375279}{200000}+\frac{507}{2000}+\frac{3331}{10000}=\frac{492599}{200000}=2.462995 .
\]
The perturbation exponent and the degree are unchanged: $\rho=519037/5000$, $d=18$. Apply the
largest-good-prime criterion with
\[
 k=\frac{3795000}{519037},\qquad \delta_0=10^{-7}.
\]
Then $\rho k=759$, $k>2$, $\eta<36$, and the window and payment margins are
\[
 \frac{2595177929037}{2595185000000}>0,
 \qquad
 \eta k-18-72\delta_0k=\frac{4372701}{519037000}>0 .
\]
This proves $|G-a/b|>b^{-759}$ for all large $b$. The limiting exponent of the paid
ledger is $18\rho/\eta=373706640/492599=758.6427\ldots<759$. For final Chebyshev
selection,
\[
 3\rho\max\left(\frac{18}{\eta},4\right)=\frac{1121119920}{492599}=2275.928\ldots<2276 .
\]
The new main theorems are \lean{catalan\_irrationalityMeasure\_759} and
\lean{catalan\_irrationalityMeasure\_2276} in \lean{Parametric/U3Main}; the earlier $878$ and $2632$
bounds remain proved.

\begin{remark}
The increment $3331/10000$ is the part of the area $1/3$ of the third-band tent that is
banked; the unbanked remainder $1/3-3331/10000$ is below $10^{-3}$. Reaching $758$
would require a further content window of area about $0.0019$ beyond Theorem~\ref{thm:u3}.
\end{remark}

\section{The sixth-window content: Lemma U6}\label{sec:u6}

The third-band content of Section~\ref{sec:u3} lives at the primes $8N<p<9N$. A
further residue-kernel family sits at the primes $4N<p<9N/2$, below every
earlier window. Unlike Lemma~U3, whose linear conditions are imposed on the
rows of the base matrix through a flag subspace, Lemma~U6 is a statement about
a block of \emph{columns}. Its derivation and formalization are due to Claude
(Anthropic) working with the author; the proof below is the one formalized in Lean.
We keep the design $(20,3,1,2,1)$, the notation of Section~\ref{sec:u3}, and work in
$\mathbb F_p[X]$.

\begin{theorem}[Lemma U6]\label{thm:u6}
Let $N\ge1$ and let $p$ be a prime with $4N<p$ and $2p<9N$. Then
\[
 \operatorname{rank}_{\mathbb F_p}\operatorname{red}(p^2A_N)\le 20N-\frac{p-4N-1}{2},
\]
that is, the nullity of the reduced scaled base matrix is at least $(p-4N-1)/2$.
\end{theorem}

Put $d=p-4N$, which is odd; the hypothesis $2p<9N$ is equivalent to $2d<N$. Put
$e=(d+1)/2$, so that $2N+\frac{p-1}2+e=p$, and $W=(1-X^2)^{(p-1)/2}$.
For a coefficient vector $c\in\mathbb F_p^{20N}$ let
$S_c=\sum_rc_r\,\mathrm{rev}(T_{m_r})$ and $U_c=\sum_rc_r\,\mathrm{rev}(U_{m_r-1})$
with $m_r=r-2N$, the reversal being taken inside degree $26N-1$; thus $P_c=(1-X)^NS_c$ and
$D_c=(1-X)^NU_c$ in the notation of Section~\ref{sec:u3}. Define
\[
 \widehat Q_c=(X-1)^N\,XW\,(1-X)^NS_c,\qquad
 \widehat D_c=(X-1)^N(1-X)^NU_c .
\]

\paragraph{Step 1: identity K6.}
Over any commutative ring,
\[
 U_{m-1}T_n-T_mU_{n-1}=U_{m-n-1},
\]
because both sides satisfy the Chebyshev recurrence in $n$ and agree for $n=0,1$.
In characteristic $p$ take $m=2p$ and use $T_p=X^p$, $U_{p-1}=(X^2-1)^{(p-1)/2}$ (Lemma~\ref{lem:u3-reflect} and
its proof), $T_{2p}=2X^{2p}-1$ and $U_{2p-1}=2T_pU_{p-1}$:
\[
 2X^p(X^2-1)^{(p-1)/2}\,T_n-(2X^{2p}-1)\,U_{n-1}=U_{2p-n-1}.
\]
Reflecting at degree $2p+26N-1$ gives, for each row with $m_r\ge-2N$,
\[
 2XW\,\mathrm{rev}(T_{m_r})-(2-X^{2p})\,\mathrm{rev}(U_{m_r-1})=\mathrm{rev}(U_{2p-m_r-1}),
\]
and the right side is divisible by $X^{24N}$ as soon as $p\ge4N$ (the degree of
$U_{2p-m_r-1}$ is then at most $2p+2N-1$; for $p<4N$ the identity fails). Summing over rows
with weights $c_r$ and multiplying by $(X-1)^N(1-X)^N$ gives, for every $c$ and every $i<24N$,
\begin{equation}\label{eq:K6}
 2\,\widehat Q_c[i]=2\,\widehat D_c[i]-\widehat D_c[i-2p],
\end{equation}
where a coefficient with negative index is $0$.

\paragraph{Step 2: a block of columns.}
Let $M=[p-7d,\,p-6d)$ and, for $J\in\{1,\dots,5\}$ and $\mu\in M$, put $k(J,\mu)=Jp+\mu-4N$.
Writing $\mu=p-7d+t$ with $0\le t<d$ one finds $k=4NJ+(J-6)d+t$, so these are $5d$ distinct
columns of $A_N$, inside $[0,20N)$. The filtered column $k$ is the alternating binomial filter
of order $N$ applied to the raw columns $3N+k+v=Jp+(\mu-N+v)$, $0\le v\le N$. Since
$\mu\ge p-7d=4N-6d>N$ and $\mu<p$ (this is the only use of $2d<N$), all of these
raw columns have the same prime digit $J$ and residues $\mu-N+v\in[0,p)$. The Lean-proved digit
formula (\lean{rawEntry\_primeDigitPair}) expresses the residue of $p^2\cdot$(raw entry) through the digits
$(XWP_c)[up+\ell]$ and $D_c[up+\ell]$, and the alternating binomial sum
$\sum_v(-1)^v\binom Nv a_{m+v}$ is the coefficient of $X^{m+N}$ in $(X-1)^N\sum_ia_iX^i$.
Hence the response of the block column $k(J,\mu)$ on $c$ is
\[
 \sum_{u}\alpha_{J,u}\,\widehat Q_c[up+\mu]-\frac32\sum_u\beta_{J,u}\,\widehat D_c[up+\mu],
\]
with constants $\alpha_{J,u},\beta_{J,u}$ independent of $c$ and $\mu$ (their values are never used).

\paragraph{Step 3: supports and elimination of $\widehat D$.}
$S_c$ is divisible by $X^{8N}$ and $U_c$ by $X^{8N+1}$, so $\widehat Q_c$ and $\widehat D_c$ have no
coefficients up to $X^{8N}$; and $\deg\widehat Q_c\le28N+p-1$, $\deg\widehat D_c\le28N-1$. For
$\mu\in M$ we have $p+\mu<8N$, $6p+\mu\ge28N$ and $7p+\mu>28N+p-1$, so only the digits
$u=2,\dots,6$ of $\widehat Q_c$ and $u=2,\dots,5$ of $\widehat D_c$ can be nonzero. For $u=2,\dots,5$
we have $up+\mu<24N$, so \eqref{eq:K6} reads
$\widehat D_c[up+\mu]=\widehat Q_c[up+\mu]+\tfrac12\widehat D_c[(u-2)p+\mu]$, and $\widehat D_c[(u-2)p+\mu]$
vanishes for $u\le3$ by order. Thus:
\emph{if $\widehat Q_c[up+\mu]=0$ for $2\le u\le6$ and $\mu\in M$, then every block column vanishes on $c$.}

\paragraph{Step 4: the Frobenius class-sum law.}
Since $(1-X)^p=1-X^p$ in characteristic $p$ and $2N+\frac{p-1}2+e=p$,
\[
 (1-X)^e\,\widehat Q_c=(1-X^p)\,Y_c,\qquad Y_c=(-1)^NX(1+X)^{(p-1)/2}S_c .
\]
For $i\ge p$ this gives $[X^i]\bigl((X-1)^e\widehat Q_c\bigr)=(-1)^e\bigl(Y_c[i]-Y_c[i-p]\bigr)$, and
summing over $i=up+\mu$, $u=2,\dots,6$, telescopes to $(-1)^e\bigl(Y_c[6p+\mu]-Y_c[p+\mu]\bigr)$.
Now $Y_c[p+\mu]=0$ because $Y_c$ has no coefficients up to $X^{8N}$, and $Y_c[6p+\mu]=0$ whenever
$6p+\mu>\deg Y_c$, i.e.\ for $\mu\ge p-7d+e$. Expanding the left side by the same binomial identity,
every $\mu=p-7d+t$ with $e\le t<d$ yields the relation
\[
 \sum_{u=2}^{6}\sum_{v=0}^{e}(-1)^v\binom ev\,\widehat Q_c\bigl[up+(p-7d)+(t-e+v)\bigr]=0 .
\]
There are $d-e=(d-1)/2$ such relations. The term $v=e$ contributes
$(-1)^e\sum_{u=2}^6\widehat Q_c[up+\mu]$ and all other terms involve strictly smaller offsets $t-e+v<t$, so
the relations are triangular.

\paragraph{Step 5: counting.}
Impose on $c$: (i) the filtered column $k$ vanishes for each of the $20N-5d$ columns outside the block;
(ii) $\widehat Q_c[up+\mu]=0$ for $2\le u\le5$ and $\mu\in M$ ($4d$ conditions);
(iii) $\widehat Q_c[6p+\mu]=0$ for the first $e$ values of $\mu\in M$ ($e$ conditions).
By strong induction on $t$ the relations of Step~4 force $\widehat Q_c[6p+(p-7d+t)]=0$ for $t\ge e$ as well, hence all digits
$2\le u\le6$ vanish, and by Step~3 so does every block column. Thus the kernel of the
$20N-5d+4d+e=20N-(d-1)/2$ conditions lies in the left kernel of $\operatorname{red}(p^2A_N)$, which therefore has dimension at least
$(d-1)/2=(p-4N-1)/2$. This proves Theorem~\ref{thm:u6}; the formal statement is \lean{u6\_canonical\_rank}.
In exact modular rank computations made while deriving the lemma, the block of $5d$ columns has rank at most $4d+e$, with nullity exactly
$(d-1)/2$, at every prime of the window for $5\le N\le41$ and for $N\in\{53,61,97,151\}$; identity K6 holds exactly when $p>4N$ and fails for $p<4N$.

\paragraph{From the rank bound to coefficient content.}
For $4N<p<9N/2$ and $N\ge10^{12}$ the odd-loss function equals $40$ and the prime gain vanishes
(the prime gain is $0$ for $p/N\le22/3$), so the canonical normalizer has the full $p$-exponent $40N$ and no
rescaling is needed. A rank deficit $e_N(p)=\lfloor(p-4N-1)/2\rfloor\le N$ gives $p^{e_N(p)}\mid Q_N(z)$
for every integer $z$, and together with the divisibility $p^{2i}\mid\operatorname{coeff}_i(Q_N)$ of the
double-pole weights it gives $p^{e_N(p)}\mid\operatorname{coeff}_i(Q_N)$ for all $i$ (formalized as
\lean{twentyMeasure}\allowbreak\lean{IntPoly\_sixth\_coeff\_dvd}). The exponent satisfies
$N\vartheta(p/N)-1\le e_N(p)\le N\vartheta(p/N)$ for $\vartheta(x)=\max(x-4,0)/2$, whose area on $[4,9/2]$
is $1/16$. If $2p=9N$ then $3\mid p$, so no prime has $2p=9N$ and the window is exactly the set of primes in
$(4N,\lfloor9N/2\rfloor]$. Weighted PNT summation gives $\log c^{(6)}_N\ge(\tfrac1{16}-o(1))N^2\ge\tfrac{624}{10000}N^2$ eventually. The primes
of this window exceed $2N$ and are disjoint from those of Section~\ref{ssec:secondary-tent} and
Section~\ref{sec:u3}, so the three contents multiply and keep all recycled prime squares. The total content rate is
\[
 \chi=\frac{507}{2000}+\frac{3331}{10000}+\frac{624}{10000}.
\]

\paragraph{The 740 ledger.}
With the unchanged real-place gap $375279/200000$ the usable decay is
\[
 \eta=\frac{375279}{200000}+\frac{507}{2000}+\frac{3331}{10000}+\frac{624}{10000}=\frac{505079}{200000}=2.525395 .
\]
The perturbation exponent and the degree are unchanged: $\rho=519037/5000$, degree $18$. Apply the
largest-good-prime criterion with
\[
 k=\frac{3700000}{519037},\qquad \delta_0=10^{-7}.
\]
Then $\rho k=740$, $k>2$, $\eta<36$, and the window and payment margins are
\[
 \frac{2595178119037}{2595185000000}>0,
 \qquad
 \eta k-18-72\delta_0k=\frac{63443}{25951850}>0 .
\]
This proves $|G-a/b|>b^{-740}$ for all large $b$. The limiting exponent of the paid
ledger is $18\rho/\eta=373706640/505079=739.8974\ldots<740$. For final Chebyshev
selection,
\[
 3\rho\max\left(\frac{18}{\eta},4\right)=\frac{1121119920}{505079}=2219.692\ldots<2220 .
\]
The new main theorems are \lean{catalan\_irrationalityMeasure\_740} and
\lean{catalan\_irrationalityMeasure\_2220} in \lean{Parametric/U6Main}; the earlier $759$, $2276$, $878$ and $2632$
bounds remain proved.

\begin{remark}
The increment $624/10000$ is the part of the area $1/16$ of the profile $\vartheta$ that is banked; the
unbanked remainder is $1/10000$. The cutoff $9N/2$ is structural: the filter window of a block column leaves
the digit $J$ once $2d>N$. Reaching $739$ would require the usable decay to exceed about $2.5285$,
that is a further content window of area about $0.0031$ beyond Theorem~\ref{thm:u6}.
\end{remark}

\section{Formalization}\label{sec:formal}
\raggedbottom

All results of this paper are formalized in Lean~4 \cite{Lean4} with Mathlib \cite{Mathlib},
on top of OpenAI's Lean formalization of the irrationality of $G$ \cite{OpenAI2026}. The
development is available at
\begin{center}
\FormalizationLink
\end{center}
and combines analytic and arithmetic proofs with generated rational data and kernel checks
for Proposition~\ref{prop:dual} and Section~\ref{ssec:weighted}. The uniform sparse and combined prime-row dependencies and the weighted-PNT denominator saving are also
proved in Lean; numerical rank scans alone are not used as proof. The historical sharpened
OpenAI certificate is retained separately. It uses OpenAI's definitions directly:
Catalan's constant is \lean{catalan}, defined as the series
$\sum_j(-1)^j/(2j+1)^2$; the matrix \eqref{eq:matrix} and its rational form are OpenAI's
\lean{determinant} and \lean{determinantRat}. The current main statements are in \lean{CatalanMeasure.Parametric};
the listed historical lemmas remain in \lean{OAI.InternalCatalan}:
\begin{itemize}
\item \lean{catalan\_irrationalityMeasure\_740}: for all sufficiently large $b\in\N$ and all $a\in\Z$, $b^{-740}<|G-a/b|$ (Theorem~\ref{thm:main});
\item \lean{catalan\_irrationalityMeasure\_2220}: the same with exponent $2\,220$, using Chebyshev for final prime selection;
\item \lean{u6\_canonical\_rank}: Theorem~\ref{thm:u6};
\item \lean{catalan\_irrationalityMeasure\_759}: the earlier bound with exponent $759$;
\item \lean{catalan\_irrationalityMeasure\_2276}: the earlier bound with exponent $2\,276$, using Chebyshev for final prime selection;
\item \lean{u3\_canonical\_rank}: Theorem~\ref{thm:u3};
\item \lean{catalan\_irrationalityMeasure\_878}: the earlier bound with exponent $878$;
\item \lean{catalan\_irrationalityMeasure\_2632}: the earlier bound with exponent $2\,632$, using Chebyshev for final prime selection;
\item \lean{catalan\_irrationalityMeasure\_955}: the retained $955$ checkpoint;
\item \lean{catalan\_irrationalityMeasure\_2864}: the same with exponent $2\,864$, using Chebyshev for final prime selection;
\item \lean{catalan\_irrationalityMeasure\_3662}: the retained historical statement with exponent $3\,662$;
\item \lean{eventually\_realDeterminant\_abs\_upper\_dual}: Proposition~\ref{prop:dual};
\item \lean{separate\_perturbation}: Theorem~\ref{thm:perturbation}, with $\rho=366.3$;
\item \lean{catalan\_irrationalityMeasure} and\\ \lean{catalan\_irrationalityMeasure\_pnt}:
 the general exponents of Proposition~\ref{prop:criterion}.
\end{itemize}
The solution has no \lean{sorry}, and the command \lean{\#print axioms} reports only the three
standard axioms \lean{propext}, \lean{Classical.choice} and \lean{Quot.sound}.
The prime number theorem enters the denominator asymptotics and secondary
prime-content sum, and also the final prime selection for $740$, $759$ and $878$.
The $2220$, $2276$ and $2632$ corollaries use Chebyshev only in that final selection step.
The $955/2864$ checkpoint has the same PNT scope.
The formal source for PNT is the PNT+ project
\cite{PNTPlus}, through OpenAI's workspace and compatibility additions.

\begingroup
\noindent The following file groups implement the indicated parts of the proof.\par\medskip
\noindent \lean{DeltaPoly}, \lean{Degree}\par
$\Delta_N(X)$; Lemma~\ref{lem:degree}.\par\medskip
\noindent \lean{Denominators}, \lean{IntegerValued}, \lean{Integrality}\par
Proposition~\ref{prop:denominators}; Lemma~\ref{lem:intvalued}; Corollary~\ref{cor:Q}.\par\medskip
\noindent \lean{SparseDenominators}, \lean{DenseDenominators}, \lean{DenseGainPNT}, \lean{DenseMain}\par
Propositions~\ref{prop:sparse-rows}--\ref{prop:sparse-denominators}; the earlier $1981$ bound.\par\medskip
\noindent \lean{Nonvanishing}\par
Proposition~\ref{prop:openai}(d) for $p\nmid\operatorname{den}z$.\par\medskip
\noindent \lean{PrimeWindow}, \lean{Criterion}, \lean{PNTWindow}, \lean{Main}\par
Proposition~\ref{prop:criterion} and the reduction to Theorem~\ref{thm:perturbation}.\par\medskip
\noindent \lean{Quadrature}, \lean{ChebyshevNodes}, \lean{QuadCircle}\par
Lemma~\ref{lem:quadrature}.\par\medskip
\noindent \lean{DetExpansion}\par
Lemma~\ref{lem:expansion}.\par\medskip
\noindent \lean{MixedAndreief}\par
Lemma~\ref{lem:andreief}.\par\medskip
\noindent \lean{VandermondeProduct}\par
Lemma~\ref{lem:genvandermonde}.\par\medskip
\noindent \lean{PinMajorant}, \lean{FixedNodes}, \lean{FixedNodeMajorant}\par
Proposition~\ref{prop:pointwise}, \eqref{eq:fixed-node}, and \eqref{eq:energy-identity}.\par\medskip
\noindent \lean{PinDampedDual}, \lean{PinSupDual}\par
Proposition~\ref{prop:energy}.\par\medskip
\noindent \lean{Cert/ListPoly}, \lean{Cert/LogApprox}, \lean{Cert/FieldEval}, \lean{Cert/FieldDeriv}, \lean{Cert/Cover}, \lean{Cert/Norm}\par
the general lemmas behind the checks of Proposition~\ref{prop:dual}.\par\medskip
\noindent \lean{Dual/*}, \lean{DualTwo}\par
the certificate data, the kernel checks, Proposition~\ref{prop:dual}.\par\medskip
\noindent \lean{SharpBarrier}\par
the remark after Proposition~\ref{prop:dual}.\par\medskip
\noindent \lean{WeightedEnergy}, \lean{WeightedBounds}\par
Section~\ref{ssec:weighted}.\par\medskip
\noindent \lean{SeparateFixedNodes}, \lean{SeparateBounds}, \lean{SeparateLemma6}\par
Theorem~\ref{thm:perturbation}.\par\medskip
\noindent \lean{SquareNonvanishing}, \lean{SquarePNTWindow}, \lean{SquareMain}\par
Proposition~\ref{prop:square-nonvanishing}, strengthened Proposition~\ref{prop:criterion}.\par\medskip
\noindent \lean{Parametric/U6Main}, \lean{U6Audit}\par
Section~\ref{sec:u6}; current $740/2220$ bounds.\par\medskip
\noindent \lean{U6Chebyshev}, \lean{U6Identity}, \lean{U6Block}, \lean{U6Digits}, \lean{U6Rank}\par
Identity K6, the Frobenius class-sum law, the block column responses and Theorem~\ref{thm:u6}.\par\medskip
\noindent \lean{U6Content}, \lean{U6PrimeGrowth}\par
Rank to coefficient content for $4N<p<9N/2$ and the area-$1/16$ prime sum.\par\medskip
\noindent \lean{Parametric/U3Main}, \lean{U3Audit}\par
Section~\ref{sec:u3}; the $759/2276$ bounds.\par\medskip
\noindent \lean{U3ChebyshevFrobenius}, \lean{U3RowIdentity}, \lean{U3Combination}, \lean{U3Digits}, \lean{U3Rank}\par
Lemma~\ref{lem:u3-reflect}, identity K, the flag subspace, the digit response and Theorem~\ref{thm:u3}.\par\medskip
\noindent \lean{U3Content}, \lean{U3PrimeGrowth}\par
Nullity to coefficient content for $8N<p<9N$ and the area-$1/3$ prime sum.\par\medskip
\noindent \lean{Parametric/GapMain}, \lean{GapFinalTransfer}\par
Section~\ref{ssec:gap878}; the $878/2632$ bounds.\par\medskip
\noindent \lean{FirstStrongTrial/*}, \lean{StrongTrial/*}\par
Supplied exact trials, point values and root-coverage certificates.\par\medskip
\noindent \lean{GapNodal}, \lean{GapCircle/*}, \lean{GapWeights}\par
Central-gap quadrature and actual joint weight bounds.\par\medskip
\noindent \lean{Cert/DescartesBudget}, \lean{Cert/IntegerHorner}\par
Distinct-root budgets and checked bracket endpoints.\par\medskip
\noindent \lean{SecondaryTentMain}, \lean{SecondaryTent}\allowbreak\lean{MeasureTransfer}\par
Section~\ref{ssec:secondary-tent}; retained $955$ bound.\par\medskip
\noindent \lean{SecondaryTentChebyshev}\par
Alternate final prime selection; $2864$ bound.\par\medskip
\noindent \lean{SecondaryTent}\allowbreak\lean{Parameters*}, \lean{SecondaryTentRow*}, \lean{SecondaryTentSource*}\par
Actual uniform row kernel, source compatibility and prime-content tent.\par\medskip
\noindent \lean{TwentyCostMain}, \lean{TwentySharperMain}, \lean{TwentyIntegerPolynomial}\par
Retained $1091/3662$ bounds and canonical integer polynomial.\par\medskip
\noindent \lean{TwentyDenominators}, \lean{TwentyTwoAdicNorm}, \lean{TwentyCombinedOddLoss}\par
Actual local arithmetic and common-denominator growth.\par\medskip
\noindent \lean{TwentyTrial/*}, \lean{TwentyFirstCost}, \lean{TwentyCostPerturbation}\par
Certified population and marked fields, mixed integration and $\rho=538/5$.\par\medskip
\endgroup

The current proofs were checked with Lean \texttt{v4.35.0-rc2} and the matching Mathlib release.
OpenAI's original repository at commit \texttt{fd4aeeb} pins Lean \texttt{v4.34.1} and Mathlib
commit \texttt{d13f23b}. The parts of that formalization used here were converted to Lean's
module system and ported to the current toolchain; the repository's README and provenance
documents describe the changes.

\section*{Disclosure of AI use}

The original development was produced by the AI system Claude Opus~5.5 (Anthropic): the
mathematics, including the perturbation estimate and all proofs; the Lean formalization; the
numerical computations and the certificate generator; the literature search; and the text of this paper. Claude worked in a series
of conversations at the request of the author, who posed the problem, directed the work, and is
responsible for this submission. The separate fixed-node decay bounds and weighted Vandermonde refinement, endpoint certificates, quadratic case refinement, dependency refactor, integer certificate computations and their soundness proofs, square-denominator nonvanishing, the prime-window refinement, uniform sparse and combined prime-row dependencies and denominator saving, the twenty-row parameter family, certified free and fixed population fields, joint atom integration, and corresponding revisions to this paper were developed by OpenAI Codex running GPT-6.1 Sol (OpenAI) at the author's request.
The full-interval marked-sheet assembly, critical-radius perturbation,
coefficient recycling, largest-good-prime criterion and the uniform secondary
coefficient-content tent with its complete source and row formalization were developed
with Codex at the author's request. The subsequent supplied-trial refinements,
central-gap interpolation, actual circle weights, reusable root-count
coverage certificates and the $878/2632$ assembly were also developed with
Codex at the author's request. Lemma~U3 (Section~\ref{sec:u3}): its derivation, including identity K and
the dimension count, its Lean formalization, the content transfer to primes in $(8N,9N)$ and the
$759/2276$ assembly were carried out by Claude (Anthropic) working with Sean Litsey, building on the
Codex-developed pipeline above. Lemma~U6 (Section~\ref{sec:u6}): its derivation, including identity K6 and the
class-sum law, its Lean formalization, the content transfer to primes in $(4N,9N/2)$ and the
$740/2220$ assembly were likewise carried out by Claude (Anthropic) working with Sean Litsey. The underlying irrationality proof and its formalization are
OpenAI's \cite{OpenAI2026}.
The formal verification in Lean is intended as an independent check of every step of the
argument above.

\begin{thebibliography}{99}

\bibitem{CDT2024}
F.~Calegari, V.~Dimitrov and Y.~Tang,
\emph{The linear independence of $1$, $\zeta(2)$, and $L(2,\chi_{-3})$},
preprint, \href{https://arxiv.org/abs/2408.15403}{arXiv:2408.15403}.

\bibitem{Carreira2026}
Marcos Costa Santos Carreira,
\emph{General designs and an irrationality exponent for Catalan's constant},
preprint v1 (October 9, 2026),
\href{https://doi.org/10.5281/zenodo.23326325}{doi:10.5281/zenodo.23326325};
sources at \url{https://github.com/MarcosCarreira/catalan-designs}.

\bibitem{Eskandari2026}
P.~Eskandari,
\emph{Improved rational approximations to Catalan's constant},
preprint (2026), \href{https://arxiv.org/abs/2609.26354}{arXiv:2609.26354}.

\bibitem{Forrester2018Andreief}
P.~J.~Forrester,
\emph{Meet Andr\'eief, Bordeaux 1886, and Andreev, Kharkov 1882--83},
preprint (2018), \href{https://arxiv.org/abs/1806.10411}{arXiv:1806.10411}.

\bibitem{Jha2026}
R.~K.~Jha,
\emph{A finite irrationality measure for Catalan's constant},
preprint v1, October 8, 2026,
\href{https://doi.org/10.5281/zenodo.23237269}{doi:10.5281/zenodo.23237269};
Lean sources at \url{https://github.com/rohitkrjha/catalan-measure}.

\bibitem{Mathlib}
The mathlib Community,
\emph{The Lean mathematical library},
in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and
Proofs (CPP 2020), 367--381.

\bibitem{Lean4}
L.~de~Moura and S.~Ullrich,
\emph{The Lean~4 theorem prover and programming language},
in: Automated Deduction -- CADE 28, Lecture Notes in Computer Science 12699, Springer, 2021,
625--635.

\bibitem{OpenAI2026}
OpenAI,
\emph{Catalan's constant is irrational},
preprint (September 24, 2026), with a Lean formalization, available at
\href{https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Catalans-constant-is-irrational-September-24-2026/paper.pdf}{the original paper PDF}
and
\href{https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/Catalan}{the Lean formalization}
(repository commit \texttt{fd4aeeb}, October 7, 2026).

\bibitem{RivoalZudilin2003}
T.~Rivoal and W.~Zudilin,
\emph{Diophantine properties of numbers related to Catalan's constant},
Math. Ann. \textbf{326} (2003), 705--721.

\bibitem{PNTPlus}
The PrimeNumberTheoremAnd contributors,
\emph{The PNT+ project: a Lean formalization of the prime number theorem
and related results},
\url{https://github.com/AlexKontorovich/PrimeNumberTheoremAnd}.
The vendored compatibility additions used here are recorded in the
repository's \texttt{NOTICE} and \texttt{PORTING.md}.

\bibitem{Sun2026}
Z.-W.~Sun,
\emph{Catalan's constant is irrational},
preprint (2026), \href{https://arxiv.org/abs/2609.04176}{arXiv:2609.04176}.

\bibitem{Wachs2026}
D.~Wachs,
\emph{A note on a recent claimed proof of the irrationality of Catalan's constant},
preprint (2026), \href{https://arxiv.org/abs/2609.22339}{arXiv:2609.22339}.

\bibitem{Zudilin2003}
W.~Zudilin,
\emph{An Ap\'ery-like difference equation for Catalan's constant},
Electron. J. Combin. \textbf{10} (2003), R14.

\end{thebibliography}

\end{document}