\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}
\setcounter{tocdepth}{1}

\newcommand{\Z}{\mathbb Z}
\newcommand{\Q}{\mathbb Q}
\newcommand{\R}{\mathbb R}
\newcommand{\C}{\mathbb C}
\newcommand{\F}{\mathbb F}
\newcommand{\N}{\mathbb N}
\newcommand{\den}{\operatorname{den}}
\newcommand{\rank}{\operatorname{rank}}
\newcommand{\corank}{\operatorname{corank}}
\newcommand{\lean}[1]{\nolinkurl{#1}}
\renewcommand{\Re}{\operatorname{Re}}
\renewcommand{\Im}{\operatorname{Im}}
\newcommand{\Lw}{\mathsf L}          % Loewner matrix
\newcommand{\cO}{\mathcal O}
\newcommand{\Id}{\mathrm{Id}}
\newcommand{\err}{\operatorname{err}}
\newcommand{\cI}{\mathcal I}

\newcommand{\MuLamU}{31.2876}
\newcommand{\MuThirdsU}{9.4998}
\newcommand{\MuFifthsU}{23.8272}
\newcommand{\MuSeventhsU}{2207.8697}
\newcommand{\MuChi}{13.7046}
\newcommand{\MuHalvesU}{6.5253}
\newcommand{\LamFour}{3.5149036}  \newcommand{\DFour}{3.7447213}  \newcommand{\gFour}{7.1904273}  \newcommand{\ExpFour}{31.28751}
\newcommand{\LamThree}{3.3104458} \newcommand{\DThree}{4.0291249} \newcommand{\gThree}{6.8272548} \newcommand{\ExpThree}{9.499725}
\newcommand{\LamFive}{3.5128488}  \newcommand{\DFive}{3.8135797}  \newcommand{\gFive}{7.1655663}  \newcommand{\ExpFive}{23.82717}
\newcommand{\LamSeven}{3.6391158643} \newcommand{\DSeven}{3.6424792669} \newcommand{\gSeven}{7.4259546075} \newcommand{\ExpSeven}{2207.870}
\newcommand{\LamHalf}{2.9923824}  \newcommand{\DHalf}{3.9785713}  \newcommand{\gHalf}{6.4350874}  \newcommand{\ExpHalf}{6.525207}
\newcommand{\LamChi}{4.0959278}   \newcommand{\DChi}{4.6435117}   \newcommand{\gChi}{7.5043742}  \newcommand{\ExpChi}{13.70452}
\newcommand{\MuChiExact}{13.704516}

\begin{document}

\title[Irrationality measures for $L(2,\chi_{-3})$ and other trigamma differences]{Irrationality measures for
$L(2,\chi_{-3})$ and other differences of trigamma values}

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

\date{November 1, 2026}

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

\keywords{Irrationality exponent, trigamma function, $L(2,\chi_{-3})$, L\"owner matrices, $p$-adic valuations,
Hermite interpolation, Andr\'eief's identity, logarithmic energy, formal verification, Lean}

\begin{abstract}
We prove irrationality measures for several differences of values of the trigamma function $\psi'$ at
rational points. Among them are
\[
 \mu\bigl(L(2,\chi_{-3})\bigr)\le\MuChi,\qquad
 \mu\Bigl(L(2,\chi_{-3})\pm\frac{\pi^2}9\Bigr)\le\MuThirdsU,
\]
\[
 \mu\Bigl(G\pm\frac{5\pi^2}{48}\Bigr)\le\MuLamU,
\]
and $\mu(\psi'(\frac k5)-\pi^2/6)\le\MuFifthsU$ and $\mu(\psi'(\frac k7)-\pi^2/6)\le\MuSeventhsU$
for $k$ prime to the denominator. For $L(2,\chi_{-3})$ and $L(2,\chi_{-3})\pm\pi^2/9$ the best bound known before
was $24781$, due to Calegari, Dimitrov and Tang. For $G\pm5\pi^2/48$, $\psi'(\frac k5)-\pi^2/6$ and
$\psi'(\frac k7)-\pi^2/6$ we know of no earlier proof of irrationality.

The approximations are determinants of rectangular L\"owner matrices built from the digamma function at
integer nodes. We bound their denominators prime by prime, using the corank of the matrix modulo $p$ and
cancellations at second and third order in its Smith normal form. Nonvanishing at rational points follows
from Hermite interpolation in characteristic zero. The size of the determinants is bounded by
Andr\'eief's identity and an energy estimate. The proof is formalized in Lean~4.
\end{abstract}

\maketitle
\tableofcontents

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

\subsection{The result}
The values $\psi'(s)=\sum_{n\ge0}(n+s)^{-2}$ of the trigamma function at rational points $s=k/q$ are among the
simplest constants of analysis. Each is a rational linear combination of $\pi^2$ and the values $L(2,\chi)$ for the
Dirichlet characters $\chi$ modulo $q$. For $q\le2$ they are rational multiples of $\pi^2$. Already for $q=3$ and
$q=4$ they involve $L(2,\chi_{-3})$ and Catalan's constant $G=L(2,\chi_{-4})$, whose irrationality was proved only in
2024 and 2026 \cite{CDT2024,OpenAI2026}. Throughout the paper we work with the differences
\[
 \Psi(s,t)=\psi'(s)-\psi'(t)=\sum_{n=0}^\infty\Bigl(\frac1{(n+s)^2}-\frac1{(n+t)^2}\Bigr)\qquad(0<s<t\le1).
\]
We prove irrationality measures for $\Psi(s,t)$ for the pairs of Table~\ref{tab:main}, by a single determinant
construction.

The \emph{irrationality exponent} $\mu(\xi)$ of a real number $\xi$ is the infimum of the real numbers $\mu$ such that
$|\xi-a/b|>b^{-\mu}$ for all integers $a$ and all sufficiently large integers $b$. It does not change under
$\xi\mapsto r\xi+r'$ with $r,r'\in\Q$ and $r\ne0$. A finite bound for $\mu(\xi)$ is an irrationality measure for
$\xi$, and it shows that $\xi$ is irrational.

\begin{table}[ht]
\centering
\begin{tabular}{@{}ccll@{}}
\toprule
$(s,t)$ & $k$ & classical form & $\mu$ \\
\midrule
$(\frac k2,1)$ & $1$ & $\pi^2$ & $\MuHalvesU$ \\
\addlinespace
$(\frac k3,1)$ & $1$ & $L(2,\chi_{-3})+\frac{\pi^2}9$ & $\MuThirdsU$ \\
& $2$ & $L(2,\chi_{-3})-\frac{\pi^2}9$ & $\MuThirdsU$ \\
$(\frac13,\frac23)$ & -- & $L(2,\chi_{-3})$ & $\MuChi$ \\
\addlinespace
$(\frac k4,1)$ & $1$ & $G+\frac{5\pi^2}{48}$ & $\MuLamU$ \\
& $3$ & $G-\frac{5\pi^2}{48}$ & $\MuLamU$ \\
\addlinespace
$(\frac k5,1)$ & $1,2,3,4$ & -- & $\MuFifthsU$ \\
\addlinespace
$(\frac k7,1)$ & $1,\dots,6$ & -- & $\MuSeventhsU$ \\
\bottomrule
\end{tabular}
\caption{The pairs of Theorem~\ref{thm:main}, grouped by the denominator of $s$. The classical form is a number in
common notation that differs from $\Psi(s,t)$ by a rational affine map. A dash means that there is none. The last column is an upper bound for $\mu(\Psi(s,t))$.}\label{tab:main}
\end{table}

The classical forms come from the values
\begin{gather*}
 \psi'(\tfrac14)=\pi^2+8G,\qquad \psi'(\tfrac34)=\pi^2-8G,\\
 \psi'(\tfrac13)=\frac{2\pi^2}3+\frac92L(2,\chi_{-3}),\qquad \psi'(\tfrac23)=\frac{2\pi^2}3-\frac92L(2,\chi_{-3}),
\end{gather*}
together with $\psi'(\frac12)=\frac{\pi^2}2$ and $\psi'(1)=\frac{\pi^2}6$. Here
\begin{gather*}
 G=L(2,\chi_{-4})=\sum_{n\ge0}\Bigl(\frac1{(4n+1)^2}-\frac1{(4n+3)^2}\Bigr)=0.91596\,55941\ldots,\\
 L(2,\chi_{-3})=\sum_{n\ge0}\Bigl(\frac1{(3n+1)^2}-\frac1{(3n+2)^2}\Bigr)=0.78130\,24128\ldots
\end{gather*}
are the values at $2$ of the Dirichlet $L$-functions of the nontrivial characters modulo $4$ and modulo $3$. So
Catalan's constant and $L(2,\chi_{-3})$ are the first two cases of the same family. In the notation of this paper
\begin{gather*}
 \Psi(\tfrac14,1)=8\Bigl(G+\frac{5\pi^2}{48}\Bigr),\qquad \Psi(\tfrac34,1)=-8\Bigl(G-\frac{5\pi^2}{48}\Bigr),
 \qquad \Psi(\tfrac14,\tfrac34)=16G,\\
 \Psi(\tfrac13,1)=\frac92\Bigl(L(2,\chi_{-3})+\frac{\pi^2}9\Bigr),\qquad
 \Psi(\tfrac23,1)=-\frac92\Bigl(L(2,\chi_{-3})-\frac{\pi^2}9\Bigr),\\
 \Psi(\tfrac13,\tfrac23)=9L(2,\chi_{-3}),\qquad \Psi(\tfrac12,1)=\frac{\pi^2}3 .
\end{gather*}
For $q=5$ and $q=7$ there is no single classical constant. For $\gcd(k,q)=1$ the number $\Psi(\frac kq,1)$ is a
rational linear combination of $\pi^2$ and the values $L(2,\chi)$ for the Dirichlet characters $\chi$ modulo $q$,
since
\[
 \psi'(\tfrac kq)=q^2\sum_{n\equiv k\ (q)}\frac1{n^2}=\frac{q^2}{\varphi(q)}\sum_{\chi\bmod q}\bar\chi(k)L(2,\chi).
\]

\begin{theorem}\label{thm:main}\label{thm:thirds}\label{thm:fifths}
Let $(s,t)$ be a pair in Table~\ref{tab:main}, and let $\mu_{s,t}$ be the entry in the last column of its row. For all
integers $a$ and all sufficiently large integers $b$,
\[
 \Bigl|\Psi(s,t)-\frac ab\Bigr|>b^{-\mu_{s,t}}.
\]
In particular $\Psi(s,t)$ is irrational and $\mu(\Psi(s,t))\le\mu_{s,t}$. The same bound holds for the classical form in
the same row.
\end{theorem}

For $q=4$, $5$ and $7$ we know of no earlier proof that $\Psi(\frac kq,1)$ is irrational. For $q=4$ this does not
follow from the irrationality of $G=\frac1{16}\Psi(\frac14,\frac34)$, since it is not known whether $1$, $G$ and
$\pi^2$ are linearly independent over $\Q$. For $q=3$ irrationality was known \cite{CDT2024}, and the theorem
improves the known measures. The bound for $q=2$ is weaker than the known bounds for $\pi^2$ and is included for
completeness.

One family of determinants, with the same three estimates, covers every row of Table~\ref{tab:main}.

Theorem~\ref{thm:main} has been verified in the Lean~4 proof assistant, together with every theorem, proposition and
lemma used in its proof. The formal proof has no unproved steps and uses only the standard axioms.
Section~\ref{sec:lean} describes it. The remarks and Section~\ref{sec:limits} discuss the method and are not part of the
formal proof. The formalization is available at \FormalizationLink. The use of AI in this work is disclosed at the end
of the paper.

\subsection{Background}
\emph{Catalan's constant.} In October 2026 OpenAI \cite{OpenAI2026} proved that $G$ is irrational and formalized the
proof in Lean. Sun's preprint \cite{Sun2026} had claimed a proof of the irrationality of $G$. Wachs \cite{Wachs2026}
reports that its main estimate is not justified. Finite irrationality exponents for $G$ were obtained after OpenAI's
proof by Jha \cite{Jha2026}, Carreira \cite{Carreira2026}, Bojnal \cite{Bojnal2026}, Xu \cite{Xu2026} and the author
\cite{Litsey2026}. Carreira \cite{Carreira2026b} also records attempts to carry the determinant method to $\beta(4)$. For
the arithmetic of $G$ and related values before these results see
\cite{RivoalZudilin2003,Zudilin2003,Zudilin02Cheb,KrattRivoal08,KrattZudilin19} and the survey \cite{Zudilin19Survey}.
Eskandari, Murty and Nemoto \cite{EMN2025} construct a $2$-dimensional mixed motive over $\Q$ with period $G$. They use
it to obtain linear forms in $1$ and $G$. Eskandari \cite{Eskandari2026} improves the approximation exponent of these
forms of Rivoal--Zudilin type from $0.52$ to $0.62$. These are explicit approximations, not a lower bound for all
rationals. Our searches found no proof that $G-5\pi^2/48$ or $G+5\pi^2/48$ is irrational.

\emph{The value $L(2,\chi_{-3})$.} Calegari, Dimitrov and Tang \cite{CDT2024} proved that $1$, $\pi^2$ and
$L(2,\chi_{-3})$ are linearly independent over $\Q$. Their proof applies a new arithmetic holonomy bound to a
construction of Zagier. In \cite{CDT2025} they made holonomy bounds effective. Theorem~5.1 there gives
$\mu(L(2,\chi_{-3}))\le24781$. The remark that follows that theorem states that the same theorem and proof hold for any
$\Q$-linear combination of $L(2,\chi_{-3})$ and $\pi^2$. So $24781$ is also the known bound for
$L(2,\chi_{-3})\pm\pi^2/9$. Theorem~\ref{thm:main} improves it to $\MuChi$ for $L(2,\chi_{-3})$ and to $\MuThirdsU$ for
$L(2,\chi_{-3})\pm\pi^2/9$. Leibtag et al.\ \cite{LBKWSK26} find numerically that Ap\'ery-like approximations from
conservative matrix fields have positive approximation exponents for $L(2,\chi_{-3})\pm\pi^2/9$. A supplement to their
paper uses one such field to give an Ap\'ery-style proof of the theorem of Calegari, Dimitrov and Tang. The exponent it
proves for each of these two numbers is only greater than $10^{-4}$.

\emph{The numbers $\psi'(\frac k5)-\pi^2/6$ and $\psi'(\frac k7)-\pi^2/6$.} Our searches found no irrationality result for
them. Prellberg \cite{Prellberg26} proved that $\mathrm{Li}_2(1/5)$ is irrational, but that is a different number.

\emph{Recent results.} Since September 2026 a series of new results has appeared in this area. Several of them were
obtained with AI systems. They join classical results such as the bound $\mu(\log2)<3.5746$ of Marcovecchio
\cite{Marcovecchio09}, the bounds of Rhin and Viola for $\pi^2$ and $\zeta(3)$ \cite{RhinViola96,RhinViola01}, which
followed Ap\'ery and Beukers \cite{Apery79,Beukers79}, and Zudilin's bound for $\pi^2$ \cite{Zudilin14}. OpenAI proved
$\mu(\pi)=2$, with a Lean formalization \cite{OpenAIPi2026}. This improves the bound $\mu(\pi)<7.1033$ of Zeilberger and
Zudilin \cite{ZeilbergerZudilin20}. Liu, Jiang and Zhang proved $\mu(\log r)=2$ for every rational $r>0$ with $r\ne1$
\cite{LiuJiangZhang26}. Their result also covers nonzero rational combinations of such logarithms. Giraudin lowered the
bound for $\mu(\pi^2)$ to $5.0193784$ with two hypergeometric constructions of Zudilin \cite{Zudilin14} at new parameters
\cite{Giraudin26}. Giraudin also lowered the bound for $\mu(\zeta(3))$ to $5.5138800$ by applying the Rhin--Viola method
at a new integral direction \cite{Giraudin26z3}. Leibtag, Barkan, Kalisch, Weinbaum, Shalyt and Kaminer \cite{LBKWSK26}
showed that the classical constructions are one-dimensional trajectories in conservative matrix fields. By searching over
other trajectories they obtained $\mu(\pi^2)<4.62675$ and $\mu(\zeta(3))<5.4197$. Prellberg \cite{Prellberg26} proved that
$\mathrm{Li}_2(-1/4)$, $\mathrm{Li}_2(1/5)$ and $\mathrm{Li}_2(-1/3)$ are irrational. These are three cases left open in
\cite{CDT2024}. The proof uses the integrals of Rhin--Viola and Viola--Zudilin. Fauzan \cite{Fauzan2026} announced a proof
that $\zeta(5)$ is irrational, using rationally normalized Hankel determinants. Lai \cite{Lai2026} combined that method
with simultaneous approximations of Zudilin and of Dauguet and Zudilin. Lai showed that $1$, $\zeta(3)$ and $\zeta(4)$
are linearly independent over $\Q$.

\emph{Determinant methods.} Irrationality proofs built on determinants of large size have a precedent in Zudilin's
determinantal criterion with Hankel determinants \cite{Zudilin}. The preprint of Liu, Jiang and Zhang on logarithms
\cite{LiuJiangZhang26} uses a separated-weight interpolation determinant. The arguments of Fauzan and Lai
\cite{Fauzan2026,Lai2026} use Hankel determinants. Brown \cite{Brown26} proposes a multivariate transfinite-diameter test
for Mellin-type integrals and applies it to $\pi^2$. The framework we use is OpenAI's \cite{OpenAI2026}. In it the decay
of the determinants is controlled by Cauchy determinants and Andr\'eief's identity, and the denominators are controlled
prime by prime. Our determinants are L\"owner matrices, that is, matrices of divided differences, of a digamma
difference. They are a matrix-valued analogue of Pad\'e and Hermite--Pad\'e approximation \cite{NikishinSorokin91}.
Formal proofs of irrationality results in Lean also include the irrationality of $\zeta(3)$ by Liu, Zhang and Zhi
\cite{LZZ25}.

\subsection{The companion paper}
Catalan's constant is also a difference of trigamma values, $G=\frac1{16}\Psi(\frac14,\frac34)$, and the construction
applies to this pair. For it, however, our bound for the denominators exceeds our bound for the decay, so we obtain no
measure for $G$. The companion paper \cite{Litsey2026} refines OpenAI's determinant instead and proves
$\mu(G)\le410$. Our computations for $(\frac14,\frac34)$ are not part of the formal proof.

The row for $\pi^2$ is included only to show the reach of the construction. Since $\zeta(2)=\pi^2/6$, much better bounds
are known, the best being $\mu(\pi^2)<4.62675$ of Leibtag et al.\ \cite{LBKWSK26}.

\subsection{What a measure requires}
Let $P(x)$ be a polynomial with rational coefficients for which $P(\xi)$ is small, and suppose that $|\xi-a/b|$ is very
small. Three estimates turn this into a lower bound for $|\xi-a/b|$.
\begin{enumerate}[label=(\roman*)]
\item \emph{Denominators.} The coefficients of $P$ have a common denominator of size $e^{(\Lambda+o(1))r^2}$.
\item \emph{Smallness on a neighbourhood.} $|P(x)|\le e^{-(D-o(1))r^2}$ for every $x$ with $|x-\xi|\le e^{-\rho r}$,
 not only at $\xi$.
\item \emph{Nonvanishing at the point.} $P(a/b)\ne0$ for some member of the family whose size can be chosen in terms
 of $b$.
\end{enumerate}
In OpenAI's argument for $G$ the size of the determinant is tied to a prime $p$, and nonvanishing is proved modulo $p$.
Here nonvanishing is proved in characteristic zero, so the size $r$ is free. The matrices are also simpler: their
entries are divided differences of a single digamma combination. We prove the three estimates once, uniformly in the
shift.

\subsection{New ideas}
The proof rests on the following ideas. Section~\ref{sec:overview} explains each of them in more detail.
\begin{enumerate}[leftmargin=*]
\item \emph{Rectangular L\"owner matrices.} The rows and columns share a long block of nodes $\{0,\dots,r-1\}$, which
 carries the variable. A further $m\approx cr/2$ row nodes and $m$ column nodes alternate beyond it. The degree of the
 determinant in the variable is still $r$, while its decay is that of a larger node set. The border nodes never meet
 the diagonal, so the denominators grow less than the decay.
\item \emph{Denominators from local bounds.} For each prime we prove a list of upper bounds for the valuation of the
 common denominator. Each is an explicit integer expression in $r$, $m$, $p$ and the first pole $k_p$. Integrated
 against $\log p$, their minimum gives the denominator exponent. Checking this minimum reduces to finitely many
 comparisons of rational numbers.
\item \emph{Primes smaller than the border.} When $p\le2m$ some residue classes contain two border nodes. Eliminating
 these pairs by Schur complements leaves a smaller matrix of the same shape, to which the separation argument for large
 primes applies at third order in the Smith normal form.
\item \emph{Nonvanishing in characteristic zero.} A kernel vector of the matrix at a rational point corresponds to a
 solution of a Hermite interpolation problem. A Wronskian argument bounds the corank independently of $r$, so a
 principal minor of bounded codimension does not vanish.
\item \emph{Decay through a trial measure.} Andr\'eief's identity turns the determinant into an integral whose
 logarithm is a discrete logarithmic energy. Comparison with a piecewise polynomial trial measure bounds this energy,
 leaving a lower bound for one explicit function on finitely many segments.
\end{enumerate}
The constants of the proof for each row of Table~\ref{tab:main} are listed in Table~\ref{tab:data}.

\subsection{Organization}
Section~\ref{sec:overview} explains the construction and the main ideas without technicalities, and states the general
deduction. Section~\ref{sec:construction} gives the construction. Sections~\ref{sec:content}, \ref{sec:nonvanishing}
and~\ref{sec:decay} prove the three estimates, for the denominators, nonvanishing and decay, uniformly in the shift.
Section~\ref{sec:chi3-quarter} treats the function $F_\chi$ of the pair $(\frac13,\frac23)$. Section~\ref{sec:proof} deduces
Theorem~\ref{thm:main} and comments on the individual rows. Section~\ref{sec:limits} discusses the limits of the method. Section~\ref{sec:lean} describes the formalization. The
disclosure of AI use follows it.

\subsection{Notation and conventions}
We write $\psi$ for the digamma function, the logarithmic derivative of Euler's gamma function, and $v_p$ for the
$p$-adic valuation. For $P\in\Q[x]$, $\den P$ is the least positive integer whose product with $P$ lies in $\Z[x]$. We
write $[0,r)=\{0,1,\dots,r-1\}$. For finite sets $X_0$, $Y_0$ of integers and a matrix $A$ indexed by integers,
$A[X_0,Y_0]$ is the submatrix with rows $X_0$ and columns $Y_0$.

%% =====================================================================
\section{Overview of the method}\label{sec:overview}

\subsection{L\"owner matrices of digamma differences}
Let $F$ be a function analytic near a finite set of distinct points. The \emph{L\"owner matrix} \cite{Loewner34} of $F$
is the matrix of divided differences indexed by the points:
\[
 \Lw_F[t,t']=\frac{F(t')-F(t)}{t'-t}\ (t\ne t'),\qquad \Lw_F[t,t]=F'(t).
\]
It is a Cauchy-like structured matrix. Hermite's formula gives
$\Lw_F=\frac1{2\pi i}\oint F(z)\,\upsilon(z)\upsilon(z)^{\top}dz$ with $\upsilon_t(z)=1/(z-t)$. A representation of $F$ as
a Stieltjes or contour integral therefore exhibits $\Lw_F$ as a Gram matrix of Cauchy kernels.

For a rational shift $0<s<1$ with denominator $q$ we take the digamma difference $F_s$. For the pair
$(\frac13,\frac23)$ we take a combination $F_\chi$ of three digamma functions. The nodes are integers. We put
\begin{equation}\label{eq:frames}
\begin{gathered}
 F_s(z)=\psi(z+1)-\psi(z+s),\qquad \omega=\tfrac1{q^2},\quad \xi_s=-\tfrac1{q^2}\Psi(s,1),\\
 F_{\chi}(z)=-\tfrac13\psi(z+\tfrac13)+\tfrac12\psi(z+\tfrac12)-\tfrac16\psi(z+1),\\
 \omega=-\tfrac16,\quad \xi_\chi=\tfrac1{36}\Psi(\tfrac13,\tfrac23).
\end{gathered}
\end{equation}
In each case $\xi=\omega\,F'(0)$. The differences $F(t')-F(t)$ and $F'(t)-F'(0)$ are rational for integers $t,t'\ge0$.
Let $R$ and $Q$ be finite sets of nonnegative integer nodes, which index the rows and the columns. Then
\begin{equation}\label{eq:shift}
 \omega\,\Lw_F[R,Q]=M[R,Q]+\xi\,\Id_{R,Q},\qquad \Id_{R,Q}[t,t']=\mathbf 1[t=t'],
\end{equation}
with an explicit symmetric function $M$ on $\Z_{\ge0}^2$ with rational values, given in \S\ref{sec:construction}.
Replacing $\xi$ by a variable $x$ gives the matrix polynomial $\Phi(x)=M[R,Q]+x\Id_{R,Q}$. Its determinant $P(x)$ has
rational coefficients and degree at most $|R\cap Q|$, and $P(\xi)=\det(\omega\,\Lw_F[R,Q])$.

Suppose that $|\xi-a/b|$ is very small. Then $P(a/b)$ is very close to $P(\xi)$, which is tiny. On the other hand
$b^{|R\cap Q|}\den(P)\,P(a/b)$ is an integer. If it is not zero, we get a contradiction as soon as
\[
 \underbrace{\log\den P}_{\text{denominators}}+|R\cap Q|\log b\ <\ \underbrace{-\log|P(a/b)|}_{\text{decay}} .
\]
Three estimates are therefore needed: an upper bound for $\log\den P$, the \emph{arithmetic estimate}; an upper bound
for $|P(x)|$ near $\xi$, the \emph{analytic estimate} or decay; and the \emph{nonvanishing} of $P(a/b)$ for some member
of a family of determinants whose size can be chosen in terms of $b$. Each estimate is proved once, for every shift,
and the families differ only in a few parameters.

\subsection{Rectangular L\"owner matrices with an alternating border}
We take a long common block $C=[0,r)$, which carries the variable $x$, and add $m$ row nodes and $m$ column nodes that
alternate beyond it:
\[
 X'=\{r,r+2,\dots,r+2m-2\},\qquad Y'=\{r+1,r+3,\dots,r+2m-1\}.
\]
The rows are $R=C\sqcup X'$ and the columns are $Q=C\sqcup Y'$ (Figure~\ref{fig:geometry}). The determinant
$P(x)=\det\Phi(x)$ has degree at most $r$, since the variable occurs only on the diagonal of the common block. So the
factor $b^{\deg P}$ in the contradiction is that of $r$ nodes, while the matrix has size $r+m$ and its decay is that of
about $(1+c/2)r$ nodes, where $c=2m/r$ is the length of the border relative to $r$. The denominators grow too, but less,
because border rows and border columns never share a node. To guarantee nonvanishing we also use the principal minors
that delete a bounded number of common nodes. A larger $c$ raises $D$ and $\Lambda$ together, and we chose $c$
numerically to minimise $\rho/(D-\Lambda)$. Its value for each constant is given in Table~\ref{tab:data}.

\begin{figure}[ht]
\centering
\setlength{\unitlength}{0.42cm}
\begin{picture}(20,13)(-6,-1)
 \put(0,0){\framebox(13,11){}}
 \put(8,0){\line(0,1){11}}
 \put(0,3){\line(1,0){13}}
 \multiput(0.5,10.5)(1,-1){8}{\makebox(0,0){$\scriptstyle x$}}
 \put(4,11.6){\makebox(0,0){$\scriptstyle 0,1,\dots,r-1$}}
 \put(10.5,11.6){\makebox(0,0){$\scriptstyle r+1,\,r+3,\,r+5$}}
 \put(-0.3,7){\makebox(0,0)[r]{$\scriptstyle 0,\dots,r-1$}}
 \put(-0.3,1.5){\makebox(0,0)[r]{$\scriptstyle r,\,r+2,\,r+4$}}
 \put(4,12.5){\makebox(0,0){$C$}}
 \put(10.5,12.5){\makebox(0,0){$Y'$}}
 \put(-4.8,7){\makebox(0,0)[r]{$C$}}
 \put(-4.8,1.5){\makebox(0,0)[r]{$X'$}}
 \put(4,1.5){\makebox(0,0){$M[X',C]$}}
 \put(10.5,7){\makebox(0,0){$M[C,Y']$}}
 \put(10.5,1.5){\makebox(0,0){$M[X',Y']$}}
\end{picture}
\caption{The geometry for $r=8$ and $m=3$. Rows are indexed by $C\sqcup X'$ and columns by $C\sqcup Y'$. The variable
$x$ occurs only on the diagonal of the common block. The border rows $X'=\{r,r+2,r+4\}$ and border columns
$Y'=\{r+1,r+3,r+5\}$ alternate and never meet the diagonal.}\label{fig:geometry}
\end{figure}

The interleaving of $X'$ and $Y'$ is essential. It keeps the two Cauchy determinants in Andr\'eief's formula comparable
(\S\ref{sec:decay}). It also gives the reduction of the matrix modulo a prime an alternating structure. Several of the
arithmetic bounds of \S\ref{sec:content} rest on this structure.

\subsection{Denominators from local bounds}
As in the work of Rhin and Viola \cite{RhinViola96,RhinViola01}, we bound the $p$-adic valuation of the common
denominator prime by prime and sum the bounds with the prime number theorem in arithmetic progressions. For $p\asymp r$
the valuation depends on $r$, $m$, $p$ and the first pole $k_p$, the least index $k_p\ge1$ at which the second digamma
term has a pole modulo $p$. One has $k_p=\kappa p+O(1)$ with $\kappa=j/q$, where the residue $j\equiv qs\,p^{-1}\pmod q$
is the \emph{root class} of $p$. The function $F_\chi$ has two first poles, and on each class of primes modulo $6$ both
are affine functions of one index of the same kind (Section~\ref{sec:chi3-quarter}).

The local bounds come from three sources: the valuations of the entries, the corank of the reduction modulo $p$, and
cancellations at second and third order in the Smith normal form. Each is an explicit piecewise linear expression in
$(r,m,p,k_p)$, valid in a range of $p/r$ described by linear inequalities. Replacing $(r,m,p,k_p)$ by
$(1,\alpha,\theta,\kappa\theta)$, with $\alpha=c/2$, turns it into a piecewise affine function of $\theta=p/r$, with an
explicitly bounded error. The \emph{denominator exponent} is
\[
 \Lambda=\frac1{\varphi(q)}\sum_j\int_0^\infty\mathcal P_j(\theta)\,d\theta,
\]
where $\mathcal P_j$ is the minimum of these functions for the root class $j$. A table of affine pieces above
$\mathcal P_j$ certifies $\Lambda$ by finitely many comparisons of rational numbers (Theorem~\ref{thm:content}). The
bounds depend on the shift only through the root class, so one table serves every shift with denominator $q$, and the
numbers $\Psi(s,1)$ for these shifts receive the same exponent.

\subsection{Primes smaller than the border}
For $p\le2m$ some residue classes modulo $p$ contain two border nodes, a row $t$ and a column $t+p$. The bounds above
are not sharp for these primes. Each such pair gives a pivot that is a $p$-adic unit, because the interval $(t,t+p]$
contains one pole of each digamma term and their contributions cannot cancel. Eliminating these pivots leaves a matrix
of the same shape with a border of $d=\|m\|_p$ rows and columns. To this smaller matrix we apply the separation
argument used for large primes, at third order. Two identities for bordered inverses show that the elimination does not
disturb the second-order terms (Lemma~\ref{lem:bordered}). A rational interpolation problem of type $(n,n)$ shows that
the remaining border nodes stay separated (Lemma~\ref{lem:harmonic}).

\subsection{Nonvanishing}
Let $x_0$ be a rational point. The kernel of $\Phi(x_0)$ is identified with a space of pairs of polynomials that satisfy
Hermite interpolation conditions at the nodes. Two such pairs have vanishing cross product, by a count of degrees and
zeros. A further pair in the kernel would give a rational antidifference of the increment of $F$. No such
antidifference exists, because the pole at $-1$ is isolated in its class modulo $\Z$. This bounds the corank of
$\Phi(x_0)$ by a number that depends only on $F$ and on the alternation of the border. A principal restriction that
deletes at most that many common nodes is then nonsingular. This is Theorem~\ref{thm:selection}. No prime enters, so
the size $r$ can be chosen freely in terms of $b$.

\subsection{Decay}
Moving Hermite's contour to a polygonal path $\Gamma$ in the left half-plane writes $\omega\,\Lw_F[R,Q]$ as a Gram matrix
$\int\upsilon_t\upsilon_{t'}\,d\Omega$. Here $\Omega$ is a complex measure. It has signed atoms at poles of $F$ and an
exponentially small density on $\Gamma$. Andr\'eief's identity with two families of functions, one for the rows and one
for the columns, gives
\[
 |\det\Lw_F[R,Q]|\le\frac1{n_*!}\int\bigl|\mathsf C_R(z)\bigr|\,\bigl|\mathsf C_Q(z)\bigr|\prod_{i=1}^{n_*}d|\Omega|(z_i),
\]
where $n_*$ is the size of the matrix and $\mathsf C_R$, $\mathsf C_Q$ are Cauchy determinants. Taking logarithms turns
the integrand into a discrete logarithmic energy. The free points $z_i$ interact with the nodes in an external field.

We bound this energy from below by comparing it with a \emph{trial measure} $\sigma$, a density that is polynomial on
each of finitely many segments. The comparison uses the conditional positive definiteness of the logarithmic kernel.
What is left is a lower bound for one explicit function $\Upsilon$ on the contour, on the segment carrying the atoms and
on the interval of the nodes. We prove it on a finite cover of these sets by cells, each checked in exact rational
arithmetic. One theorem, Theorem~\ref{thm:decay}, gives the decay for every geometry parameter $c\le1$ and every
function $F$ whose poles are separated from the contour. Each family then supplies only $\sigma$, the polygon and the
cover.

\subsection{The deduction}
Write $\eta=D-\Lambda$, where $D$ is the \emph{decay rate}, and let $\rho$ be the \emph{neighbourhood exponent} of the
decay estimate: the decay holds at every point within $e^{-\rho r}$ of $\xi$. Section~\ref{sec:proof} combines the
three estimates into
\[
 \mu(\xi)\le\frac\rho\eta=\frac\rho{D-\Lambda}.
\]
This is the bound $d\rho/\eta$ of the companion paper \cite{Litsey2026} with degree $d=1$ per unit of scale.

\subsection{Formal verification}
Every step is formalized in Lean~4 with Mathlib \cite{Lean4,Mathlib}: the local arithmetic bounds and the conditions on
the tables for $\Lambda$, the interpolation argument for nonvanishing, the contour representation, the cell checks of
the decay estimate, and the prime number theorem in arithmetic progressions. The formal proofs share one core, which
contains rectangular determinants, Gauss valuations, the local bounds, the tables for $\Lambda$, the selection in
characteristic zero, the decay theorem and the deduction. A family supplies its function $F$, its geometry parameter and
its numerical tables. The written proofs below are at the level of a research article. For long computations we point
to the formal proof, which is the basis for the correctness of Theorem~\ref{thm:main}.

%% =====================================================================
\section{The construction}\label{sec:construction}

\subsection{The entries of $M$}
Let $0<s<1$ be rational with denominator $q$. Put $u=q(1-s)$, so that $k-1+s=(qk-u)/q$. For the function $F_s$ of
\eqref{eq:frames}, the rational matrix $M$ of \eqref{eq:shift} is as follows. Here $0\le t<t'$ are integers, and
$M[t',t]=M[t,t']$.
\begin{align*}
 M[t,t']&=\frac1{q^2(t'-t)}\sum_{k=t+1}^{t'}\Bigl(\frac1k-\frac q{qk-u}\Bigr),\\
 M[t,t]&=-\frac1{q^2}\sum_{k=1}^{t}\Bigl(\frac1{k^2}-\frac{q^2}{(qk-u)^2}\Bigr).
\end{align*}
For $s=\frac34$ this is $M[t,t']=-\frac1{t'-t}\sum_{k=t+1}^{t'}\frac1{16k(4k-1)}$. For the function $F_\chi$,
\[
 M[t,t']=\frac1{6(t'-t)}\sum_{k=t+1}^{t'}g(k),\qquad M[t,t]=\frac16\sum_{k=1}^{t}g'(k),
\]
with $g(k)=\frac1{3k-2}-\frac1{2k-1}+\frac1{6k}$. Then
$-\frac16g'(k)=\frac1{2(3k-2)^2}-\frac1{3(2k-1)^2}+\frac1{36k^2}$.

We write each function as $F=\sum_{\varsigma\in\mathcal T}w_\varsigma\psi(z+\varsigma)$, where $\mathcal T$ is the set of
shifts of $F$ and $\sum_\varsigma w_\varsigma=0$. For $F_s$, $\mathcal T=\{1,s\}$ with $w_1=1$ and $w_s=-1$. For
$F_\chi$, $\mathcal T=\{\frac13,\frac12,1\}$. The number $|\mathcal T|$ of digamma terms is $2$ for $F_s$ and $3$ for
$F_\chi$.

\begin{lemma}\label{lem:loewner}
For each function of \eqref{eq:frames}, $\omega\,\Lw_F[R,Q]=M[R,Q]+\xi\Id_{R,Q}$ for all finite sets
$R,Q\subset\Z_{\ge0}$, with $\omega$ and $\xi$ as in \eqref{eq:frames}.
\end{lemma}
\begin{proof}
From $\psi(w+1)-\psi(w)=1/w$ one gets $F_s(k)-F_s(k-1)=\frac1k-\frac1{k-1+s}=\frac1k-\frac q{qk-u}$. Telescoping gives the
off-diagonal entries. In the same way $\psi'(w+1)-\psi'(w)=-1/w^2$ gives $F_s'(t)-F_s'(0)$. Finally
$\omega F_s'(0)=q^{-2}(\psi'(1)-\psi'(s))=-q^{-2}\Psi(s,1)=\xi_s$. For $F_\chi$ the entries are computed in the same way.
For the value at $0$, the multiplication formula $\sum_{i<n}\psi'(z+\frac in)=n^2\psi'(nz)$ gives
$\psi'(\frac12)=3\psi'(1)$ and $\psi'(\frac13)+\psi'(\frac23)=8\psi'(1)$. Hence
$F_\chi'(0)=-\frac13\psi'(\frac13)+\frac12\psi'(\frac12)-\frac16\psi'(1)=-\frac16\Psi(\frac13,\frac23)$, and
$-\frac16F_\chi'(0)=\frac1{36}\Psi(\frac13,\frac23)=\xi_\chi$.
\end{proof}

Since $\mu$ is invariant under rational affine maps, Theorem~\ref{thm:main} is a statement about the numbers $\xi$ of
\eqref{eq:frames}.

\subsection{Geometries}
\begin{definition}\label{def:geometry}
Let $r,m\ge0$. The \emph{geometry} $\mathcal G(r,m)$ consists of the common nodes $C=[0,r)$, the row nodes
$X'=\{r+2i:0\le i<m\}$ and the column nodes $Y'=\{r+2i+1:0\le i<m\}$. Rows are indexed by $R=C\sqcup X'$ and columns by
$Q=C\sqcup Y'$. Let $I\subseteq C$ be a set of deleted common nodes. The matrix
\[
 \Phi_{\mathcal G,I}(x)=\bigl(M[t,t']+x\,\mathbf 1[t=t'\in C\setminus I]\bigr)_{t\in R\setminus I,\ t'\in Q\setminus I}
\]
is square of size $|C\setminus I|+m$. Put $P_{\mathcal G,I}(x)=\det\Phi_{\mathcal G,I}(x)\in\Q[x]$. We write
$\Phi_{\mathcal G}$ and $P_{\mathcal G}$ when $I=\emptyset$, and we write $\bar N=r+2m$ for the number of nodes.
\end{definition}

By Lemma~\ref{lem:loewner}, $\Phi_{\mathcal G}(\xi+h)=\omega\,\Lw_F[R,Q]+h\Id_{R,Q}$ for real $h$. The geometry with
$m=0$ is the square L\"owner matrix of size $r$.

\begin{definition}\label{def:altgeom}
Let $0<c\le1$ and $\alpha=c/2$. The \emph{alternating geometry} of parameter $c$ at an even scale $r$ is
$\mathcal G(r,m(r))$ with $m(r)=\lceil\alpha r-\frac12\rceil$. Then $|m(r)-\alpha r|\le\frac12$, and the border
$[r,r+2m)$ has length $cr+O(1)$. For a depth $K\ge0$, its \emph{members} are the matrices
$\Phi_{r,I}=\Phi_{\mathcal G,I}$ with $|I|\le K$. We put $P_{r,I}=\det\Phi_{r,I}$.
\end{definition}

For the functions $F_s$ we use $c=\frac3{10},\frac15,\frac3{10},\frac29,\frac16$ for $q=2,4,3,5,7$. For $F_\chi$ we use
$c=\frac12$, as explained in Section~\ref{sec:chi3-quarter}. All $o(1)$ terms below are uniform over the members as
$r\to\infty$.

\begin{lemma}[integrality]\label{lem:integrality}
$P_{\mathcal G,I}$ has degree at most $|C\setminus I|$. If $a$ and $b\ge1$ are integers with
$P_{\mathcal G,I}(a/b)\ne0$, then $|\den(P_{\mathcal G,I})\,P_{\mathcal G,I}(a/b)|\ge b^{-|C\setminus I|}$.
\end{lemma}
\begin{proof}
The variable occurs only in the $|C\setminus I|$ diagonal entries indexed by $C\setminus I$. So each Leibniz term has
degree at most $|C\setminus I|$. Then $b^{|C\setminus I|}\den(P_{\mathcal G,I})\,P_{\mathcal G,I}(a/b)$ is a nonzero
integer.
\end{proof}

\emph{Example.} Take $s=\frac34$, $r=2$ and $m=1$, so that $C=\{0,1\}$, $X'=\{2\}$ and $Y'=\{3\}$. Then
\[
 \Phi_{\mathcal G}(x)=\begin{pmatrix}
 x & -\frac1{48} & -\frac{67}{7392}\\[2pt]
 -\frac1{48} & x+\frac7{144} & -\frac{47}{14784}\\[2pt]
 -\frac{17}{1344} & -\frac1{224} & -\frac1{528}
 \end{pmatrix}
\]
and
\[
 P_{\mathcal G}(x)=-\frac{x^2}{528}-\frac{823\,x}{3725568}-\frac{239}{37158912}.
\]
The variable occurs only at the common nodes $0$ and $1$, so the degree is $|C|=2$ although the matrix has size $3$. When $M[X',Y']$ is invertible, a Schur complement shows that $P_{\mathcal G}$
is, up to a constant factor, the characteristic polynomial of a rational matrix of size $|C|$, as in the square case.
We do not use this factorisation.

%% =====================================================================
\section{Arithmetic: the denominators}\label{sec:content}

In this section we bound the common denominator of the coefficients of the members $P_{r,I}$ for the functions $F_s$.
The method is that of Rhin and Viola \cite{RhinViola96,RhinViola01}: the $p$-adic valuation of the denominator is bounded
prime by prime, and the bounds are summed against $\log p$ with the prime number theorem in arithmetic progressions.
What is new is the form of the local bounds. Each is an explicit integer expression in four integers attached to the
prime, and their minimum, integrated, gives the denominator exponent.

The local bounds come from four mechanisms, of increasing depth.
\begin{enumerate}[label=(\alph*)]
\item \emph{Valuations of the entries.} The assignment bounds (T1)--(T5) of \S\ref{sssec:trop} use only the
 valuations of single entries and LP duality.
\item \emph{Corank modulo $p$.} The bounds (LP1), (LP2) and (R) of \S\S\ref{sssec:lp} and~\ref{sssec:rank} compute the
 corank of the reduction of a rescaled matrix.
\item \emph{Second order.} The bounds (W) and (S) of \S\S\ref{sssec:window} and~\ref{ssec:sep} use the pairing of kernel
 vectors modulo $p^2$ (\S\ref{ssec:second}).
\item \emph{Third order.} The bounds (U$_n$) of \S\ref{sssec:wrap} treat the primes smaller than the border.
\end{enumerate}
Comparing the local bounds with a table of affine pieces is a finite computation with rational numbers, and
Theorem~\ref{thm:content} turns an admissible table into the arithmetic estimate. Section~\ref{sec:chi3-quarter} treats the
function $F_\chi$.

\subsection{The root class of a prime}
Fix the function $F_s$, with $s$ of denominator $q$, and the alternating geometry of parameter $c=2\alpha$.
Let $p>q$ be a prime. The indices $k\ge1$ at which the entries of $M$ acquire a denominator divisible by $p$ are the
multiples of $p$ and the solutions of $qk\equiv u\pmod p$. Let $k_p$ be the least of the latter. Then
\[
 qk_p=jp+u,\qquad 0<j<q,\qquad j\equiv qs\,p^{-1}\pmod q .
\]
We call $j$ the \emph{root class} of $p$ and put $\kappa=\kappa_j=j/q$. Then $k_p-\kappa p=u/q\in[\frac1q,1-\frac1q]$. So
the first pole is at distance less than one from $\kappa p$, uniformly in $s$. Throughout we assume $q(r+2m)<p^2$. Then
every pole below $\bar N$ is simple, and only the first power of $p$ matters. The primes with $p^2\le q(r+2m)$ and the prime
powers contribute $O(r^{3/2}\log r)$ in total.

\subsection{Gauss valuations, the assignment bound and the rank of the reduction}
Fix a prime $p$. Let $\cO\subset\Q(x)$ be the localisation of $\Z_{(p)}[x]$ at the prime ideal $(p)$. It is a discrete
valuation ring with uniformiser $p$ and residue field $\F_p(x)$. Its valuation $v$, restricted to $\Q[x]$, is the
\emph{Gauss valuation} $v(f)=\min_k v_p(f_k)$ for $f=\sum f_kx^k$. By Gauss's lemma $v(fg)=v(f)+v(g)$, and
$v_p(\den f)=\max(0,-v(f))$. For a member we write $e_p(r,I)=v_p(\den P_{r,I})$.

\begin{lemma}[assignment bound and LP duality]\label{lem:trop}
Let $A$ be a square matrix over $\Q[x]$ with rows $X_0$ and columns $Y_0$. Let $W_{tt'}=\max(0,-v(A_{tt'}))$, and let
$\tau(W)$ be the largest weight $\sum W_{tt'}$ of a perfect matching between $X_0$ and $Y_0$. Then
$v(\det A)\ge-\tau(W)$. If real numbers $u_t$, $u'_{t'}$ satisfy $W_{tt'}\le u_t+u'_{t'}$ for all $t\in X_0$ and
$t'\in Y_0$, then $\tau(W)\le\sum_tu_t+\sum_{t'}u'_{t'}$.
\end{lemma}
\begin{proof}
Each Leibniz term is a product of entries along a perfect matching. So its valuation is at least minus the weight of the
matching. The valuation of a sum is at least the minimum of the valuations of its terms. The second statement is weak
LP duality for the assignment problem. The weight of a perfect matching is at most $\sum_tu_t+\sum_{t'}u'_{t'}$.
\end{proof}

\begin{lemma}[rank of the reduction]\label{lem:rank}
Let $(u,u')$ be integer potentials with $W_{tt'}\le u_t+u'_{t'}$ for the matrix $\Phi_{r,I}$ at $p$, of value
$\tau'=\sum_tu_t+\sum_{t'}u'_{t'}$. Then $\widetilde\Phi=\operatorname{diag}(p^{u})\,\Phi_{r,I}\,
\operatorname{diag}(p^{u'})$ has entries in $\cO$, and
\[
 e_p(r,I)\le\tau'-\corank_{\F_p(x)}(\widetilde\Phi\bmod p).
\]
\end{lemma}
\begin{proof}
We have $v(\det\Phi_{r,I})=-\tau'+v(\det\widetilde\Phi)$. Over the discrete valuation ring $\cO$ the Smith normal form
shows $v(\det\widetilde\Phi)\ge\corank(\widetilde\Phi\bmod p)$.
\end{proof}

\subsection{Second-order information}\label{ssec:second}
The rank bounds below use a refinement of Lemma~\ref{lem:rank} at second order. Suppose that, after a unimodular change
of rows and columns over $\cO$, the first $n_1$ rows and the first $n_2$ columns of $\widetilde\Phi$ are divisible by
$p$. Suppose also that the $n_1\times n_2$ block where they meet is divisible by $p^2$. Dividing the first $n_1$ rows by
$p$ leaves the first $n_2$ columns divisible by $p$. So
\begin{equation}\label{eq:corner}
 v(\det\widetilde\Phi)\ge n_1+n_2 .
\end{equation}

The vectors that produce such rows and columns are kernel vectors of the reduction of $\widetilde\Phi$ on single residue
classes. The condition on the corner is a statement about their pairing at first order, which we now describe. Let
$\widetilde\Phi=p^2\Phi_{r,I}$, so that all potentials equal $1$. Since $q(r+2m)<p^2$, two distinct nodes $t\ne t'$ have
$v_p(t'-t)\ge1$ only if $t\equiv t'\pmod p$, and then $v_p(t'-t)=1$. Hence $\widetilde\Phi$ has entries in $\cO$. Its
reduction is block diagonal over the residue classes modulo $p$, which we call the \emph{fibres}. For nodes $t$, $t'$
in distinct fibres,
\begin{equation}\label{eq:firstorder}
 \widetilde\Phi_{tt'}\equiv\frac{p\,(V(t')-V(t))}{t'-t}\pmod{p^2}.
\end{equation}
Here $V(t)\in\F_p$ is the residue of $p$ times the partial sum $\sum_{k\le t}(\frac1k-\frac q{qk-u})$, up to the
normalising factor $q^{-2}$. The function $V$ is a step function of $t$ which jumps only at the poles $t\equiv0$ and
$t\equiv k_p$. Since $t'-t$ is prime to $p$, only its residue matters in \eqref{eq:firstorder}.

For a vector $\mathbf y$ indexed by nodes, its \emph{moment pair} is
\[
 \hat{\mathbf y}=\Bigl(\sum_ty_t,\ \sum_ty_tV(t)\Bigr).
\]

\begin{lemma}[pairing]\label{lem:pairing}
Let $\mathbf y$ be supported on the rows of one fibre and $\mathbf y'$ on the columns of a different fibre. Let $t$ and
$t'$ be nodes of the first and of the second fibre. Then
\[
 \mathbf y^{\top}\widetilde\Phi\,\mathbf y'\equiv\frac p{t'-t}\,
 \det\begin{pmatrix}\hat{\mathbf y}\\ \hat{\mathbf y}'\end{pmatrix}\pmod{p^2}.
\]
In particular the pairing vanishes modulo $p^2$ whenever the moment pairs of $\mathbf y$ and $\mathbf y'$ are
proportional.
\end{lemma}
\begin{proof}
Expand $\mathbf y^{\top}\widetilde\Phi\,\mathbf y'$ with \eqref{eq:firstorder}.
\end{proof}

The moment pairs are never both zero. This follows from the displacement structure of L\"owner matrices.

\begin{lemma}[moment lemma]\label{lem:moment}
Let $A$ be a matrix with rows indexed by a set $X_0$ of distinct integers and columns by a set $Y_0$, with
$|X_0|=|Y_0|+1$. Suppose that its off-diagonal entries are $A(t,t')=(\mathcal L(t')-\mathcal L(t))/(t'-t)$ for some
function $\mathcal L$, and that its diagonal entries, on $X_0\cap Y_0$, are arbitrary. Then $A$ has a nonzero left kernel
vector $\mathbf y$ with $(\sum_ty_t,\sum_ty_t\mathcal L(t))\ne(0,0)$.
\end{lemma}
\begin{proof}
Write $\operatorname{diag}(X_0)$ and $\operatorname{diag}(Y_0)$ for the diagonal matrices of the indices. Then
$\operatorname{diag}(X_0)A-A\operatorname{diag}(Y_0)=\mathcal L_{X_0}\mathbf 1^{\top}-\mathbf 1\mathcal L_{Y_0}^{\top}$,
because the diagonal entries cancel on common indices. The left kernel $\mathcal V$ of $A$ is nonzero. Suppose that
every $\mathbf y\in\mathcal V$ had zero moment pair. Multiplying on the left by $\mathbf y^{\top}$ would give
$\mathbf y^{\top}\operatorname{diag}(X_0)A=0$. So $\operatorname{diag}(X_0)$ would preserve $\mathcal V$. As this matrix
is diagonal with distinct entries, $\mathcal V$ would contain a standard basis vector. That vector is supported on one
index $t$, and its moment pair is $(1,\mathcal L(t))\ne(0,0)$. This is a contradiction.
\end{proof}

\subsection{The local bounds}
We now list the local bounds. Each is a statement of the following form. Let $P_{r,I}$ be a member with $|I|\le K$, and
let $p>p_0$ be a prime with $q(r+2m)<p^2$ that satisfies the stated conditions. Then
\begin{equation}\label{eq:localform}
 e_p(r,I)\le\tau(r,m,p,k_p)+\epsilon_\tau\,|I| .
\end{equation}
Here $\tau$ is the expression in the table and $\epsilon_\tau\in\{0,1\}$ is given in its last column. The
constant $p_0$ depends only on $F$. We write $(\cdot)_+=\max(\cdot,0)$, $\|m\|_p$ for the distance of $m$ to
$p\Z$, and $\bar u=(k_p+p-r)_+$.

\begin{theorem}[local bounds]\label{thm:local}
The following bounds of the form \eqref{eq:localform} hold.
\begin{center}
{\renewcommand{\arraystretch}{1.2}
\begin{tabular}{@{}lp{0.47\textwidth}p{0.27\textwidth}c@{}}
\toprule
 & bound $\tau$ & conditions & $\epsilon_\tau$\\
\midrule
(T1) & $2(r+m)$ & none & $0$\\
(T1$'$) & $2r+2m-\|m\|_p$ & none & $0$\\
(T2) & $2(r-\bar u)_++2m+\min(\bar u,2m)$ & $2m<p\le r$ & $0$\\
(T3) & $2r+m$ & $2m<p\le r$ & $0$\\
(T4) & $2(r-k_p)_++2m+(2m-(p-r))_+$ & $r<p$ & $0$\\
(T5) & $(2m-(k_p-r)_+)_+$ & $\bar N\le p$, $r\le k_p$ & $0$\\
(LP1) & $\tau_{\rm T2}-(\min(\bar u,2m)-m)_+$ & $p\le r<p+k_p$, $\bar N\le2p$ & $1$\\
(LP2) & $2(r-k_p)+3m$ & $r<p<r+m$, $k_p\le r$, $\bar N\le2p$ & $1$\\
(W) & $2r+2m-(t_2-t_1)$ for each window $[t_1,t_2)$ of Theorem~\ref{thm:window} & as there & $0$\\
(R) & $\Pi_R$ of \eqref{eq:PiR} & $2m<p$ & $0$\\
(S) & $\Pi_S$ of \eqref{eq:PiS} & $2m\le p$ & $1$\\
(U$_n$) & $\Pi_{U,n}$ of \eqref{eq:PiU}, $n\ge0$ & $np\le m<(n+1)p$, and $p\le2m$ if $n=0$ & $0$\\
\bottomrule
\end{tabular}}
\end{center}
\end{theorem}

The rest of this subsection proves Theorem~\ref{thm:local}, family by family.

\subsubsection{The assignment bounds (T1)--(T5)}\label{sssec:trop}
These follow from Lemma~\ref{lem:trop} with explicit potentials. Consider an off-diagonal entry $M[t,t']$. By the
ultrametric inequality, $-v_p(M[t,t'])$ is at most the number of the following two events that occur: the interval
$(t,t']$ contains a pole, and $p$ divides $t'-t$. A diagonal entry $M[t,t]$ has $-v_p\le2$ if $t\ge k_p$ and $-v_p\le0$
if $t<k_p$. The bound (T1) is the trivial bound, with potentials $1$ on every row and column.

For (T1$'$) the potentials depend on the residue class modulo $p$. On the rows of a class they are $\frac12$,
$\frac32$ or $1$, according as $X'$ has more, fewer or as many nodes in the class as $Y'$. On the columns they are
$\frac32$, $\frac12$ or $1$ in the same three cases. The border alternates between $X'$ and $Y'$. So the imbalance is
at most one per class, and the number of unbalanced classes is $2\|m\|_p$.

For (T2)--(T5) one starts from the potential $\mathbf 1[t\ge k_p]$ on the common nodes $t$, which accounts for the diagonal.
One adds $1$, or $1+\mathbf 1[t\ge p]$, on the border nodes $t$. Then one raises the potentials of the common nodes that
have a congruent partner in the border. In each range one checks $W\le u+u'$ entrywise. Two facts are used. Two distinct
nodes not congruent modulo $p$ have weight at most $1$. Two border nodes are never congruent once $2m<p$. For (T5) we
have $\bar N\le p$ and $r\le k_p$. Then no common node accounts for the diagonal, and only the border nodes beyond $k_p$ carry
potential $1$. So (T5) vanishes once $k_p\ge \bar N$, which happens for $p/r>\max(1+2\alpha,1/\kappa)+o(1)$. All cases are
checked in the formal proof.

\subsubsection{Primes near $r$: the bounds (LP1) and (LP2)}\label{sssec:lp}
For $p$ close to $r$ the reduction of the rescaled matrix has a large block of rank one per residue class. Its corank
can be computed. We give the proof of (LP2). The bound (LP1) applies to the primes with $p\le r<p+k_p$ and $\bar N\le2p$. It
is proved by the same method. With the potentials of (T2), eliminating an invertible block of common nodes brings the
reduction to the form $\begin{psmallmatrix}\tilde x\Id&\mathcal J_Y\\ \mathcal J_X&0\end{psmallmatrix}$, where $\tilde x$
is the variable $x$ plus a constant. In this form the border nodes below $p+k_p$ contribute rows and columns
proportional to unit vectors. The Frobenius--K\"onig theorem bounds its rank. The saving over (T2) is
$(\min(2m,p+k_p-r)-m)_+$, where $\min(2m,p+k_p-r)$ is the number of border nodes below $p+k_p$. We refer to the formal
proof for the details.

\begin{theorem}\label{thm:lp2}
Assume $r<p<r+m$, $k=k_p\le r$ and $\bar N=r+2m\le2p$, and that every pole below $\bar N$ is simple. Then
$v(\det\Phi_{r,\emptyset})\ge-(2(r-k)+3m)$. The same holds for every member, with $\epsilon_\tau=1$.
\end{theorem}
\begin{proof}
Use the potentials $u(t)=\mathbf 1[k\le t]$ for common nodes $t<r$ and $u(t)=1+\mathbf 1[p\le t]$ for border nodes $t$.
Their value is $\tau'=2(r-k)+2m+(\bar N-p)$. Since $\bar N\le2p$, the poles below $\bar N$ are $k$, $p$, and $p+k$ if $p+k<\bar N$. Each is
simple. The residues of $p$ times the increment $\frac1t-\frac q{qt-u}$ at these poles are $-q/j$, $1$ and $-q/(q+j)$.

\emph{Rows and columns beyond $p+k$ vanish.} Let $t\in[p+k,\bar N)$ be a border node, so that $u(t)=2$. Let $t'$ be a node of
the other kind. If $t'<k$, then $u(t')=0$. The partial sum over $(t',t]$ then has valuation at least $-1$, and
$t-t'\in(p,2p)$ is prime to $p$. Otherwise $u(t')\ge1$ and $v_p(M[t',t])\ge-2$. In both cases the rescaled entry is
divisible by $p$.

\emph{The remaining entries.} For nodes below $p+k$ the only poles are $k$ and $p$. Put $C_0=[0,k)$ and $C_1=[k,r)$.
Recall that $\omega=q^{-2}$ is the normalisation of \eqref{eq:frames}. The reduction has the following blocks. On
$C_0\times C_0$ it is the regular part plus $x$ on the diagonal. On $C_0\times C_1$ the entries are
$-\omega q/(j(t-t'))$ with $t'\in C_0$ and $t\in C_1$. On $C_1\times C_1$ it is the scalar matrix $\omega(q/j)^2\Id$. A
border node $t\in[r,p)$ against $t'\in C_0$ gives $\omega q/(j(t-t'))$. A border node $t\in[p,p+k)$ against $t'\in C_0$
gives $\omega(1-q/j)$ if $t'=t-p$, and $0$ otherwise. All other border entries vanish.

\emph{Rank.} Delete the zero rows and columns found above. This does not change the rank. Eliminate the scalar block on
$C_1$. The Schur complement on $C_0$ is $\tilde x\Id$ plus a constant multiple of the matrix with entries
$\sum_{i=1}^{p-r}\frac1{(t+i)(t'+i)}$ for $t,t'\in C_0$. Here $\tilde x$ is $x$ plus a constant, and the computation uses
the reflection $H_{p-1-n}\equiv H_n\pmod p$ of harmonic numbers. The border nodes $t\in[r,p)$ are indexed by $i=p-t$.
They are all present because $\bar N>p$. Even offsets are rows and odd offsets are columns, and together they cover
$1\le i\le p-r$. So row and column operations remove that multiple and leave
$\begin{psmallmatrix}\tilde x\Id&\mathcal J_Y\\ \mathcal J_X&0\end{psmallmatrix}$. Here it is essential that $x$ is an
indeterminate, so that $\tilde x$ is a unit. A Schur complement on $\tilde x\Id$ then shows that the rank is
$k+\rank(\mathcal J_X\mathcal J_Y)$. In $\mathcal J_X\mathcal J_Y$ the block between the high rows and the high columns is
zero, since their offsets $t-p$ have opposite parities. So $\rank(\mathcal J_X\mathcal J_Y)\le p-r$. In total the rank of
the reduction is at most $(r-k)+k+(p-r)=p$, and the corank is at least $r+m-p$. Lemma~\ref{lem:rank} gives
$v(\det)\ge(r+m-p)-\tau'=-(2(r-k)+3m)$. Deleting a common node changes the potentials by at most one.
\end{proof}

Under the hypothesis $\bar N\le p+k$ the third pole does not occur, and the proof is shorter. The border nodes beyond $p+k$
only contribute rows and columns that vanish modulo $p$. This observation allows the whole range $\bar N\le2p$, which is
automatic on the interval $r<p<r+m$.

\subsubsection{Pole-free windows: the bound (W)}\label{sssec:window}
Like the rank bounds, the bound (W) does not come from the valuations of the entries alone. Between two consecutive
poles the step function $V$ of \eqref{eq:firstorder} is constant. The reductions of the fibres of nearby residue classes
are then translates of one another. Kernel vectors can be transported from one fibre to the next. Their pairings vanish
modulo $p^2$ by Lemma~\ref{lem:pairing}. The corner bound \eqref{eq:corner} turns this into a saving at second order.

A \emph{cut} is an integer $t$ with $t\equiv0$, $t\equiv k_p$ or $t\equiv r\pmod p$. A window $[t_1,t_2)$ of integers is
\emph{cut-free} if no cut lies in the open interval $(t_1,t_2)$.

\begin{theorem}\label{thm:window}
Assume that every pole below $\bar N$ is simple and $\bar N<p^2$. Let $n\ge0$ with $np\le m$, and put $\bar N_n=r+2(m-np)$. Let
$[t_1,t_2)$ be a cut-free window with $\max(r,\bar N_n-p)\le t_1\le t_2\le\min(\bar N_n,r+p)$. Then every member satisfies
\[
 e_p(r,I)\le2r+2m-(t_2-t_1).
\]
\end{theorem}
For $n=0$ the windows lie in the border above $\max(r,\bar N-p)$, and the bound applies to primes $p>m$. For
$n=\lfloor m/p\rfloor\ge1$ it applies to the small primes $p\le m$. For these primes only (T1) and (T1$'$) are
available among the assignment bounds. Read modulo $p$, the window range is then the arc of residues that receive an odd
number of border nodes. The saving over (T1$'$) is the amount, if any, by which the length of the longest cut-free run
of this arc exceeds $\|m\|_p$. For other $n$ the window range is empty. The proof uses $F$ only through its poles.
For a function with several digamma terms the same statement holds when the cuts are the residues of all the poles and
of $r$.

\begin{proof}
Let $\widetilde\Phi=p^2\Phi$, with independent diagonal variables on the common nodes. Every member is a coefficient of
this determinant, so a bound for it bounds every member. Let $i<i'$ be two positions of the window. They lie in
different residue classes. The translation $t\mapsto t+(i'-i)$ maps the nodes of the fibre of $i$ bijectively onto those
of the fibre of $i'$. It maps common nodes to common nodes, since no $t\equiv r$ lies in $(i,i']$. It maps border nodes
to border nodes, since both classes lie in the window range. It maps $X'$ to $Y'$ when $i'-i$ is odd. There is no pole
in $(i,i']$. So the step function $V$ and the diagonal residues are unchanged, and so are the differences of nodes.
Hence the reduced block of the fibre of $i'$ equals that of $i$ when $i'-i$ is even, and its transpose when $i'-i$ is
odd.

In the window the fibres alternate between one more row than column and one more column than row. Take a nonzero left
kernel vector $\mathbf y$ of one block and transport it to every fibre of the window. It is a left kernel vector on the
fibres with a surplus row and a right kernel vector on the others. Its moment pair is the same everywhere. By
Lemma~\ref{lem:pairing} all pairings between these vectors vanish modulo $p^2$. There are $n_1$ such vectors on rows and
$n_2$ on columns, with $n_1+n_2=t_2-t_1$. Extending them to unimodular matrices, \eqref{eq:corner} gives
$v(\det\widetilde\Phi)\ge t_2-t_1$. Since $\det\widetilde\Phi=p^{2(r+m)}\det\Phi$, the theorem follows.
\end{proof}

\subsubsection{The rank bound (R)}\label{sssec:rank}
Let $2m<p$. Write $r=k_0p+r_p$ with $0\le r_p<p$. Note that $k_p=\lceil jp/q\rceil$, since $0<u<q$. Put
$\mathrm{arc}_0=[0,k_p-1]$ and $\mathrm{arc}_1=[k_p,p-1]$. For $k\ge0$ and $\iota\in\{0,1\}$ let
\[
\begin{gathered}
 n_{k,\iota}=\bigl|[r,r+2m)\cap[kp+\min\mathrm{arc}_\iota,\,kp+\max\mathrm{arc}_\iota]\bigr|,\\
 n_{\rm sq}=\bigl|[\max(0,r+2m-p),\min(r,k_p))\bigr|,
\end{gathered}
\]
and
\begin{multline}\label{eq:PiR}
 \Pi_R=2(r+m)\\-\max\bigl(m+n_{\rm sq},\ n_{0,0}+n_{1,0}+2n_{\rm sq},\ n_{k_0,0},\ n_{k_0,1},\ n_{k_0+1,0},\ n_{k_0+1,1}\bigr).
\end{multline}

\begin{proof}[Proof of the bound (R)]
Every node is $t=i+pk$ with residue $i\in[0,p)$ and digit $k$. Write $k(i)$ for the number of common nodes in the fibre
of $i$. The border has length $2m<p$. So this fibre contains the common digits $0,\dots,k(i)-1$ and at most one border
digit, namely $k(i)\in\{k_0,k_0+1\}$. This border node is a row or a column according to the parity of $i+pk(i)-r$. The
step function $V$ is constant on the fibre up to the bit $\iota(i)=\mathbf 1[i\ge k_p]$. Thus the reduced block of a fibre
depends only on $(k(i),\iota(i))$ and on the role of its border digit. Its entries have the L\"owner form of
Lemma~\ref{lem:moment}.

A fibre with a border row has a left kernel vector with nonzero moment pair. A fibre with a border column has such a
right kernel vector. For the digit $0$ below the pole the step function vanishes. So these fibres have moment pairs
proportional to $(1,0)$. A fibre of type $(1,0)$ without border digit has the zero block and contributes one row and one
column. Choosing one such vector per fibre annihilates $m+n_{\rm sq}$ rows and as many columns. This gives the saving
$m+n_{\rm sq}$.

Within a class of fibres of the same type $(k,\iota)$ all moment pairs are equal. So by Lemma~\ref{lem:pairing} the
pairings between the annihilated rows and columns of one class vanish modulo $p^2$. Then \eqref{eq:corner} gives a saving
equal to the number of annihilated coordinates of the class. This number is $n_{k,\iota}$ for $k\ge1$ and
$(k,\iota)\ne(1,0)$. It is $n_{0,0}+n_{1,0}+2n_{\rm sq}$ for the class with moment pair $(1,0)$. Taking the best class gives
\eqref{eq:PiR}. A deleted common node changes at most one fibre. Give up that fibre, and one further fibre to restore the
balance of rows and columns. The trivial certificate then costs at most two annihilated coordinates of each kind. The smaller
matrix compensates for them, so $\epsilon_\tau=0$.
\end{proof}

\subsubsection{Separated border nodes: the bound (S)}\label{ssec:sep}
The bound (S) uses a different source of cancellation. Choose a window $[t_0,t_v]$ of border nodes whose residues lie in
one arc between consecutive poles. Consider a border node outside it. Suppose the interval between the node and $t_0$
contains a singular index. Then the residues modulo $p$ of $p$ times the partial sums at the two nodes differ, because
two singular contributions in an interval of length less than $p$ cannot cancel. The leading coefficient in $x$ of the
bordered determinant of a fibre is this residue. So the cross product of the two bordered fibre determinants has a
nonzero leading coefficient. The border node is then eliminated against $t_0$ with no further information. Count the
residues of the window together with the residues of the eliminated border nodes. This gives an explicit bound, a
minimum over the four window types $(k,\iota)\in\{k_0,k_0+1\}\times\{0,1\}$, which we now state.

Let $2m\le p$, and let $k_0$, $r_p$, $\mathrm{arc}_0$, $\mathrm{arc}_1$ and $n_{k,\iota}$ be as in \S\ref{sssec:rank}.
For a type $(k,\iota)$ let $\mathcal K_{k,\iota}$ be the interval of the integers $kp+i$ with $i\in\mathrm{arc}_\iota$,
and with $i<r_p$ if $k=k_0+1$. The border nodes in $\mathcal K_{k,\iota}$ form the window, and there are $n_{k,\iota}$ of
them. Let $n_K$ be the number of border nodes in $\mathcal K_{k,\iota}$ and in its two translates
$\mathcal K_{k,\iota}\pm p$. Put
\[
 n_\emptyset=p-|\mathcal K_{k,\iota}|-(2m-n_K),\qquad n_+=(n_{k,\iota}-m)_+ .
\]
Since $2m\le p$, each residue class receives at most one border node. So $n_K$ is the number of border nodes whose
residues are those of $\mathcal K_{k,\iota}$. And $n_\emptyset$ is the number of the other residue classes that receive
no border node. Then
\begin{equation}\label{eq:PiS}
 \Pi_S=\min_{(k,\iota)}\bigl(2r+m-n_+-(n_+-n_\emptyset)_+\bigr),
\end{equation}
where a type whose window is empty contributes $2r+m$. The bound (S) is $e_p(r,I)\le\Pi_S+|I|$. Its proof carries out the
elimination above for every border node outside the window. We refer to the formal proof for it.

\subsubsection{Primes smaller than the border: the bound (U$_n$)}\label{sssec:wrap}
When $p\le2m$ the border meets some residue classes more than once, and the bound (S) is not available. The bound (U$_n$)
extends it to these primes. It works at third order in the Smith normal form. We show two things. After the elimination
of a block of unit pivots, the rescaled matrix has the Smith invariants of a smaller geometry, to which the separation
argument of (S) applies. The third-order information of that argument survives the elimination.

Write $m=np+\bar m$ with $0\le\bar m<p$, so that $n=\lfloor m/p\rfloor$. Put
\[
 d=\|m\|_p=\min(\bar m,p-\bar m),\qquad \bar r=r+m-d .
\]
For $i\in\{0,1,2\}$ and $\iota\in\{0,1\}$ let $Z_i=p\lfloor r/p\rfloor+(n+i)p$, and put
\[
 w_0=Z_i+\min\mathrm{arc}_\iota,\quad t_0=\max(\bar r,w_0),\quad t_v=\min(Z_i+\max\mathrm{arc}_\iota,\,\bar r+p-1).
\]
We call the geometry with common block $[0,\bar r)$ and border $[\bar r,\bar r+2d)$ the \emph{auxiliary geometry}
$(\bar r,d)$. In it, let
$n_+=\bigl(\min(t_v+1,\bar r+2d)-t_0-d\bigr)_+$. Let $n_K$ be the number of border nodes in $[w_0,t_v]$ and in its two
translates by $\pm p$, and let $n_\emptyset=p-(t_v+1-w_0)-(2d-n_K)$. Then
\begin{equation}\label{eq:PiU}
 \Pi_{U,n}=\min_{i,\iota}\Bigl(2(r+m)-d-n_+-(n_+-n_\emptyset)_+\Bigr),
\end{equation}
all subtractions being truncated. This is the expression \eqref{eq:PiS} for the auxiliary geometry $(\bar r,d)$, with the
windows $[w_0,t_v]$ in place of $\mathcal K_{k,\iota}$. Note that $2(r+m)-d=2\bar r+d$.

\begin{theorem}\label{thm:wrap}
Let $p>p_0$ be a prime with $q(r+2m)<p^2$, and let $n\ge0$ with $np\le m<(n+1)p$. Assume $p\le2m$ if $n=0$. Then every
member satisfies $e_p(r,I)\le\Pi_{U,n}$.
\end{theorem}

We first describe the proof for $n=0$, that is $m<p\le2m$. We then give the changes for $n\ge1$. As in the proof of
Theorem~\ref{thm:window} we work with $\widetilde\Phi=p^2\Phi$. We put an independent indeterminate $x_t$ on each common
diagonal entry. We work over the discrete valuation ring $\cO$ of Gauss valuations in these indeterminates. Every member
is a coefficient of $\det\widetilde\Phi$, up to the deletion of common rows and columns, which we treat at the end.

\emph{Pivots from pairs of border nodes.} For $n=0$ there are $2m-p$ residue classes that carry two border nodes $t<t+p$, one a row and the
other a column. There are $2d$ classes that carry one border node, and they lie in an interval of length $2d<p$.
Eliminate the common block. Its fibres are invertible because the $x_t$ are indeterminates. Consider a class with two
border nodes. Let $A$ be its common fibre, let $\mathbf a$ and $\mathbf a'$ be the couplings of its border column and
border row to $A$, and let $\varkappa$ be its border entry. After the elimination the class has the pivot
$\varpi=\varkappa-\mathbf a'^{\top}A^{-1}\mathbf a$. As the $x_t$ tend to infinity, $\varpi$ tends to a nonzero multiple
of the residue of $p$ times the increment of $F$ over $(t,t+p]$. This interval contains exactly one pole of each
digamma term. Let $k'p$ be the multiple of $p$ in it, and $t'$ the pole of the second term. If the two contributions
cancelled, then $q(t'-k'p)\equiv u$ with $|q(t'-k'p)-u|<q$. Hence $q(t'-k'p)=u$, which is impossible for $0<u<q$. So
these $2m-p$ pivots are units.

After them, the matrix of size $r+m=\bar r+d$ is equivalent over $\cO$ to $\operatorname{diag}(\Id_{\bar r},p\,\Xi)$,
with $\Xi$ of size $d$. Its Schur complement on the border has the expansion
\begin{equation}\label{eq:schur3}
 S=p\,S_1+p^2\bigl(S_2-\mathcal C_{UB}\mathcal B^{-1}\mathcal C_{BU}\bigr)+O(p^3).
\end{equation}
Here $\mathcal B$ is the diagonal of these pivots. The matrices $\mathcal C_{UB}$ and $\mathcal C_{BU}$ are the
first-order couplings between these pivots and the single border nodes. The correction term in \eqref{eq:schur3} is not
negligible. The following identities account for it.

\begin{lemma}[bordered inverses]\label{lem:bordered}
Let $A$ be an invertible square matrix over a commutative ring, and let $\mathbf u$ be a vector.
\begin{enumerate}[label=(\alph*),leftmargin=*]
\item Let $A'$ be obtained from $A$ by replacing one column by a vector $\mathbf w$, and suppose that $A'$ is invertible.
 Let $\mathbf u'$ be obtained from $\mathbf u$ by replacing the corresponding entry by $\mathbf u^\top A^{-1}\mathbf w$.
 Then $\mathbf u'^{\top}A'^{-1}\mathbf u=\mathbf u^\top A^{-1}\mathbf u$.
\item Suppose that the matrix
 \[
  A'=\begin{pmatrix}A&\mathbf a\\ \mathbf a'^\top&\varkappa\end{pmatrix}
 \]
 is invertible. Then
 $(\mathbf u,y)^\top A'^{-1}(\mathbf u,\mathbf a'^\top A^{-1}\mathbf u)=\mathbf u^\top A^{-1}\mathbf u$ for every
 scalar $y$.
\end{enumerate}
No symmetry of $A$ or $A'$ is assumed.
\end{lemma}
\begin{proof}
(a) Comparing columns gives $\mathbf u'^{\top}=\mathbf u^\top A^{-1}A'$. (b) We have
$A'\,(A^{-1}\mathbf u,0)^\top=(\mathbf u,\mathbf a'^\top A^{-1}\mathbf u)^\top$.
\end{proof}

\emph{Moments.} In the separation argument of (S), a border node is counted when its moment relative to a reference
node vanishes. That moment is the bilinear form $\mathbf u^\top A^{-1}\mathbf u$ in the inverse of the common fibre $A$
of its residue class. After the elimination, the common fibre of a class with two border nodes is replaced by a mixed
block $A'$ as in Lemma~\ref{lem:bordered}. Its lower node is a row and its upper node a column, or conversely. The
product added to $A'^{-1}$ is exactly the product subtracted in \eqref{eq:schur3}. So, by Lemma~\ref{lem:bordered}, the
moments of the counted classes are unchanged. The single border nodes outside the window are separated from it as in
(S), since two singular contributions in an interval of length $2d<p$ cannot cancel. Applied to the auxiliary geometry
$(\bar r,d)$, the count of (S) then gives \eqref{eq:PiU}. It uses the third-order analogue of \eqref{eq:corner}. Call
the \emph{coupling} of a residue class the residue modulo $p$ of its border entry minus its moment against the reference
node. Suppose that $n_+$ kernel vectors on each side survive, and that at most $n_0$ residue classes have a nonzero
coupling. Then
$\sum_i\min(v_i,3)\ge d+n_++(n_+-n_0)_+$, where $v_1,v_2,\dots$ are the valuations of the
Smith invariants. The first term $d$ is the factor $p$ of $p\,\Xi$.

\emph{Members.} Deleting $\ell$ common nodes lowers the trivial bound $2(r+m)$ by $2\ell$. Consider a class with one
deleted common node whose bordered system keeps its value at infinity $\vartheta$ (Lemma~\ref{lem:interp} below). Then
the class keeps its moment. Indeed, let $A$ be the common fibre and delete its last coordinate. The residual of the
smaller solution is supported on that coordinate. Since the two values at infinity are equal, its pairing with the data
vanishes. A class whose value at infinity changes gives a new separation instead. Classes with
two or more deleted nodes, and classes outside the window, cost at most one each. Let $k_1$, $k_2$ and $k'$ be the
numbers of classes of these three kinds. Then $k_1+2k_2+k'\le\ell$. An elementary inequality for the count
$n_++(n_+-n_0)_+$ shows that the loss is at most $2\ell$. Hence the bound holds for every
member with $\epsilon_\tau=0$.

\emph{Larger $n$.} Let $np\le m<(n+1)p$. Each class of the remaining border absorbs $n$ pairs of border nodes. Its block
after the elimination is a mixed block. Its rows and columns are the nodes of $2n+1$ consecutive quotients
$\beta,\beta+1,\dots,\beta+2n$. Here $\beta$ is the number of common nodes in the class, and the quotient of a node $t$ in
the class of a residue $i$ is $(t-i)/p$. The window counts are those of the first case at the scale $r+np$, translated by
$np$. The new difficulty is to show that a remaining border node separated from the window by a pole has a nonzero
coupling. The values at infinity are now those of $(n+1)\times(n+1)$ bordered systems, which we describe first.

\begin{lemma}[bordered systems and rational interpolation]\label{lem:interp}
Let $\mathbb K$ be a field and $\mathcal Z=\{0,1,\dots,2n\}$, with $(2n)!\ne0$ in $\mathbb K$. Let
$\mathcal L:\mathcal Z\to\mathbb K$, and let $\mathcal Z=X\sqcup Y$ with $|X|=n+1$ and $|Y|=n$. Consider the bordered
system
\[
 \sum_{y\in Y}\frac{\mathcal L(y)-\mathcal L(x)}{y-x}\,z_y+\vartheta=\mathcal L(x)\qquad(x\in X)
\]
in the unknowns $z_y$ and $\vartheta$, with data $\mathcal L$. Its solutions correspond bijectively to the pairs $(\mathcal N,\mathcal D)$ of
polynomials with $\mathcal D$ monic of degree $n$, $\deg\mathcal N\le n$ and $\mathcal N(t)=\mathcal L(t)\mathcal D(t)$
for $t\in\mathcal Z$. Under this correspondence $\vartheta$ is the coefficient of $t^n$ in $\mathcal N$. In particular the
system is nonsingular exactly when the interpolation problem of type $(n,n)$ has a unique solution. Then
$\vartheta=\lim_{t\to\infty}\mathcal N(t)/\mathcal D(t)$ depends only on $\mathcal L$ and not on the split. We call $\vartheta$ the \emph{value at infinity} of the system.
\end{lemma}
\begin{proof}
Let $\mathcal W(t)=\prod_{y\in Y}(t-y)$, and let $\mathcal W_y=\mathcal W/((t-y)\mathcal W'(y))$ be the Lagrange
polynomials of $Y$. Given a solution, put $\mathcal D=\mathcal W-\sum_yz_y\mathcal W'(y)\,\mathcal W_y$ and
$\mathcal N=\vartheta\mathcal W-\sum_yz_y\mathcal L(y)\mathcal W'(y)\,\mathcal W_y$. Then
$\mathcal N(y)=\mathcal L(y)\mathcal D(y)$ for $y\in Y$. Dividing $\mathcal N(x)-\mathcal L(x)\mathcal D(x)$ by
$\mathcal W(x)\ne0$ gives the equation of the row $x$. Conversely, Lagrange interpolation on $Y$ recovers
$z_y=-\mathcal D(y)/\mathcal W'(y)$ and $\vartheta$ from $(\mathcal N,\mathcal D)$.
\end{proof}

\begin{lemma}[harmonic data]\label{lem:harmonic}
Let $\mathcal A\in\mathbb K$ with $\mathcal A+i\ne0$ for $0\le i<2n$, and let
$\mathcal L_{\mathcal A}(t)=\sum_{0\le i<t}1/(\mathcal A+i)$. Let the characteristic of $\mathbb K$ be $0$ or larger than
$2n$. For every split, the bordered system of Lemma~\ref{lem:interp} with $\mathcal L=\mathcal L_{\mathcal A}$ is
nonsingular. Its value at infinity is $\vartheta=\mathcal L_{\mathcal A}(n)+\mathsf c_n$, with $\mathsf c_n\in\mathbb K$
depending only on $n$. Consequently, for the harmonic data $\mathcal L(t)=H_t$ on the quotients $\beta,\dots,\beta+2n$ the
value at infinity is $H_{\beta+n}+\mathsf c_n$. The values at infinity of two classes with $\beta$ and $\beta+1$ common nodes differ by
$1/(\beta+n+1)$.
\end{lemma}
\begin{proof}
Write $\Delta$ for the forward difference. For $l\ge1$ one has
$\Delta^l\mathcal L_{\mathcal A}(k)=(-1)^{l-1}(l-1)!/(\mathcal A+k)_l$, where $(y)_l$ is the rising factorial. One also
has $\Delta^l[\binom tk f(t)](0)=\binom lk\Delta^{l-k}f(k)$. By Lemma~\ref{lem:interp} a solution is a pair
$(\mathcal N,\mathcal D)$ with $\mathcal N=\mathcal L_{\mathcal A}\mathcal D$ on $\mathcal Z$. Since $\mathcal N$ has degree
at most $n$, this means $\Delta^l(\mathcal L_{\mathcal A}\mathcal D)(0)=0$ for $n<l\le2n$. Write
$\mathcal D=\sum_k\mathsf d_k\binom tk$ and insert the two formulas. After removing nonzero factors of the rows and
columns, these $n$ equations become a system for the coefficients $\mathsf d_k$ with $k<n$. Its matrix is the Cauchy
matrix $\bigl(1/(l-k)\bigr)_{n<l\le2n,\,0\le k<n}$, and its right-hand side comes from $\mathsf d_n=1$. The Cauchy matrix
is nonsingular. So $\mathcal D$ is unique, which is the nonsingularity.

The same computation shows that $\mathsf d_k/(\mathcal A+k)_{n-k}$ does not depend on $\mathcal A$. For $k<n$,
$\Delta^{n-k}\mathcal L_{\mathcal A}(k)$ is a constant multiple of $1/(\mathcal A+k)_{n-k}$. Hence
$\vartheta=\Delta^n(\mathcal L_{\mathcal A}\mathcal D)(0)/n!=\mathcal L_{\mathcal A}(n)+\mathsf c_n$ with
$\mathsf c_n$ independent of $\mathcal A$. For the harmonic data on the quotients $\beta+t$ we have
$H_{\beta+t}=H_\beta+\mathcal L_{\beta+1}(t)$. A constant added to $\mathcal L$ is added to $\vartheta$. So the value at infinity is
$H_\beta+\mathcal L_{\beta+1}(n)+\mathsf c_n=H_{\beta+n}+\mathsf c_n$.
\end{proof}

\begin{remark}\label{rem:hahn}
We note without proof that the interpolation problem of Lemma~\ref{lem:harmonic} can be solved in closed form. Its denominator is the polynomial
$\mathcal D_n(t)=\sum_{k=0}^n\binom nk\binom{2n-k}{n-k}(\mathcal A+k)_{n-k}\,t(t-1)\cdots(t-k+1)$, of Hahn type \cite{KLS}.
The constant is $\mathsf c_n=2H_n$. The determinant of the bordered system is
$\operatorname{sf}(n)^2\operatorname{sf}(n-1)^2\big/\bigl(\prod_{x\in X,y\in Y}|x-y|\cdot\prod_{i<n}(\mathcal A+i)_{n+1}\bigr)$,
with $\operatorname{sf}(n)=\prod_{i\le n}i!$. All its prime factors are at most $2n$ or divide some $\mathcal A+i$. These
closed forms are not used in the proof and are not part of the formalization.
\end{remark}

\emph{Separation for $n\ge1$.} Between a remaining border node and the reference node of the window lies a cut. Suppose
first that the cut is a pole of the second digamma term. Deform the shift to $s+pY$, with an indeterminate $Y$. Evaluate
at the value of $Y$ at which that pole becomes central. After multiplication by the vanishing factor, the bordered systems
of the two classes become block systems built from Cauchy matrices on the quotients. The square blocks are nonsingular
by Cauchy's determinant formula. A rectangular Cauchy matrix with $k+1$ rows and $k$ columns has a left kernel vector
with nonzero coordinate sum. Otherwise the rational function $\sum_iy_i/(T_i-T)$, formed from a kernel vector $(y_i)$
and the row nodes $T_i$, would vanish at the $k$ column nodes while its numerator has degree less than $k$. This gives the
two values at infinity the values $0$ and the weight of the term, which differ.

Suppose next that the cut is a multiple of $p$. Take instead the leading coefficient in $Y$. Every fractional pole term
tends to $0$, and the data become the harmonic numbers. The two classes have $\beta$ and $\beta+1$ common nodes.
Lemma~\ref{lem:harmonic} gives values at infinity that differ by $1/(\beta+n+1)$. This is a unit because $\beta+2n+1<p$, by
$q(r+2m)<p^2$.

In both cases the comparison is made on the cleared numerators of the original determinants, not on inverses. The result
returns to $Y=0$ by Gauss's lemma. The cleared denominators are products of the elementary denominators of the entries,
which are units at $Y=0$. So a lower bound for the Gauss valuation of the deformed determinant gives the same lower bound
for every coefficient of the original one. With these separations, the count and the treatment of the members are those
of the case $n=0$.

\subsection{Profiles}\label{ssec:profiles}
Let $\mathcal E$ be the set of integer expressions in $r,p,m,k$ built from integer constants with the following
operations: addition, multiplication by integer constants, truncated subtraction $(X-Y)_+$, $\min$, $\max$, and the
distance $\|X\|_p$ of an expression $X$ to $p\Z$. The quantities $p\lfloor r/p\rfloor$ and $r\bmod p$ are also allowed.
Every bound of Theorem~\ref{thm:local} lies in $\mathcal E$. For (R) and (S) this is \eqref{eq:PiR} and \eqref{eq:PiS}.
The ends of the intervals $\mathcal K_{k,\iota}$ are $kp=p\lfloor r/p\rfloor+(k-k_0)p$ plus $0$, $k_p$, $k_p-1$, $p-1$ or
$r_p-1$. For (U$_n$) this is \eqref{eq:PiU} with $d=\|m\|_p$ and $Z_i=p\lfloor r/p\rfloor+(n+i)p$. For (W) the window
ends are the cuts nearest to the ends of the window range, which are expressions of the same kind.

The \emph{homogenisation} $\hat\tau(\theta)$ of $\tau\in\mathcal E$ replaces $r,p,m,k$ by $1,\theta,\alpha,\kappa\theta$.
It replaces every constant by $0$, $\|X\|_p$ by $\theta\|\hat X/\theta\|$ and $p\lfloor r/p\rfloor$ by
$\theta\lfloor1/\theta\rfloor$. It is piecewise affine with rational breakpoints, finitely many in every interval bounded
away from $0$.

\begin{lemma}[homogenisation]\label{lem:homog}
For each $\tau\in\mathcal E$ there is an explicit constant $\err(\tau)$ such that
$|\tau(r,p,m(r),k_p)-r\hat\tau(p/r)|\le\err(\tau)$ for all $r,p\ge1$. It is computed recursively from
$\err(m)=\frac12$, $\err(k)=1-\frac1q$ and the rules $\err(\tau+\tau')=\err(\tau)+\err(\tau')$ and
$\err(\min(\tau,\tau'))\le\max(\err(\tau),\err(\tau'))$.
\end{lemma}
\begin{proof}
The real version of $\tau$, with the constants dropped, is positively homogeneous of degree one. Every operation is
$1$-Lipschitz in the maximum norm. The inputs differ from their homogeneous values by $|m-\alpha r|\le\frac12$ and
$|k_p-\kappa p|\le1-\frac1q$. Induct on $\tau$.
\end{proof}

The conditions of Theorem~\ref{thm:local} are linear inequalities in $r,p,m,k$, strict or not. They homogenise to
intervals of $\theta$. At an endpoint the error of such an inequality is a combination of $m-\alpha r$ and $k_p-\kappa p$.
With the rounding $m=\lceil\alpha r-\frac12\rceil$ two endpoints are \emph{exact}. These are $\theta=2\alpha$, from
$2m<p$, and $\theta=(1+2\alpha)/(1+\kappa)$, from $\bar N\le p+k$. At an exact endpoint the condition holds for every prime on
the correct side. The other endpoints are exact, or hold outside a strip of primes of bounded width around the endpoint.
On that strip another bound must be used.

\subsection{Tables for $\Lambda$ and the arithmetic estimate}\label{ssec:checker}
For the root class $j$ let $\mathcal P_j(\theta)$ be the minimum of the homogenised bounds $\hat\tau(\theta)$ over the
bounds $\tau$ of Theorem~\ref{thm:local} valid at $\theta$. A \emph{table for $\Lambda$}, for the function $F_s$ and
the geometry of parameter $c$, consists of the parameters $(q,\alpha,K)$ and the following data for every root class $j$:
\begin{itemize}
\item breakpoints $0<\theta_0<\theta_1<\dots<\theta_{\rm end}$;
\item on each interval $(\theta_{i-1},\theta_i]$, an affine function $\ell_i$, a constant $\err_i\ge0$ and a local bound
 $\tau_i$ of Theorem~\ref{thm:local}, with a second bound at each inexact endpoint of the range of $\tau_i$;
\item a constant $\ell_0$ for the initial interval $(0,\theta_0]$;
\end{itemize}
together with a rational number $\Lambda_{\rm fin}$. We call the table \emph{admissible} if it satisfies the following
conditions.
\begin{enumerate}[label=(C\arabic*),leftmargin=*]
\item For each shift of the table, every unit class modulo the modulus $q^*$ of the prime number theorem used is assigned
 a root class with a table.
\item On each piece $\ell_i$ is nonnegative, and the piece lies in the validity interval of its bound. Moreover
 $\hat\tau$ lies below $\ell_i$ at both ends and at both one-sided limits of each breakpoint inside the piece.
\item At each inexact endpoint the second bound is valid on both sides and lies below $\ell_i$ there. The constant
 $\err_i$ exceeds the error constants of Lemma~\ref{lem:homog}, the numbers $\epsilon_\tau K$, the strip widths times the slopes,
 and the trivial bound at the scales below an explicit threshold.
\item $\ell_0\ge2+2\alpha$ and $0<\theta_0\le1$. Also $\theta_{\rm end}\ge\max(q(1+2\alpha),p_0/2)$ and
 $\kappa_j\theta_{\rm end}\ge1+2\alpha$.
\item $\frac1{\varphi(q)}\sum_j\bigl(\ell_0\theta_0+\sum_i\int_{\theta_{i-1}}^{\theta_i}\ell_i(\theta)\,d\theta\bigr)
 =\Lambda_{\rm fin}$.
\end{enumerate}
Each condition is a finite set of comparisons of rational numbers.

\begin{theorem}[denominators]\label{thm:content}
Let $0<c\le1$, and let $F_s$ be the function with shift $s$ of denominator $q$. Suppose that an admissible table for $\Lambda$ of
depth $K$ has $s$ among its shifts. Then for every even $r$ and every member with $|I|\le K$,
\[
 \log\den P_{r,I}\le(\Lambda_{\rm fin}+o(1))\,r^2 .
\]
\end{theorem}
\begin{proof}
By definition $\den P_{r,I}=\prod_pp^{e_p(r,I)}$. Fix a piece $(\theta_{i-1},\theta_i]$ of the root class $j$. Let $p$ be
a prime in a unit class assigned to $j$, with $\theta_{i-1}r<p\le\theta_ir$. Let $r$ be beyond the threshold of (C3).
Then the conditions of the bound $\tau_i$ hold, either exactly or outside a strip where the second bound applies.
Lemma~\ref{lem:homog} with (C2) and (C3) gives $e_p(r,I)\le r\,\ell_i(p/r)+\err_i$. Below the threshold the trivial bound
is at most $\err_i$.

For $p\le\theta_0r$ the bound (T1) gives $e_p\le\ell_0r+O(1)$. The primes with $p^2\le q(r+2m)$, the prime powers and the
finitely many primes below $p_0$ contribute $O(r^{3/2}\log r)$. For $p>\theta_{\rm end}r$, (C4) gives $\bar N\le p$ and
$k_p\ge \bar N$, and (T5) gives $e_p=0$.

Fix a unit class modulo $q^*$. By the prime number theorem in arithmetic progressions,
\[
 \sum_{\substack{\theta_{i-1}r<p\le\theta_ir\\ p\text{ in the class}}}r\,\ell_i(p/r)\log p
 =\frac{r^2}{\varphi(q^*)}\int_{\theta_{i-1}}^{\theta_i}\ell_i(\theta)\,d\theta+o(r^2).
\]
The class $j$ receives $\varphi(q^*)/\varphi(q)$ unit classes modulo $q^*$, because the map that sends a unit to $qs$
times its inverse permutes the units modulo $q$. Summing and using (C5) gives the theorem. The constants $\err_i$
contribute $O(r)$.
\end{proof}

The tables of this paper are generated from the functions $\mathcal P_j$ themselves. The pieces are the maximal intervals
on which $\mathcal P_j$ is affine and attained by one bound. So $\Lambda_{\rm fin}=\frac1{\varphi(q)}\sum_j\int\mathcal P_j$
up to the initial interval. Every bound of Theorem~\ref{thm:local} is available to the tables: (T1)--(T5), (LP1), (LP2), (R), (S),
the windows (W) and the bounds (U$_n$). The windows with $n=0$ are used for $m<p$, between consecutive cuts.

On $(0,\alpha]$, that is for $p\le m$, the only other bounds are (T1), (T1$'$) and (U$_n$). With (T1$'$) alone the
profile there is the sawtooth $2+2\alpha-\theta\|\alpha/\theta\|$. Its integral is
\[
 \int_0^\alpha\Bigl(2+2\alpha-\theta\Bigl\|\frac\alpha\theta\Bigr\|\Bigr)d\theta=2\alpha+\frac{\alpha^2}2+2\alpha^2\log2,
\]
since $\int_1^\infty\|y\|y^{-3}\,dy=\frac32-2\log2$. The windows with $n=\lfloor m/p\rfloor\ge1$ lower this profile on the
strips $\alpha/(n+1)<\theta\le\alpha/n$. The tables use them for $n\le8$, again with each window running between two
consecutive cuts. For $q=3,4,5,7$ the tables also use (U$_0$) on $(\alpha,2\alpha]$ and (U$_n$) on the strips with
$1\le n\le24$. The table for $q=2$ uses only the other bounds. Beyond the strips used, a table resolves the sawtooth on each
interval $(\alpha/(n+1),\alpha/n]$ with $n<n_0$. It ends with a constant piece on $(0,\alpha/n_0]$, which costs $\alpha^2T_{n_0}$ with
$0<T_n\le1/(4n^2)$. The number $\Lambda_{\rm fin}$ is then rational, and (C5) is an identity between rational numbers.
The bounds depend on the shift $s$ only through the root class, and their profiles only through $(q,j,\alpha)$. So one
table serves all shifts with denominator $q$.

%% =====================================================================
\section{Nonvanishing}\label{sec:nonvanishing}

The deduction needs, for every rational $x_0$ and every large scale, one member of the family that does not vanish at
$x_0$. For the functions of \eqref{eq:frames} this holds in characteristic zero. The number of deleted common nodes is
bounded independently of $r$. This is the statement used in Section~\ref{sec:proof}.

\subsection{Selection in characteristic zero}\label{ssec:selection}
Normalise $F$ so that the divided differences of $F$ at consecutive nodes have partial sums $f_t$, with
$f_{t+1}-f_t=\Delta_F(t)$. The diagonal partial sums $\tilde f_t$ satisfy $\tilde f_{t+1}-\tilde f_t=-\Delta_F'(t)$. For
$F_s$,
\[
 \Delta_F(z)=\omega\Bigl(\frac1{z+1}-\frac1{z+s}\Bigr)=\frac{\omega(s-1)}{(z+1)(z+s)} .
\]
For $F_\chi$, with $\omega=-\frac16$,
\[
 \Delta_F(z)=\frac{1-z}{216\,(z+1)(z+\frac13)(z+\frac12)} .
\]

\begin{theorem}[selection]\label{thm:selection}
Let $F$ be a function of \eqref{eq:frames}, and consider the alternating geometry of parameter $c$. There is $K$, depending
only on $|\mathcal T|$, with the following property. For every large even $r$ and
every $x_0\in\Q$ some member $P_{r,I}$ with $|I|\le K$ satisfies $P_{r,I}(x_0)\ne0$.
\end{theorem}

\begin{proof}[Sketch of proof]
By barycentric interpolation, a vector in the right kernel of $\Phi_{r,\emptyset}(x_0)$ corresponds to a
pair of polynomials $(\mathsf u,\mathsf w)$ of degree less than $r+m$. The pair satisfies the \emph{value conditions}
$\mathsf w(t)=f_t\mathsf u(t)$ at the $\bar N$ nodes. It satisfies the \emph{jet conditions}
$\mathsf w'(t)=f_t\mathsf u'(t)+(x_0-\tilde f_t)\mathsf u(t)$ at the common nodes $t$. The left kernel is described
in the same way. Two such pairs have zero cross product $\mathsf w_1\mathsf u_2-\mathsf w_2\mathsf u_1$. Indeed its
degree is at most $2(r+m)-2$, while the value and jet conditions give $\bar N+r=2(r+m)$ zeros, counted with multiplicity.

Consider a pair whose degrees are small enough. Write $\Delta_F=n_\Delta/d_\Delta$ in lowest terms. The discrete
Wronskian
\[
 \mathrm{Wr}(z)=d_\Delta(z)\bigl[\mathsf w(z+1)\mathsf u(z)-\mathsf w(z)\mathsf u(z+1)\bigr]
 -n_\Delta(z)\mathsf u(z)\mathsf u(z+1)
\]
has more prescribed zeros at the nodes than its degree allows. So it vanishes identically. Then
$\mathsf w/\mathsf u$ would be a rational antidifference of $\Delta_F$. This is impossible, because the simple pole of
$\Delta_F$ at $-1$ is isolated in its class modulo $\Z$. The other poles of $\Delta_F$ are $-s$ for $F_s$, and $-\frac13$
and $-\frac12$ for $F_\chi$. None of them is congruent to $-1$ modulo $\Z$. Clearing denominators in
$\mathsf w(z+1)/\mathsf u(z+1)-\mathsf w(z)/\mathsf u(z)=\Delta_F(z)$ would propagate a root of the denominator
indefinitely in one direction. Counting the zeros along chains of nodes of step $2$ bounds the dimension of the kernel.
So the corank of $\Phi_{r,\emptyset}(x_0)$ is at most a number $K$ that depends only on $|\mathcal T|$ and on the number
of such chains. That number is bounded independently of $r$.

Finally, the left and right kernels map to the same interpolation space. At a common node $t$ their coordinates are the
values $\mathsf u(t)$ times nonzero factors. No nonzero kernel pair has $\mathsf u$ vanishing at every common node.
Otherwise, dividing by the node polynomial of the common nodes would give a pair of degree less than $m$ that satisfies
the value conditions at all $\bar N$ nodes, and the Wronskian argument applies again. Hence there is a set $I$ of
$|I|=\corank$ common nodes such that no nonzero left or right kernel vector vanishes on $I$. The rows outside $I$ then
span the row space, and the columns outside $I$ span the column space. So the principal minor that deletes $I$ is
nonzero.
\end{proof}

The theorem applies to every function of \eqref{eq:frames}. For $F_\chi$ the pole of $\Delta_F$ at $-1$ is again isolated
in its class modulo $\Z$, since the other poles are $-\frac13$ and $-\frac12$. In the formal proof the depth is $K\le64$
for all the functions of this paper.

%% =====================================================================
\section{Analytic decay}\label{sec:decay}

In this section we bound $|P_{r,I}(x)|$ for $x$ near $\xi$. The argument is that of OpenAI \cite{OpenAI2026} for square
determinants, with three changes. The determinant has two families of nodes, one for the rows and one for the columns.
The comparison measure is a density on finitely many segments rather than an explicit equilibrium measure. The
inequalities that remain are verified on a finite cover by cells. The result is one theorem for every geometry parameter
$c\le1$ and every function of \eqref{eq:frames}.

\subsection{A contour representation}
Hermite's formula gives $\Lw_F[t,t']=\frac1{2\pi i}\oint F(z)\upsilon_t(z)\upsilon_{t'}(z)\,dz$ with
$\upsilon_t(z)=1/(z-t)$. The contour encloses the nodes and no pole of $F$. Write
$F=\sum_{\varsigma\in\mathcal T}w_\varsigma\psi(z+\varsigma)$ as in \S\ref{sec:construction}. The reflection formula
$\psi(w)=\psi(1-w)-\pi\cot\pi w$ splits $F=\tilde F+E$. Here $\tilde F$ is analytic in the left half-plane and
$O(1/|z|)$ there, and
\[
 E(z)=-\pi\sum_{\varsigma\in\mathcal T}w_\varsigma\cot\pi(z+\varsigma).
\]
The function $E$ is $1$-periodic. Since the weights sum to zero, $E(z)=O(e^{-2\pi|\Im z|})$ for $|\Im z|\ge1$. For
$F_s$ one has $E(z)=\pi[\cot\pi(z+s)-\cot\pi z]$.

Let $\Gamma$ be a polygonal path, symmetric under complex conjugation. It crosses the real axis at a point $x^*<0$ that
is not a pole of $F$, runs through the left half-plane and ends in two rays. The poles of $F$ are the points
$-(i+\varsigma)$ with $i\ge0$ and $\varsigma\in\mathcal T$. Moving the contour to $\Gamma$ picks up the residues of $F$
at the poles in $(x^*,0)$. The part of the integrand with $\tilde F$ integrates to $0$ over $\Gamma$. Hence, for all
integers $t,t'\ge0$,
\begin{equation}\label{eq:gram}
 \Lw_F[t,t']=\int\upsilon_t\upsilon_{t'}\,d\Omega .
\end{equation}
Here $\Omega$ is the complex measure with the mass $-\operatorname{res}_y(F)$ at each pole $y\in(x^*,0)$ of $F$ and the
density $(2\pi i)^{-1}E(z)\,dz$ on $\Gamma$. This is a Gram representation with respect to a measure with finitely many
atoms and an exponentially small density on $\Gamma$. After scaling by $r$, the atoms lie on a segment $[-r_0,0]$ with
density $|\mathcal T|$. The separation condition on $x^*$ is a finite check on the fractional parts of $\varsigma-x^*$
for $\varsigma\in\mathcal T$.

\subsection{Two-family Andr\'eief bound}
For a set $C''\subseteq C$ of common nodes put $\mathcal M_{C''}=\omega\,\Lw_F[C''\sqcup X',C''\sqcup Y']$. Consider a
member with common nodes $C'=C\setminus I$. Put $R'=C'\sqcup X'$, $Q'=C'\sqcup Y'$ and $n_*=|C'|+m$. By multilinearity in
the diagonal,
\begin{equation}\label{eq:expand}
 P_{r,I}(\xi+h)=\sum_{C''\subseteq C'}h^{|C'|-|C''|}\det\mathcal M_{C''} .
\end{equation}
Andr\'eief's identity \cite{Forrester2018Andreief} for the two families $(\upsilon_t)_{t\in R'}$ and
$(\upsilon_{t'})_{t'\in Q'}$ gives
\[
 \det\Lw_F[R',Q']=\frac1{n_*!}\int\det[\upsilon_t(z_i)]\,\det[\upsilon_{t'}(z_i)]\prod_{i=1}^{n_*}d\Omega(z_i).
\]
Cauchy's determinant formula evaluates both factors. We take absolute values. The logarithmic potential theory behind
what follows is in \cite{SaffTotik}. We obtain
\begin{multline*}
 |\det\Lw_F[R',Q']|\le\frac1{n_*!}\int\prod_{i<i'}|z_i-z_{i'}|^2\,\\
 \prod_{\mathcal F\in\{R',Q'\}}\frac{\prod_{t<t'\in\mathcal F}|t'-t|}{\prod_{i,\,t\in\mathcal F}|z_i-t|}\
 \prod_id|\Omega|(z_i).
\end{multline*}
The integrand is the exponential of minus a discrete logarithmic energy. The free points $z_i$ repel each other with
weight $1$. Each node family repels itself with weight $\frac12$ and attracts the free points with weight $1$. The
density $|E|\approx e^{-2\pi|\Im z|}$ acts as an external field. The rows and columns differ only in the interleaved
border. So the two node families have the same macroscopic density. After scaling by $r$, both are
\[
 \nu_c=\mathrm{Leb}|_{[0,1]}+\tfrac12\mathrm{Leb}|_{[1,1+c]},
\]
of mass $|\nu_c|=1+c/2$.

\subsection{The energy certificate}
For a regularisation radius $\epsilon>0$ let $k_\epsilon(z,w)=-\frac12\log(|z-w|^2+\epsilon^2)$. Then $k_\epsilon(z,w)\le-\log|z-w|$.

\begin{lemma}[conditional positive definiteness]\label{lem:cpd}
Let $z_i\in\C$ be finitely many points and $y_i$ real numbers with $\sum_iy_i=0$. Then
$\sum_{i,j}y_iy_jk_\epsilon(z_i,z_j)\ge0$.
\end{lemma}
\begin{proof}
We use Frullani's integral $\log T=\int_0^\infty(e^{-u}-e^{-Tu})\,du/u$ for $T>0$. Together with $\sum_iy_i=0$ it gives
$\sum_{i,j}y_iy_j(-\log(|z_i-z_j|^2+\epsilon^2))=\int_0^\infty\frac{e^{-u\epsilon^2}}u\sum_{i,j}y_iy_je^{-u|z_i-z_j|^2}du$.
Gaussian kernels are positive definite. Indeed, expanding $e^{2u\langle z,z'\rangle}$ in powers and using the binomial
theorem writes the inner sum as a convergent sum of squares.
\end{proof}

A \emph{trial measure} is a probability measure $\sigma$, symmetric under conjugation, carried by finitely many
segments $\mathcal S_i\subset\Gamma\cup[-r_0,0]\cup[0,1]$ with rational endpoints. On each segment it has a density
$\sigma_i(y)\,dy$ in the parameter $y\in[0,1]$ of the segment. Here $\sigma_i$ is a polynomial with rational coefficients,
and $0\le\sigma_i\le\bar\sigma_i$ for a rational $\bar\sigma_i$. We write $\Theta_\sigma=\sum_i\bar\sigma_i/|\mathcal S_i|$
for the sum of the bounds of its densities with respect to arclength.

We compare the free points and the deleted nodes with $|\nu_c|\sigma$ through Lemma~\ref{lem:cpd}. This bounds the
free--free energy from below by a sum of one-point terms and the constant $|\nu_c|^2\cI(\sigma)$. Riemann-sum comparisons
replace the node sums by the potential $U^{\nu_c}$ and the node self-energy by $\cI(\nu_c)$, up to $O(r\log r)$. With the
external field one arrives at the function
\[
 \Upsilon(z)=|\nu_c|\,U^\sigma(z)-U^{\nu_c}(z)+(1-\varepsilon_0)\pi|\Im z|
\]
for a small fixed $\varepsilon_0>0$. Here $U^\sigma(z)=\int\log\frac1{|z-w|}\,d\sigma(w)$ is the logarithmic potential of
$\sigma$, and $U^{\nu_c}$ is that of $\nu_c$. A \emph{certificate} consists of $\sigma$ and rational numbers
$\Upsilon_\Gamma$, $\Upsilon_0$, $J$, $\cI_\sigma$, $\cI_\nu$ with the following properties.
\begin{enumerate}[label=(\alph*),leftmargin=*]
\item $\Upsilon\ge\Upsilon_\Gamma$ on $\Gamma$.
\item $\Upsilon\ge\Upsilon_0$ on $[0,1]$, the scaled position of the deleted common nodes.
\item $J\le\int_{-r_0}^0\min(\Upsilon(x)-\Upsilon_\Gamma,0)\,dx$.
\item $\cI(\sigma)\le\cI_\sigma$ and $\cI(\nu_c)\ge\cI_\nu$.
\end{enumerate}

\begin{theorem}[decay on a neighbourhood]\label{thm:decay}
Let $0<c\le1$. Let $F$ be a function of \eqref{eq:frames} whose poles are separated from $x^*$. Let
$(\sigma,\Upsilon_\Gamma,\Upsilon_0,J,\cI_\sigma,\cI_\nu)$ be a certificate for $\Gamma$ and $\nu_c$. Let $\epsilon>0$,
$\delta_\epsilon\ge\pi\epsilon\,\Theta_\sigma$, $\delta_{\rm m}>0$ and $\delta_J>0$ be rational, and put
\[
 \delta=3|\nu_c|^2\delta_\epsilon+4|\nu_c|^2\delta_{\rm m}+2|\mathcal T|\,\delta_J .
\]
Let $D$ and $\rho$ be rational numbers with
\[
 D\le2(|\nu_c|\Upsilon_\Gamma+|\mathcal T|J)-|\nu_c|^2\cI_\sigma+\cI_\nu-\delta,\qquad
 \rho\ge2(\Upsilon_\Gamma-\Upsilon_0).
\]
Then for every depth $K$, every member of the alternating geometry of parameter $c$ and every real $h$ with
$|h|\le e^{-\rho r}$,
\[
 |P_{r,I}(\xi+h)|\le\exp\bigl(-(D-o(1))r^2\bigr).
\]
\end{theorem}

The loss $\delta$ comes from replacing $\sigma$ by finitely many atoms in the comparison with the free points. The
regularisation radius $\epsilon$ of Lemma~\ref{lem:cpd} and the mesh of the atoms lower $\Upsilon_\Gamma$ by
$|\nu_c|(\delta_\epsilon+\delta_{\rm m})$. They raise $\cI_\sigma$ by $\delta_\epsilon+2\delta_{\rm m}$. Darboux sums for the
integral in (c) lower $J$ by $\delta_J$. Inserted in the expression for $D$, these changes give $\delta$. The tolerances
$\delta_{\rm m}$ and $\delta_J$ may be any positive rational numbers, since the atoms can be taken as fine as needed. In
the certificates of this paper $\epsilon=10^{-12}$ and $\delta<10^{-9}$.

The node energy $\cI(\nu_c)$ is a finite rational combination of the values $\mathcal H(y_k)$, where
$\mathcal H(y)=\frac12y^2\log|y|-\frac34y^2$ and the $y_k$ are the rational differences of the endpoints of the two pieces
of $\nu_c$. The lower bound $\cI_\nu$ is checked with rational enclosures of the logarithms. These come from the series of
$\operatorname{artanh}$ and a reduction to $[1,2)$. The energy $\cI(\sigma)$ is a finite sum of pair energies of
polynomial densities on segments. Each is a closed form of the type polynomial times logarithm plus arctangent, and is
bounded in the same way. The conditions (a)--(c) are statements about $\Upsilon$ on sets of positive measure. They are
proved on a cover by cells.

\subsection{The cover by cells}\label{ssec:slope-cert}
Each of the conditions (a)--(c) is checked on a finite cover by cells with exact rational arithmetic. On a cell, the
potential $U^\sigma$ is split into the contribution of the segments of $\sigma$ near the cell and the rest. A near segment
is bounded by a Taylor polynomial in the cell variable with an explicit remainder. For a cell that meets the line of a
segment beyond its end, the same bound is used for the segment with its orientation reversed. At a corner of $\Gamma$ the
two incident segments are treated together. Far segments are bounded by a multipole expansion with an explicit tail. The
potential $U^{\nu_c}$ is an explicit elementary function, and it is bounded above by monotonicity on the cell.

For (a) the cells are intervals of the arclength on each edge of $\Gamma$. The bound is proved on a horizontal
neighbourhood of the edge of fixed width. Beyond the last vertex the ray is handled by an analytic tail bound. For (b)
the cells are intervals of $[0,1]$. For (c) the integrand is bounded above on each cell of $[-r_0,0]$ by a constant or by
a chord. Then $J$ is the sum of the integrals of these majorants.

\begin{proposition}[certified constants]\label{prop:cert}
For each row of Table~\ref{tab:data} there is a trial measure $\sigma$ on a polygon $\Gamma$, with a cover by cells
satisfying the checks above, for which Theorem~\ref{thm:decay} gives the constants $D$ and $\rho$ of the table.
\end{proposition}

All inequalities are verified by the Lean kernel, as described in Section~\ref{sec:lean}. The certificate data are the
polygon, the density $\sigma$ and the cells. They were computed with floating-point optimisation and interval arithmetic
in Arb \cite{Arb}. Lean checks them with rational arithmetic only. The data play no role in the proof beyond satisfying these
checks.

\begin{remark}[how good a certificate can be]\label{rem:certlimit}
For an exponent $\mu_0$ the certificate meets $\mu_0$ exactly when $\mu_0(D-\Lambda)-\rho\ge0$. This quantity is a concave function
of $\sigma$. Its maximum over all probability measures on $\Gamma\cup[-r_0,0]\cup[0,1]$ is attained at a measure
$\sigma^*$. For this measure $|\nu_c|\sigma^*$ is the weighted equilibrium measure of the constrained energy problem on
this set, with the external field $(1-\varepsilon_0)\pi|\Im z|-U^{\nu_c}$ and the upper constraint $|\mathcal T|\,dx$ on
the segment \cite{SaffTotik}. Weak duality expresses the deficit of any certificate as a sum of nonnegative terms. The
first is the energy of $2\mu_0|\nu_c|(\sigma-\sigma^*)$. This is the difference between $2\mu_0|\nu_c|\sigma$ and the optimal
dual measure $2\mu_0|\nu_c|\sigma^*$. So a certificate close to the best possible one must be close to $\sigma^*$ in energy.
Then $\Upsilon-\Upsilon_\Gamma$ is a small ripple on the support of $\sigma^*$. This is why a pointwise verification on a
cover is needed. This remark is not used in the proof of Theorem~\ref{thm:main} and is not part of the formalization.
\end{remark}

\subsection{Node removal and the neighbourhood}
The argument applies to every subset $C''\subseteq C'$ of the common nodes. Removing common nodes turns them into points
of the configuration that are not integrated over. Only common nodes can be removed. A node removed from one family only
would leave an uncancelled term of weight $\frac12$. By condition (b) one obtains
\[
 |\det\mathcal M_{C''}|\le\exp\bigl(-(D-o(1))r^2+\rho r\,|C'\setminus C''|\bigr),
\]
uniformly in $C''$. Insert this into \eqref{eq:expand} with $|h|e^{\rho r}\le1$. The sum has at most
$2^{|C'|}=e^{O(r)}$ terms, each at most $e^{-(D-o(1))r^2}$. This gives Theorem~\ref{thm:decay}. The deletion of at most
$K$ common nodes in a member changes the energy by $O(r)$.

%% =====================================================================
\section{The pair of shifts \texorpdfstring{$(\frac13,\frac23)$}{(1/3,2/3)}}
\label{sec:chi3-quarter}

For $\Psi(\frac13,\frac23)$ we use the function $F_\chi$ of \eqref{eq:frames}, which combines three digamma terms, with
the alternating geometry of parameter $c=\frac12$ at all even scales $r$. Then $\alpha=\frac14$ and
$m=\lceil r/4-\frac12\rceil$. The decay and nonvanishing estimates of Theorems~\ref{thm:decay} and~\ref{thm:selection}
apply unchanged. The denominators need more care. At a prime $p$ the increments $g(k)$ of \S\ref{sec:construction} have
poles in three residue classes instead of two, so the local bounds depend on two first poles. This section describes the
two poles, the bounds we use, and the resulting constant.

\subsection{The first poles}
Let $p>3$ be a prime. The increment $g(k)=\frac1{3k-2}-\frac1{2k-1}+\frac1{6k}$ has a pole modulo $p$ exactly when $p$
divides $k$, $3k-2$ or $2k-1$. Let $k_A$ and $k_B$ be the least $k\ge1$ with $p\mid3k-2$ and with $p\mid2k-1$. Then
\[
 k_B=\frac{p+1}2,\qquad
 k_A=\begin{cases}\frac{p+2}3,&p\equiv1\pmod6,\\[3pt]\frac{2p+2}3,&p\equiv5\pmod6.\end{cases}
\]
The residues of $p\,g(k)$ at $k_A$ and $k_B$ are $1$ and $-1$ if $p\equiv1\pmod6$, and $\frac12$ and $-1$ if
$p\equiv5\pmod6$. In the first case $k_A<k_B$ and the two residues cancel. So the partial sums $\sum_{k\le t}g(k)$ are
$p$-integral for $t<k_A$, and again for $k_B\le t<p$.

Both first poles are affine in one index. Define $k_p$ by $6k_p=jp+5$ with $0<j<6$. Then $j=1$ for $p\equiv1\pmod6$ and
$j=5$ for $p\equiv5\pmod6$, $k_p=\frac j6p+O(1)$, and
\[
 (k_A,k_B)=\begin{cases}(2k_p-1,\ 3k_p-2),&p\equiv1\pmod6,\\[2pt](2k_p-p-1,\ 3k_p-2p-2),&p\equiv5\pmod6.\end{cases}
\]
Thus $j$ plays the role of the root class of \S\ref{sec:content}, with $q$ replaced by $6$.

\subsection{The local bounds}
Fix a prime $p>6$ with $6\bar N<p^2$. Every pole below $\bar N$ is then simple. Call a node $t$ \emph{regular} if
$t<\min(k_A,k_B)$, or if $p\equiv1\pmod6$ and $t$ is a border node with $k_B\le t<p$. At a regular node the partial sum
of the increments up to $t$ is $p$-integral. When $t$ is a common node, its diagonal entry is $p$-integral too.

\begin{proposition}\label{prop:chi3-local}
Every member of the alternating geometry of parameter $\frac12$ for $F_\chi$ satisfies $e_p(r,I)\le\tau$ for each of the
following $\tau$.
\begin{enumerate}[label=(\roman*),leftmargin=*]
\item The bounds (T1) and (T1$'$), namely $2(r+m)$ and $2r+2m-\|m\|_p$.
\item If $\bar N\le2p$, the bound $2r+2m-n_{\rm reg}$. Here $n_{\rm reg}$ is the number of pairs formed by a regular node $t$
 and a side on which $t$ lies, row or column, such that $t+p$ is not a node of the other side.
\item If $\bar N<\min(k_A,k_B)$, the bound $0$.
\item The bound $2r+2m-(t_2-t_1)$ of Theorem~\ref{thm:window}, for every $n$ and every window $[t_1,t_2)$ as there, with
 the cuts $t\equiv0$, $t\equiv k_A$, $t\equiv k_B$ and $t\equiv r\pmod p$.
\end{enumerate}
\end{proposition}

\begin{proof}
The bounds (i) are proved as in \S\ref{sssec:trop}. For (ii) we apply Lemma~\ref{lem:trop} with the following potentials.
At a node that is not regular, the potential is $1$ on its row and on its column. At a regular node $t$, the potential on
its row is $1$ if $t+p$ is a column node, and $0$ otherwise. The potential on its column is $1$ if $t+p$ is a row node,
and $0$ otherwise. Their sum is $2(r+m)-n_{\rm reg}$, and they dominate the weights $W$. Indeed, a diagonal weight is $0$
at a regular common node and at most $2$ in general. Two nodes that are not congruent modulo $p$ have weight at most $1$,
since all poles are simple. Their weight is $0$ if both are regular. Two distinct congruent nodes have weight at most
$2$. Since $\bar N\le2p$ and regular nodes are smaller than $p$, at most one of them is regular. Suppose that the row node $t$
of such an entry is regular. Then its column node is $t+p$, so the potential on the row of $t$ is $1$. The case of a
regular column node is symmetric.

For (iii), the condition $\bar N<\min(k_A,k_B)$ implies $\bar N<p$. Then no index below $\bar N$ is a pole and no two nodes are
congruent modulo $p$, so every entry is $p$-integral. For (iv), the proof of Theorem~\ref{thm:window} uses $F$ only
through its poles. The step function $V$ and the diagonal residues are constant between consecutive cuts. This is what
the translation between the fibres of the window needs.
\end{proof}

The bounds (T2)--(T5), (LP1), (LP2), (R) and (S) of Theorem~\ref{thm:local} are not used for $F_\chi$.

\subsection{The denominators}
The tables for $\Lambda$ of \S\ref{ssec:checker} and Theorem~\ref{thm:content} apply to $F_\chi$ with $q$ replaced by $6$. The root
class is $j\in\{1,5\}$ as above, and the bounds are those of Proposition~\ref{prop:chi3-local}. These bounds are
expressions of the class $\mathcal E$ in $r,p,m,k_A,k_B$. On each class of primes modulo $6$ the substitution above makes
them expressions in $r,p,m,k_p$. Their homogenisations are taken with $\kappa=j/6$. The proof of
Theorem~\ref{thm:content} uses $F$ only through these bounds and the root class. It goes through with the bound
(iii) in place of (T5) beyond the end of the table.

The table of the formal proof starts at $\theta_0=\frac1{68}=\alpha/17$. Below it the trivial bound $\ell_0r$ with
$\ell_0=\frac52=2+2\alpha$ is used. On $(\alpha/17,\alpha]$ the table uses the bounds (i) and the windows (iv) with
$1\le n\le16$. Beyond $\alpha$ it uses (i), (ii), the windows (iv) with $n=0$ between consecutive cuts, and the bound
(iii), which ends the table. The table is admissible for the two classes $j=1,5$. The arithmetic estimate therefore
holds for every even $r$ and every member with $|I|\le64$, with the denominator exponent
\[
 \Lambda_\chi=4.09592776731\ldots
\]
This is an explicit rational number, whose numerator and denominator have $117$ and $116$ digits.

\subsection{Decay and nonvanishing}
The decay estimate is Theorem~\ref{thm:decay} for the function $F_\chi$, with $|\mathcal T|=3$ and $c=\frac12$. The node
measure $\nu_{1/2}$ has mass $\frac54$ and energy
\[
 \cI(\nu_{1/2})=\frac{75}{32}-\frac98\log\frac32-\frac1{16}\log2 .
\]
A trial measure on a polygon, with a cover by cells satisfying the checks of \S\ref{ssec:slope-cert}, gives
\[
\begin{gathered}
 D=\frac{4643511791526209475773}{10^{21}}=4.64351\ldots,\\ \rho=\frac{37521870783566737}{5\cdot10^{15}}=7.50437\ldots
\end{gathered}
\]
Nonvanishing is Theorem~\ref{thm:selection} for $F_\chi$. Its increment $\Delta_F$ has its pole at $-1$ isolated in its
class modulo $\Z$, and the depth is $K\le64$. The deduction of Section~\ref{sec:proof}, at the even scales, gives
\[
 \mu\bigl(\Psi(\tfrac13,\tfrac23)\bigr)\le\frac\rho{D-\Lambda_\chi}=\MuChiExact\ldots<\MuChi,
\]
since $\Psi(\frac13,\frac23)=36\,\xi_\chi$.

%% =====================================================================
\section{Proof of Theorem~\ref{thm:main}}\label{sec:proof}

The three estimates combine as follows.

\begin{theorem}[deduction]\label{thm:deduction}
Let $F$ be a function of \eqref{eq:frames} with its geometry. Let $K$ be a depth such that, for every large $r$ and every
rational $x_0$, some member $P_{r,I}$ with $|I|\le K$ satisfies $P_{r,I}(x_0)\ne0$, as in Theorem~\ref{thm:selection}.
Suppose that the denominator exponent $\Lambda$ of Theorem~\ref{thm:content} and the constants $D$, $\rho$ of
Theorem~\ref{thm:decay} satisfy $\Lambda<D$. Then $\mu(\xi)\le\rho/(D-\Lambda)$.
\end{theorem}

\begin{proof}
Let $\eta=D-\Lambda$, and let $\mu_0>\mu_1>\rho/\eta$. Suppose that $|\xi-a/b|<b^{-\mu_0}$ with $b$ large. Let $r$ be
the least admissible scale with $r\ge\mu_1\log b/\rho$. By Theorem~\ref{thm:selection} with $x_0=a/b$ there is a member
with $P_{r,I}(a/b)\ne0$. By Lemma~\ref{lem:integrality}, $|\den(P_{r,I})\,P_{r,I}(a/b)|\ge b^{-r}$. Write $a/b=\xi+h$.
Then $|h|<b^{-\mu_0}\le e^{-\rho r}$, because $\rho r\le\mu_1\log b+O(1)<\mu_0\log b$ for large $b$. By
Theorems~\ref{thm:content} and~\ref{thm:decay},
\[
 |\den(P_{r,I})\,P_{r,I}(a/b)|\le e^{(\Lambda+o(1))r^2}e^{-(D-o(1))r^2}=e^{-(\eta-o(1))r^2}.
\]
Comparing the two bounds gives $(\eta-o(1))r^2\le r\log b$. But $\eta r\ge(\mu_1\eta/\rho)\log b$ with
$\mu_1\eta/\rho>1$. This is a contradiction for large $b$.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
For each row of Table~\ref{tab:main} the function, the geometry parameter and the constants are those of
Table~\ref{tab:data}. The denominator exponent is given by Theorem~\ref{thm:content} with the table for $\Lambda$ of the formal
proof. For the pair $(\frac13,\frac23)$ it is given by Section~\ref{sec:chi3-quarter}. The decay rates are given by
Proposition~\ref{prop:cert}, and nonvanishing by Theorem~\ref{thm:selection}. Theorem~\ref{thm:deduction}, applied at the even scales, gives
$\mu(\xi)\le\rho/(D-\Lambda)$, and in every row $\rho/(D-\Lambda)<\mu_{s,t}$. By \eqref{eq:frames}, $\xi$ is a
nonzero rational multiple of $\Psi(s,t)$, so $\mu(\Psi(s,t))<\mu_{s,t}$. Since this inequality is strict, the
definition of $\mu$ gives $|\Psi(s,t)-a/b|>b^{-\mu_{s,t}}$ for all integers $a$ and all sufficiently large $b$. This
proves Theorem~\ref{thm:main}.
\end{proof}

\begin{table}[ht]
\centering
{\setlength{\tabcolsep}{2pt}
\begin{tabular}{@{}lcccccc@{}}
\toprule
$(s,t)$ & $c$ & $\Lambda$ & $D$ & $\rho$ & $\rho/\eta$ & $\mu$\\
\midrule
$(\frac12,1)$ & $\frac3{10}$ & $\LamHalf$ & $\DHalf$ & $\gHalf$ & $\ExpHalf$ & $\MuHalvesU$\\
$(\frac k3,1)$ & $\frac3{10}$ & $\LamThree$ & $\DThree$ & $\gThree$ & $\ExpThree$ & $\MuThirdsU$\\
$(\frac13,\frac23)$ & $\frac12$ & $\LamChi$ & $\DChi$ & $\gChi$ & $\ExpChi$ & $\MuChi$\\
$(\frac k4,1)$ & $\frac15$ & $\LamFour$ & $\DFour$ & $\gFour$ & $\ExpFour$ & $\MuLamU$\\
$(\frac k5,1)$ & $\frac29$ & $\LamFive$ & $\DFive$ & $\gFive$ & $\ExpFive$ & $\MuFifthsU$\\
$(\frac k7,1)$ & $\frac16$ & $\LamSeven$ & $\DSeven$ & $\gSeven$ & $\ExpSeven$ & $\MuSeventhsU$\\
\bottomrule
\end{tabular}}
\caption{The data of the proof of Theorem~\ref{thm:main}, with $k$ prime to the denominator. For each pair of shifts the table gives the geometry parameter
$c$, the denominator exponent $\Lambda$, the decay rate $D$, the neighbourhood exponent $\rho$ and the exponent. The constants
are the rational numbers of the formal proof, rounded outward to the digits shown: $\Lambda$ and $\rho$ up, $D$ down.
The column $\rho/\eta$, with $\eta=D-\Lambda$, is the exact quotient, rounded up.}\label{tab:data}
\end{table}

\begin{remark}[relation to linear independence criteria]
The deduction is a one-dimensional version of the familiar scheme behind the criteria of Nesterenko
\cite{Nesterenko85} and their use by Ball and Rivoal \cite{BallRivoal01}. The nonzero integer
$b^{|C\setminus I|}\den(P_{r,I})\,P_{r,I}(a/b)$ plays the role of a small linear form with integer coefficients. There are
two differences. The lower bound for the form comes from an arithmetic nonvanishing statement rather than from an analytic
asymptotic. The size $r$ of the determinant is chosen in terms of $b$.
\end{remark}

\subsection{Notes on the rows}\label{sec:families}
Except for the pair $(\frac13,\frac23)$ of Section~\ref{sec:chi3-quarter}, the function of each row is $F_s$ of
\eqref{eq:frames} with $s=k/q$, $\omega=q^{-2}$ and $\xi_s=-q^{-2}\Psi(\frac kq,1)$. The table for $\Lambda$, the trial
measure and the cover are data of the formal proof. All shifts with the same denominator share one table for $\Lambda$,
indexed by the root classes, and one certificate. Indeed the bounds depend on the shift only through the root class, and
the decay depends on it only through the separation of the poles from the contour. For $q=4$ the root classes
$j\equiv kp^{-1}\pmod 4$ of $k=1$ and $k=3$ exchange the two classes of primes modulo $4$. For $q=3$ the table uses the
primes in the classes modulo $6$, and the root classes $j=1,2$ correspond to first poles near $p/3$ and $2p/3$. For $q=7$
there are six root classes. Here $D-\Lambda$ is only about $3\cdot10^{-3}$, which explains the large exponent. A small
further gain in either constant would lower it substantially (Section~\ref{sec:limits}). For $q=2$ there is one root
class, $j=1$, with first pole $k_p=\frac{p+1}2$. The resulting bound is weaker than the known ones for this number.

%% =====================================================================
\section{Limits of the method}\label{sec:limits}

The exponents are determined by three constants through $\rho/(D-\Lambda)$. Since $\partial\mu/\partial D=-\rho/\eta^2$,
the exponent is most sensitive to the decay where $\eta$ is small. For the shifts $\frac14$ and $\frac34$,
$\rho/\eta^2\approx136$. For the shifts $\frac k7$ it is about $6.6\cdot10^5$.

On the arithmetic side, the profiles $\mathcal P_j$ are minima of the bounds of Theorem~\ref{thm:local}. Every further
local bound lowers $\Lambda$ by the integral of the amount by which it lies below $\mathcal P_j$. The denominator exponent of
the method is the integral of the true exponent $e_p$, which the local bounds approximate from above. At third order this
approximation is close to exhaustion for the shifts $\frac k5$ and $\frac k7$. We computed the Smith normal forms exactly
at scales $r\le2400$ and primes $p\le2m$. There the minimum of the local bounds, with (U$_n$) included, equals the true
exponent at all but a few isolated primes. For the shifts $\frac k7$ the invariants of valuation at least $4$ contribute
about $5\cdot10^{-6}$ to $\Lambda$. The bounds (U$_n$) gain about $7\cdot10^{-4}$. So at third order the local bounds are
essentially exhausted. These computations are not part of the proof.

On the analytic side, Remark~\ref{rem:certlimit} explains why a certificate of the present form cannot do better than the
constrained equilibrium measure on the chosen contour. A larger decay rate needs a different contour or a different
treatment of the energy problem. The geometry parameter $c$ trades the two sides against each other. A longer border
increases $D$, through the larger node measure. It also increases $\Lambda$, through the border rows and columns of the
assignment bound.

%% =====================================================================
\section{Formalization}\label{sec:lean}
\raggedbottom

The proof of Theorem~\ref{thm:main} is formalized in Lean~4 \cite{Lean4} with Mathlib \cite{Mathlib}, together with every
theorem, proposition and lemma it uses. The remarks and Section~\ref{sec:limits} are not part of the formalization. The
development is available at
\begin{center}
\FormalizationLink
\end{center}
It combines analytic and arithmetic proofs with generated rational data. Kernel checks verify the tables for $\Lambda$ of
Section~\ref{sec:content} and the decay certificates of Section~\ref{sec:decay}. Numerical computations alone are not
used as proof.

The statements of Theorem~\ref{thm:main} are in the file \lean{ChallengeHybrid.lean}. Their proofs are in
\lean{SolutionHybrid.lean}, in the namespace \lean{TrigammaDifferences}. Each final theorem concerns one row of
Table~\ref{tab:main}. Its number $\xi$ is written as a series: the classical form where there is one, and
$\Psi(s,t)$ otherwise. The theorem states that
$b^{-\mu_{s,t}}<|\xi-a/b|$ for all $a\in\Z$ and all sufficiently large $b$. The theorems
are the following.
\begin{itemize}
\item \lean{lambda_plus_measure} and \lean{lambda_minus_measure}: the pairs $(\frac14,1)$ and $(\frac34,1)$,
 with $\mu_{s,t}=\MuLamU$.
\item \lean{chi3_measure}: the pair $(\frac13,\frac23)$, with $\mu_{s,t}=\MuChi$.
\item \lean{chi3_plus_pi2_measure} and \lean{chi3_minus_pi2_measure}: the pairs $(\frac13,1)$ and $(\frac23,1)$, with
 $\mu_{s,t}=\MuThirdsU$.
\item \lean{fifths1_measure}, \dots, \lean{fifths4_measure}: the pairs $(\frac k5,1)$ for $k=1,\dots,4$, with
 $\mu_{s,t}=\MuFifthsU$.
\item \lean{sevenths1_measure}, \dots, \lean{sevenths6_measure}: the pairs $(\frac k7,1)$ for $k=1,\dots,6$, with
 $\mu_{s,t}=\MuSeventhsU$.
\item \lean{pi2_measure}: the pair $(\frac12,1)$, with $\mu_{s,t}=\MuHalvesU$.
\end{itemize}
The shared results are in the namespace \lean{CatalanCore.Uniform}.
\begin{itemize}
\item \lean{Content.BankShared.Check.hasScaledContent_of_check} is Theorem~\ref{thm:content}. The local bounds of
 Theorem~\ref{thm:local} are proved in \lean{Check/Catalogue.lean}, \lean{Check/LP2W.lean},
 \lean{Check/Prefix.lean} and \lean{Check/UF.lean}, with the closed rank bound and the branches of
 Theorem~\ref{thm:wrap}. Its form for functions with several first poles is
 \lean{Content.BankShared.KTerm.hasScaledContent_of_kcheck}.
\item \lean{Content.BankShared.TwoTerm.LP2HypW.gle} is Theorem~\ref{thm:lp2}.
\item \lean{Content.BankShared.TwoTerm.Pre.prefix_gle} is Theorem~\ref{thm:window}.
\item \lean{Content.UFSimple.WrapCheck.catValid_wrap} and \lean{Content.UFSimple.WrapPrefixCheck.catValid_prefix_full}
 are Theorem~\ref{thm:wrap} for $n=0$ and for $n\ge1$. Lemma~\ref{lem:harmonic} is
 \lean{Content.UFSimple.WrapPrefixClosed.HSplit.det_ne} with \lean{HSplit.dir}.
\item \lean{BlockGeom.hasNV0} is Theorem~\ref{thm:selection}.
\item \lean{Decay.AltDecay.altGeom_hasScaledDecay} is Theorem~\ref{thm:decay}. It uses the node energy check
 \lean{Decay/Nodes/EnergyCheck.lean}, the contour check \lean{Decay/ContourCheck.lean} and the cell checks
 \lean{Decay/PolyWire3}.
\item \lean{measure_of_family_nv0_even} is Theorem~\ref{thm:deduction} at the even scales.
\end{itemize}
The solution has no \lean{sorry} and no \lean{native_decide}. The command \texttt{\#print axioms} reports only the three
standard axioms \lean{propext}, \lean{Classical.choice} and \lean{Quot.sound}. The prime number theorem in arithmetic
progressions enters the asymptotics of the denominators. Its formal source is the PNT+ project \cite{PNTPlus}, through OpenAI's
workspace and compatibility additions. We use its Wiener--Ikehara theorem.

The proofs were checked with Lean \texttt{v4.35.0-rc2} and the matching Mathlib release. The vendored files from OpenAI's
repository and from the PNT+ project were converted to Lean's module system and ported to the current toolchain. The repository's README and provenance documents describe the changes. The certificate data were generated with
the interval arithmetic of Arb \cite{Arb}, through \texttt{python-flint}, and Lean re-checks them.

\section*{Disclosure of AI use}
The mathematics, the Lean formalization, the certificate generators and the text of this paper were produced by AI
systems at the request of the author. The author posed the problems, directed the work and is responsible for the
paper. The systems were Claude Opus~5.5, Claude Sonnet~5.5 and Claude Haiku~5.5 (Anthropic), running in Claude Code,
and GPT-6.1 Sol (OpenAI), running in Codex. The underlying irrationality proof for Catalan's constant and its Lean
formalization are due to OpenAI \cite{OpenAI2026}.

\subsection*{Acknowledgements}
We thank the authors of Mathlib and of the PNT+ project, and OpenAI for making its formalization available.

\providecommand{\bysame}{\leavevmode\hbox to3em{\hrulefill}\thinspace}
\providecommand{\MR}{\relax\ifhmode\unskip\space\fi MR }
% \MRhref is called by the amsart/book/proc definition of \MR.
\providecommand{\MRhref}[2]{%
  \href{http://www.ams.org/mathscinet-getitem?mr=#1}{#2}
}
\providecommand{\href}[2]{#2}
\begin{thebibliography}{10}

\bibitem{Apery79}
Roger Ap\'ery, \emph{Irrationalit\'e de {$\zeta(2)$} et {$\zeta(3)$}},
  Ast\'erisque \textbf{61} (1979), 11--13.

\bibitem{BallRivoal01}
Keith Ball and Tanguy Rivoal, \emph{Irrationalit\'e d'une infinit\'e de valeurs
  de la fonction z\^eta aux entiers impairs}, Invent. Math. \textbf{146}
  (2001), no.~1, 193--207.

\bibitem{Beukers79}
Frits Beukers, \emph{A note on the irrationality of {$\zeta(2)$} and
  {$\zeta(3)$}}, Bull. London Math. Soc. \textbf{11} (1979), no.~3, 268--272.

\bibitem{Bojnal2026}
Hrishik~Sai Bojnal, \emph{An irrationality exponent below 2402 for {C}atalan's
  constant}, GitHub repository, October 15, 2026,
  \url{https://github.com/proof-factory/catalan-exponent}; design search and
  certification by Claude Fable~5.1 (Anthropic), 2026.

\bibitem{Brown26}
Francis Brown, \emph{Mellin transforms, transfinite diameter and rational
  approximations of integrals}, 2026, Preprint, 22 April 2026,
  \href{https://arxiv.org/abs/2604.20741}{arXiv:2604.20741}.

\bibitem{CDT2024}
Frank Calegari, Vesselin Dimitrov, and Yunqing Tang, \emph{The linear
  independence of {$1$}, {$\zeta(2)$}, and {$L(2,\chi_{-3})$}}, 2024,
  \href{https://arxiv.org/abs/2408.15403}{arXiv:2408.15403}.

\bibitem{CDT2025}
\bysame, \emph{Arithmetic holonomy bounds and effective {D}iophantine
  approximation}, 2025, Theorem 5.1 gives $\mu(L(2,\chi_{-3}))\le 24781$,
  \href{https://arxiv.org/abs/2510.04156}{arXiv:2510.04156}.

\bibitem{Carreira2026b}
Marcos Costa Santos~Carreira, \emph{Determinant constructions for the
  {D}irichlet beta value at four}, Preprint, 9 October 2026,
  \href{https://doi.org/10.5281/zenodo.23326647}{doi:10.5281/zenodo.23326647},
  2026.

\bibitem{Carreira2026}
\bysame, \emph{General designs and an irrationality exponent for {C}atalan's
  constant}, Preprint, 9 October 2026, revised 21 October 2026,
  \href{https://doi.org/10.5281/zenodo.23532239}{doi:10.5281/zenodo.23532239};
  sources at \url{https://github.com/MarcosCarreira/catalan-designs}, 2026.

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

\bibitem{Eskandari2026}
Payman Eskandari, \emph{Improved rational approximations to {C}atalan's
  constant}, 2026, Preprint, 22 September 2026,
  \href{https://arxiv.org/abs/2609.26354}{arXiv:2609.26354}.

\bibitem{EMN2025}
Payman Eskandari, Kumar Murty, and Yusuke Nemoto, \emph{Mixed motives and
  linear forms in the {C}atalan constant}, 2025, Preprint, October 2025 (v3: 29
  August 2026), \href{https://arxiv.org/abs/2510.20648}{arXiv:2510.20648}.

\bibitem{Fauzan2026}
Aabir Fauzan, \emph{{$\zeta(5)$} is irrational}, Preprint v1, September 17,
  2026, Zenodo,
  \href{https://doi.org/10.5281/zenodo.22826419}{doi:10.5281/zenodo.22826419},
  2026.

\bibitem{Forrester2018Andreief}
Peter~J. Forrester, \emph{Meet {A}ndr\'eief, {B}ordeaux 1886, and {A}ndreev,
  {K}harkov 1882--83}, 2018,
  \href{https://arxiv.org/abs/1806.10411}{arXiv:1806.10411}.

\bibitem{Giraudin26}
David~Niedbala Giraudin, \emph{A new upper bound for the irrationality exponent
  of {$\zeta(2)$}}, 2026, Preprint, 2 October 2026,
  \href{https://arxiv.org/abs/2610.02912}{arXiv:2610.02912}.

\bibitem{Giraudin26z3}
\bysame, \emph{A new upper bound for the irrationality exponent of
  {$\zeta(3)$}}, 2026, Preprint, 22 September 2026,
  \href{https://arxiv.org/abs/2609.26980}{arXiv:2609.26980}.

\bibitem{Jha2026}
R.~K. Jha, \emph{A finite irrationality measure for {C}atalan'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}, 2026.

\bibitem{Arb}
Fredrik Johansson, \emph{Arb: efficient arbitrary-precision midpoint-radius
  interval arithmetic}, IEEE Trans. Comput. \textbf{66} (2017), no.~8,
  1281--1292, \href{https://arxiv.org/abs/1611.02831}{arXiv:1611.02831}.

\bibitem{KLS}
Roelof Koekoek, Peter~A. Lesky, and Ren\'e~F. Swarttouw, \emph{Hypergeometric
  orthogonal polynomials and their {$q$}-analogues}, Springer Monographs in
  Mathematics, Springer, Berlin, 2010.

\bibitem{KrattRivoal08}
Christian Krattenthaler and Tanguy Rivoal, \emph{On a linear form for
  {C}atalan's constant}, South East Asian J. Math. Math. Sci. \textbf{6}
  (2008), no.~2, 3--15,
  \href{https://arxiv.org/abs/0810.1927}{arXiv:0810.1927}.

\bibitem{KrattZudilin19}
Christian Krattenthaler and Wadim Zudilin, \emph{Hypergeometry inspired by
  irrationality questions}, Kyushu J. Math. \textbf{73} (2019), no.~1,
  189--203, \href{https://arxiv.org/abs/1802.08856}{arXiv:1802.08856}.

\bibitem{Lai2026}
Li~Lai, \emph{The linear independence of {$1$}, {$\zeta(3)$}, and
  {$\zeta(4)$}}, 2026, Preprint, 5 October 2026 (v2: 15 October 2026),
  \href{https://arxiv.org/abs/2610.06838}{arXiv:2610.06838}.

\bibitem{LBKWSK26}
Elyasheev Leibtag, Hila Barkan, Rotem Kalisch, Shachar Weinbaum, Michael
  Shalyt, and Ido Kaminer, \emph{New directions in irrationality}, 2026,
  Preprint, 20 October 2026,
  \href{https://arxiv.org/abs/2610.27799}{arXiv:2610.27799}; supplement and
  code at
  \url{https://github.com/RamanujanMachine/new-directions-in-irrationality}.

\bibitem{Litsey2026}
Sean Litsey, \emph{An irrationality measure for {C}atalan's constant}, Hexagon
  preprint hexagon:2610.00187v4, \url{https://hexagonmath.org/2610.00187v4},
  2026.

\bibitem{LiuJiangZhang26}
Jingwen Liu, Kai Jiang, and Pingwen Zhang, \emph{Irrationality exponents of
  logarithms of positive rational numbers}, 2026, Preprint, 7 October 2026,
  revised 8 October 2026 (v2),
  \href{https://arxiv.org/abs/2610.10192}{arXiv:2610.10192}.

\bibitem{LZZ25}
Junqi Liu, Jujian Zhang, and Lihong Zhi, \emph{A formal proof of the
  irrationality of {$\zeta(3)$} in {L}ean 4}, 2025,
  \href{https://arxiv.org/abs/2503.07625}{arXiv:2503.07625}.

\bibitem{Loewner34}
Karl L\"owner, \emph{\"{U}ber monotone {M}atrixfunktionen}, Math. Z.
  \textbf{38} (1934), 177--216.

\bibitem{Marcovecchio09}
Raffaele Marcovecchio, \emph{The {R}hin--{V}iola method for {$\log 2$}}, Acta
  Arith. \textbf{139} (2009), no.~2, 147--184.

\bibitem{Nesterenko85}
Yu.~V. Nesterenko, \emph{On the linear independence of numbers}, Vestnik
  Moskov. Univ. Ser. I Mat. Mekh. (1985), no.~1, 46--49, In Russian; English
  translation: Moscow Univ. Math. Bull. 40 (1985), no. 1, 69--74.

\bibitem{NikishinSorokin91}
E.~M. Nikishin and V.~N. Sorokin, \emph{Rational approximations and
  orthogonality}, Translations of Mathematical Monographs, vol.~92, American
  Mathematical Society, Providence, RI, 1991.

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

\bibitem{OpenAIPi2026}
\bysame, \emph{The irrationality exponent of {$\pi$} is 2}, Preprint dated
  September 24, 2026, released October 6, 2026,
  \url{https://github.com/openai/math/tree/main/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026},
  2026.

\bibitem{Prellberg26}
Thomas Prellberg, \emph{Three irrationality results for the dilogarithm:
  {R}hin--{V}iola and {V}iola--{Z}udilin constructions at {$-1/4$}, {$1/5$},
  and {$-1/3$}}, 2026, Preprint, 7 September 2026,
  \href{https://arxiv.org/abs/2609.06895}{arXiv:2609.06895}.

\bibitem{RhinViola96}
Georges Rhin and Carlo Viola, \emph{On a permutation group related to
  {$\zeta(2)$}}, Acta Arith. \textbf{77} (1996), no.~1, 23--56.

\bibitem{RhinViola01}
\bysame, \emph{The group structure for {$\zeta(3)$}}, Acta Arith. \textbf{97}
  (2001), no.~3, 269--293.

\bibitem{RivoalZudilin2003}
Tanguy Rivoal and Wadim Zudilin, \emph{Diophantine properties of numbers
  related to {C}atalan's constant}, Math. Ann. \textbf{326} (2003), no.~4,
  705--721.

\bibitem{SaffTotik}
Edward~B. Saff and Vilmos Totik, \emph{Logarithmic potentials with external
  fields}, Grundlehren der mathematischen Wissenschaften, vol. 316, Springer,
  Berlin, 1997.

\bibitem{Sun2026}
Zhi-Wei Sun, \emph{Catalan's constant is irrational}, 2026,
  \href{https://arxiv.org/abs/2609.04176}{arXiv:2609.04176}.

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

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

\bibitem{Wachs2026}
Dane Wachs, \emph{A note on a recent claimed proof of the irrationality of
  {C}atalan's constant}, 2026,
  \href{https://arxiv.org/abs/2609.22339}{arXiv:2609.22339}.

\bibitem{Xu2026}
Ryan Xu, \emph{Improved {$\kappa=2$} trial: {$\mu(G)\le727.03$}}, GitHub issue,
  October 22, 2026,
  \url{https://github.com/slitsey/catalan-irrationality-measure/issues/5}; data
  and scripts at \url{https://github.com/ry-xu/slightlysupervised}, 2026.

\bibitem{ZeilbergerZudilin20}
Doron Zeilberger and Wadim Zudilin, \emph{The irrationality measure of {$\pi$}
  is at most {$7.103205334137\ldots$}}, Mosc. J. Comb. Number Theory \textbf{9}
  (2020), no.~4, 407--419,
  \href{https://arxiv.org/abs/1912.06345}{arXiv:1912.06345}.

\bibitem{Zudilin02Cheb}
Wadim Zudilin, \emph{A few remarks on linear forms involving {C}atalan's
  constant}, Chebyshevskii Sb. \textbf{3} (2002), no.~2(4), 60--70, In Russian,
  \href{https://arxiv.org/abs/math/0210423}{arXiv:math/0210423}.

\bibitem{Zudilin2003}
\bysame, \emph{An {A}p\'ery-like difference equation for {C}atalan's constant},
  Electron. J. Combin. \textbf{10} (2003), Research Paper 14,
  \href{https://arxiv.org/abs/math/0201024}{arXiv:math/0201024}.

\bibitem{Zudilin14}
\bysame, \emph{Two hypergeometric tales and a new irrationality measure of
  {$\zeta(2)$}}, Ann. Math. Qu\'ebec \textbf{38} (2014), no.~1, 101--117,
  \href{https://arxiv.org/abs/1310.1526}{arXiv:1310.1526}.

\bibitem{Zudilin}
\bysame, \emph{A determinantal approach to irrationality}, Constr. Approx.
  \textbf{45} (2017), no.~2, 301--310,
  \href{https://arxiv.org/abs/1507.05697}{arXiv:1507.05697}.

\bibitem{Zudilin19Survey}
\bysame, \emph{Arithmetic of {C}atalan's constant and its relatives}, Abh.
  Math. Semin. Univ. Hambg. \textbf{89} (2019), no.~1, 45--53,
  \href{https://arxiv.org/abs/1804.09922}{arXiv:1804.09922}.

\end{thebibliography}

\end{document}