\documentclass[11pt]{amsart}
\IfFileExists{lmodern.sty}%
  {\usepackage[T1]{fontenc}\usepackage{lmodern}\usepackage{microtype}}%
  {\usepackage[expansion=false]{microtype}}
\usepackage{amssymb,mathtools}
\usepackage{booktabs,array,longtable}
\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 13, 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^{-1\,281}$ for every integer $a$ and every sufficiently large
integer $b$. Thus $\mu(G)\le1\,281$; replacing the prime number theorem
in the final approximation criterion by Chebyshev's estimates gives $3\,662$.
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. Four exact energy
certificates and a separate treatment of free and fixed populations give a
uniform mixed-integrand bound. Restricted quadrature and joint atom weights
then control the determinant polynomial on $|x-G|\le e^{-120N}$.
Prime-index nonvanishing when $p^2\nmid b$ completes the 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^{-1\,281}.
\]
In particular $\mu(G)\le 1\,281$. If in the last step the prime number theorem is replaced by
Chebyshev's bounds, the same argument gives $|G-a/b|>b^{-3\,662}$.
\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
functions, and the new parameter family has perturbation exponent $\rho=120$
(Section~\ref{sec:twenty}). 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}.

\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$. Joint quadrature weights give perturbation exponent
$120$; the arithmetic gap permits decay rate $\eta=1.77$ after normalization.
\item The prime-window criterion of Section~\ref{sec:criterion} applied with
$d=18$, $\eta=1.77$ and $\rho=120$ gives exponents less than $1281$ and $3662$.
\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. The contribution $\rho/2$ of the square-prime window alone exceeds
two even for the improved $\rho=120$, so reaching irrationality exponent two requires
a further structural improvement; the present proof does not establish such a bound.
\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 and prove the stronger bound in
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 resulting measure}
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
Theorem~\ref{thm:main}. The Lean statements in \lean{Parametric/TwentyMain}
are \lean{catalan\_irrationalityMeasure\_1281} and its \lean{3662}
counterpart; the public series statements appear in \lean{Solution.lean}.

\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\_1281}: for all sufficiently large $b\in\N$ and all $a\in\Z$, $b^{-1281}<|G-a/b|$ (Theorem~\ref{thm:main});
\item \lean{catalan\_irrationalityMeasure\_3662}: the same 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}
There is 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 through OpenAI's
workspace, which already uses it for Proposition~\ref{prop:openai}(c).

\begin{center}\small
\begin{tabular}{>{\raggedright\arraybackslash}p{0.38\textwidth}>{\raggedright\arraybackslash}p{0.53\textwidth}}
\toprule
File & Content\\
\midrule
\lean{DeltaPoly}, \lean{Degree} & $\Delta_N(X)$; Lemma~\ref{lem:degree}\\
\lean{Denominators}, \lean{IntegerValued}, \lean{Integrality} & Proposition~\ref{prop:denominators}; Lemma~\ref{lem:intvalued}; Corollary~\ref{cor:Q}\\
\lean{SparseDenominators}, \lean{DenseDenominators}, \lean{DenseGainPNT}, \lean{DenseMain} & Propositions~\ref{prop:sparse-rows}--\ref{prop:sparse-denominators}; the earlier $1981$ bound\\
\lean{Nonvanishing} & Proposition~\ref{prop:openai}(d) for $p\nmid\operatorname{den}z$\\
\lean{PrimeWindow}, \lean{Criterion}, \lean{PNTWindow}, \lean{Main} & Proposition~\ref{prop:criterion} and the reduction to Theorem~\ref{thm:perturbation}\\
\lean{Quadrature}, \lean{ChebyshevNodes}, \lean{QuadCircle} & Lemma~\ref{lem:quadrature}\\
\lean{DetExpansion} & Lemma~\ref{lem:expansion}\\
\lean{MixedAndreief} & Lemma~\ref{lem:andreief}\\
\lean{VandermondeProduct} & Lemma~\ref{lem:genvandermonde}\\
\lean{PinMajorant}, \lean{FixedNodes}, \lean{FixedNodeMajorant} & Proposition~\ref{prop:pointwise}, \eqref{eq:fixed-node}, and \eqref{eq:energy-identity}\\
\lean{PinDampedDual}, \lean{PinSupDual} & Proposition~\ref{prop:energy}\\
\lean{Cert/ListPoly}, \lean{Cert/LogApprox}, \lean{Cert/FieldEval}, \lean{Cert/FieldDeriv}, \lean{Cert/Cover}, \lean{Cert/Norm} & the general lemmas behind the checks of Proposition~\ref{prop:dual}\\
\lean{Dual/*}, \lean{DualTwo} & the certificate data, the kernel checks, Proposition~\ref{prop:dual}\\
\lean{SharpBarrier} & the remark after Proposition~\ref{prop:dual}\\
\lean{WeightedEnergy}, \lean{WeightedBounds} & Section~\ref{ssec:weighted}\\
\lean{SeparateFixedNodes}, \lean{SeparateBounds}, \lean{SeparateLemma6} & Theorem~\ref{thm:perturbation}\\
\lean{SquareNonvanishing}, \lean{SquarePNTWindow}, \lean{SquareMain} & Proposition~\ref{prop:square-nonvanishing}, strengthened Proposition~\ref{prop:criterion}\\
\lean{Parametric/TwentyMain}, \lean{TwentyIntegerPolynomial} & Section~\ref{sec:twenty}; the current $1281/3662$ bounds\\
\lean{TwentyDenominators}, \lean{TwentyTwoAdicNorm}, \lean{TwentyCombinedOddLoss} & Actual local arithmetic and common-denominator growth\\
\lean{TwentyTrial/*}, \lean{TwentyUniformEnergy}, \lean{TwentyPerturbation} & Certified population fields, mixed integration and $\rho=120$\\
\bottomrule
\end{tabular}
\end{center}

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 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{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
\url{https://github.com/openai/math} (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{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}