\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 10, 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 recent proof that Catalan's constant
$G=\sum_{j\ge0}(-1)^j/(2j+1)^2$ is irrational, we prove that
\[
 \left|G-\frac ab\right|>b^{-8\,127}
\]
for all integers $a$ and all sufficiently large integers $b$. Thus the irrationality
exponent of $G$ is at most $8\,127$; without the prime number theorem in the final step the same argument gives $23\,168$. The previous best bound, due to Jha, is $10^8$. The new
ingredient is a perturbation estimate for OpenAI's determinant, viewed as a polynomial
$\Delta_N(X)$ in the constant: on the interval $|x-G|\le e^{-404.25N}$ the polynomial moves by
no more than OpenAI's bound for $|\Delta_N(G)|$. It is proved by a quadrature formula for
the coefficient of the constant, an Andr\'eief identity with fixed columns, a
generalized Vandermonde bound, and OpenAI's energy method rerun for configurations with
fewer points. We also give a new certificate, with re-optimized trial sequences, for one of
the two cases of OpenAI's logarithmic-energy dual; it raises the margin of the argument by a
factor of almost eight. Every step, including the final theorem, is formalized in Lean~4 on top of
OpenAI's formalization, without \texttt{sorry} and with only the standard axioms.
\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^{-8\,127}.
\]
In particular $\mu(G)\le 8\,127$. If in the last step the prime number theorem is replaced by
Chebyshev's bounds, the same argument gives $|G-a/b|>b^{-23\,168}$.
\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 each perturbed column costs a factor $e^{\rho N}$ with $\rho=404.25$
(Theorem~\ref{thm:perturbation}). Our exponent is smaller than Jha's by a factor of about $12\,000$; the difference comes from this step and from the new energy certificate described below. 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}
OpenAI's matrix has entries in $\Q+\Q G$ (Proposition~\ref{prop:openai}(a)). Replacing $G$ by a
variable gives a polynomial $\Delta_N(X)\in\Q[X]$, and we proceed in four steps.
\begin{enumerate}[label=(\roman*)]
\item \emph{Arithmetic} (Section~\ref{sec:arith}). $\deg\Delta_N\le44N$ (Lemma~\ref{lem:degree}).
 OpenAI's local estimates, applied at integer points, give a common denominator $D_N$ with
 $\log D_N\le(\mathsf A+o(1))n^2$ (Proposition~\ref{prop:denominators}). So
 $Q_N=(44N)!\,D_N\,\Delta_N(X)$ has integer coefficients. OpenAI's nonvanishing argument gives
 $Q_p(a/b)\ne0$ for primes $p\nmid b$ (Proposition~\ref{prop:openai}(d)).
\item \emph{Perturbation} (Section~\ref{sec:perturbation}). For $|x-G|\le e^{-404.25N}$,
 $|\Delta_N(x)-\Delta_N(G)|\le e^{-(\mathsf U-\varepsilon)n^2}$ (Theorem~\ref{thm:perturbation}).
 Together with OpenAI's real bound this makes $|Q_p(x)|\le e^{-\eta p^2}$ on that interval, for any $\eta<2304\gamma_0$, where $\gamma_0=\mathsf U-\mathsf A$.
\item \emph{Criterion} (Section~\ref{sec:criterion}). A good approximation $a/b$ of $G$ lies in
 the small interval for a prime $p\nmid b$ of size about $\log b$, which contradicts
 $|Q_p(a/b)|\ge b^{-44p}$.
\item \emph{The real-place constant} (Section~\ref{ssec:dual}). OpenAI's real-place bound
 comes from a dual of a logarithmic energy, with certified trial sequences, in each of two
 cases. For the second case we construct new trial sequences and certify them with a
 computation checked by Lean's kernel. This improves the real-place constant from
 $2.290939875-\frac12\log2$ to $\mathsf U=2.29180925-\frac12\log2$ (Proposition~\ref{prop:dual})
 and raises $\gamma_0$ from $1.30\cdot10^{-4}$ to $1.00\cdot10^{-3}$.
\item \emph{Numerics} (Section~\ref{sec:proof}). The exponent is about
 $\rho\cdot44/(2304\gamma_0)\approx404.25\cdot19.1$, up to the factor coming from the size of
 the prime window.
\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{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{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\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:denominators}. The denominator of $a/b$ divides $b$, so
Proposition~\ref{prop:openai}(d) 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)$.
\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$.
\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=404.25$. 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|\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$.

\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^{nm}\,(2^{2h})^m\exp\Bigl(n^2\bigl(E^{(p)}_\kappa(x,s)+\tfrac12\log2\bigr)\Bigr).
\]
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
\[
 2^{nm}\,|\cR_n(z)|\prod_jw(y_j)\cdot\cJ^{(p)}(x,s).
\]
For a fixed node $-1<y<0$ we use $|y|\le1$, $(1-y)^{2h}\le2^{2h}$ and $1+y^2\ge1$, together
with $C-1+g-(n-1)=A=19N$ (OpenAI's $A$) and $(n-1)/2<C-1+h$:
\begin{equation}\label{eq:fixed-node}
 w(y)\,(1+y^2)^{\frac{n-1}2}|y|^{g-(n-1)}\le2^{C-1}2^{2h},\qquad
 w(y)\,|y|^{g-(n-1)}\le2^{C-1}2^{2h}.
\end{equation}
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^{nm}(2^{2h})^m\exp\bigl(n^2(E^{(p)}_1+\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^{nm}(2^{2h})^m\exp\bigl(n^2(E^{(p)}_2+\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}$ from $w(y)$. It is exactly compensated by the
difference between the $n$-node and $p$-node normalizations of the energy, so what remains is
$2^{2h}=4^{2N}$ per fixed node, coming from $(1-y)^{2h}$.
\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 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}

The kernel checks take about half an hour of computing time.

\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{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},
Proposition~\ref{prop:energy} and $U_\kappa<-2.29180925=-\mathsf U-\frac12\log 2$, every $f$
with $m=m(f)$ satisfies
\[
 |\det M_f|\le2^nK_n\,2^{nm}(2^{2h})^m\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^n\,2^{2h}\,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)+(n+2h)\log2+N\log K+nc^*\\ &=52N\log2+N\log K+48Nc^*+\log(8\cdot48\cdot65^3N^4),
\end{align*}
and $52\log2+\log K+48c^*=404.1708\ldots<404.25$; so $nJBc\le e^{404.25N}$ for $N\ge2000$. If $|\delta|\le e^{-404.25N}$ 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 cost $\log(Bc)$ of one perturbed
column splits as follows: the quadrature weights contribute $\log K\approx110.47$ (the
maximum bounded in the proof of Lemma~\ref{lem:quadrature} is $e^{110.394\ldots}$, so a
finer check would save another $0.08$); the
generalized Vandermonde bound, $48\log2\approx33.3$; the fixed nodes, $4\log2\approx2.8$; and
the energy lost by the missing point, $48c^*\approx257.7$.
\end{remark}

\section{Proof of the main theorem}\label{sec:proof}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Let $\gamma_0=\mathsf U-\mathsf A$ and $\eta=2304\cdot9.996945\cdot10^{-4}$, so that
$0<\eta<2304\gamma_0$ by \eqref{eq:gap}, and let $\varepsilon=(\gamma_0-\eta/2304)/3>0$. For large
primes $p$ and $|x-G|\le e^{-404.25p}$, Proposition~\ref{prop:dual} and
Theorem~\ref{thm:perturbation} give $|\Delta_p(x)|\le2e^{n^2(-\mathsf U+\varepsilon/2)}$. Also
$\log\bigl(2\,(44p)!\bigr)\le\frac\varepsilon2n^2$ for large $p$, and
$\log D_p\le(\mathsf A+\varepsilon)n^2$ by Proposition~\ref{prop:denominators}. Hence
\[
 |Q_p(x)|\le e^{-n^2(\gamma_0-2\varepsilon)}\le e^{-n^2(\gamma_0-3\varepsilon)}
 =e^{-n^2\eta/2304}=e^{-\eta p^2},
\]
since $n^2=2304p^2$. By Corollary~\ref{cor:Q} the hypotheses of
Proposition~\ref{prop:criterion} hold with $\xi=G$, $d=44$, this $\eta$ and $\rho=404.25$, and
\[
 \frac d\eta=\frac{44}{2304\cdot9.996945\cdot10^{-4}}=19.10305\ldots\le R=19.1031 .
\]
With the prime number theorem, $c=10001/10000$ and $\varepsilon=c/R=10001/191031$, the exponent is
\[
 \Bigl(1+\frac{10001}{191031}\Bigr)\cdot404.25\cdot R=404.25\,(R+c)=8\,126.71\ldots\le8\,127 .
\]
With Chebyshev's bounds it is at most $3\cdot404.25\cdot R=23\,167.28\ldots\le23\,168$.
\end{proof}

\begin{remark}[Limits of the method]\label{rem:limits}
The exponent is essentially $\rho\,(d/(2304\gamma_0)+c)\approx404.25\cdot20.1\approx8.1\cdot10^3$.
Further improvements must come from $\rho$, that is, from the contributions listed in the
remark at the end of Section~\ref{sec:perturbation}, or from a larger gap $\gamma_0$. Numerically,
enlarging the space of trial sequences in Proposition~\ref{prop:dual} changes $U_2$ only in the
sixth decimal, so a substantially larger $\gamma_0$ would require a different dual or a
different determinant. The energy $48c^*$ lost per missing point is the largest part of $\rho$;
we have not tried to optimize it.
\end{remark}

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

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 consists of about $8\,900$ lines of hand-written proofs in twenty-nine files, together with nineteen generated files (about $1\,400$ lines) holding the data and the kernel checks of Proposition~\ref{prop:dual} and the change of constants in OpenAI's certificate described in the remark after Proposition~\ref{prop:dual}. 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 main statements, in the namespace
\lean{OAI.InternalCatalan}, are:
\begin{itemize}
\item \lean{catalan\_irrationalityMeasure\_8127}: for all sufficiently large $b\in\N$ and all $a\in\Z$, $b^{-8127}<|G-a/b|$ (Theorem~\ref{thm:main});
\item \lean{catalan\_irrationalityMeasure\_23168}: the same with exponent $23\,168$;
\item \lean{eventually\_realDeterminant\_abs\_upper\_dual}: Proposition~\ref{prop:dual};
\item \lean{lemma6\_perturbation}: Theorem~\ref{thm:perturbation}, with $\rho=404.25$;
\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}
\begin{tabular}{>{\raggedright\arraybackslash}p{0.33\textwidth}>{\raggedright\arraybackslash}p{0.58\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{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{GenVandermonde}, \lean{GenVandermondeSharp} & Lemma~\ref{lem:genvandermonde}\\
\lean{PinMajorant} & Proposition~\ref{prop:pointwise} 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{Lemma6} & nodes, certified constants, Theorem~\ref{thm:perturbation}, Theorem~\ref{thm:main}\\
\bottomrule
\end{tabular}
\end{center}

The proofs were checked with Lean \texttt{v4.34.1} and Mathlib at commit \texttt{d13f23b}, the
versions pinned by OpenAI's repository at commit \texttt{fd4aeeb}. The Palomar registry of
formalized mathematics requires a newer Lean version and Lean's module system. For it, the
repository also contains the parts of OpenAI's formalization that the proof uses, converted to
modules; its README describes the details.

\section*{Disclosure of AI use}

The entire work reported here is due to 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 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}