\documentclass[11pt]{amsart}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{booktabs}
\usepackage{array}
\usepackage{hyperref}

% ---------------------------------------------------------------------------
% Revision of 2026-11-07: the main theorem is now Theorem V (chi_2(sqrt(m^2+1) - m), m >= 2, m not in
% {3,5,7,9,15}); Theorem U (m = 2, the golden-ratio form) is Corollary 1.2. Source of the new material:
% schanuel/four_exp/strong4/pilot_V/PROOF_V.md (after its gate referee REFEREE_V and change log). The U-only version
% is kept in old_U_only/.
% Revision of 2026-11-08 (extensions): Theorem V_odd (odd a, all norm -1 units outside 47) and Theorem V_i (Ti_2 at
% norm +1 units), new Section 8. Sources: handoff/log2log3/pilot_za/PROOF_VODD.md (gate referee REFEREE_VODD) and
% schanuel/four_exp/strong4/pilot_w3/PROOF_TI2.md (gate referee REFEREE_TI2), with their change logs. Numbers recomputed
% in ext_checks/. Backup of the text before this revision: old_U_only/main_before_ext.tex.
% Revision of 2026-11-09: Theorem V_odd is formalised in Lean (lean_chi2u, Chi2U.VOdd.theoremVOdd, standard axioms);
% abstract, Section 1, Section 8 and the Lean section updated (fix R3 of lean_chi2u/FIDELITY_REFEREE_VODD.md).
% Revision of 2026-11-09 (later): Theorem V_i is formalised in Lean (lean_chi2u, Chi2U.Ti.theoremVi, standard axioms);
% abstract, Section 1, Section 8, the acknowledgements and the Lean section updated (fix R4 of
% lean_chi2u/FIDELITY_REFEREE_VI.md). Backup of the text before this revision: old_U_only/main_before_vi.tex.
% ---------------------------------------------------------------------------

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

\numberwithin{equation}{section}
\setlength{\emergencystretch}{2em}

% ---------------------------------------------------------------------------
% Macros
% ---------------------------------------------------------------------------
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\KK}{\mathbb{K}}
\newcommand{\cK}{\mathcal{K}}
\newcommand{\cF}{\mathcal{F}}
\newcommand{\cM}{\mathcal{M}}
\newcommand{\cP}{\mathcal{P}}
\newcommand{\cE}{\mathcal{E}}
\newcommand{\cO}{\mathcal{O}}
\newcommand{\fp}{\mathfrak{p}}
\newcommand{\fl}{\mathfrak{l}}
\newcommand{\fP}{\mathfrak{P}}
\newcommand{\fL}{\mathfrak{L}}
\newcommand{\one}{\mathbf{1}}
\newcommand{\eps}{\varepsilon}
\newcommand{\ind}[1]{[\,#1\,]}
\newcommand{\lev}{\operatorname{lev}^{*}}
\newcommand{\adj}{\operatorname{adj}}
\newcommand{\Li}{\operatorname{Li}}
\newcommand{\cross}{\operatorname{cross}}
\newcommand{\Vand}{\operatorname{Vand}}
\newcommand{\artanh}{\operatorname{artanh}}
\newcommand{\ccell}{c_{\mathrm{cell}}}
\newcommand{\Ti}{\operatorname{Ti}}
\newcommand{\Cl}{\operatorname{Cl}}
\newcommand{\lean}[1]{{\def\_{\textunderscore\allowbreak}\texttt{#1}}}

\begin{document}

% Title: the owner's choice of 2026-11-08, after the extensions of Section 8 (it replaces "chi_2(sqrt(m^2+1)-m) is
% irrational for every m >= 16" of 2026-11-07). The exact counts (47 units of norm -1, 57 of norm +1) are in the abstract.
% The title states what is proved, not a novelty claim: the large-trace tails are due to DHK 2022.
\title[$\chi_2$ and $\Ti_2$ at units of real quadratic fields]{Irrationality of \texorpdfstring{$\chi_2$}{chi\_2} and
\texorpdfstring{$\Ti_2$}{Ti\_2} at units of real quadratic fields}

\author{Shawn Krisman}

\subjclass[2020]{Primary 11J72; Secondary 33B30, 11R27, 31A15, 41A21, 68V20}
\keywords{golden ratio, Legendre chi function, dilogarithm, inverse tangent integral, Clausen function, irrationality,
Hankel determinants, units of real quadratic fields, logarithmic potential theory, formal verification, Lean}

\date{\today}

\begin{abstract}
We prove that $\chi_2(\sqrt{m^2+1}-m)$, a value of Legendre's chi function at a unit of norm $-1$, is irrational for
every integer $m\ge2$ except $m=3,5,7,9,15$. For $m=2$ this shows that $\pi^2-18\log^2\varphi$ is irrational, where
$\varphi$ is the golden ratio. The method extends to all units of norm $-1$ in real quadratic fields, giving
$\chi_2(\eps)\notin\QQ$ outside an explicit set of $47$ units, and, through a twist identity, to the inverse tangent
integral $\Ti_2$ at units of norm $+1$, outside $57$ units. The proof combines Hankel determinants of a
reflection-symmetric Pad\'e machine, arithmetic bounds on their denominators, a discrete log-gas bound certified in
interval arithmetic, and a nonvanishing argument modulo a prime. Below the range covered by the criteria of David,
Hirata-Kohno and Kawashima, these results appear to be new. All three theorems are formalised in Lean~4 with Mathlib,
using only the standard axioms.
\end{abstract}

\maketitle

\tableofcontents

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

For $|q|\le1$ let
\[
  \chi_2(q)=\sum_{n=0}^{\infty}\frac{q^{2n+1}}{(2n+1)^2}=\tfrac12\bigl(\Li_2(q)-\Li_2(-q)\bigr)
\]
be Legendre's chi function (see \cite{Lewin1981}). For an integer $m\ge1$ put
\[
  z_m:=\sqrt{m^2+1}-m\in(0,1).
\]
Then $z_m^2+2mz_m-1=0$, so $z_m$ is a unit of norm $-1$ in the real quadratic field $\QQ(\sqrt{m^2+1})$, with
Galois conjugate $-1/z_m$. Put $\cE:=\{3,5,7,9,15\}$.

\begin{theorem}[Theorem V]\label{thm:V}
For every integer $m\ge2$ with $m\notin\cE$, the number $\chi_2(\sqrt{m^2+1}-m)$ is irrational.
\end{theorem}

For $m\ge4\,346\,237$ the stronger statement $\chi_2(z_m)\notin\QQ(\sqrt{m^2+1})$ follows from the criterion of
David, Hirata-Kohno and Kawashima \cite[Thm.~1]{DHK2022b} (our evaluation, Section~\ref{sec:lit}). Their earlier
criterion \cite[Thm.~2.1]{DHK2020}, whose proof is given there only in outline and which \cite[Rem.~1(iii)]{DHK2022b}
describes as announced without proof, would give the same conclusion already for $m\ge2\,517\,046$. What
Theorem~\ref{thm:V} adds is the range $2\le m\le2\,517\,045$ with $m\notin\cE$, where we know of no earlier result,
and, if the announced result is set aside, the range up to $m=4\,346\,236$. The proof is computer-assisted: it uses
one dual certificate checked in interval arithmetic (at $m=2$) and a table of
margins for the odd $m\le65$, also computed in interval arithmetic. The case $m=2$ is the golden-ratio statement. Let
$\varphi=(1+\sqrt5)/2$.

\begin{corollary}[Theorem U]\label{thm:U}
The number
\[
  \pi^2-18\log^2\varphi=5.70143763069985955388\ldots
\]
is irrational. Equivalently, the number
\[
  \chi_2(\sqrt5-2)=\frac{\pi^2}{24}-\frac34\log^2\varphi=0.23755990127916081474\ldots
\]
is irrational.
\end{corollary}

The two forms are equivalent by the identity
\begin{equation}\label{eq:closedform}
  \chi_2(\sqrt5-2)=\frac{\pi^2}{24}-\frac34\log^2\varphi ,
\end{equation}
which follows from Landen's identity
$\chi_2\bigl(\tfrac{1-x}{1+x}\bigr)+\chi_2(x)=\tfrac{\pi^2}{8}+\tfrac12\log x\,\log\tfrac{1+x}{1-x}$
(see \cite{Lewin1981}) at $x=\sqrt5-2=\varphi^{-3}$, for which $(1-x)/(1+x)=\varphi^{-1}$, together with the
classical value $\chi_2(\varphi^{-1})=\pi^2/12-\frac34\log^2\varphi$. Theorem~\ref{thm:V}, Corollary~\ref{thm:U} and the identity
\eqref{eq:closedform} are formalised in Lean (Section~\ref{sec:lean}), and so are Theorems~\ref{thm:Vodd}
and~\ref{thm:Vi} below.

Theorem~\ref{thm:V} covers every even $m\ge2$ and every odd $m\ge11$ except $15$. For example,
\[
  \chi_2(\sqrt{17}-4)\notin\QQ,\qquad \chi_2(\sqrt{37}-6)\notin\QQ,\qquad \chi_2(\sqrt{65}-8)\notin\QQ .
\]
For $m\ge3$ these values are of a different kind from $\chi_2(\sqrt5-2)$: they have no expression through $\pi^2$ and
products of logarithms by dilogarithm identities that preserve the symbol (Proposition~\ref{prop:symbol}). Only $m=1$ and
$m=2$ have a Landen closed form. The method does not reach $m=1$, where
$\chi_2(\sqrt2-1)=\pi^2/16-\frac14\log^2(1+\sqrt2)$, nor $m\in\cE$ (Section~\ref{sec:margins}).

\emph{Extensions.} Every unit $\eps\in(0,1)$ of norm $-1$ of a real quadratic field is
\[
  \alpha_a:=\frac{\sqrt{a^2+4}-a}2,\qquad a:=\eps^{-1}-\eps\in\ZZ_{\ge1},
\]
since $\eps$ and $-1/\eps$ are the roots of $X^2+aX-1$; and $\alpha_{2m}=z_m$. So Theorem~\ref{thm:V} is the case of
even $a$. For odd $a$ the prime $2$ is inert in $\QQ(\sqrt{a^2+4})$ and $1-\alpha_a^2=a\alpha_a$ is a $2$-adic unit;
one new lemma at the prime $2$ (Lemma~\ref{lem:tenzero}) and ten further dual certificates give the following
(Section~\ref{sec:odd-a}). Let $\cE_{\mathrm{odd}}$ be the following set of $39$ odd numbers:
\[
  \cE_{\mathrm{odd}}:=\{5,7,9,\dots,57\}\cup\{63,65,69,75,77,81,85,87,93,99,105,165\}
\]

\begin{theorem}[Theorem V$_{\mathrm{odd}}$]\label{thm:Vodd}
For every odd integer $a\ge5$ with $a\notin\cE_{\mathrm{odd}}$, the number $\chi_2\bigl((\sqrt{a^2+4}-a)/2\bigr)$ is
irrational.
\end{theorem}

\begin{corollary}[units of norm $-1$]\label{cor:normminus}
Let $\eps\in(0,1)$ be a unit of norm $-1$ of a real quadratic field, and $a:=\eps^{-1}-\eps$. If
$a\notin\{1,3\}\cup\cE_{\mathrm{odd}}\cup\{2,6,10,14,18,30\}$, then $\chi_2(\eps)\notin\QQ$. The excluded set consists of
$47$ units.
\end{corollary}

The corollary is Theorems~\ref{thm:V} and~\ref{thm:Vodd} together ($a=2m$ with $m\in\{1\}\cup\cE$ gives the six even
exceptions). The first odd $a$ covered are $59,61,67,71,73,79,83,89,91,95,\dots$, and every odd $a>165$ is covered; for
example $\chi_2\bigl((\sqrt{3485}-59)/2\bigr)\notin\QQ$.

The same machine with the odd character $\chi_4$ modulo $4$ on the atoms reaches the units of norm $+1$. Let
$\Ti_2(x):=\sum_{k\ge0}(-1)^kx^{2k+1}/(2k+1)^2$ be the inverse tangent integral \cite[Ch.~2]{Lewin1981}, and let $\cE_i$ be the following set of $17$ numbers:
\[
  \cE_i:=\{75,77,81,85,87,91,93,95,99,105,111,117,123,135,147,165,195\}.
\]

\begin{theorem}[Theorem V$_i$]\label{thm:Vi}
\begin{enumerate}
\item[(a)] For every integer $m\ge4$ with $m\notin\{5,7,9,15\}$, the number $\Ti_2(m-\sqrt{m^2-1})$ is irrational.
\item[(b)] For every odd integer $n\ge71$ with $n\notin\cE_i$, the number $\Ti_2\bigl((n-\sqrt{n^2-4})/2\bigr)$ is
  irrational. In particular this holds for every odd $n\ge197$.
\end{enumerate}
\end{theorem}

The points are the units $\beta_n:=(n-\sqrt{n^2-4})/2\in(0,1)$ of norm $+1$, with trace $n$ ($n=2m$ in (a)); every unit
of norm $+1$ in $(0,1)$ is one of them. With $\theta:=\arctan\beta_n$ one has $\sin2\theta=2/n$ and the classical formula (see \cite{Lewin1981})
\[
  \Ti_2(\tan\theta)=\theta\log\tan\theta+\tfrac12\bigl(\Cl_2(2\theta)+\Cl_2(\pi-2\theta)\bigr),
\]
so Theorem~\ref{thm:Vi}
concerns Clausen values at the angles $2\theta=\arcsin(2/n)$, which for $n\ge5$ are not rational multiples of $\pi$
(Section~\ref{sec:closed-ext}). An example is $\Ti_2(4-\sqrt{15})\notin\QQ$ ($\sin2\theta=\frac14$). The proof rests on
the identity $\chi_4(t)=-i\cdot i^t$ for odd $t$: the $\chi_4$-twisted machine at $\beta_n$ is $-i$ times the machine of
Theorem~\ref{thm:V} at the complex point $i\beta_n$, which the conjugation fixing $i$ sends to $-1/(i\beta_n)$
(Section~\ref{sec:Ti2}). Not covered are $n=3$, $n=4$ (where
$\Ti_2(2-\sqrt3)=\frac23G-\frac\pi{12}\log(2+\sqrt3)$ is classical, $G$ Catalan's constant), $n=6,10,14,18,30$ and the
odd $n\le69$. So, outside an explicit set of $57$ units, $\Ti_2(\eps)\notin\QQ$ for every unit $\eps\in(0,1)$ of norm
$+1$ of a real quadratic field.

As for Theorem~\ref{thm:V}, the criteria of David, Hirata-Kohno and Kawashima give stronger conclusions far out:
\cite[Thm.~1]{DHK2022b} for $a\ge8\,692\,474$ and $n\ge8\,692\,474$, and \cite[Thm.~2.1]{DHK2020}, as stated and with
its proof only outlined, already for $a\ge5\,034\,092$ and $n\ge5\,034\,092$ (Section~\ref{sec:closed-ext}). Each extension was checked by one AI referee.
Theorems~\ref{thm:Vodd} and~\ref{thm:Vi} are formalised in Lean, with only Lean's three standard axioms
(Section~\ref{sec:lean}). So, with Theorem~\ref{thm:V}, every unit covered by Corollary~\ref{cor:normminus}, and every
unit of norm $+1$ outside the $57$ just mentioned, is covered by a formal statement; the corollary and the statement on
units of norm $+1$ are not themselves stated in Lean.

\subsection{Context}\label{sec:context}
% Related work for m = 2 from schanuel/four_exp/strong4/pilot_U/novelty/NOVELTY.md (finished version, Sections 2--5, read
% 2026-11-07 by the whole-chain referee of the U-only version). For general m: pilot_V/PROOF_V.md Section 10 and
% pilot_V/referee/REFEREE_V.md Sections 5 and 7.
\emph{General $m$.} For $m\ge4\,346\,237$, Theorem~1 of David, Hirata-Kohno and Kawashima \cite{DHK2022b} gives
$\chi_2(z_m)\notin\QQ(\sqrt{m^2+1})$, which is stronger than Theorem~\ref{thm:V}; this is our evaluation of their
criterion (Section~\ref{sec:lit}). Theorem~2.1 of their earlier paper \cite{DHK2020}, as stated, would give the same already
for $m\ge2\,517\,046$; its proof is only outlined there, and \cite{DHK2022b} describes it as announced without proof. So
the infinite part of Theorem~\ref{thm:V} is not new by itself. We have found no result that covers any $m$ with
$2\le m\le2\,517\,045$, and no proved result that covers any $m$ with $2\le m\le4\,346\,236$. For $m\ge3$ that search
was short: our own notes, two web searches, and a reading of the criteria listed in Section~\ref{sec:lit}; it did not
cover MathSciNet, and no expert has been consulted. Our method also covers the ranges of these criteria independently,
with the weaker conclusion.

\emph{The extensions.} For Theorems~\ref{thm:Vodd} and~\ref{thm:Vi} the searches were of the same limited kind (our own
notes, two web searches for each, and for $\Ti_2$ an earlier sweep of arXiv for irrationality results on related
values); they found closed-form identities but no irrationality result for $\chi_2$ at the units $\alpha_a$ with odd
$a$, or for $\Ti_2$ or $\Cl_2$ at the points $\beta_n$, below the thresholds of \cite{DHK2020} (announced) and
\cite{DHK2022b} (proved) (Section~\ref{sec:closed-ext}).

\emph{The case $m=2$.} We have not found Corollary~\ref{thm:U}, or the irrationality of any number
$\pi^2+c\log^2\varphi$ with $c\in\QQ\setminus\{0\}$, in the literature, and as far as we can see it does not follow
from known results. By the analytic class number formula, $L(1,\chi_5)=2\log\varphi/\sqrt5$ for the quadratic character
$\chi_5$ modulo $5$, so the corollary can also be written as $6\zeta(2)-\frac{45}{2}L(1,\chi_5)^2\notin\QQ$.
\begin{itemize}
\item \emph{The golden-ratio dilogarithm values are different numbers.} The classical evaluations
  \[
    \begin{aligned}
    \Li_2(\varphi^{-2})&=\tfrac{\pi^2}{15}-\log^2\varphi,&\quad \Li_2(\varphi^{-1})&=\tfrac{\pi^2}{10}-\log^2\varphi,\\
    \Li_2(-\varphi^{-1})&=-\tfrac{\pi^2}{15}+\tfrac12\log^2\varphi,&\quad \Li_2(-\varphi)&=-\tfrac{\pi^2}{10}-\log^2\varphi
    \end{aligned}
  \]
  (Landen; see \cite{Lewin1981,Lewin1982}) all lie in $\QQ\pi^2+\QQ\log^2\varphi$. Normalised to the form
  $\pi^2+c\log^2\varphi$ they have $c=-15$, $-10$, $-\frac{15}{2}$ and $+10$, while Corollary~\ref{thm:U} has $c=-18$.
  Since $\log\varphi$ is transcendental, $\pi^2+c\log^2\varphi$ can be algebraic for at most one $c\in\overline\QQ$; this
  does not say which. The irrationality of one member of the family says nothing about another, and as far as we know
  the irrationality of each of the four classical values is open.
\item \emph{Homogeneous statements.} The theorem of Gel'fond and Schneider \cite[Ch.~2]{Baker1975}, applied to
  $e^{\log\varphi}=\varphi$ and $e^{i\pi}=-1$, shows that $\log\varphi/(i\pi)$ is transcendental, so
  $\log^2\varphi/\pi^2\notin\overline{\QQ}$. This says that $\pi^2$ and $\log^2\varphi$ are linearly independent over
  $\QQ$; it says nothing about a relation that also involves $1$. The only member of the family
  $\pi^2+c\log^2\varphi$, $c\in\QQ$, whose irrationality we know to be established is $c=0$. The linear independence of
  $1,\pi^2,\log^2\varphi$ over $\QQ$ is open as far as we know.
\item \emph{Criteria at algebraic points.} The linear independence criteria for polylogarithms and Lerch functions at
  algebraic points \cite{DHK2020,DHK2022,DHK2022b,Kawashima2026}, and the explicit form of the Bombieri--Andr\'e
  principle of global relations \cite{Orr2026}, need a point that is small in comparison with its height. Here
  $\chi_2(\sqrt5-2)=\frac12(\Li_2(z)-\Li_2(-z))=z+\frac z4\Phi_2(\frac12,z^2)$, where
  $\Phi_2(x,q)=\sum_{k\ge0}q^{k+1}/(k+x+1)^2$ is the Lerch function and $z=\sqrt5-2=\varphi^{-3}$ is a unit of height
  $\frac32\log\varphi=0.7218\ldots$ whose conjugate $-\varphi^3$ has absolute value $>1$, so that $|z|\,|\sigma z|=1$.
  Evaluating the criteria in the form they are stated, their key quantity is negative by a wide margin at this
  point: about $-26.1$ for \cite[Thm.~2.2]{Kawashima2026}, about $-15.1$ and $-14.5$ for the two ways of applying
  \cite[Thm.~1]{DHK2022b} (through $\Li_2(\pm z)$, or through $\Phi_2(\frac12,z^2)$), and about $-14.0$ for
  \cite[Thm.~2.1]{DHK2020} (through $\Phi_2(\frac12,z^2)$, normalised as in Section~\ref{sec:lit}). The
  Bombieri--Andr\'e bound of \cite{Orr2026}, applied to this system, needs by our estimate a height of about $1450$.
  These evaluations are ours and have not been checked by the authors of the criteria.
\item \emph{Rational points.} The irrationality and linear independence results for dilogarithms at rational points
  \cite{Hata1990,Hata1993,RhinViola2005,RhinViola2019,ViolaZudilin2018}, the recent claims
  \cite{Prellberg2026,TanZhang2026} (unrefereed), and our result $\chi_2(1/3),\chi_2(1/5)\notin\QQ$ \cite{Chi2Paper} all
  concern rational arguments, as do the weight-two results of Calegari, Dimitrov and Tang \cite{CDT} (at sixth roots
  of unity, and for products $\log(1+1/m)\log(1+1/n)$) and Hata's irrationality of $\log(1+1/q)\log(1-1/q)$
  \cite{Hata1998}. The results on products of logarithms are homogeneous and contain no $\pi^2$.
\item \emph{The closest analogue.} The nearest result we know is $\Li_2(\frac12)=\frac{\pi^2}{12}-\frac12\log^22\notin\QQ$,
  proved in Lean by Q.~Tang \cite{TangLi2} and, with many more rational points, by S.~Liu \cite{LiuLi2}; neither is
  accompanied by a refereed paper. It has the same shape, $\pi^2+c\log^2$ of a number, with $c=-6$ and the number $2$
  instead of a unit. Over $\QQ(\sqrt5)$ we have found nothing comparable.
\end{itemize}
For $m=2$ our searches for prior work, in four passes, covered the web, arXiv (through its API), zbMATH Open, OpenAlex,
Crossref, Semantic Scholar (only partly, because of rate limits), the Hexagon repository, the \texttt{openai/math}
manuscript list and recent Lean repositories (the last pass on 7 November 2026). They did not cover MathSciNet or Google
Scholar, and no expert has been consulted. All searches, for $m=2$ and for general $m$, were carried out by AI systems.

\subsection{The method}\label{sec:method}
Fix $m\ge1$ and put
\[
  z:=z_m=\sqrt{m^2+1}-m,\qquad y:=z^2,\qquad T:=\chi_2(z)=\sum_{t\text{ odd}\ge1}\frac{z^t}{t^2}.
\]
Then $z^2+2mz-1=0$, so $1-y=2mz$, and the Galois conjugate of $z$ is $-1/z$. For $m=2$ this is $z=\sqrt5-2$ and $1-y=4z$.
The proof transposes the proof of \cite{Chi2Paper} for $\chi_2(1/q)$ to these points. For even $h$ we take the $K:=h+1$
poles $x_k:=2(k-h/2)$, i.e.\ the even integers in $[-h,h]$, put $D(t):=\prod_k(t-x_k)$, and consider the functional
\[
  \Lambda(g):=\sum_{t\text{ odd}\ge1}z^t\Bigl(\frac{g}{D}\Bigr)'(t)\qquad(g\in\QQ[t]).
\]
Partial fractions give $\Lambda=A+T\,B$ with $\KK$-valued functionals $A,B$, where $\KK:=\QQ(\sqrt{m^2+1})$, so the Hankel
determinant $\det(\Lambda(t^{i+j}))_{i,j<h}$ is the value at $X=T$ of $\Delta_h(X):=\det(A(t^{i+j})+XB(t^{i+j}))_{i,j<h}$,
a polynomial of degree at most $h$.

What differs from \cite{Chi2Paper} is the \emph{reflection} (Lemma~\ref{lem:R}). The pole set is symmetric under
$t\mapsto-t$, $D(-t)=-D(t)$, and the conjugation $\sigma\colon z\mapsto-1/z$ maps the partial sums of $\chi_2$ at the poles
$x$ to those at $-x$. Together these give $\sigma(\Lambda_X(t^a))=(-1)^a\Lambda_X(t^a)$, which forces $\Delta_h\in\QQ[X]$
although its entries lie in $\KK$. So we never pay for the conjugate place, where $|\sigma z|=1/z>1$ and the defining
series diverges. The three inputs are then as in \cite{Chi2Paper}.
\begin{enumerate}
\item \emph{Denominators} (Sections~\ref{sec:odd}--\ref{sec:two}). The moments of $\Lambda$ have the denominators
  $(1-y)^{b+1}=(2mz)^{b+1}$. At odd primes $p\nmid m$ the elements $z$, $y$, $1-y$ are units, and the bounds do not
  depend on $m$. Primes $p<K/3$ obey a plateau bound $2h\lev(p)+v_p(h!)$, which we prove through a bordered version of the
  Lagrange Gram identity (Lemmas~\ref{lem:bordered} and~\ref{lem:nine}), and primes $K/3\le p<K$ obey a class count
  $3(K-p)$ (Lemmas~\ref{lem:eight} and~\ref{lem:classcount}). The prime number theorem sums these to
  $\frac23+\frac23=\frac43$ per $h^2$ (Theorem~\ref{thm:A}). An odd prime $p$ with $e:=v_p(m)\ge1$ costs at most
  $c_p(e):=\bigl(\frac e4+\frac1{4(p-1)}\bigr)\log p$ per $h^2$ (Lemma~\ref{lem:S}). The prime $2$ costs at most
  $c_2(\nu):=|\nu-2|\frac{\log2}4$ per $h^2$, where $\nu:=1+v_2(m)$ is the $2$-adic valuation of $1-y$
  (Lemma~\ref{lem:tennu}); for $m=2$, $\nu=2$ and the cost is only $O(h\log h)$ (Lemma~\ref{lem:ten}).
\item \emph{Size} (Section~\ref{sec:analytic}). A discrete log-gas argument bounds $h^{-2}\log|\Delta_h(T)|$ by the value
  $\Phi_z$ of any dual certificate for a constrained equilibrium problem with external field
  $x\log z-\frac12\int_{x-1}^{x+1}\log|s|\,ds$ (Theorem~\ref{thm:B}). An explicit certificate at $z=\sqrt5-2$, checked
  in interval arithmetic, gives $\Phi\le\Phi_U:=-1.3592161834586374$ (Theorem~\ref{thm:cert}). A shift lemma
  (Lemma~\ref{lem:shift}) moves it to $z_m$ and gives $\Phi\le\Phi_U-\frac12L(m)$ with
  $L(m):=\log\bigl((m+\sqrt{m^2+1})/(2+\sqrt5)\bigr)$ (Corollary~\ref{cor:shift}).
\item \emph{Nonvanishing} (Section~\ref{sec:nonvan}). For $h=3\ell-1$ with $\ell\ge7$ prime and $\ell\nmid m$, the Gram
  matrix of $\Lambda$ in the Lagrange basis is block diagonal modulo a prime of $\KK$ above $\ell$, with $3\times3$ blocks
  in closed form, so $\Delta_h(a/b)\ne0$ whenever $\ell^2\nmid b$ (Lemma~\ref{lem:P}).
\end{enumerate}
The proof of Theorem~\ref{thm:V} therefore shows
\begin{equation}\label{eq:budget}
  \limsup_{h}\frac1{h^2}\log|F_h(T)|\le M(m):=\Phi_U-\tfrac12L(m)+\tfrac43+c_2(\nu)+\sum_{p^e\parallel m,\ p\text{ odd}}c_p(e)
\end{equation}
along a suitable infinite set of $h$, for primitive $F_h\in\ZZ[X]$ of degree $\le h$ with $F_h(T)=\Delta_h(T)\cdot
(\text{integer})$, and $M(m)<0$ exactly when $m\ge2$ and $m\notin\cE$ (Section~\ref{sec:margins}).
Table~\ref{tab:budget} shows the budget for $m=2$ and $m=4$.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}llrr@{}}
\toprule
contribution (per $h^2$, $\limsup$) & source & $m=2$ & $m=4$\\
\midrule
odd primes $p\nmid m$ & Thm.~\ref{thm:A} & $1.333333$ & $1.333333$\\
$p=2$ & Lemmas~\ref{lem:ten}, \ref{lem:tennu} & $0$ & $0.173287$\\
odd primes $p\mid m$ & Lemma~\ref{lem:S} & none & none\\
\midrule
arithmetic & & $1.333333$ & $1.506620$\\
analytic $\Phi$ & Cor.~\ref{cor:shift} & $\le-1.359216$ & $\le-1.684754$\\
\midrule
margin $M(m)$ & & $\le-0.025882$ & $\le-0.178134$\\
\bottomrule
\end{tabular}
\caption{The exponential budget for $m=2$ (Corollary~\ref{thm:U}) and $m=4$ ($\chi_2(\sqrt{17}-4)$). For $m=2$ the
analytic value is the upper endpoint $-1.3592161834586374$ of the certified Arb ball, rounded up, and the margin is
$-0.0258828501\ldots$, rounded up; for $m=4$ the values $-1.6847547\ldots$ and $-0.1781346\ldots$ are rounded up. Other values of $m$ are in Table~\ref{tab:margins}.}\label{tab:budget}
\end{table}

For $m=2$ the margin is about $1.9\%$ of the arithmetic part. It is smaller than in \cite{Chi2Paper} for $q=3$ in
relative terms, but no constant in the budget is estimated: each is a proved upper bound. The margins vary with $m$; among
$m\notin\cE$ the smallest in absolute value are $m=11$ ($-0.0179$), $m=21$ ($-0.0204$) and $m=2$ ($-0.0259$).

\subsection{The formalisation}
Theorem~\ref{thm:V}, Corollary~\ref{thm:U} and the identity \eqref{eq:closedform} are formalised in Lean~4
\cite{LeanFour} with Mathlib \cite{Mathlib} and checked by the Lean kernel. The headline theorems are
\lean{Chi2U.V.theoremV} (Theorem~\ref{thm:V}), \lean{Chi2U.chi2\_sqrt5\_sub\_two\_irrational}
($\chi_2(\sqrt5-2)\notin\QQ$), \lean{Chi2U.golden\_irrational'} ($\pi^2-18\log^2\varphi\notin\QQ$) and
\lean{Chi2U.chi2\_sqrt5\_sub\_two\_eq} (the identity \eqref{eq:closedform}). They depend only on Lean's three standard
axioms (\lean{propext}, \lean{Classical.choice}, \lean{Quot.sound}); there is no \lean{sorry} and no
\lean{native\_decide}. The formal proof of the analytic bound follows the lattice-energy route of \cite{Chi2Paper}, not
the route of Section~\ref{sec:analytic}, and uses its own, coarser certificate; Section~\ref{sec:lean} describes both
differences. For general $m$ the formal proof transports this certificate by the shift lemma; the exception set is
the same $\cE$. Theorems~\ref{thm:Vodd} and~\ref{thm:Vi} are formalised as well (\lean{Chi2U.VOdd.theoremVOdd} and
\lean{Chi2U.Ti.theoremVi}, with the same three axioms), with the same exception sets $\cE_{\mathrm{odd}}$ and $\cE_i$:
Theorem~\ref{thm:Vodd} with eleven direct certificates of its own instead of ten, Theorem~\ref{thm:Vi} with the
certificate of Corollary~\ref{thm:U} and the shift lemma alone. Corollary~\ref{cor:normminus} is not stated in Lean.

\subsection{Two points}
Section~\ref{sec:M1} transposes the proof once more, to units of the biquadratic fields $\QQ(z)$ where $z$ is a root of
$X^4+nX^3+2X^2-nX+1$. There the reflection removes the two conjugates $-1/z$ and $-1/w$, where the series diverge,
and the remaining conjugate $w$ is a second convergent place, which enters through a norm. The result is a disjunction,
proved separately for six values of $n$, with interval-arithmetic certificates. The smallest instance is the following.

\begin{theorem}[M1 at $n=730$]\label{thm:M1-730}
Let $z>w$ be the two roots in $(0,1)$ of $X^4+730X^3+2X^2-730X+1$. Then at least one of the following holds:
\[
  \frac{\pi^2}{8}-\frac18\log^2\bigl(366+\sqrt{133955}\bigr)+\frac18\log^2\bigl(364+11\sqrt{1095}\bigr)\notin\QQ,
\]
\[
  \chi_2(z)-\chi_2(w)\notin\sqrt{1101}\,\QQ .
\]
\end{theorem}

The first number is $\chi_2(z)+\chi_2(w)$, by Landen's identity. Theorem~\ref{thm:M1-730} is not formalised.

\subsection{Organisation and notation}
An earlier version of this paper treated only $m=2$. Section~\ref{sec:construction}, Sections~\ref{sec:atom}--\ref{sec:oddsum},
Sections~\ref{sec:equil}--\ref{sec:cert} and Section~\ref{sec:nonvan} are that version's arguments with $z=z_m$: they use
only $\sigma(z)=-1/z$ and that $z$, $y$, $1-y$ are units at the primes concerned, and they hold verbatim for every $m$
except where the text says otherwise. New in this version are Lemma~S (Section~\ref{sec:special}), Lemma~$10_\nu$
(Section~\ref{sec:two}), the shift lemma (Section~\ref{sec:shift}), the hypothesis $\ell\nmid m$ in Lemma~P$'$, and the
margins (Section~\ref{sec:margins}). The latest revision adds Section~\ref{sec:ext} (Theorems~\ref{thm:Vodd}
and~\ref{thm:Vi}) and Section~\ref{sec:closed-ext}; it changes no statement about Theorem~\ref{thm:V},
Corollary~\ref{thm:U} or Theorem~\ref{thm:M1}.

Section~\ref{sec:construction} sets up the functional, proves the pole expansion and the reflection, and states the
criterion. Sections~\ref{sec:odd} and~\ref{sec:two} bound the denominators, Section~\ref{sec:analytic} bounds the size,
Section~\ref{sec:nonvan} proves nonvanishing, and Section~\ref{sec:proof} assembles the proof and computes the margins.
Section~\ref{sec:ext} proves the two extensions as deltas to this proof. Section~\ref{sec:closed} discusses closed forms and compares Theorem~\ref{thm:V} with known criteria.
Section~\ref{sec:M1} treats two points, Section~\ref{sec:lean} describes the formalisation, and Section~\ref{sec:comp}
lists the computations and the numerical evidence.

Throughout, $p$ and $\ell$ denote primes, $v_p$ is the $p$-adic valuation, $\lfloor\cdot\rfloor$ is the floor,
$(x)_+=\max(x,0)$, and $\ind{P}$ is $1$ if $P$ holds and $0$ otherwise. For a function $G$ on $\ZZ_{\ge0}$,
$\Delta G(s)=G(s+1)-G(s)$ is the forward difference. We write $\theta(x)=\sum_{p\le x}\log p$ and
$\psi(x)=\sum_{p^e\le x}\log p$, and $s_2(b)$ for the binary digit sum of $b$, so $v_2(b!)=b-s_2(b)$. The letter $m$
always denotes the parameter of Theorem~\ref{thm:V}; poles are indexed by $k$.

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

\subsection{Data}\label{sec:data}
Fix an integer $m\ge1$, put $d_m:=m^2+1$ (not a square), let $\KK=\QQ(\sqrt{d_m})$, embedded in $\RR$ with $\sqrt{d_m}>0$,
and let $\sigma$ be its nontrivial automorphism. With $z=z_m=\sqrt{d_m}-m$ and $y=z^2$ we have
\[
  z^2+2mz-1=0,\qquad 1-y=2mz,\qquad \sigma(z)=-1/z .
\]
So $z$ is a unit of $\cO_\KK$. At every odd prime $p\nmid m$ the elements $z$, $y$ and $1-y$ are units; this includes the
primes dividing $d_m$. At an odd prime $p\mid m$, $v_p(1-y)=v_p(m)$. At every prime of $\KK$ above $2$, normalised by
$v(2)=1$, $v(1-y)=\nu:=1+v_2(m)$. The prime $2$ is ramified in $\KK$ for odd $m$, inert for $m\equiv2\bmod4$ and split
for $4\mid m$: write $d_m=f^2d_0$ with $d_0$ squarefree; $f$ is odd, so $d_0\equiv d_m\bmod8$, and $d_m\equiv2,5,1\bmod8$
in the three cases. For $m=2$: $\KK=\QQ(\sqrt5)$, $z=\varphi^{-3}$, $1-y=4z$, $\nu=2$.

Fix an even $h\ge2$ and put $J:=h/2$ and $K:=h+1$. The poles are $x_k:=2(k-J)$ for $0\le k<K$, i.e.\ the even integers
$\pm2j$, $|j|\le J$, and
\begin{gather*}
  D(t):=\prod_{k<K}(t-x_k),\\
  D'(x_k)=\prod_{l\ne k}2(k-l)=(-1)^{K-1-k}2^{K-1}k!\,(K-1-k)! .
\end{gather*}
For a rational function $f$ regular at the odd positive integers and of polynomial growth put
\[
  \cM(f):=\sum_{t\text{ odd}\ge1}z^tf'(t),
\]
an absolutely convergent series, and $\Lambda(g):=\cM(g/D)$ for $g\in\QQ[t]$. For an even integer $x$ define the partial
sums
\[
  P(x):=\begin{cases}\displaystyle\sum_{n\text{ odd},\,0<n<|x|}\frac{z^n}{n^2},&x<0,\\[10pt]
  \displaystyle-\sum_{n\text{ odd},\,-x<n<0}\frac{z^n}{n^2},&x>0,\\[8pt] 0,&x=0.\end{cases}
\]
Only odd $n$ with $|n|\le|x|-1\le h-1$ occur.

\subsection{The pole expansion}

\begin{lemma}[Lemma~1$'$, pole expansion]\label{lem:pole}
For every even integer $x$, $\cM\bigl(1/(t-x)\bigr)=-z^x\bigl(T-P(x)\bigr)$. For a polynomial $F$,
\begin{equation}\label{eq:mahler}
  \cM(F)=z\sum_{b\ge0}\Delta^bG(0)\,\frac{y^b}{(1-y)^{b+1}},\qquad G(s):=F'(2s+1),
\end{equation}
a finite sum. Consequently, writing $g/D=R_g+\sum_kg(x_k)/(D'(x_k)(t-x_k))$ with $R_g\in\QQ[t]$,
\begin{gather*}
  \Lambda(g)=A(g)+T\,B(g),\\
  A(g):=\cM(R_g)+\sum_k\frac{g(x_k)}{D'(x_k)}z^{x_k}P(x_k),\qquad
  B(g):=-\sum_k\frac{g(x_k)}{D'(x_k)}z^{x_k},
\end{gather*}
with $A,B\colon\QQ[t]\to\KK$ linear.
\end{lemma}

\begin{proof}
$\cM(1/(t-x))=-\sum_{t\text{ odd}\ge1}z^t/(t-x)^2$. With $n=t-x$ (odd, $n\ge1-x$) and $z^t=z^xz^n$, the sum is
$z^x\sum_{n\text{ odd}\ge1-x}z^n/n^2=z^x(T-P(x))$ by the definition of $P$. For a polynomial, substitute $t=2s+1$,
expand $G(s)=\sum_b\Delta^bG(0)\binom sb$, and use $\sum_{s\ge0}\binom sby^s=y^b/(1-y)^{b+1}$. All series converge
absolutely since $0<z<1$.
\end{proof}

For an indeterminate $X$ put $\Lambda_X:=A+X\,B$, $E_a:=\Lambda_X(t^a)\in\KK[X]$ and
\begin{gather*}
  \Delta_h(X):=\det\bigl(E_{i+j}\bigr)_{0\le i,j<h}\in\KK[X],\qquad\deg\Delta_h\le h,\\
  \Delta_h(T)=\det\bigl(\Lambda(t^{i+j})\bigr)_{i,j<h}.
\end{gather*}
We use the same notation for every finite family: if $a_0,\dots,a_{h-1}$ and $b_0,\dots,b_{h-1}$ have degrees $<h$ and
coefficient matrices $C_a,C_b$, then $\det(\Lambda_X(a_ib_j))=\det C_a\det C_b\,\Delta_h(X)$.

\subsection{The reflection}
Extend $A$ and $B$ to rational functions $f=R+\sum_kc_k/(t-x_k)$ ($R\in\QQ[t]$, $c_k\in\QQ$) by
$A(f):=\cM(R)+\sum_kc_kz^{x_k}P(x_k)$ and $B(f):=-\sum_kc_kz^{x_k}$, so that $\cM(f)=A(f)+TB(f)$, and put
$\tilde f(t):=f(-t)$.

\begin{lemma}[Lemma~R, reflection]\label{lem:R}
For every such $f$, $\sigma(A(f))+\sigma(B(f))X=-\bigl(A(\tilde f)+B(\tilde f)X\bigr)$.
\end{lemma}

\begin{proof}
We have $\tilde f=\tilde R+\sum_k(-c_k)/(t-(-x_k))$, and the pole set is symmetric. \emph{The $X$-part.} Since $x_k$ is
even, $\sigma(z^{x_k})=(-1/z)^{x_k}=z^{-x_k}$, so $\sigma(B(f))=-\sum_kc_kz^{-x_k}=-B(\tilde f)$. \emph{The pole part
of $A$.} For $x<0$, $\sigma(P(x))=\sum_{0<n<|x|}(-1)^nz^{-n}/n^2=-\sum_{-|x|<n'<0}z^{n'}/n'^2=P(-x)$ (odd $n$, $n'=-n$),
and likewise for $x>0$. Hence $\sigma\bigl(\sum_kc_kz^{x_k}P(x_k)\bigr)=\sum_kc_kz^{-x_k}P(-x_k)$, which is minus the pole
part of $A(\tilde f)$. \emph{The polynomial part.} For a polynomial $R$, $\cM(R)=M_R(z)$ with
$M_R(q):=\sum_{t\text{ odd}\ge1}R'(t)q^t$, a rational function of $q$ with rational coefficients and poles only at
$q=\pm1$; so $\sigma(\cM(R))=M_R(-1/z)$. Since $R'$ is a polynomial, the reciprocity of rational generating functions
gives $\sum_{t\text{ odd}\ge1}R'(t)q^t=-\sum_{t\text{ odd}\le-1}R'(t)q^t$ as rational functions, the right side being
expanded at $q=\infty$: for $R'(t)=t^a$ apply $(q\,d/dq)^a$ to $\sum_{t\text{ odd}\ge1}q^t=q/(1-q^2)=-\sum_{t\text{ odd}\le-1}q^t$. At $q=-1/z$ the
right side is $-\sum_{u\text{ odd}\ge1}R'(-u)(-z)^{u}=\sum_{u\text{ odd}\ge1}R'(-u)z^u=-M_{\tilde R}(z)$, because
$\tilde R'(u)=-R'(-u)$. So $\sigma(\cM(R))=-\cM(\tilde R)$.
\end{proof}

\begin{corollary}[Corollary~R]\label{cor:R}
$\sigma(E_a)=(-1)^aE_a$ coefficientwise, and $\Delta_h(X)\in\QQ[X]$.
\end{corollary}

\begin{proof}
For $f=t^a/D$ we have $D(-t)=(-1)^KD(t)=-D(t)$ ($K$ is odd), so $\tilde f=(-1)^{a+1}f$, and Lemma~\ref{lem:R} gives
$\sigma(E_a)=(-1)^aE_a$. Thus $E_a\in\QQ[X]$ for even $a$ and $E_a\in\sqrt{d_m}\,\QQ[X]$ for odd $a$. The matrix
$\tilde E_{ij}:=E_{i+j}\sqrt{d_m}^{\,\ind{i\text{ odd}}-\ind{j\text{ odd}}}$ has entries in $\QQ[X]$, and
$\tilde E=\operatorname{diag}(\sqrt{d_m}^{\,\ind{i\text{ odd}}})\,(E_{i+j})\,\operatorname{diag}(\sqrt{d_m}^{\,-\ind{j\text{ odd}}})$,
so $\det\tilde E=\Delta_h$.
\end{proof}

Lemma~\ref{lem:R} and Corollary~\ref{cor:R} use only $\sigma(z)=-1/z$; whether $d_m$ is squarefree plays no role.

\subsection{Valuations and the criterion}
For a prime $p$ and a prime $\fp\mid p$ of $\KK$ let $v_\fp$ be normalised by $v_\fp(p)=1$ (so $v_\fp$ takes values in
$\frac12\ZZ$ at ramified primes), extended to $\KK[X]$ as the Gauss valuation (the minimum over the coefficients). On
$\QQ[X]$ every $v_\fp$ restricts to $v_p$. For $\Delta_h\not\equiv0$ put
\begin{gather*}
  n_p:=-v_p(\Delta_h),\qquad F_h:=\Delta_h\prod_pp^{n_p}\in\ZZ[X]\ \text{(primitive)},\\
  \log|F_h(T)|=\log|\Delta_h(T)|+\sum_pn_p\log p .
\end{gather*}
Upper bounds for $n_p$ may be computed from the $\KK$-valued entries at any one $\fp\mid p$, since $\Delta_h\in\QQ[X]$.

\begin{proposition}[Lemma~E]\label{prop:criterion}
Let $\xi\in\RR$ and let $\mathcal H$ be an infinite set of positive integers. Suppose that for $h\in\mathcal H$ there are
$F_h\in\ZZ[X]$ with $\deg F_h\le h$ and $\limsup_{h\in\mathcal H}h^{-2}\log|F_h(\xi)|<0$, and that $F_h(a/b)\ne0$ for
all $h\in\mathcal H$, where $a\in\ZZ$, $b\ge1$. Then $\xi\ne a/b$.
\end{proposition}

\begin{proof}
If $\xi=a/b$, then $b^hF_h(a/b)$ is a nonzero integer, so $h\log b+\log|F_h(\xi)|\ge0$ for $h\in\mathcal H$. Dividing by
$h^2$ contradicts the hypothesis.
\end{proof}

This is the criterion of \cite[Prop.~3.1]{Chi2Paper}, with the nonvanishing set allowed to depend on $b$.

% ===========================================================================
\section{Denominators I: the odd primes}\label{sec:odd}
% ===========================================================================

In Sections~\ref{sec:atom}--\ref{sec:oddsum}, $p$ is an odd prime with $p\nmid m$, and $v=v_\fp$ for a prime $\fp\mid p$ of
$\KK$. Odd primes dividing $m$ are treated in Section~\ref{sec:special}. Since $D$ is monic with integer coefficients,
$R_g\in\ZZ[t]$ for $g\in\ZZ[t]$, and by \eqref{eq:mahler}, with $y$ and $1-y=2mz$ units at $\fp$,
\begin{equation}\label{eq:step3}
  v\bigl(\cM(F)\bigr)\ge\min_{t\text{ odd}\ge1}v_p\bigl(F'(t)\bigr)\qquad(F\in\ZZ_{(p)}[t]),
\end{equation}
because $\Delta^bG(0)$ is an integer combination of values $F'(t)$ at odd $t$. For odd $t$ we have
$t-x_k=(t+2J)-2k$, so for a level $p^e$ the indices $k$ with $p^e\mid t-x_k$ form one residue class $k_0(t)$ modulo
$p^e$ among the $K$ consecutive integers $0,\dots,K-1$. Put
\[
  \lev(p):=\#\{e\ge1:p^e\le h\}.
\]

\subsection{The atom expansion and the class count}\label{sec:atom}
Let $V_{k,i}:=x_k^i$ ($k<K$, $i<h$), $\cP_{ij}:=\cM(R_{t^{i+j}})$ and $\gamma_k(X):=-z^{x_k}(X-P(x_k))/D'(x_k)$. By
Lemma~\ref{lem:pole}, $(E_{i+j})=\cP+V^{\mathsf T}\operatorname{diag}(\gamma)V$.

\begin{lemma}[Lemma~7$'$, atom expansion]\label{lem:atom}
\[
  \Delta_h(X)=\sum_{|I|=|I'|=|S|}\pm\det\cP_{I^cI'^c}\,\det V_{S,I}\,\det V_{S,I'}\prod_{k\in S}\gamma_k(X),
\]
over $I,I'\subseteq\{0,\dots,h-1\}$ and $S\subseteq\{0,\dots,K-1\}$. Moreover $\det V_{S,I}\in\Vand(x_S)\ZZ$, and
$\prod_{k\in S}|D'(x_k)|=\Vand(x_S)^2\cross(S)$ with $\cross(S):=\prod_{k\in S,\,l\notin S}|x_k-x_l|$.
\end{lemma}

\begin{proof}
Expand $\det(\cP+M)$ by the complementary minors of $\cP$ and $M=V^{\mathsf T}\operatorname{diag}(\gamma)V$, and each minor
$\det M_{II'}$ by the Cauchy--Binet formula. A generalised Vandermonde determinant is $\Vand(x_S)$ times a Schur
polynomial with integer coefficients. The last identity splits $\prod_{l\ne k}|x_k-x_l|$ into $l\in S$ and $l\notin S$.
\end{proof}

Lemma~\ref{lem:atom} is algebra and holds at every prime. For an odd level $d$ put $w_d(k):=2\ind{|x_k|>d}$, let
$C_c:=\{k<K:k\equiv c\bmod d\}$, $n_c:=|C_c|$, and
\[
  A_K(d):=\sum_{c\bmod d}\ \max_{S_c\subseteq C_c}\Bigl[|S_c|(n_c-|S_c|)+\sum_{k\in S_c}w_d(k)\Bigr].
\]

\begin{lemma}[Lemma~8$'$, per-level bound]\label{lem:eight}
For every odd prime $p\nmid m$, $n_p\le\sum_{e\ge1,\,p^e<K}A_K(p^e)$.
\end{lemma}

\begin{proof}
$\cP$ is $\fp$-integral by \eqref{eq:step3}. In the term of Lemma~\ref{lem:atom} indexed by $(I,I',S)$, the factors
$\det V_{S,I}\det V_{S,I'}$ cancel $\Vand(x_S)^2$, so by Lemma~\ref{lem:atom} the term has valuation at least
$v(\det\cP_{I^cI'^c})-v_p(\cross(S))+\sum_{k\in S}v(X-P(x_k))$, using that $z^{x_k}$ is a unit. Here
$v_p(\cross(S))=\sum_{e\ge1}\#\{(k,l):k\in S,\ l\notin S,\ p^e\mid k-l\}$ since $x_k-x_l=2(k-l)$, and
$v(X-P(x_k))\ge-2\max_{n\text{ odd},|n|<|x_k|}v_p(n)\ge-2\sum_{e\ge1}\ind{p^e<|x_k|}$. At level $d=p^e$ the pairs
counted are those inside residue classes, $\sum_c|S\cap C_c|(n_c-|S\cap C_c|)$, and $\ind{p^e<|x_k|}=\frac12w_d(k)$.
Bounding the maximum over $S$ level by level and class by class gives the claim. Levels $p^e\ge K$ contribute nothing:
the classes are singletons and $|x_k|\le h<p^e$.
\end{proof}

\begin{lemma}[Lemma~8A$'$, class count]\label{lem:classcount}
For odd $d$ with $K/3\le d<K$ we have $A_K(d)=3(K-d)$, and $A_K(d)=0$ for $d\ge K$.
\end{lemma}

\begin{proof}
For $d\ge K$ all classes are singletons and all weights vanish. Let $K/3\le d<K$. Then $w_d(k)=0$ if and only if
$|k-J|\le(d-1)/2$, a block of $d$ consecutive indices inside $[0,K)$; so every class contains exactly one atom of weight
$0$, and the others have weight $2$. A class with $n$ atoms contributes $V(n):=\max_t[t(n-t)+2\min(t,n-1)]$ (take the
weight-$0$ atom last), and $V(1)=0$, $V(2)=3$, $V(3)=6$. Since $3d\ge K$, classes have at most three atoms. If
$K/3\le d\le K/2$ there are $K-2d$ classes of size $3$ and $3d-K$ of size $2$, with total $6(K-2d)+3(3d-K)=3(K-d)$. If
$K/2<d<K$ there are $K-d$ pairs and $2d-K$ singletons, with total $3(K-d)$.
\end{proof}

\subsection{The plateau: a bordered Lagrange Gram identity}
In \cite{Chi2Paper} the number of poles equals the size $h$ of the determinant, and the Lagrange basis has the right
dimension. Here $K=h+1$, and the $K$ Lagrange polynomials $f_i:=D/(t-x_i)$ have degree $h$: they span the polynomials of
degree $\le h$, one dimension too many. The adjugate of the $(h+1)$-Gram matrix repairs this.

\begin{lemma}[Lemma~B, bordered identity]\label{lem:bordered}
Let $G^f(X):=(\Lambda_X(f_if_j))_{i,j<K}$. Then
\[
  \Delta_h(X)=(-1)^{K(K-1)/2}\,\frac{\one^{\mathsf T}\adj\bigl(G^f(X)\bigr)\one}{\prod_{i<K}D'(x_i)} .
\]
\end{lemma}

\begin{proof}
Let $H_{h+1}:=(E_{a+b})_{a,b\le h}$. Then $\Delta_h=\adj(H_{h+1})_{hh}$. Let $C$ be the coefficient matrix of the
$f_i$ (row $i$ lists the coefficients of $t^0,\dots,t^h$ in $f_i$). Then $G^f=CH_{h+1}C^{\mathsf T}$, so
$\adj(G^f)=(\det C)^2C^{-\mathsf T}\adj(H_{h+1})C^{-1}$ and $\adj(H_{h+1})=(\det C)^{-2}C^{\mathsf T}\adj(G^f)C$. Column $h$
of $C$ is $\one$, since every $f_i$ is monic of degree $h$; hence $\Delta_h=(\det C)^{-2}\one^{\mathsf T}\adj(G^f)\one$.
Finally $(f_i(x_k))_{i,k}=\operatorname{diag}(D'(x_i))=CW$ with $W=(x_k^a)_{a,k}$, and
$\prod_iD'(x_i)=(-1)^{K(K-1)/2}(\det W)^2$, so $(\det C)^2=(-1)^{K(K-1)/2}\prod_iD'(x_i)$.
\end{proof}

\begin{lemma}[Lemma~9$'$, plateau bound]\label{lem:nine}
For every odd prime $p\nmid m$, $n_p\le2h\lev(p)+v_p(h!)$.
\end{lemma}

\begin{proof}
Put $N_e(i):=\#\{k<K:k\ne i,\ p^e\mid k-i\}$ and $N(i):=\sum_eN_e(i)=v_p(D'(x_i))$. Note that $N_e(i)\ge1$ needs
$p^e\le K-1=h$. We first prove the \emph{row claim}
\begin{equation}\label{eq:rowclaim}
  v\bigl(G^f_{ij}\bigr)\ge N(i)-2\lev(p)\qquad(i,j<K).
\end{equation}
Fix an odd $t$ and a level $d=p^e$, and let $k_0=k_0(t)$. The class of $i$ modulo $d$ has $N_e(i)+1$ elements in
$[0,K)$, and classes modulo $d$ in $[0,K)$ differ in size by at most one, so the class $k_0$ has at least $N_e(i)$
elements.

\emph{Off-diagonal entries} ($i\ne j$). Here $f_if_j/D=F:=\prod_{k\ne i,j}(t-x_k)$, so $G^f_{ij}=\cM(F)$. Each term of
$F'(t)$ omits one factor. At level $d$ the factors divisible by $d$ are those with $k\equiv k_0$, $k\ne i,j$; after the
omission at least $N_e(i)-2$ remain, whether $k_0\equiv i$ or not. Summing over levels, every term has $v_p\ge
\sum_e(N_e(i)-2\ind{N_e(i)\ge1})\ge N(i)-2\lev(p)$, and \eqref{eq:step3} gives \eqref{eq:rowclaim}.

\emph{Diagonal entries.} Put $g:=\prod_{k\ne i}(t-x_k)$. Then $f_i^2/D=g/(t-x_i)=Q+g(x_i)/(t-x_i)$ with
$Q:=(g(t)-g(x_i))/(t-x_i)$ and $g(x_i)=D'(x_i)$. By Lemma~\ref{lem:pole} the pole part contributes
$-D'(x_i)z^{x_i}(X-P(x_i))$, of valuation at least $N(i)-2\#\{e:p^e<|x_i|\}\ge N(i)-2\lev(p)$, since $|x_i|\le h$. For
$Q$, list the roots $x_k$, $k\ne i$, of $g$ as $\alpha_1,\dots,\alpha_h$ in order of decreasing $v_p(k-i)$; telescoping
gives
\[
  Q(t)=\sum_{r=1}^{h}\prod_{s<r}(x_i-\alpha_s)\prod_{s>r}(t-\alpha_s),
\]
and for every level $e$ the $\alpha_s=x_k$ with $p^e\mid k-i$ form an initial segment of length $N_e(i)$ (note
$x_i-x_k=2(i-k)$). Fix a term $r$ of $Q'(t)$, which omits one more factor of the second product, and a level $d$. If
$r>N_e(i)$, the first product has $N_e(i)$ factors divisible by $d$. If $r\le N_e(i)$ and $k_0\equiv i$, it has $r-1$,
and the remaining $N_e(i)-r$ class members sit at positions $s>r$, at most one of them omitted: in total at least
$N_e(i)-2$. If $r\le N_e(i)$ and $k_0\not\equiv i$, the whole class $k_0$ (at least $N_e(i)$ members, all with
$v_p(k-i)<e$) sits at positions $s>N_e(i)\ge r$: in total at least $N_e(i)-1$. So \eqref{eq:rowclaim} holds for $Q$
too, by \eqref{eq:step3}.

\emph{The minors.} $\one^{\mathsf T}\adj(G^f)\one=\sum_{a,b}\pm M_{ba}$, where $M_{ba}$ is the minor with row $b$ and
column $a$ deleted. By \eqref{eq:rowclaim} and the Leibniz expansion, $v(M_{ba})\ge\sum_{i\ne b}(N(i)-2\lev(p))\ge
\sum_iN(i)-2h\lev(p)-\max_bN(b)$. Lemma~\ref{lem:bordered} and $v_p(\prod_iD'(x_i))=\sum_iN(i)$ give
$v(\Delta_h)\ge-2h\lev(p)-\max_bN(b)$. Finally $N(b)=v_p(b!\,(h-b)!)\le v_p(h!)$.
\end{proof}

\begin{remark}
At $m=2$, on the exact profiles computed for $h=16,\dots,256$, the bound of Lemma~\ref{lem:nine} is never violated, and
it is attained at most single-level plateau primes; for example at $h=128$ the primes $13,17,19,23,31,37,41,43$ have
$n_p=256+v_p(128!)$ exactly. The row claim \eqref{eq:rowclaim} was checked entrywise at $h=16,24,32,40$ and $p\le13$, with
minimum slack $0$. For other $m$, Lemmas~\ref{lem:eight} and~\ref{lem:nine} were checked at every odd $p\nmid m$ on exact
profiles for $m=3,4,5,6,9,15$ and $h\le48$, and in $47$ further pairs $(m,h)$ by an independent implementation; there
was no violation.
\end{remark}

\subsection{The sum over the odd primes not dividing \texorpdfstring{$m$}{m}}\label{sec:oddsum}

\begin{theorem}[Theorem~A$'$]\label{thm:A}
For every $\eps>0$ and all large even $h$, $\sum_{p\text{ odd},\,p\nmid m}n_p\log p\le(\frac43+\eps)h^2$.
\end{theorem}

\begin{proof}
For $p<K/3$ use Lemma~\ref{lem:nine}:
\begin{align*}
  \sum_{p<K/3}\bigl(2h\lev(p)+v_p(h!)\bigr)\log p&\le2h\bigl(\theta(K/3)+\psi(h)-\theta(h)\bigr)+\log h!\\
  &=\tfrac23h^2+o(h^2)
\end{align*}
by the prime number theorem. For $K/3\le p<K$ we have $p^2\ge K^2/9\ge K$ for $h\ge8$, so only the level $e=1$ occurs,
and Lemmas~\ref{lem:eight} and~\ref{lem:classcount} give $n_p\le3(K-p)$. By the prime number theorem and partial
summation, $\sum_{K/3\le p<K}3(K-p)\log p=3h^2\int_{1/3}^1(1-x)\,dx+o(h^2)=\frac23h^2+o(h^2)$. For $p\ge K$,
$n_p\le0$ by Lemma~\ref{lem:eight}.
\end{proof}

The finite sums of these bounds over all odd primes, divided by $h^2$, are $1.3380$, $1.3350$ and $1.3337$ at $h=1442$,
$20836$ and $875032$. The primes dividing $d_m$ (for $m=2$, the prime $5$) need no separate treatment: $z$ and $1-y=2mz$
are units there, so every step above holds with $v(p)=1$.

\subsection{Odd primes dividing \texorpdfstring{$m$}{m}: Lemma S}\label{sec:special}
At an odd prime $p\mid m$ the matrix $\cP$ is no longer $\fp$-integral, since $v_p(1-y)=v_p(m)>0$. The bound of
Lemma~\ref{lem:eight} survives with an extra term.

\begin{lemma}[Lemma~S]\label{lem:S}
Let $p$ be an odd prime with $e:=v_p(m)\ge1$. Then for every even $h$,
\[
  n_p\le\sum_{l\ge1,\,p^l<K}A_K(p^l)+e\,\frac{(h-2)^2}4 .
\]
Consequently $\limsup_{h\to\infty}n_p/h^2\le\frac e4+\frac1{4(p-1)}$, i.e.\ the prime $p$ costs at most
$c_p(e)=\bigl(\frac e4+\frac1{4(p-1)}\bigr)\log p$ per $h^2$.
\end{lemma}

\begin{proof}
Lemma~\ref{lem:atom} still holds. In the proof of Lemma~\ref{lem:eight} every factor other than $\det\cP_{I^cI'^c}$ is
treated as before: $V$ is integral, $z^{x_k}$ is a unit, $P(x)$ has denominators $n^2$ with $n$ odd, and the class count
does not involve $\cP$. This gives $v(\text{term})\ge v(\det\cP_{I^cI'^c})-\sum_lA_K(p^l)$. For the polynomial part,
$\cP_{ij}=\cM(R_{t^{i+j}})$, where $R_{t^{i+j}}\in\ZZ[t]$ is the quotient of $t^{i+j}$ by $D$ (monic of degree $K$). So
$\cP_{ij}=0$ for $i+j\le K$, since then $R$ is constant and $\cM$ of a constant is $0$. For $r:=i+j-K\ge1$, the Mahler
form \eqref{eq:mahler} with $G(s)=R'(2s+1)\in\ZZ[s]$ of degree $r-1$, and $\Delta^bG(0)\in b!\,\ZZ$, gives
\[
  v(\cP_{ij})\ge\min_{0\le b\le r-1}\bigl(v_p(b!)-e(b+1)\bigr)\ge-e\,r .
\]
So $v(\cP_{ij})\ge-e(i+j-K)_+$. For any bijection $\tau\colon I^c\to I'^c$,
$(i+\tau(i)-K)_+\le(i-K/2)_++(\tau(i)-K/2)_+$, hence
\[
  v(\det\cP_{I^cI'^c})\ge-2e\sum_{i<h}(i-K/2)_+=-e(h/2-1)^2=-e\,\frac{(h-2)^2}4
\]
($h$ even, $K=h+1$). Adding the two bounds gives the first claim. For the limit, a class with $n_c\le K/d+1$ atoms
contributes at most $\max_s[s(n_c-s)+2s]\le(K/d+3)^2/4$ to $A_K(d)$, so $A_K(d)\le d(K/d+3)^2/4=K^2/(4d)+O(K)$, and
$\sum_{l\ge1}p^{-l}=1/(p-1)$; there are $O(\log K)$ levels.
\end{proof}

\emph{Checks.} On exact profiles there was no violation. For $p=3$, $e=1$ (at $m=3$, $6$ and $15$, where $n_3$ was the
same): $n_3=101,202,355,752$ at $h=16,24,32,48$, against the bounds $117,249,441,971$. For $m=9$ ($e=2$):
$n_3=150,579$ at $h=16,32$, against $166,666$. At $m=6$, $h=48$, the generic part of $n_3$ (the value $279$ at $m=2$)
plus $e(h-2)^2/4=529$ gives $808\ge752$, so the term $e(h-2)^2/4$ is close to sharp, while the plateau term of
Lemma~\ref{lem:eight} ($442$) overshoots the generic $279$. These data suggest that the true cost of a special prime is
about $\frac e4\log p$ per $h^2$, and that the extra $\frac1{4(p-1)}\log p$ comes from using Lemma~\ref{lem:eight}
instead of Lemma~\ref{lem:nine} at $p$; we have not proved this (see Remark~\ref{rem:closeE}).

% ===========================================================================
\section{Denominators II: the prime 2}\label{sec:two}
% ===========================================================================

Let $\fP$ be a prime of $\KK$ above $2$ and $v:=v_\fP$, normalised by $v(2)=1$. Then $v(z)=0$ and
$v(1-y)=\nu=1+v_2(m)$ (Section~\ref{sec:data}). For $m=2$, $2$ is inert and $\nu=2$.

\emph{Rescaling.} Put $\tau:=t/2$. The atoms become $\tau=s+\frac12$ ($s\ge0$), the poles $\xi_k:=k-J\in\ZZ$, and
$D(t)=2^K\tilde D(\tau)$ with $\tilde D(\tau):=\prod_{k<K}(\tau-\xi_k)$. With $\tilde\cM(F):=\sum_{s\ge0}z^{2s+1}F'(s+\frac12)$
and $\tilde\Lambda(g):=\tilde\cM(g/\tilde D)$ we get $\Lambda(t^a)=2^{a-K-1}\tilde\Lambda(\tau^a)$, hence
$\Delta_h=2^{-3h}\tilde\Delta_h$ with $\tilde\Delta_h:=\det(\tilde\Lambda_X(\tau^{i+j}))$, since
$\sum_{i<h}2i-h(K+1)=-3h$.

\emph{Anchored basis.} Put $a_i:=\prod_{l<i}(\tau-\xi_l)$ and $b_j:=\prod_{l<j}(\tau-\xi_{K-1-l})$. Both families are
monic of degrees $i$ and $j$, so $\det(G_{ij})=\tilde\Delta_h$ for $G_{ij}:=\tilde\Lambda_X(a_ib_j)$.

\subsection{The entries}

\begin{lemma}[Lemma~$10_\nu$]\label{lem:tennu}
Let $i,j<h$.
\begin{enumerate}
\item[(L)] If $\pi:=i+j-K\ge1$, then $v(G_{ij})\ge1-\pi-\nu+\min_{0\le b\le\pi-1}\bigl((2-\nu)b-s_2(b)\bigr)$. If
  $\pi=0$, then $G_{ij}=0$.
\item[(U)] If $N_0:=K-1-i-j\ge1$, then
  \begin{multline*}
    v(G_{ij})\ge\min\Bigl\{2+(\nu-1)N_0+s_2(N_0),\\
    2-N_0+s_2(N_0)+\min_{0\le r\le N_0-1}\bigl(2r-s_2(r)+\nu(N_0-1-r)\bigr)\Bigr\}.
  \end{multline*}
  If $N_0=0$, then $v(G_{ij})=2$.
\end{enumerate}
\end{lemma}

\begin{proof}
(L) The products $a_i$ and $b_j$ cover the index ranges $[0,i-1]$ and $[K-j,K-1]$, which overlap in $\pi$ indices, so
$a_ib_j/\tilde D=F:=\prod_{l=K-j}^{i-1}(\tau-\xi_l)=2^{-\pi}H(2\tau)$ with $H(U):=\prod_l(U-2\xi_l)\in\ZZ[U]$. So
$F'(s+\frac12)=2^{1-\pi}H'(2s+1)$, and by \eqref{eq:mahler} (with $s$ in place of $(t-1)/2$),
$\tilde\cM(F)=z\sum_{b<\pi}\Delta^bG(0)y^b/(1-y)^{b+1}$, $G(s)=2^{1-\pi}H'(2s+1)$. The Newton coefficients of
$s\mapsto(2s+1)^a$ are $\Delta^b[(2s+1)^a](0)=\sum_{j'\ge b}\binom a{j'}2^{j'}\,b!\,S(j',b)$, of valuation
$\ge b+v_2(b!)=2b-s_2(b)$, while $y^b/(1-y)^{b+1}$ has valuation $-\nu(b+1)$. Hence
$v(G_{ij})\ge1-\pi+\min_{b<\pi}\bigl(2b-s_2(b)-\nu(b+1)\bigr)$, which is the claim. There is no $X$-part. If $\pi=0$ then
$F=1$ and $\tilde\cM(1)=0$.

(U) Now the ranges leave a gap of $N_0+1$ indices, and with $\zeta_l:=\xi_i+l$,
\[
  \frac{a_ib_j}{\tilde D}=\prod_{l=0}^{N_0}\frac1{\tau-\zeta_l}=\frac1{N_0!}\sum_{l=0}^{N_0}(-1)^{N_0-l}\binom{N_0}l\frac1{\tau-\zeta_l}.
\]
For an integer $\zeta$, $\tilde\cM(1/(\tau-\zeta))=-4\sum_sz^{2s+1}/(2s+1-2\zeta)^2=-4z^{2\zeta}(X-S(\zeta))$ (at $X=T$),
where $S(\zeta+1)-S(\zeta)=-z^{-1-2\zeta}/(2\zeta+1)^2$; so $S(\zeta)$ has only odd denominators and $v(S(\zeta))\ge0$.
With $z^{2\zeta_l}=z^{2\xi_i}y^l$ and $S(\zeta_l)=S(\xi_i)-\sum_{r<l}z^{-1-2\xi_i-2r}g(r)$, $g(r):=(s_0+2r)^{-2}$,
$s_0:=2\xi_i+1$,
\[
  G_{ij}=-\frac4{N_0!}\Bigl[z^{2\xi_i}(y-1)^{N_0}\bigl(X-S(\xi_i)\bigr)+z^{-1}\sum_l(-1)^{N_0-l}\binom{N_0}l\sum_{r<l}y^{l-r}g(r)\Bigr].
\]
The first part of the bracket has valuation $\nu N_0$. In the second, write $y^{l-r}=y\sum_{e'}\binom{l-r-1}{e'}\eta^{e'}$
with $\eta:=y-1$ ($v(\eta)=\nu$) and $g(r)=\sum_a\gamma_a\binom ra$; expanding
$g(r)=s_0^{-2}\sum_c(-1)^c(c+1)(2/s_0)^cr^c$ (convergent in $\ZZ_2$) and using $\Delta^ar^c(0)=a!\,S(c,a)$ gives
$v_2(\gamma_a)\ge a+v_2(a!)=2a-s_2(a)$. The identities $\sum_{r<l}\binom ra\binom{l-1-r}{e'}=\binom l{a+e'+1}$ and
$\sum_l(-1)^{N_0-l}\binom{N_0}l\binom lM=\ind{M=N_0}$ collapse the second part to $z^{-1}y\sum_{a+e'=N_0-1}\gamma_a\eta^{e'}$,
of valuation $\ge\min_{0\le a\le N_0-1}(2a-s_2(a)+\nu(N_0-1-a))$. With $v_2(N_0!)=N_0-s_2(N_0)$ and $v(4)=2$ this gives
(U). If $N_0=0$ then $G_{ij}=-4z^{2\xi_i}(X-S(\xi_i))$, of valuation exactly $2$.
\end{proof}

Nothing in this proof uses a particular value of $\nu$; for $\nu=2$ it is the computation of the earlier version.

\subsection{The content}

\begin{proposition}\label{prop:ntwo}
For every even $h\ge2$:
\[
  n_2\le\begin{cases}(\nu-1)\dfrac{(h-2)^2}4-\dfrac{h^2}4+h\lfloor\log_2h\rfloor+5h-1,&\nu\ge2,\\[8pt]
  \dfrac{(h-2)^2}4+3h,&\nu=1.\end{cases}
\]
Hence $\limsup_hn_2/h^2\le|\nu-2|/4$, and the prime $2$ costs at most $c_2(\nu)=|\nu-2|\frac{\log2}4$ per $h^2$.
\end{proposition}

\begin{proof}
\emph{$\nu\ge2$.} In (L), $(2-\nu)b\ge(2-\nu)(\pi-1)$ and $s_2(b)\le\lfloor\log_2\pi\rfloor+1$, so
$v(G_{ij})\ge-(\nu-1)\pi-2-\lfloor\log_2\pi\rfloor$. In (U), $2r-s_2(r)+\nu(N_0-1-r)\ge2(N_0-1)-s_2(r)$, so
$v(G_{ij})\ge N_0-1+s_2(N_0)-\lfloor\log_2N_0\rfloor\ge N_0-\lfloor\log_2N_0\rfloor$; the first term of the minimum in (U)
is larger. Hence $v(G_{ij})\ge\hat g(i+j)-\lfloor\log_2h\rfloor-2$ for all $i,j$, with the piecewise linear function
\[
  \hat g(s):=K-1-s\quad(s\le K),\qquad \hat g(s):=-1-(\nu-1)(s-K)\quad(s\ge K),
\]
which is concave since its slopes $-1$ and $-(\nu-1)$ decrease (at $s=K$ the entry vanishes, and at $s=K-1$ its
valuation is $2\ge0$). For a permutation $\sigma$ of $\{0,\dots,h-1\}$ the vector $(i+\sigma(i))_i$ is majorised by
$(2i)_i$: the $k$ largest entries of $i+\sigma(i)$ sum to at most twice the $k$ largest $i$, and the totals are equal. By
Karamata's inequality, $\sum_i\hat g(i+\sigma(i))\ge\sum_i\hat g(2i)=\frac{h^2}4+1-(\nu-1)\frac{(h-2)^2}4$. By the
Leibniz expansion, $v(\tilde\Delta_h)\ge\frac{h^2}4+1-(\nu-1)\frac{(h-2)^2}4-h(\lfloor\log_2h\rfloor+2)$, and
$n_2=-v(\Delta_h)=3h-v(\tilde\Delta_h)$.

\emph{$\nu=1$.} (L) gives $v(G_{ij})\ge-\pi$, since $\min_b(b-s_2(b))=0$. In (U) the first term is $2+s_2(N_0)$ and the
second is $1+s_2(N_0)+\min_r(r-s_2(r))=1+s_2(N_0)\ge2$. So $v(G_{ij})\ge\hat g_1(i+j)$ with the concave
$\hat g_1(s):=-(s-K)_+$, and $\sum_i\hat g_1(2i)=-(1+3+\dots+(h-3))=-(h/2-1)^2$. Conclude as before.
\end{proof}

At $\nu=3$ (for example $m=4$) the bound reads $n_2\le h^2/4+h\lfloor\log_2h\rfloor+3h+1$. On exact profiles at $m=4$,
$n_2=23,94,201,349,523,737,1277$ at $h=8,16,24,32,40,48,64$, against the bounds $65,177,313,513,721,961,1601$; the
share $n_2\log2/h^2$ is $0.249$ at $h=8$ and $0.216$ at $h=64$, and $0.2046$, $0.2002$ at $h=96$, $128$, falling towards
the proved limit bound $0.1733$. At $m=8$ ($\nu=4$), $n_2=2205$ at $h=64$ against the bound $2562$. Every entry bound (L), (U)
was checked on the exact Gram matrices for $m=1,3,4,6,8,12,16$ and $h\le64$ (both embeddings where $2$ splits), with no
violation and with equality attained. In \cite{Chi2Paper} the corresponding quantity is $v_2(1-q^{-2})=3$, which costs
$\frac14\log2$ per $h^2$, in agreement with $c_2(3)$.

\subsection{The case \texorpdfstring{$\nu=2$}{nu = 2}}
At $\nu=2$ Proposition~\ref{prop:ntwo} gives $n_2\le h\lfloor\log_2h\rfloor+4h$. The direct assignment gives a slightly
better bound; for $m=2$ this is the bound used in the earlier version.

\begin{lemma}[Lemma~10$'$]\label{lem:ten}
Let $\nu=2$ (that is, $m\equiv2\bmod4$) and $i,j<h$.
\begin{enumerate}
\item[(L)] If $\pi\ge1$, then $v(G_{ij})\ge-\pi-\lfloor\log_2\pi\rfloor-2$. If $\pi=0$, then $G_{ij}=0$.
\item[(U)] If $N_0\ge1$, then $v(G_{ij})\ge N_0-\lfloor\log_2N_0\rfloor$. If $N_0=0$, then $v(G_{ij})=2$.
\end{enumerate}
Consequently $n_2\le h\lfloor\log_2h\rfloor+3h$.
\end{lemma}

\begin{proof}
(L) and (U) are Lemma~\ref{lem:tennu} at $\nu=2$: in (L), $1-\pi-2+\min_{b<\pi}(-s_2(b))\ge-\pi-\lfloor\log_2\pi\rfloor-2$;
in (U), the second term is $N_0-1+s_2(N_0)-\lfloor\log_2N_0\rfloor$ and the first, $N_0+2+s_2(N_0)$, is larger.
\emph{Assignment.} In all cases $v(G_{ij})\ge K-i-j-\lfloor\log_2h\rfloor-2$, since $\pi,N_0\le h$. By the Leibniz
expansion, $v(\tilde\Delta_h)\ge\sum_{i<h}(K-i-\sigma(i))-h(\lfloor\log_2h\rfloor+2)=-h\lfloor\log_2h\rfloor$ for every
permutation $\sigma$, and $n_2=3h-v(\tilde\Delta_h)$.
\end{proof}

The mechanism is $\nu=2$: both triangles (L) and (U) then have slope $1$ in $i+j$, and the permutation sum of the
bound is constant. Section~\ref{sec:M1} shows what happens when $\nu=1$ in a biquadratic setting. At $m=2$ the exact values
$n_2=54,96,142,240,350,576,830$ at $h=16,24,32,48,64,96,128$ lie below the bound of Lemma~\ref{lem:ten}
($112,168,256,384,576,864,1280$), and $n_2/(h\log_2h)$ rises from $0.84$ to $0.94$ for $h\le256$.

% ===========================================================================
\section{The size of \texorpdfstring{$\Delta_h(T)$}{Delta\textunderscore h(T)}: Theorem B\texorpdfstring{$'$}{'}}\label{sec:analytic}
% ===========================================================================

\subsection{The equilibrium problem and weak duality}\label{sec:equil}
For $0<z<1$ put
\[
  \Psi(x):=\tfrac12\int_{x-1}^{x+1}\log|s|\,ds,\qquad v_z(x):=x\log z-\Psi(x).
\]
$\Psi$ is even, increasing on $[0,\infty)$, and $\Psi(0)=-1$. The function $v_z$ is continuous, and
$v_z'(x)=\log z-\frac12\log|(x+1)/(x-1)|$ for $x\ne\pm1$. For $x>0$, $x\ne1$, the logarithm is positive, so
$v_z'<\log z<0$; for $-1<x\le0$, $v_z'(x)=\log z+\artanh|x|<0$ if and only if $|x|<\tanh(\log(1/z))$. For
$0<z\le\sqrt5-2$ we have $\tanh(\log(1/z))\ge\tanh(\log(2+\sqrt5))=0.8945\ldots$. Hence
\begin{equation}\label{eq:vmono}
  v_z\text{ is strictly decreasing on }(-0.894,\infty)\supset[-1/h,\infty)
\end{equation}
for every $h\ge2$ and $0<z\le\sqrt5-2$.
This covers every $z_m$ with $m\ge2$, since $z_m$ decreases in $m$. For a finite positive measure $\rho$ with compact
support put $U^\rho(x):=\int\log|x-s|\,d\rho(s)$ and $E(\rho):=\iint\log|x-s|\,d\rho(x)\,d\rho(s)$.

Call $\mu$ \emph{admissible} if it is a density with $0\le\mu\le1$, mass $1$ and $\operatorname{supp}\mu\subset[0,2]$.
For admissible $\mu$ and $\lambda\in\RR$ put
\[
  F_\mu:=2U^\mu+v_z,\qquad \Phi_z(\mu,\lambda):=-E(\mu)+\lambda+\int_0^\infty(F_\mu-\lambda)_+\,dx .
\]
If $\rho$ is a density with $0\le\rho\le1$, mass $1$ and compact support, then $E(\rho-\mu)\le0$
\cite[Lemma~I.1.8]{SaffTotik}, i.e.\ $E(\rho)\le2\int U^\mu\,d\rho-E(\mu)$, so
\begin{equation}\label{eq:weakdual}
  E(\rho)+\int v_z\,d\rho\le-E(\mu)+\lambda+\int(F_\mu-\lambda)\,d\rho .
\end{equation}
The supremum of the left side over such $\rho$ supported in $[0,\infty)$ is the constrained equilibrium constant $C_z$;
by \eqref{eq:weakdual}, $C_z\le\Phi_z(\mu,\lambda)$.

\subsection{The theorem}

\begin{theorem}[Theorem~B$'$]\label{thm:B}
Let $0<z\le\sqrt5-2$ and $T=\chi_2(z)$. Let $\mu$ be admissible, $\lambda\in\RR$ and $\ccell\ge0$, and suppose that
\begin{enumerate}
\item[(i)] $F_\mu-\lambda\le-1.13-0.94(x-4)$ on $[4,\infty)$, and
\item[(ii)] $F_\mu-\lambda\le\ccell$ on $[-1/100,0]$.
\end{enumerate}
Then for every even $h\ge100$,
\[
  \log|\Delta_h(T)|\le h^2\,\Phi_z(\mu,\lambda)+E_{\mathrm{an}}(h),
\]
where $c_1(h):=\log(2h)+1+\log(2+\log(2h+1))$ and
\begin{multline*}
  E_{\mathrm{an}}(h):=2h\log(4h)+h\log4+(2h+1)\log3\\
  +h\,c_1(h)+(\ccell+2.362)h-h\log h+1 .
\end{multline*}
In particular $\limsup_{h\to\infty}h^{-2}\log|\Delta_h(T)|\le\Phi_z(\mu,\lambda)$.
\end{theorem}

For $m=2$ the certified pair of Section~\ref{sec:cert} has $\ccell=5.38$, which gives the constant $7.742$ of the earlier
version. The proof follows the proof of Theorem~B in \cite{Chi2Paper} in the first two steps and then departs from it: the
poles now lie on both sides of the atoms, which is handled by an exact Jensen-type bound (step~4), and the discretisation
spreads the particles into cells (step~5) instead of using a lattice energy inequality. Steps 1--4 do not involve $z$;
step~5 uses only \eqref{eq:vmono}, and step~6 only the hypotheses (i) and (ii).

\begin{proof}
Write $\phi:=1/D$.

\emph{1. Node expansion.} For $a,b\in\QQ[t]$, $(ab\phi)'=a'b\phi+ab'\phi+ab\phi'$, so
$\Lambda(ab)=\sum_{t\text{ odd}\ge1}(a,a')(t)\,M_t\,(b,b')(t)^{\mathsf T}$ with
$M_t:=z^t\bigl(\begin{smallmatrix}\phi'&\phi\\\phi&0\end{smallmatrix}\bigr)(t)$. Let $H^{(t_{\max})}$ be the Hankel matrix of
the sums truncated at $t\le t_{\max}$. Each node $t$ carries a \emph{value slot} (the row $(t^i)_{i<h}$) and a
\emph{derivative slot} (the row $(it^{i-1})_{i<h}$). By the Cauchy--Binet formula, $\det H^{(t_{\max})}$ is a sum over
\emph{patterns} $n=(n_t)$, $n_t\in\{0,1,2\}$, $\sum_tn_t=h$, and over pairs $(S,S')$ of slot sets with $n_t$ slots at
node $t$, of $\pm\det E_S\,\det\mathbb M_{S,S'}\,\det E_{S'}$, where $E_S$ is the matrix of the rows in $S$ and
$\mathbb M$ is block diagonal with blocks $M_t$. There are at most $4^h$ pairs $(S,S')$ per pattern.

\emph{2. Slot weights.} $|\det\mathbb M_{S,S'}|\le\prod_t(z^t\omega_t)^{n_t}$ with $\omega_t:=\max(|\phi(t)|,|\phi'(t)|)$
(for $n_t=2$ note $|\det M_t|=z^{2t}\phi(t)^2$). The $K$ numbers $t-x_k$ are distinct odd integers, so
$|\phi'/\phi|(t)\le\sum_k1/|t-x_k|\le2\sum_{c=0}^h1/(2c+1)\le2+\log(2h+1)$, and $\omega_t\le|\phi(t)|(2+\log(2h+1))$.

\emph{3. Vandermonde determinants with derivative rows.} $|\det E_S|\le(4h)^h\prod_{t<t'}|t-t'|^{n_tn_{t'}}$. Indeed,
replace the derivative-only slots $s_1,\dots,s_r$ of $S$ by value rows at free variables; the result is a confluent
Vandermonde determinant $\pm\prod_{a<b}(a-b)^{n_an_b}$, and $\det E_S$ is obtained by applying
$\partial_{s_1}\cdots\partial_{s_r}$ and evaluating at the nodes. By induction, after $c$ derivatives the expression is a sum
of at most $(h-1)^c$ terms, each a product of $c$ exponents (each $\le2$) times $\prod(a-b)^{e'_{ab}}$ with
$0\le e'_{ab}\le n_an_b$. At the nodes $|a-b|\ge2>1$, so each term is at most $2^c\prod|a-b|^{n_an_b}$, and
$(2(h-1))^r\le(4h)^h$.

\emph{4. The pole product.} For odd $t$ the numbers $t-x_k$ are the odd integers in $[t-h,t+h]$. For every odd $u$,
$\log|u|\ge\frac12\int_{u-1}^{u+1}\log|s|\,ds$, by concavity of $\log$ on $(0,\infty)$ and on $(-\infty,0)$ (the
singular endpoint is integrable). The intervals $[u-1,u+1]$ tile $[t-h-1,t+h+1]$, so with $x:=t/h$ and $s=u/h$,
\begin{align*}
  \log|D(t)|&\ge\tfrac12\int_{t-h-1}^{t+h+1}\log|u|\,du\\
  &=(h+1)\log h+h\Psi(x)+\tfrac h2\Bigl[\int_{x+1}^{x+1+1/h}+\int_{x-1-1/h}^{x-1}\Bigr]\log|s|\,ds .
\end{align*}
Each bracketed integral is over an interval of length $1/h$, hence at least $\int_{-1/(2h)}^{1/(2h)}\log|s|\,ds=-(\log(2h)+1)/h$.
So $\log|D(t)|\ge(h+1)\log h+h\Psi(x)-\log(2h)-1$ and, with step~2,
\begin{equation}\label{eq:nodeweight}
  t\log z+\log\omega_t\le h\,v_z(t/h)-(h+1)\log h+c_1(h).
\end{equation}
By steps 1--4, the pattern $n$ contributes at most $4^h(4h)^{2h}e^{D(n)}$ with
$D(n):=\sum_{t\ne t'}n_tn_{t'}\log|t-t'|+\sum_tn_t\bigl(h\,v_z(t/h)-(h+1)\log h+c_1(h)\bigr)$.

\emph{5. Discrete to continuum.} Spread the $n_t$ slots of node $t$ uniformly over $I_t:=[(t-2)/h,t/h]$: the density
$\rho_n:=\sum_t\frac{n_t}2\one_{I_t}$ satisfies $0\le\rho_n\le1$, has mass $1$, and is supported in $[-1/h,\infty)$. By
\eqref{eq:vmono}, $v_z(t/h)\le v_z$ on $I_t$, so $\sum_tn_th\,v_z(t/h)\le h^2\int v_z\,d\rho_n$. For $t\ne t'$ with
$|t-t'|=2d$, writing $x=(t-2+2a)/h$, $a\in[0,1]$,
\begin{gather*}
  h^2\iint_{I_t\times I_{t'}}\log|x-s|\,d\rho_n\,d\rho_n=n_tn_{t'}\bigl(\log|t-t'|-\log h-\operatorname{gap}(d)\bigr),\\
  \operatorname{gap}(d):=\log d-\int_0^1\!\!\int_0^1\log|d+a-a'|\,da\,da',
\end{gather*}
and $0\le\operatorname{gap}(d)\le0.1137/d^2$ (with equality at $d=1$ up to rounding). A cell with itself gives
$n_t^2(\log2-\log h-\frac32)$. Summing, and using $n_{t'}\le2$ and $\sum_tn_t^2\le2h$,
\[
  \sum_{t\ne t'}n_tn_{t'}\log|t-t'|\le h^2E(\rho_n)+h^2\log h+0.748h+1.614h
\]
($4\cdot0.1137\,\zeta(2)\le0.748$ and $2(\frac32-\log2)\le1.614$). The terms in $\log h$ combine to
$h^2\log h-h(h+1)\log h=-h\log h$, so
\[
  D(n)\le h^2J(\rho_n)-h\log h+h\,c_1(h)+2.362h,\qquad J(\rho):=E(\rho)+\int v_z\,d\rho .
\]

\emph{6. Dual, the cell below $0$, and far nodes.} By \eqref{eq:weakdual},
$h^2J(\rho_n)\le h^2(-E(\mu)+\lambda)+h^2\int(F_\mu-\lambda)\,d\rho_n$. On $[0,4]$ the integral is at most
$\int_0^4(F_\mu-\lambda)_+dx$, since $\rho_n\le1$. On $[-1/h,0]\subset[-1/100,0]$, which only the cell $I_1$ meets, (ii)
gives $F_\mu-\lambda\le\ccell$, so the contribution to $h^2J$ is at most $\ccell h$. On $[4,\infty)$, by (i), a slot at a
node $t\ge4h+3$ contributes at most $-a_t$ with $a_t:=h(1.13+0.94((t-2)/h-4))\ge1.13h$; the node $4h+1$, whose cell
straddles $4$, has $F_\mu-\lambda<0$ on its part beyond $4$. So for every pattern
\[
  h^2J(\rho_n)\le h^2\Phi_z(\mu,\lambda)+\ccell h-\sum_{t\ge4h+3}n_ta_t .
\]
The $2h+1$ odd nodes $t\le4h+1$ carry at most $3^{2h+1}$ patterns, and the nodes beyond contribute at most
$\prod_{t\ge4h+3}(1+e^{-a_t}+e^{-2a_t})\le\exp\bigl(2e^{-1.13h}/(1-e^{-1.88})\bigr)\le e$. Collecting,
\begin{multline*}
  \log|\det H^{(t_{\max})}|\le h\log4+2h\log(4h)+(2h+1)\log3\\
  +h^2\Phi_z(\mu,\lambda)+\ccell h-h\log h+h\,c_1(h)+2.362h+1,
\end{multline*}
uniformly in $t_{\max}$. As $t_{\max}\to\infty$ the truncated matrices converge entrywise to $(\Lambda(t^{i+j}))$, and
the determinant is continuous.
\end{proof}

\begin{remark}
On $[-1/h,0]$ we have $U^\mu(x)\le\log(2+1/h)$ (as $\operatorname{supp}\mu\subset[0,2]$) and $v_z(x)\le|\log z|/h-\Psi(0)
=1+|\log z|/h$; so (ii) holds with $\ccell=2\log(2.01)+1+|\log z|/100-\lambda$ whenever this is $\ge0$. For any $h\ge2$
one may instead use $U^\mu(x)\le\int_1^2\log(s+1)\,ds=0.9095\ldots$ on $[-1/h,0]$ (because $\mu\le1$ and
$\operatorname{supp}\mu\subset[0,2]$); at $m=2$ this gives $F_\mu-\lambda\le7.23$ there and the bound of
Theorem~\ref{thm:B} for every even $h\ge2$ with $\ccell+2.362$ replaced by $9.592$. Only the $O(h)$ term changes.
\end{remark}

\subsection{The certificate at \texorpdfstring{$\sqrt5-2$}{sqrt5 - 2}}\label{sec:cert}

\begin{theorem}\label{thm:cert}
For $z=z_2=\sqrt5-2$ there is an admissible pair $(\mu_U,\lambda_U)$ satisfying the hypotheses of Theorem~\ref{thm:B}
with $\ccell=5.38$ and
\[
  \Phi_{z_2}(\mu_U,\lambda_U)\le\Phi_U:=-1.3592161834586374 .
\]
\end{theorem}

The proof is a finite computation in ball arithmetic (Arb \cite{Arb}, through python-flint \cite{pythonflint}) at $128$
bits. The density $\mu$ is constant on $N$ equal cells of $[0,2]$, with rational heights in $[0,1]$ and mass exactly $1$
(checked in exact rational arithmetic). The energy $E(\mu)$ is computed from the exact double antiderivative
$\frac12u^2\log|u|-\frac34u^2$ as a Toeplitz sum over cell offsets. The grid has step $d/r$ ($d=2/N$ the cell width,
$r$ even, so cell midpoints are grid points), and on each grid interval $I=[a,b]$:
\begin{itemize}
\item the three cells nearest to $I$ are treated exactly: each cell potential is unimodal with its minimum at the cell
  midpoint, so its maximum on $I$ is at an endpoint that can be chosen exactly;
\item the far field $f=2\sum_{\text{far}}\mu_jU_j$ (every far cell is at distance $\ge d$ from $I$) satisfies
  $f''\ge-4/d$, because $f''=-2\int_{\text{far}}\mu(s)(x-s)^{-2}ds$ and $\mu\le1$; and $v''(x)=1/(x^2-1)$ is $\ge-1/(1-b^2)$
  for $b<1$ and $\ge0$ for $a>1$. A function $g$ with $g''\ge-\kappa$ on $I$ satisfies
  $\sup_Ig\le\max(g(a),g(b))+\kappa(b-a)^2/8$; this is applied to $f+v$ with $\kappa=4/d+1/(1-b^2)$ (if $b<1$) or
  $\kappa=4/d$ (if $a>1$). On the two intervals touching $x=1$, $v$ is bounded by $v(a)$;
\item $\int(F_\mu-\lambda)_+\le\sum_I|I|\max(S_I-\lambda,0)$, with $S_I$ the resulting upper bound on $I$; on
  $[4,\infty)$, $F_\mu(x)\le2\log x+x\log z-\log(x-1)$, which is $<\lambda$ and decreasing there.
\end{itemize}
A first version with per-cell maxima everywhere loses the cancellation between neighbouring cells and gives only
$-1.313$ at $N=100$. Table~\ref{tab:cert} lists the results; the last row proves Theorem~\ref{thm:cert}.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}rrcccc@{}}
\toprule
$N$ & $r$ & $-E(\mu)$ & $\lambda$ & $\int(F_\mu-\lambda)_+\le$ & certified $\Phi$\\
\midrule
200 & 16 & 1.21902586 & $-2.96219282$ & 0.38673 & $-1.35643705$\\
400 & 32 & 1.21902867 & $-2.96297388$ & 0.38528 & $-1.35866119$\\
800 & 32 & 1.21902407 & $-2.96310589$ & 0.38505 & $-1.35903096$\\
1600 & 32 & 1.21902464 & $-2.96316943$ & 0.384929 & $-1.35921618345864$\\
\bottomrule
\end{tabular}
\caption{Dual certificates for Theorem~\ref{thm:B} at $z=\sqrt5-2$ (decimal values rounded; $\lambda$ is a rational
number). For $N=1600$ the certified Arb ball is $[-1.35921618345864\pm2.6\cdot10^{-15}]$, with upper endpoint
$-1.3592161834586374$.}\label{tab:cert}
\end{table}

The side conditions of Theorem~\ref{thm:B} hold for the certified pair: at $x=4$,
$2\log x+x\log z-\log(x-1)-\lambda=-1.137\ldots$, and the slope of this bound on $[4,\infty)$ is at most
$2/x+\log z\le-0.94$; on $[-1/h,0]$, $h\ge100$, we have $U^\mu\le\log(2+1/h)$ and $v_z\le1+1.4437/h$, hence
$F_\mu\le2.4108$ and $F_\mu-\lambda\le2.4108+2.96317\le5.374<5.38$.

\begin{remark}[the equilibrium at $m=2$]\label{rem:equil}
An active-set quadratic program (and two independent codes) give the primal value $C_{z_2}\approx-1.3594016$, with
maximiser saturated ($\rho=1$) on $[0,0.5475]$, a free band up to $1.9525$, and $\lambda^*\approx-2.96317$; so the
certificate is within about $1.9\cdot10^{-4}$ of the optimum. The finite-$h$ values $h^{-2}\log|\Delta_h(T)|$, computed in
ball arithmetic, are $-1.4379$, $-1.4195$, $-1.4093$, $-1.4015$, $-1.3930$, $-1.3876$, $-1.3815$, $-1.3781$ at $h=16$,
$32$, $48$, $64$, $96$, $128$, $192$, $256$. They increase towards the constant from below; fits of the form
$a+b\log h/h\,(+c/h)$ give limits between $-1.373$ and $-1.364$, below $C_{z_2}$, so these data do not indicate that
Theorem~\ref{thm:B} is sharp. This costs nothing, since only the upper bound is used.
\end{remark}

\subsection{The shift lemma}\label{sec:shift}
A smaller $z$ only helps, and by a computable amount.

\begin{lemma}[shift lemma]\label{lem:shift}
Let $0<z'\le z\le\sqrt5-2$ and $L:=\log(z/z')\ge0$. For every admissible $\mu$ and every $\lambda\in\RR$,
\[
  \Phi_{z'}(\mu,\lambda-L)\le\Phi_z(\mu,\lambda)-\tfrac L2 .
\]
If $(\mu,\lambda)$ satisfies (i) of Theorem~\ref{thm:B} at $z$, then $(\mu,\lambda-L)$ satisfies (i) at $z'$; if
$(\mu,\lambda)$ satisfies (ii) at $z$ with $\ccell$, then $(\mu,\lambda-L)$ satisfies (ii) at $z'$ with
$\ccell+1.01L$.
\end{lemma}

\begin{proof}
Write $F_\mu$ and $F'_\mu$ for the functions at $z$ and $z'$. Since $v_{z'}(x)=v_z(x)-Lx$, we have $F'_\mu=F_\mu-Lx$ and
\[
  F'_\mu-(\lambda-L)=(F_\mu-\lambda)-L(x-1).
\]
With $a:=F_\mu(x)-\lambda$: on $[0,1]$, $(a+L(1-x))_+\le a_++L(1-x)$; on $[1,\infty)$, $(a-L(x-1))_+\le a_+$. Integrating,
$\int_0^\infty(F'_\mu-\lambda+L)_+\,dx\le\int_0^\infty(F_\mu-\lambda)_+\,dx+\frac L2$, so
$\Phi_{z'}(\mu,\lambda-L)\le-E(\mu)+\lambda-L+\int(F_\mu-\lambda)_++\frac L2=\Phi_z(\mu,\lambda)-\frac L2$. On $[4,\infty)$
the shift $-L(x-1)$ only lowers $F-\lambda$; on $[-1/100,0]$ it raises it by at most $L(1+1/100)$.
\end{proof}

\begin{corollary}\label{cor:shift}
For every $m\ge2$, the pair $(\mu_U,\lambda_U-L(m))$ satisfies the hypotheses of Theorem~\ref{thm:B} at $z=z_m$ with
$\ccell=5.38+1.01L(m)$, and
\[
  \Phi_{z_m}\bigl(\mu_U,\lambda_U-L(m)\bigr)\le\Phi_U-\tfrac12L(m),\qquad L(m):=\log\frac{m+\sqrt{m^2+1}}{2+\sqrt5}.
\]
In particular $\limsup_hh^{-2}\log|\Delta_h(\chi_2(z_m))|\le\Phi_U-\frac12L(m)$.
\end{corollary}

\begin{proof}
$1/z_m=m+\sqrt{m^2+1}$, so $L(m)=\log(z_2/z_m)\ge0$. Apply Lemma~\ref{lem:shift} to Theorem~\ref{thm:cert}.
\end{proof}

For $m=4$ the bound is $\Phi_U-\frac12L(4)=-1.6847547\ldots$, with $L(4)=0.651077\ldots$ (rounded up:
$-1.684754$). The proof of Theorem~\ref{thm:V} uses only
Corollary~\ref{cor:shift}, i.e.\ Theorem~\ref{thm:cert} and the shift lemma.

\subsection{Direct certificates at \texorpdfstring{$m=4$}{m = 4} and \texorpdfstring{$m=8$}{m = 8}}\label{sec:certV}
The program of Section~\ref{sec:cert}, with only $z$ changed, gives direct certificates at $z_4=\sqrt{17}-4$ and
$z_8=\sqrt{65}-8$ (Table~\ref{tab:certV}). They improve the analytic bound at these points but are not needed for
Theorem~\ref{thm:V}, because the margins from Corollary~\ref{cor:shift} are already negative there
(Table~\ref{tab:margins}).

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}rrcccc@{}}
\toprule
$m$ & $N$ & $-E(\mu)$ & $\lambda$ & $\int(F_\mu-\lambda)_+\le$ & certified $\Phi$\\
\midrule
4 & 200 & 1.36321476 & $-3.71770185$ & 0.63797 & $-1.71651998814$\\
4 & 800 & 1.36321826 & $-3.71810316$ & 0.63714 & $-1.71774955485$\\
4 & 1600 & 1.36321769 & $-3.71817249$ & 0.636999 & $-1.7179552750082241$\\
8 & 1600 & 1.43562390 & $-4.44201260$ & 0.934075 & $-2.0723141156759906$\\
\bottomrule
\end{tabular}
\caption{Direct certificates at $m=4$ and $m=8$ (upper endpoints of Arb balls). Not used in the proof of
Theorem~\ref{thm:V}.}\label{tab:certV}
\end{table}

Their side conditions hold: at $x=4$, $F_\mu-\lambda\le-2.987$ ($m=4$) and $-4.990$ ($m=8$), with slopes at most $-1.595$
and $-2.276$; on the cell, $F_\mu-\lambda\le6.14$ ($m=4$, $h\ge100$). An independent projected-gradient computation of
the primal problem gives $C_{z_4}\ge-1.7181612$ and $C_{z_8}\ge-2.0725380$, so the certificates are within about
$2.1\cdot10^{-4}$ and $2.3\cdot10^{-4}$ of the optimum.

% ===========================================================================
\section{Nonvanishing: Lemma P\texorpdfstring{$'$}{'}}\label{sec:nonvan}
% ===========================================================================

\subsection{Setting}
Let $\ell\ge7$ be a prime with $\ell\nmid m$, $h:=3\ell-1$ (even) and $K=3\ell$. The classes modulo $\ell$ are
$C_\gamma=\{\gamma,\gamma+\ell,\gamma+2\ell\}$, $\gamma<\ell$, all of size $3$. Since $|k-i|<3\ell<\ell^2$ there is a single
level, and $N(i)=v_\ell(D'(x_i))=2$ for every $i$. Let $\fl$ be a prime of $\cO_\KK$ above $\ell$, $v:=v_\fl$, and
$\zeta:=z^\ell\bmod\fl$. If $\ell$ splits or ramifies in $\KK$, the residue field is $\mathbb F_\ell$ and $\zeta=z$; if
$\ell$ is inert, $\zeta=\sigma(z)=-1/z$. Since $\ell\nmid2m$, the elements $z$, $y$, $1-y=2mz$, $1-z^{-2}=-2m/z$ and
$1-\zeta^{\pm2}$ are $\fl$-units. (For ramified $\ell$, $\ell\mid d_m$, so $z\equiv-m$, $z^2\equiv-1$ and
$1-z^{\pm2}\equiv2$.) For $m=2$: $\ell$ splits if $\ell\equiv\pm1\bmod5$ and is inert otherwise.

When $d_m$ is not squarefree, primes dividing the index $[\cO_\KK:\ZZ[\sqrt{d_m}]]$ (for example $\ell=13$ at $m=70$,
$d_{70}=4901=13^2\cdot29$) need no special care: every step below works with the prime $\fl$ of $\cO_\KK$ and valuations
in $\cO_\KK$, never with $\ZZ[\sqrt{d_m}]$.

\emph{Positions.} $x_{\gamma+r\ell}=x_\gamma+2r\ell$ with $x_\gamma=2\gamma-3\ell+1\in[-3\ell+1,-\ell-1]$: in each class the
pole with $r=0$ is large and negative ($|x|>\ell$), the pole with $r=1$ is small ($|x|<\ell$), and the pole with $r=2$ is
large and positive. For odd $t$ we have $\ell\mid t-x_k$ exactly for $k$ in one class $C_{\gamma(t)}$, and the odd $t\ge1$
with $\gamma(t)=\gamma$ form the progression $t=x_\gamma+\ell Y$, $Y\in\{3,5,7,\dots\}$. Put $t_\gamma:=x_\gamma+3\ell$.

\begin{lemma}[Lemma~P$'$]\label{lem:P}
Let $\ell\ge7$ be prime with $\ell\nmid m$, $h=3\ell-1$, and $c_j:=[X^j]\Delta_h$. Then $v_\ell(c_0)=-2K$ and
$v_\ell(c_j)\ge-2K+2j$ for all $j$. Hence $\Delta_h(a/b)\ne0$ for every $a/b\in\QQ$ with $v_\ell(b)\le1$.
\end{lemma}

\begin{proof}
\emph{1. Lemma B.} $\ell^{2K}\Delta_h(X)=(-1)^{K(K-1)/2}u_\ell\,\one^{\mathsf T}\adj(G^f(X))\one$ with
$u_\ell:=\ell^{2K}/\prod_iD'(x_i)$ an $\ell$-unit.

\emph{2. The $X$-part.} $B(f_if_j)=0$ for $i\ne j$, because $f_if_j/D$ is a polynomial, and $B(f_i^2)=-D'(x_i)z^{x_i}$, of
valuation exactly $2$. So $G^f(X)=G^f(0)+X\operatorname{diag}(d_i)$ with $v(d_i)=2$.

\emph{3. Integrality and block diagonality.} By the row claim \eqref{eq:rowclaim} with $N(i)-2\lev(\ell)=0$ (valid since
$\ell\nmid m$), $G^f(0)$ is $\fl$-integral. On each progression, $\cM$ restricted to $\gamma$ is
$z^{t_\gamma}\sum_c z^{2\ell c}F'(t_\gamma+2\ell c)=z^{t_\gamma}\sum_b\Delta^bG_\gamma(0)z^{2\ell b}/(1-z^{2\ell})^{b+1}$,
$G_\gamma(c):=F'(t_\gamma+2\ell c)$, with $1-z^{2\ell}\equiv1-\zeta^2$ a unit; so \eqref{eq:step3} holds progression by
progression. Off the diagonal, $F=\prod_{k\ne i,j}(t-x_k)$ has on the progression $\gamma$ exactly
$3-\ind{\gamma=c(i)}-\ind{\gamma=c(j)}$ factors divisible by $\ell$ ($c(i)$ is the class of $i$), and $F'$ keeps all but
one; so a unit is possible only if $c(i)=c(j)=\gamma$. On the diagonal, the polynomial part on a progression
$\gamma\ne c(i)$ has valuation at least $3-1=2$: the class $\gamma$ has three members, all after the initial segment of
the telescoping order, and the derivative loses at most one. Hence $G^f(0)\bmod\fl$ is block diagonal over the
classes, each block receiving only its own progression and its own pole terms.

\emph{4. The blocks.} Fix $\gamma$ with members $k_r=\gamma+r\ell$, put $W(t):=\prod_{k\notin C_\gamma}(t-x_k)$ and
$U_\gamma:=\prod_{k\notin C_\gamma}(x_\gamma-x_k)$, so $W(t)\equiv U_\gamma\bmod\ell$ on the progression. Off the diagonal
($r\ne s$, $q$ the third index) $F=W(t)(t-x_{k_q})$ and $F'\equiv W\equiv U_\gamma$. For the diagonal polynomial part,
$Q=W\cdot(t+x_{k_r}-x_{k_a}-x_{k_b})+p(x_{k_r})\,W[x_{k_r},t]$ with $\{a,b\}$ the other indices, $p(t)=(t-x_{k_a})(t-x_{k_b})$ and
$p(x_{k_r})\equiv0\bmod\ell^2$; so $Q'\equiv U_\gamma$ too. In the progression sum, $\Delta^0G_\gamma(0)\equiv U_\gamma$ and
$\Delta^bG_\gamma(0)\equiv0$ for $b\ge1$, so it is $\equiv U_\gamma z^{t_\gamma}/(1-z^{2\ell})\equiv U_\gamma z^{x_\gamma}\zeta^3/(1-\zeta^2)$.
The pole terms at $X=0$ are $D'(x)z^xP(x)$ with $\ell^2P(x_{k_r})\equiv\zeta,0,-\zeta^{-1}$ for $r=0,1,2$ (the only odd
multiples of $\ell$ below $|x|\le3\ell-1$ in absolute value are $\pm\ell$), $D'(x_{k_r})/\ell^2\equiv U_\gamma\cdot(8,-4,8)_r$,
and $z^{x_{k_r}}\equiv z^{x_\gamma}\zeta^{2r}$. Hence
\begin{gather*}
  G^f(0)|_{C_\gamma}\equiv e_\gamma M,\qquad e_\gamma:=U_\gamma z^{x_\gamma},\\
  M:=c\,\one\one^{\mathsf T}+\operatorname{diag}(8\zeta,0,-8\zeta^3),\qquad c:=\frac{\zeta^3}{1-\zeta^2}.
\end{gather*}

\emph{5. The bordered determinant.} For $M=\operatorname{diag}(d_0,0,d_2)+c\one\one^{\mathsf T}$ we have
$\det M=c\,d_0d_2=-64c\zeta^4$ and $\one^{\mathsf T}\adj(M)\one=d_0d_2=-64\zeta^4$, both units. For the block-diagonal
reduction,
\[
  \one^{\mathsf T}\adj\Bigl(\bigoplus_\gamma e_\gamma M\Bigr)\one=(\det M)^{\ell-1}\,\one^{\mathsf T}\adj(M)\one\,
  \Bigl(\prod_\gamma e_\gamma^3\Bigr)\sum_\gamma e_\gamma^{-1}.
\]
Modulo $\ell$, $U_\gamma\equiv\prod_{k\not\equiv\gamma}2(\gamma-k)\equiv2^{3(\ell-1)}((\ell-1)!)^3\equiv-1$ for every $\gamma$
(Fermat, Wilson). So $\sum_\gamma e_\gamma^{-1}\equiv-z^{3\ell-1}\sum_{\gamma<\ell}z^{-2\gamma}=-z^{3\ell-1}(1-z^{-2\ell})/(1-z^{-2})$, and
$1-z^{-2\ell}\equiv1-\zeta^{-2}$ and $1-z^{-2}=-2m/z$ are units. Hence $\one^{\mathsf T}\adj(G^f(0))\one$ is an $\fl$-unit, and
$v_\ell(c_0)=-2K$ by step~1.

\emph{6. The gap.} $[X^j]\one^{\mathsf T}\adj(G^f(X))\one$ is a sum of products containing $j$ factors $d_i$, so it has
valuation $\ge2j$. If $v_\ell(b)\le1$, the $j$-th term of $\Delta_h(a/b)$ has valuation $\ge-2K+2j-j>-2K$ for $j\ge1$.
\end{proof}

The only place where $m$ enters is the list of units in the setting, and they are units exactly when $\ell\nmid2m$. So
every prime $\ell\ge7$ with $\ell\nmid m$ works, whether it splits, is inert or ramifies. In \cite{Chi2Paper} the partial
sums reach past $3\ell$ and the block constants are fixed rationals that must avoid $\ell$, so finitely many primes are
excluded; here only $n=\pm\ell$ enters. At $m=2$, steps~4--5 were checked entrywise modulo $\ell$ for $\ell=7,11,\dots,41$
(split and inert), and the conclusion on the exact $\Delta_h$ for $\ell=7,\dots,29$. For other $m$ the conclusion
($v_\ell(c_0)=-2K$ and the gap) was checked on the exact $\Delta_h$ at $m=4$ ($\ell=7,11,13,17,19$; $\ell=17$ ramified),
$m=6$ ($\ell=7,11,13$), and, by an independent implementation, at $m=3,7,9,11,12,13,18,21$ (17 cases, among them three
ramified $\ell$: $\ell=17$ at $m=13$, $\ell=13$ at $m=21$, and $\ell=13$ at $m=18$, where $d_{18}=325=5^2\cdot13$). As a
control, at $m=7$, $\ell=7$ (so $\ell\mid m$) the conclusion fails: $v_\ell(c_0)+2K=-67$.

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

\subsection{The proof}
Fix $m\ge2$ with $m\notin\cE$, let $\nu=1+v_2(m)$, and suppose that $T=\chi_2(z_m)=a/b$ with $a\in\ZZ$, $b\ge1$. Let
\[
  \mathcal H:=\{3\ell-1:\ \ell\ge37\text{ prime},\ \ell\nmid m,\ \ell^2\nmid b\},
\]
an infinite set of even integers $h\ge110$. For $h\in\mathcal H$, Lemma~\ref{lem:P} gives $\Delta_h\not\equiv0$ and
$F_h(a/b)\ne0$, where $F_h\in\ZZ[X]$ is the primitive polynomial of Section~\ref{sec:construction}, of degree $\le h$. We
have $\log|F_h(T)|=\log|\Delta_h(T)|+\sum_pn_p\log p$, and along $\mathcal H$:
\begin{itemize}
\item odd primes $p\nmid m$: $\limsup h^{-2}\sum n_p\log p\le\frac43$ (Theorem~\ref{thm:A});
\item odd primes $p\mid m$, $e=v_p(m)$: $\limsup h^{-2}n_p\log p\le c_p(e)$ (Lemma~\ref{lem:S});
\item $p=2$: $\limsup h^{-2}n_2\log2\le c_2(\nu)$ (Proposition~\ref{prop:ntwo});
\item size: $\limsup h^{-2}\log|\Delta_h(T)|\le\Phi_U-\frac12L(m)$ (Corollary~\ref{cor:shift}).
\end{itemize}
So $\limsup_{h\in\mathcal H}h^{-2}\log|F_h(T)|\le M(m)$, with $M(m)$ as in \eqref{eq:budget}, and $M(m)<0$ by
Proposition~\ref{prop:margins} below. This contradicts Proposition~\ref{prop:criterion}. \qed

\emph{Proof of Corollary~\ref{thm:U}.} At $m=2$, $\nu=2$, there are no odd primes dividing $m$, $L(2)=0$, and
$n_2=O(h\log h)$ by Lemma~\ref{lem:ten}. So $M(2)=\Phi_U+\frac43=-0.0258828\ldots<0$, and
$T=\chi_2(\sqrt5-2)$ is irrational; so is $24T=\pi^2-18\log^2\varphi$ by \eqref{eq:closedform}. \qed

\subsection{The margins}\label{sec:margins}
Table~\ref{tab:margins} lists $M(m)$ for some $m$. The entries are computed in Arb and rounded to the digits shown;
in the rows $m\notin\cE$ the last two columns are rounded up, so they are upper bounds.

\begin{table}[ht]
\centering\footnotesize
\setlength{\tabcolsep}{4pt}
\begin{tabular}{@{}rrrlrrr@{}}
\toprule
$m$ & $\nu$ & $c_2(\nu)$ & odd $p\mid m$: $\sum c_p(e)$ & arithmetic & $\Phi_U-\frac12L(m)$ & $M(m)$\\
\midrule
2 & 2 & 0 & --- & 1.333333 & $-1.359216$ & $-0.025882$\\
4 & 3 & 0.173287 & --- & 1.506620 & $-1.684754$ & $-0.178134$\\
6 & 2 & 0 & $3$: 0.411980 & 1.745313 & $-1.883288$ & $-0.137975$\\
8 & 4 & 0.346574 & --- & 1.679907 & $-2.025634$ & $-0.345727$\\
10 & 2 & 0 & $5$: 0.502949 & 1.836283 & $-2.136509$ & $-0.300227$\\
11 & 1 & 0.173287 & $11$: 0.659421 & 2.166041 & $-2.183949$ & $-0.017908$\\
12 & 3 & 0.173287 & $3$: 0.411980 & 1.918600 & $-2.227291$ & $-0.308691$\\
13 & 1 & 0.173287 & $13$: 0.694674 & 2.201294 & $-2.267184$ & $-0.065890$\\
16 & 5 & 0.519860 & --- & 1.853194 & $-2.370753$ & $-0.517560$\\
21 & 1 & 0.173287 & $3,7$: 0.979537 & 2.486157 & $-2.506516$ & $-0.020359$\\
\midrule
3 & 1 & 0.173287 & $3$: 0.411980 & & & $+0.3720$\\
5 & 1 & 0.173287 & $5$: 0.502949 & & & $+0.2160$\\
7 & 1 & 0.173287 & $7$: 0.567557 & & & $+0.1147$\\
9 & 1 & 0.173287 & $3$ ($e=2$): 0.686633 & & & $+0.1091$\\
15 & 1 & 0.173287 & $3,5$: 0.914929 & & & $+0.0830$\\
\bottomrule
\end{tabular}
\caption{Limit margins $M(m)$ per $h^2$ (in the rows above the line, upper bounds; the analytic column uses only
Corollary~\ref{cor:shift}). The rows below the line are the exceptional set $\cE$, where $M(m)$ is positive. The direct certificates of
Table~\ref{tab:certV} improve the rows $m=4$ and $m=8$ to $M(4)\le-0.211335$ and $M(8)\le-0.392407$.}\label{tab:margins}
\end{table}

\begin{proposition}\label{prop:margins}
$M(m)<0$ for every integer $m\ge2$ with $m\notin\cE$, and $M(m)>0$ for $m\in\cE\cup\{1\}$.
\end{proposition}

\begin{proof}
Write $m=2^aq$ with $q$ odd. Since $m+\sqrt{m^2+1}>2m$, $L(m)>\log(2m)-\log(2+\sqrt5)$. For odd $p$,
$1/(4(p-1))\le1/8$, so $\sum_{p^e\parallel q}c_p(e)\le\frac14\log q+\sum_{p\mid q}\frac{\log p}{4(p-1)}\le\frac38\log q$.

If $a\ge1$, then $\nu=a+1\ge2$ and $c_2(\nu)=(a-1)\frac{\log2}4$, so
\begin{align*}
  M(m)&<\Bigl[\Phi_U+\tfrac43+\tfrac12\log(2+\sqrt5)-\tfrac34\log2\Bigr]-\tfrac a4\log2-\tfrac18\log q\\
  &=0.176075\ldots-0.173287\ldots\,a-\tfrac18\log q .
\end{align*}
This is negative unless $a=1$ and $q=1$, i.e.\ $m=2$, where $M(2)=\Phi_U+\frac43=-0.0258828\ldots<0$ (proof of
Corollary~\ref{thm:U} above).

If $a=0$, then $\nu=1$ and $c_2(1)=\frac{\log2}4$, so
\begin{align*}
  M(m)&<\Bigl[\Phi_U+\tfrac43+\tfrac12\log(2+\sqrt5)-\tfrac14\log2\Bigr]-\tfrac14\log q+\sum_{p\mid q}\frac{\log p}{4(p-1)}\\
  &\le0.522648\ldots-\tfrac18\log q,
\end{align*}
which is negative for $q>e^{8\cdot0.522648\ldots}=65.443\ldots$. For the odd $m\le65$ we evaluate $M(m)$ in Arb, with the
exact $L(m)$; for $3\le m\le65$ it is negative except for $m\in\cE$, where the enclosures are positive, between
$+0.083$ ($m=15$) and $+0.372$ ($m=3$) (Table~\ref{tab:margins}). For $m=1$, $L(1)<0$ and the right side of
\eqref{eq:budget} is $M(1)=0.42853\ldots$ (Arb; also found by the independent computation mentioned below). For $m=1$
this number is only the value of the formula: Corollary~\ref{cor:shift} needs $m\ge2$.
\end{proof}

So every $m>65$ is covered by the closed form, the odd $m\le65$ by the table, and the set of $m\ge2$ for which the
method as written concludes is exactly $\{m\ge2\}\setminus\cE$. An independent computation in mpmath interval arithmetic
(shift lemma only, no shared code) found $M(m)\ge0$ exactly for $m\in\{1,3,5,7,9,15\}$ among $1\le m\le3000$, and agreed
with the table to all printed digits for $m\le60$. The tightest margins, $m=11$ and $m=21$, depend on the digits of
$\Phi_U$ only at the level $10^{-2}$.

\emph{The excluded values.} For $m\in\cE$ the method does not conclude, although the exact finite-$h$ scores there are
negative at $h\le48$ (Table~\ref{tab:evidenceV}). They rise with $h$ (for $m=3$: $-0.1326$, $-0.0734$, $-0.0340$ at
$h=32,48,64$) and are not evidence for these $m$. For $m=1$ the margin is positive and so are the finite-$h$ scores:
$+0.0595$, $+0.2144$, $+0.2524$, $+0.2876$ at $h=16,32,48,64$. So $\chi_2(\sqrt2-1)=\pi^2/16-\frac14\log^2(1+\sqrt2)$ is out
of reach of this method.

\begin{remark}[towards $\cE$]\label{rem:closeE}
The following is not proved. The data after Lemma~\ref{lem:S} suggest that the term $\frac1{4(p-1)}\log p$ in $c_p(e)$
can be removed by a plateau bound of the quality of Lemma~\ref{lem:nine} at special primes. That would bring $m=9$ and
$m=15$ into Theorem~\ref{thm:V}. For $\nu=1$ the exact $2$-adic shares (for example $0.112$ at $h=64$, against the
limit bound $0.173$) suggest that $c_2(1)<\frac14\log2$; with direct certificates this might reach $m=7$. The values
$m=3$ and $m=5$ look out of reach of this machine.
\end{remark}

\subsection{Effectivity}

\begin{remark}[effectivity at $m=2$]\label{rem:effective}
Every bound above is explicit at finite $h$ except the prime number theorem in Theorem~\ref{thm:A}. At a single $h$ one
can instead evaluate the proved finite-$h$ bound
\[
  \log|F_h(T)|\le h^2\Phi+E_{\mathrm{an}}(h)+B_{\mathrm{odd}}(h)+h(\lfloor\log_2h\rfloor+3)\log2,
\]
where $B_{\mathrm{odd}}(h)=\sum_{3\le p<K/3}(2h\lev(p)+v_p(h!))\log p+\sum_{K/3\le p<K}\min(2h+v_p(h!),3(K-p))\log p$ is an
exact finite sum. At $m=2$, in exact arithmetic, this bound is negative at every even $h$ with $2432\le h\le40000$, and at
every sampled $h$ up to $8.75\cdot10^5$, with $|\text{bound}|/h^2$ increasing towards $0.0259$. A proof that it stays
negative for all larger $h$ would need explicit error terms in the prime number theorem, which we have not carried out.
As an effective consequence, if $\chi_2(\sqrt5-2)=a/b$ with $\log b\le800$, a single $h=3\ell-1\le36000$ with $\ell\nmid b$
gives a contradiction. The exact scores $h^{-2}\log|F_h(T)|$ are much better than this bound, for example $-0.066$ at
$h=192$ (Table~\ref{tab:evidence}).
\end{remark}

\begin{remark}[effectivity at $m=4$]
The same finite-$h$ bound at $m=4$, with the direct certificate of Table~\ref{tab:certV}, Proposition~\ref{prop:ntwo} at $\nu=3$
and Lemmas~\ref{lem:eight}, \ref{lem:classcount}, \ref{lem:nine}, is negative at every even $h$ with $178\le h\le40000$
and at every sampled $h$ up to $6\cdot10^5$; the last nonnegative value is at $h=176$. For example it is $-0.0749h^2$ at
$h=242$ and $-0.1648h^2$ at $h=1004$. So if $\chi_2(\sqrt{17}-4)=a/b$, a single $h=3\ell-1$ with $\ell\nmid b$ and
$h\ge242$, of size about $5\log b+300$, gives a contradiction. This uses the direct certificate, which the proof of
Theorem~\ref{thm:V} does not need.
\end{remark}

% ===========================================================================
\section{Extensions: the other units of norm \texorpdfstring{$-1$}{-1}, and the inverse tangent integral}\label{sec:ext}
% ===========================================================================
% Sources: pilot_za/PROOF_VODD.md (Sections 0-4, change log) and pilot_w3/PROOF_TI2.md (Sections 0-8, change log).
% Every number below was recomputed in ext_checks/ (ext_numbers.py, side_conditions.py, karamata_check.py, and a
% re-run of the ten load-bearing certificates with a verbatim copy of cert_za.py).

Both extensions are deltas to the proof of Theorem~\ref{thm:V}: every lemma of
Sections~\ref{sec:construction}--\ref{sec:nonvan} not named below holds verbatim, with the data indicated. We extend the
notation $c_2(\nu):=|\nu-2|\frac{\log2}4$ to $\nu=0$, so $c_2(0)=\frac12\log2$.

\subsection{Odd \texorpdfstring{$a$}{a}: Theorem V\texorpdfstring{$_{\mathrm{odd}}$}{\_odd}}\label{sec:odd-a}
\emph{Data.} Let $a\ge1$ be odd, $d:=a^2+4$, $\KK:=\QQ(\sqrt d)$ and $z:=\alpha_a=(\sqrt d-a)/2$. Then
\[
  z^2+az-1=0,\qquad\sigma(z)=-1/z,\qquad y:=z^2,\qquad 1-y=az .
\]
Here $z\in\cO_\KK$ but $z\notin\ZZ[\sqrt d]$; as in Section~\ref{sec:nonvan}, every valuation is taken in $\cO_\KK$. Since
$d\equiv5\bmod8$, writing $d=f^2d_0$ with $d_0$ squarefree gives $f$ odd and $d_0\equiv5\bmod8$, so \emph{$2$ is inert in
$\KK$}. Since $\gcd(a,a^2+4)=1$, at every odd prime $p\nmid a$ (including the primes dividing $d$) the elements $z$, $y$,
$1-y$ are units, and at an odd prime $p\mid a$ we have $v_p(1-y)=v_p(a)$. At the prime above $2$, $z$ and $1-y=az$ are
units: $\nu=0$.

\emph{What holds verbatim} (with $2m$ replaced by $a$): Lemma~\ref{lem:pole}, Lemma~\ref{lem:R} and
Corollary~\ref{cor:R} (they use only $\sigma(z)=-1/z$), so $\Delta_h\in\QQ[X]$; Lemmas~\ref{lem:atom}--\ref{lem:nine}
and Theorem~\ref{thm:A} at odd $p\nmid a$; Lemma~\ref{lem:S} at odd $p\mid a$ with $e:=v_p(a)$ (its proof uses only
$v_p(1-y)=e$); Theorem~\ref{thm:B} and the shift lemma, since $\alpha_a\le\alpha_5=0.1925\ldots<\sqrt5-2$ for $a\ge5$,
with
\[
  L(a):=\log\frac{\sqrt5-2}{\alpha_a}=\log\frac{a+\sqrt{a^2+4}}{4+\sqrt{20}},
\]
so that $\Phi\le\Phi_U-\frac12L(a)$ at $z=\alpha_a$, with $\ccell=5.38+1.01L(a)$; and Lemma~\ref{lem:P} for primes
$\ell\ge7$ with $\ell\nmid a$. In the setting of Lemma~\ref{lem:P} the units are now $1-y=az$ and $1-z^{-2}=-a/z$, which
are $\fl$-units if and only if $\ell\nmid a$; for $\ell\mid d$ we have $\sqrt d\equiv0$, $z\equiv-a/2$, $z^2\equiv-1$
and $1-z^{\pm2}\equiv2$ modulo $\fl$, also at the primes dividing the index of $\ZZ[\sqrt d]$ (for example $a=29$,
$\ell=13$, $d=5\cdot13^2$). The only new ingredient is the prime $2$ at $\nu=0$.

\begin{lemma}[Lemma~$10_0$]\label{lem:tenzero}
Let $a$ be odd, $\fP$ the prime of $\KK$ above $2$ and $v:=v_\fP$ with $v(2)=1$. In the notation of
Section~\ref{sec:two} (rescaling, anchored basis, $G_{ij}=\tilde\Lambda_X(a_ib_j)$), for $i,j<h$:
\begin{enumerate}
\item[(L)] if $\pi=i+j-K\ge1$, then $v(G_{ij})\ge1-\pi$; if $\pi=0$, then $G_{ij}=0$;
\item[(U)] if $N_0=K-1-i-j\ge1$, then $v(G_{ij})\ge2-N_0+s_2(N_0)$; if $N_0=0$, then $v(G_{ij})=2$.
\end{enumerate}
Consequently $n_2\le h^2/2+h$ for every even $h$, so the prime $2$ costs at most $c_2(0)=\frac12\log2$ per $h^2$.
\end{lemma}

\begin{proof}
The rescaling $\Delta_h=2^{-3h}\tilde\Delta_h$ and the anchored basis do not involve $z$. Since $2$ is inert, $v$ is
integer-valued and restricts to $v_2$ on $\QQ$, so $n_2=-v_2(\Delta_h)=3h-v(\tilde\Delta_h)$ for the rational polynomial
$\Delta_h$. In the proof of Lemma~\ref{lem:tennu} the quantity $\nu$ enters only through $v(y^b/(1-y)^{b+1})=-\nu(b+1)$
in (L) and $v(\eta)=\nu$ for $\eta=y-1$ in (U). The other inputs are independent of $z$ and of $\nu$: the Newton
coefficients of $s\mapsto(2s+1)^c$ have valuation $\ge2b-s_2(b)$; $S(\zeta)$ has odd denominators and powers of the
unit $z$, so $v(S(\zeta))\ge0$; the Newton coefficients $\gamma_r$ of $g$ (called $\gamma_a$ there) satisfy
$v_2(\gamma_r)\ge2r-s_2(r)$; and $v_2(N_0!)=N_0-s_2(N_0)$. Here $y$ and $1-y=az$ are
$2$-adic units, so the proof applies with $\nu=0$ (it never used $\nu\ge1$), and the bounds of Lemma~\ref{lem:tennu} at
$\nu=0$ read: in (L), $1-\pi+\min_{b<\pi}(2b-s_2(b))=1-\pi$ (at $b=0$); in (U),
$\min\{2-N_0+s_2(N_0),\ 2-N_0+s_2(N_0)+\min_{r<N_0}(2r-s_2(r))\}=2-N_0+s_2(N_0)$. The cases $\pi=0$ and $N_0=0$ are as
there.

\emph{The content.} Put $g(s):=\min(s-K+3,\,K+1-s)$, a concave function. Then $v(G_{ij})\ge g(i+j)$ for all $i,j<h$: for
$s=i+j\le K-2$, (U) gives at least $2-N_0+1=s-K+4>g(s)$ (as $s_2(N_0)\ge1$); for $s=K-1$ the valuation is $2=g(s)$; for
$s=K$ the entry is $0$; for $s\ge K+1$, (L) gives $K+1-s=g(s)$. For a permutation $\sigma$ of $\{0,\dots,h-1\}$ the vector
$(i+\sigma(i))_i$ is majorised by $(2i)_i$ (proof of Proposition~\ref{prop:ntwo}), so Karamata's inequality gives
$\sum_ig(i+\sigma(i))\ge\sum_ig(2i)$. With $K=h+1$, $g(2i)=2i-h+2$ for $2i\le h$ and $g(2i)=h+2-2i$ for $2i\ge h+2$, so
\[
  \sum_{i<h}g(2i)=\bigl(\tfrac h2+1\bigr)\bigl(2-\tfrac h2\bigr)+\bigl(\tfrac h2-1\bigr)\bigl(2-\tfrac h2\bigr)=2h-\tfrac{h^2}2 .
\]
By the Leibniz expansion $v(\tilde\Delta_h)\ge2h-h^2/2$, hence $n_2\le h^2/2+h$.
\end{proof}

The minorant is a tent around $s=K$, with slopes $+1$ and $-1$, instead of the monotone $\hat g$ of
Proposition~\ref{prop:ntwo}; diagonal rescalings cannot improve a Leibniz bound of this kind. With $c_2(0)=\frac12\log2$
the formula $c_2(\nu)=|\nu-2|\frac{\log2}4$ of Proposition~\ref{prop:ntwo} holds for every $\nu\ge0$.

\emph{Checks.} The bounds (L), (U) were checked on the exact Gram matrices at $a=1,3,5,11$ for $h=8,16,24,32$, and by an
independent implementation at $a\in\{1,3,5,11,59,135,165\}$ for $h\in\{8,16,\dots,48\}$, with no violation and with
equality attained in both. The exact $n_2$ depends only on $\nu$: for every odd $a$ tested, $n_2=104,352,737,1248$ at
$h=16,32,48,64$, against the bound $144,544,1200,2112$. The share $n_2\log2/h^2$ falls from $0.282$ to $0.211$ over
this range, and to $0.195$ at $h=128$ (a proved lower bound for $n_2$); a three-term fit suggests the limit
$\frac14\log2$, half the proved constant. We have not proved this. Lemma~\ref{lem:S} and Lemma~\ref{lem:P} were checked
on exact data at odd $a$ (for example $a=3,9,15,21$ for Lemma~\ref{lem:S}, and Lemma~\ref{lem:P} at $a=1,3,5,7,9,11,29,59,135$,
including ramified $\ell$ and the index prime $\ell=13$ at $a=29$), with no violation; at $a=7$, $\ell=7$ (so $\ell\mid a$)
Lemma~\ref{lem:P} fails, as it must. For $p\ge K$ dividing $a$ (for example $p=59$ at $a=59$) the exact values are
$n_p=(h-2)^2/4$, so the term $e(h-2)^2/4$ of Lemma~\ref{lem:S} is attained.

\emph{The margins.} The proof of Section~\ref{sec:proof}, with $\mathcal H:=\{3\ell-1:\ell\ge37\text{ prime},\ \ell\nmid
a,\ \ell^2\nmid b\}$, Lemma~\ref{lem:tenzero} at $p=2$ and $\Phi(a)$ an admissible analytic bound at $z=\alpha_a$, gives
\begin{equation}\label{eq:Modd}
  \limsup_{h\in\mathcal H}\frac1{h^2}\log|F_h(T)|\le M_{\mathrm{odd}}(a):=\Phi(a)+\tfrac43+\tfrac12\log2
  +\sum_{p^e\parallel a}c_p(e),
\end{equation}
where $\Phi(a)$ is either $\Phi_U-\frac12L(a)$ (shift lemma) or the value of a direct certificate at $\alpha_a$.

\begin{proposition}\label{prop:marginsodd}
For odd $a\ge5$, with the shift lemma and the ten certificates of Table~\ref{tab:certodd}, $M_{\mathrm{odd}}(a)<0$ if and
only if $a\notin\cE_{\mathrm{odd}}$.
\end{proposition}

\begin{proof}
Since $a+\sqrt{a^2+4}>2a$, $-\frac12L(a)<-\frac12\log2-\frac12\log a+\frac12\log(4+\sqrt{20})$, and $c_2(0)=\frac12\log2$
cancels the $-\frac12\log2$. For odd $p$, $\frac1{4(p-1)}\le\frac18\le\frac e8$, so $\sum_{p^e\parallel a}c_p(e)\le
\frac38\log a$. Hence
\[
  M_{\mathrm{odd}}(a)<C_0-\tfrac18\log a,\quad C_0:=\Phi_U+\tfrac43+\tfrac12\log(4+\sqrt{20})=1.0425084777\ldots,
\]
which is negative for $a>e^{8C_0}=4188.3737\ldots$. For the odd $a$ with $5\le a\le5001$ we evaluate $M_{\mathrm{odd}}(a)$
in Arb at $200$ bits. With the shift lemma alone there are $49$ values with $M_{\mathrm{odd}}(a)\ge0$, the largest $195$.
Ten of them have negative margins with the certificates of Table~\ref{tab:certodd}; the remaining $39$ are
$\cE_{\mathrm{odd}}$, where the margins are positive, also with the further certificates we computed there (for
example $+0.0088$ at $a=165$ and $+0.4580$ at $a=11$, where $\alpha_{11}=\varphi^{-5}$, both with a direct certificate).
\end{proof}

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}rcccc@{}}
\toprule
$a$ & $M_{\mathrm{odd}}(a)$, shift lemma & certified $\Phi(a)\le$ & $M_{\mathrm{odd}}(a)\le$ & $\ccell\le$\\
\midrule
59 & $+0.0406$ & $-2.730260$ & $-0.013393$ & $8.21$\\
61 & $+0.0318$ & $-2.746986$ & $-0.022232$ & $8.24$\\
67 & $+0.0072$ & $-2.794044$ & $-0.047037$ & $8.34$\\
91 & $+0.0492$ & $-2.947508$ & $-0.005370$ & $8.65$\\
95 & $+0.0455$ & $-2.969059$ & $-0.009198$ & $8.69$\\
111 & $+0.0275$ & $-3.047021$ & $-0.027329$ & $8.85$\\
117 & $+0.0427$ & $-3.073383$ & $-0.012169$ & $8.90$\\
135 & $+0.0541$ & $-3.145029$ & $-0.000887$ & $9.05$\\
147 & $+0.0133$ & $-3.187657$ & $-0.041735$ & $9.13$\\
195 & $+0.0156$ & $-3.329068$ & $-0.039558$ & $9.42$\\
\bottomrule
\end{tabular}
\caption{The ten certificates on which Theorem~\ref{thm:Vodd} depends ($N=1600$, $r=32$; upper endpoints of Arb
balls, rounded up). The second column is the margin with the shift lemma alone, rounded; it is positive, so these $a$
need their certificate. The last column is the cell constant of Theorem~\ref{thm:B}(ii) for $h\ge100$.}\label{tab:certodd}
\end{table}

\emph{The certificates.} They are produced by the program of Section~\ref{sec:cert} with only $z$ changed to $\alpha_a$;
at $a=4$ it reproduces the value $\Phi_U$ of Theorem~\ref{thm:cert} bit for bit. For this paper all ten were re-run, and
they reproduced the stored upper endpoints bit for bit; the AI referee of Theorem~\ref{thm:Vodd} had re-run four of them
($a=59,91,135,195$) with the same result, and an independent floating-point primal computation lies below every
certified value, by about $2.7\cdot10^{-4}$. The side conditions of Theorem~\ref{thm:B} hold for each of the ten: at
$x=4$, $F_\mu-\lambda\le-8.87$ (required: $-1.13$), the slope of the tail bound is at most $-3.57$ (required: $-0.94$),
and on $[-1/h,0]$, $h\ge100$, $F_\mu-\lambda\le2\log(2+1/h)+1+|\log z|/h-\lambda\le\ccell$ with $\ccell$ as in
Table~\ref{tab:certodd}; $\ccell$ enters only the $O(h)$ term $E_{\mathrm{an}}(h)$. The other covered $a$ need only
the shift lemma, for instance $M_{\mathrm{odd}}(101)\le-0.099782$. The margins at $a=135$ and $a=91$ are rigorous but thin,
so the effective $h_0$ there is large; $a=123$ has $M_{\mathrm{odd}}(123)\le-0.000034$ with the shift lemma alone. (The
formal proof uses a weaker constant in place of $\Phi_U$ and therefore needs a direct certificate at $a=123$ too;
Section~\ref{sec:lean}.)

\begin{proof}[Proof of Theorem~\ref{thm:Vodd}]
Let $a\ge5$ be odd with $a\notin\cE_{\mathrm{odd}}$, and suppose $T=\chi_2(\alpha_a)=a'/b$. For $h\in\mathcal H$,
Lemma~\ref{lem:P} with $\ell\nmid a$ gives $F_h(a'/b)\ne0$. Along $\mathcal H$ the odd primes $p\nmid a$ contribute at
most $\frac43$ (Theorem~\ref{thm:A}), the odd $p\mid a$ at most $c_p(v_p(a))$ (Lemma~\ref{lem:S}), the prime $2$ at most
$\frac12\log2$ (Lemma~\ref{lem:tenzero}), and the size at most $\Phi(a)$ (Theorem~\ref{thm:B} with the shift lemma, or
with the certificate of Table~\ref{tab:certodd}). So the $\limsup$ is at most $M_{\mathrm{odd}}(a)<0$
(Proposition~\ref{prop:marginsodd}), contradicting Proposition~\ref{prop:criterion}.
\end{proof}

\begin{remark}
The cases $a=1$ ($\varphi^{-1}$) and $a=3$ are not covered: there $\alpha_a>\sqrt5-2$, so the shift lemma does not apply,
and numerically the margins are positive. Two improvements, neither proved, are suggested by the data: the $2$-adic
constant $c_2(0)=\frac14\log2$, and the removal of the term $\frac1{4(p-1)}\log p$ from $c_p(e)$ (cf.\
Remark~\ref{rem:closeE}); for the latter the bound $n_p\le2h\lev(p)+v_p(h!)+e(h-2)^2/4$ at special primes held in every
one of $39$ exact data points. Each would shrink $\cE_{\mathrm{odd}}$; $a=11$ ($\varphi^{-5}$) seems out of reach of this
machine even with both.
\end{remark}

\subsection{The inverse tangent integral: Theorem V\texorpdfstring{$_i$}{\_i}}\label{sec:Ti2}
\emph{Data.} Let $n\ge3$, $\KK:=\QQ(\sqrt{n^2-4})$, $\beta:=\beta_n=(n-\sqrt{n^2-4})/2$ and $u_n:=1/\beta_n=(n+\sqrt{n^2-4})/2$.
Then $\beta^2-n\beta+1=0$ and $\sigma(\beta)=1/\beta$, so $\beta$ is a unit of norm $+1$; $\beta_{2m}=m-\sqrt{m^2-1}$. Let
$\chi_4$ be the nontrivial character modulo $4$, so that $\Ti_2(x)=\sum_{t\text{ odd}\ge1}\chi_4(t)x^t/t^2$, and define the
$\chi_4$-twisted machine with the poles and atoms of Section~\ref{sec:data}:
\[
  \cM^\natural(f):=\sum_{t\text{ odd}\ge1}\chi_4(t)\beta^tf'(t),\qquad\Lambda^\natural(g):=\cM^\natural(g/D),\qquad
  T^\natural:=\Ti_2(\beta).
\]
Put $w:=i\beta$, $\cF:=\KK(i)$, and let $\cM_w$, $\Lambda_w$, $A_w$, $B_w$, $P_w$, $\Delta_{h,w}$ be the objects of
Section~\ref{sec:construction} with $z$ replaced by $w$ (the series converge absolutely since $|w|=\beta<1$, and
Lemma~\ref{lem:pole} holds at $w$ with the same proof, with $T$ replaced by $\chi_2(w)$). Then
\[
  y:=w^2=-\beta^2,\qquad 1-y=1+\beta^2=n\beta .
\]
This is the only change of data: in Theorem~\ref{thm:V}, $1-y=2mz$.

\begin{lemma}[the identity]\label{lem:identity}
For every rational function $f$ in the span of Section~\ref{sec:construction}, $\cM^\natural(f)=-i\,\cM_w(f)$. Hence
$\Lambda^\natural=A^\natural+T^\natural B^\natural$ with $A^\natural:=-iA_w$ and $B^\natural:=B_w$, both with values in
$\KK$, and
\[
  \Delta^\natural_h(X):=\det\bigl(A^\natural(t^{i+j})+XB^\natural(t^{i+j})\bigr)_{i,j<h}=(-i)^h\,\Delta_{h,w}(iX)\in\QQ[X].
\]
\end{lemma}

\begin{proof}
For odd $t$, $\chi_4(t)=i^{t-1}=-i\cdot i^t$, so $\chi_4(t)\beta^t=-i\,w^t$, which gives the first claim. Also
$\chi_2(w)=\sum_{t\text{ odd}}i^t\beta^t/t^2=i\,\Ti_2(\beta)$, so $-i\Lambda_w=-iA_w+\Ti_2(\beta)B_w$. For even $x$,
$w^x=(-1)^{x/2}\beta^x\in\KK$; so $B_w$ takes values in $\KK$, and so does $A^\natural$: by the computation of
Lemma~\ref{lem:pole} applied to $\cM^\natural$ directly (using $\chi_4(n+x)=i^x\chi_4(n)$ for even $x$), its pole part
consists of $(-1)^{x/2}\beta^x$ times partial sums $\sum\chi_4(n)\beta^n/n^2$, and its polynomial part
$\sum_{t\text{ odd}}\chi_4(t)\beta^tR'(t)$ is a rational function of $\beta$ with rational coefficients. The determinant
identity follows from $A^\natural+XB^\natural=-i(A_w+iXB_w)$.

\emph{Reflection.} Extend $\sigma$ to $\cF$ by $\sigma(i)=i$. Then $\sigma(w)=i/\beta=-1/w$. The proofs of
Lemma~\ref{lem:R} and Corollary~\ref{cor:R} use only $\sigma(z)=-1/z$ and that the coefficients are rational functions of
$z$ with rational coefficients (they are algebraic identities, so $|\sigma(w)|>1$ is irrelevant). Hence
$\Delta_{h,w}\in\cF^\sigma[X]=\QQ(i)[X]$, so $\Delta^\natural_h\in\QQ(i)[X]$. Its coefficients also lie in $\KK$, and
$\KK\cap\QQ(i)=\QQ$.
\end{proof}

\begin{remark}[the sign rule]\label{rem:signrule}
More generally, for weight $k$, atoms carrying a periodic character $\chi$ with parity $s_\chi:=\chi(-t)/\chi(t)$, and a
unit $z$ of norm $N(z)$, the analogue of Lemma~\ref{lem:R} reads $\sigma(a(f))=\eta\,a(\tilde f)$,
$\sigma(b(f))=-b(\tilde f)$ with $\eta:=N(z)\,s_\chi(-1)^k$, and the Hankel determinant polynomial lies in $\QQ[X]$ when
$\eta=-1$; when $\eta=+1$ it has the form $G(\sqrt d\,X)$ with $G\in\QQ[Y]$ and the method proves only $T\notin\sqrt d\,\QQ$.
(Sketch: for the polynomial part, $S_r(q):=\sum_{t\ge1}\chi(t)q^tt^r$ is rational and $S_r(1/q)=-s_\chi(-1)^rS_r(q)$; for
the pole part substitute $n\mapsto-n$ in the partial sums.) Theorem~\ref{thm:V} has $(N,s_\chi,k)=(-1,+1,2)$ and
Theorem~\ref{thm:Vi} has $(+1,-1,2)$, both with $\eta=-1$; for the latter Lemma~\ref{lem:identity} gives a complete
proof, and only that case is used. The general rule was checked exactly in $64$ cases ($k\le4$, two characters, eight
units, $h=6$), and in $8$ more for a variant with even atoms.
\end{remark}

\emph{Valuations.} The coefficients of $\Delta^\natural_h$ and of $\Delta_{h,w}$ differ by powers of $i$, so at every prime
of $\cF$ their Gauss valuations agree, and since $\Delta^\natural_h\in\QQ[X]$ the common value is the rational one. After
the factor $-i$, every formula of Sections~\ref{sec:construction}--\ref{sec:nonvan} involves $w$ only through $y=w^2$,
even powers $w^{2\xi}=(-1)^\xi\beta^{2\xi}$, and $-iw=\beta$; so each lemma may be read at $w$ over $\cF$, or directly in
$\KK$ with $y=-\beta^2$. We now list what transfers.
\begin{itemize}
\item \emph{Odd $p\nmid n$.} $\beta$, $y$ and $1-y=n\beta$ are $p$-units, also for $p\mid n^2-4$ (as $\gcd(n,n^2-4)\mid4$).
  Lemmas~\ref{lem:atom}--\ref{lem:nine} and Theorem~\ref{thm:A} hold verbatim: at most $\frac43$ per $h^2$.
\item \emph{Odd $p\mid n$.} Lemma~\ref{lem:S} with $e:=v_p(n)$, since $v_p(1-y)=v_p(n)$.
\item \emph{The prime $2$.} $\nu:=v(1-y)=v_2(n)$. For even $n=2m$, $\nu=1+v_2(m)\ge1$, and Lemma~\ref{lem:tennu} and
  Proposition~\ref{prop:ntwo} hold verbatim (at any prime of $\KK$ above $2$, normalised by $v(2)=1$). For odd $n$,
  $n^2-4\equiv5\bmod8$, so $2$ is inert in $\KK$ and $\nu=0$; Lemma~\ref{lem:tenzero} holds verbatim, read in $\KK$ with
  $y=-\beta^2$: its proof uses only that $y$ and $1-y$ are $2$-adic units, and $z$-free facts, and the signs
  $\chi_4(t)=\pm1$ in the partial sums $S(\zeta)$ do not affect their $2$-integrality. In all cases the cost is at most
  $c_2(v_2(n))$.
\item \emph{Size.} In the proof of Theorem~\ref{thm:B} the weights enter only through step~2, $|\det\mathbb
  M_{S,S'}|\le\prod_t(|\chi_4(t)\beta^t|\,\omega_t)^{n_t}$, so the signs never enter, and Theorem~\ref{thm:B} holds for
  $T^\natural$ at every $0<\beta\le\sqrt5-2$, i.e.\ for $n\ge5$ ($\beta_5=0.2087\ldots$). The shift lemma gives
  $\Phi\le\Phi_U-\frac12L_i(n)$ with $L_i(n):=\log(u_n/(2+\sqrt5))=\log((\sqrt5-2)/\beta_n)>0$.
\item \emph{Nonvanishing.} See Lemma~\ref{lem:Pti}.
\end{itemize}

\begin{lemma}[Lemma~P$'_n$]\label{lem:Pti}
Let $\ell\ge7$ be prime with $\ell\nmid n$, $h=3\ell-1$, and $c_j:=[X^j]\Delta^\natural_h$. Then $v_\ell(c_0)=-2K$ and
$v_\ell(c_j)\ge-2K+2j$ for all $j$; hence $\Delta^\natural_h(a'/b)\ne0$ whenever $v_\ell(b)\le1$.
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:identity}, $v_\ell(c_j)$ is the valuation of the $j$-th coefficient of $\Delta_{h,w}$ at a prime $\fl$
of $\cF$ above $\ell$ (normalised by $v_\fl(\ell)=1$). We run the proof of Lemma~\ref{lem:P} at $w$, with
$\zeta:=w^\ell\bmod\fl$. Since the conjugates of $w$ are $\pm w$ and $\pm1/w$, $\zeta\in\{w,-1/w,-w,1/w\}$ (according to
the splitting of $\ell$ in $\KK$ and $\ell\bmod4$; for $\ell\mid n^2-4$, $\beta\equiv1/\beta$ and $\zeta=\pm w$), and in
all cases $\zeta^2\in\{w^2,w^{-2}\}$. So $1-\zeta^{\pm2}$ and $1-w^{\pm2\ell}$ reduce to $1-w^{\pm2}$, and $1-w^2=n\beta$,
$1-w^{-2}=n/\beta$ are $\fl$-units exactly when $\ell\nmid n$; with $w$, $y$, $1-y$ also units, steps~1--3 of
Lemma~\ref{lem:P} go through. In steps~4--5 every quantity is a unit for each choice of $\zeta$: $c=\zeta^3/(1-\zeta^2)$,
$\det M=-64c\zeta^4$, $\one^{\mathsf T}\adj(M)\one=-64\zeta^4$, $U_\gamma\equiv-1$ (independent of the point), and
$\sum_{\gamma<\ell}w^{-2\gamma}=(1-w^{-2\ell})/(1-w^{-2})\equiv1$ or $-w^2$. Step~6 is unchanged. Index primes are
handled in $\cO_\cF$ as in Section~\ref{sec:nonvan}.
\end{proof}

The conclusion of Lemma~\ref{lem:Pti} was checked on the exact $\Delta^\natural_h$ for $\ell=7,11,13$ at $n=4,8,12$,
and, independently, for one to four primes $\ell\le17$ each at $n=5,9,10,15,21,22,197,199$, covering the four Frobenius classes and ramified $\ell$; at $\ell\mid n$
($n=21$, $\ell=7$; $n=22$, $\ell=11$; $n=7$, $\ell=7$) it fails, as it must. The identity of Lemma~\ref{lem:identity} was
checked exactly ($A^\natural=-iA_w$ and $B^\natural=\pm B_w$, the sign depending only on the normalisation of $T$) at five
pairs $(n,h)$ by an implementation independent of the one used for the profiles; Lemma~\ref{lem:tenzero} was checked
entrywise on the $\chi_4$ machine at $n=3,5,9,15,197$, with no violation and equality attained, and with
$n_2=104,352,737,1248$ at $h=16,32,48,64$ for every odd $n$ tested, the same values as for odd $a$.

\emph{The margins.} The proof of Section~\ref{sec:proof}, with $\mathcal H:=\{3\ell-1:\ell\ge37\text{ prime},\ \ell\nmid
n,\ \ell^2\nmid b\}$ and Lemma~\ref{lem:Pti}, gives the bound
\begin{equation}\label{eq:Mti}
  M_i(n):=\Phi_U-\tfrac12L_i(n)+\tfrac43+c_2(v_2(n))+\sum_{p^e\parallel n,\ p\text{ odd}}c_p(e)\qquad(n\ge5).
\end{equation}
For even $n=2m$ the arithmetic is that of Theorem~\ref{thm:V} term by term ($\nu=1+v_2(m)$, and the odd primes of $n$ are
those of $m$, with the same $e$), so
\[
  M_i(2m)=M(m)+\tfrac12\log\frac{m+\sqrt{m^2+1}}{m+\sqrt{m^2-1}},
\]
with $M(m)$ as in \eqref{eq:budget}. The correction is positive and at most
$\frac12(\sqrt{m^2+1}-\sqrt{m^2-1})/(m+\sqrt{m^2-1})\le\frac1{4(m^2-1)}$; its largest value for $m\ge3$ is $0.027850$
(at $m=3$). For odd $n$ there is no counterpart in Theorem~\ref{thm:V}: $\nu=0$, every odd prime factor of $n$ is special,
and the shift is from $\sqrt5-2$ to $\beta_n$ directly.

\begin{proposition}\label{prop:marginsti}
Let $n\ge5$. Then $M_i(n)<0$ if and only if $n$ is not one of $6,10,14,18,30$, not an odd number $\le69$, and not in
$\cE_i$.
\end{proposition}

\begin{proof}
\emph{Uniform tail.} For $n\ge5$ we have $u_n\ge n-1$, $\sum_{p^e\parallel n,\,p\text{ odd}}\frac e4\log p=\frac14\log
n-\frac\nu4\log2$, $c_2(\nu)-\frac\nu4\log2=(|\nu-2|-\nu)\frac{\log2}4\le\frac{\log2}2$, and, for any $P\ge3$, the primes
$p>P$ dividing $n$ contribute at most $\frac{\log n}{4P}$ to the terms $\frac{\log p}{4(p-1)}$. Hence
\[
  M_i(n)\le A+\tfrac12\log2+\tfrac14S_P+\tfrac12\log\frac n{n-1}-\tfrac14\bigl(1-\tfrac1P\bigr)\log n,
\]
with $A:=\Phi_U+\frac12\log(2+\sqrt5)+\frac43=0.6959348874\ldots$ and $S_P:=\sum_{3\le p\le P}\frac{\log p}{p-1}$. The right
side decreases in $n$. For $P=13$, $S_{13}=1.7295192876\ldots$, and at $n=599$ the right side is
$-0.000105877\ldots<0$ (Arb). So $M_i(n)<0$ for every $n\ge599$.

\emph{Table.} For $5\le n\le20\,000$ we evaluate $M_i(n)$ in Arb at $200$ bits; no ball contains $0$. The even $n$ with
$M_i(n)>0$ are exactly $6,10,14,18,30$, and the odd ones are the odd $n\le69$ and the $17$ elements of $\cE_i$, the largest
$195$ (with $M_i(195)\ge+0.0156$).
\end{proof}

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}rlccc|rlc@{}}
\toprule
$n$ & $\beta_n$ & $\sin2\theta$ & $\nu$ & $M_i(n)\le$ & $n$ & & $M_i(n)\le$\\
\midrule
8 & $4-\sqrt{15}$ & $1/4$ & 3 & $-0.162496$ & 115 & & $-0.007466$\\
12 & $6-\sqrt{35}$ & $1/6$ & 2 & $-0.131029$ & 71 & & $-0.007838$\\
16 & $8-\sqrt{63}$ & $1/8$ & 4 & $-0.341821$ & 129 & & $-0.012699$\\
22 & $11-\sqrt{120}$ & $1/11$ & 1 & $-0.015842$ & 73 & & $-0.015115$\\
197 & $(197-\sqrt{38805})/2$ & $2/197$ & 0 & $-0.271540$ & 42 & & $-0.019792$\\
\midrule
6 & $3-2\sqrt2$ & $1/3$ & 1 & $\ge+0.3998$ & 119 & & $-0.026888$\\
195 & & $2/195$ & 0 & $\ge+0.0156$ & & & \\
\bottomrule
\end{tabular}
\caption{Margins \eqref{eq:Mti} for Theorem~\ref{thm:Vi} (Arb; upper bounds rounded up, and lower bounds for the two
exceptions below the line). The right half and $n=22$ are all covered $n$ with $M_i(n)>-0.03$.}\label{tab:marginsti}
\end{table}

All values in Table~\ref{tab:marginsti} rest only on proved constants and on the certified endpoint $\Phi_U$. The
tightest cases $n=71$ and $n=115$ use the constant $c_2(0)=\frac12\log2$ of Lemma~\ref{lem:tenzero} exactly.

\begin{proof}[Proof of Theorem~\ref{thm:Vi}]
Let $n$ be as in the theorem ($n=2m$ in part (a)), so $n\ge8$ and, by Proposition~\ref{prop:marginsti}, $M_i(n)<0$.
Suppose $\Ti_2(\beta_n)=a'/b$. For $h\in\mathcal H$, Lemma~\ref{lem:Pti} gives $F_h(a'/b)\ne0$, where $F_h$ is the
primitive part of $\Delta^\natural_h$. Along $\mathcal H$ the arithmetic is bounded by the items above and the size by
$\Phi_U-\frac12L_i(n)$, so $\limsup_{h\in\mathcal H}h^{-2}\log|F_h(\Ti_2(\beta_n))|\le M_i(n)<0$, contradicting
Proposition~\ref{prop:criterion}.
\end{proof}

\emph{Evidence and limits.} At $n=8$ the exact finite-$h$ scores (Arb analytic part, exact contents) are $-0.528$,
$-0.379$, $-0.336$, $-0.308$ at $h=16,32,48,64$, and $F_h(T^\natural)\ne0$ in every computed case. At $n=2m$ the exact
per-prime profiles agree with those of Theorem~\ref{thm:V} at $m$ up to a few units. The case $n=4$, i.e.\
$\Ti_2(2-\sqrt3)$, is out of reach: $\beta_4>\sqrt5-2$, so the shift lemma points the wrong way, and a numerical solution of
the equilibrium problem suggests that the method misses by about $0.04$ per $h^2$. Direct certificates at odd $\beta_n$,
which reduced the exceptions for $\chi_2$ at odd $a$ from $49$ to $39$, have not been computed, and neither improvement
mentioned after Theorem~\ref{thm:Vodd} is proved; any of them would shrink $\cE_i$.

\subsection{Status of the extensions}
Theorems~\ref{thm:Vodd} and~\ref{thm:Vi} are formalised in Lean (Section~\ref{sec:lean}). Each was checked by
one AI referee at a single gate,
with code independent of the code used to find the results (Lemma~\ref{lem:tenzero}, the transferred lemmas on exact
data, the exception sets by independent interval arithmetic, and for Theorem~\ref{thm:Vi} the identity of
Lemma~\ref{lem:identity}); both referees asked for minor fixes, which were applied. For Theorem~\ref{thm:Vi} the referee
reviewed the first write-up, and the detailed delta proof written afterwards to apply the fixes has not been re-read by a
referee. No human has read either proof.

% ===========================================================================
\section{Closed forms and known results}\label{sec:closed}
% ===========================================================================

\subsection{Closed forms}
Put $w_m:=(1-z_m)/(1+z_m)$, so that Landen's identity reads
\begin{equation}\label{eq:landenm}
  \chi_2(z_m)+\chi_2(w_m)=\frac{\pi^2}8-\frac12\log z_m\,\log w_m .
\end{equation}
For $m=1$, $z_1=w_1=\sqrt2-1$, and \eqref{eq:landenm} gives $\chi_2(\sqrt2-1)=\pi^2/16-\frac14\log^2(1+\sqrt2)$. For
$m=2$, $w_2=\varphi^{-1}$, and \eqref{eq:landenm} with the value of $\chi_2(\varphi^{-1})$ gives \eqref{eq:closedform}.

\begin{proposition}\label{prop:symbol}
Let $m\ge1$. Then $w_m=(\sqrt{m^2+1}-1)/m$, $\sigma(w_m)=-1/w_m$ and $mw_m^2+2w_m-m=0$; so $w_m$ is an algebraic integer
if and only if $m\mid2$. For $m\ge3$, $z_m$ and $w_m$ are multiplicatively independent, and $z_m\wedge w_m\ne0$ in
$\Lambda^2(\KK^\times)\otimes\QQ$.
\end{proposition}

\begin{proof}
The formula for $w_m$ and its quadratic equation are direct computations; the product of the roots is $-1$, so
$\sigma(w_m)=-1/w_m$, and the monic equation $X^2+(2/m)X-1$ has integer coefficients iff $m\mid2$. For $m\ge3$, $w_m$ is
not integral, so $v_\fp(w_m)<0$ at some prime $\fp$, while $z_m$ is a unit. If $z_m^\alpha w_m^\beta=\pm1$, then
$\beta v_\fp(w_m)=0$, so $\beta=0$, and then $\alpha=0$ since $0<z_m<1$. Hence $z_m$, $w_m$ are linearly independent in
$\KK^\times\otimes\QQ$, and $z_m\wedge w_m\ne0$.
\end{proof}

From $\delta\Li_2(x)=-(1-x)\wedge x$ one gets $\delta\chi_2(z)=\pm\frac12\,w\wedge z$ modulo torsion, with
$w=(1-z)/(1+z)$. The symbol of $\pi^2$ and of a product of two logarithms is $0$ in $\Lambda^2$. So for $m\ge3$ no
dilogarithm identity that preserves the symbol expresses $\chi_2(z_m)$ through $\pi^2$ and products of logarithms; for
$m=1,2$ the symbol vanishes, as Landen's evaluations require. This is a statement about symbols only: an unconditional
statement that $\chi_2(z_m)$ is not of this form would need algebraic independence results that are not available.

By \eqref{eq:landenm}, Theorem~\ref{thm:V} can equally be stated as
$\chi_2(w_m)+\frac12\log z_m\log w_m\notin\frac{\pi^2}8+\QQ$. At $m=4$, Hakimoglu-Brown \cite[Cor.~14]{HakimogluBrown2026}
(unrefereed) gives two identities for Rogers' dilogarithm $L$ over $\QQ(\sqrt{17})$, in the bases $a=(\sqrt{17}-3)/4$
and $b=\sqrt{17}-4$. Their sum isolates $4\Li_2(b)-\Li_2(b^2)=4\chi_2(b)$, and gives
\begin{multline*}
  12\chi_2(\sqrt{17}-4)=18L(a)-6L(a^2)+18L(2a)-3L(4a^2)-2\pi^2\\
  -6\log b\log(1-b)+3\log b\log(1-b^2),
\end{multline*}
which we checked numerically to $10^{-120}$. It is a relation among non-elementary values ($a$ and $1-a$ are not units),
not a closed form; Theorem~\ref{thm:V} at $m=4$ is equivalent to the irrationality of its right side.

\subsection{Known criteria}\label{sec:lit}
Table~\ref{tab:lit} compares Theorem~\ref{thm:V} with the general criteria of Section~\ref{sec:context}, evaluated at
$z_m$ at the real place where $z_m$ is small. As there, $\chi_2(z)=z+\frac z4\Phi_2(\frac12,z^2)$, and the height of
$z_m^{-2}$ at that place is $\log(1/z_m)$. The evaluations are ours; that of \cite[Thm.~1]{DHK2022b} through
$\Phi_2(\frac12,z^2)$ was re-derived by the AI referee of Theorem~\ref{thm:V} from the statement in the arXiv version
(arXiv:2010.09167) of \cite{DHK2022b}, and that of \cite[Thm.~2.1]{DHK2020} by a separate reference check from the
statement in arXiv:1912.03811v2. The absolute values of \cite{DHK2020} are not normalised by the degree; there, with
$r=2$, the point $1$, $\beta=z_m^{-2}$, $x=\frac12$ and $\KK$ real quadratic, the quantity of Theorem~2.1 is
$2\log(1/z_m)-16-\log2\,851\,875=2\log(1/z_m)-30.863487\ldots$, and the table lists half of it. The thresholds in the
table and in Section~\ref{sec:closed-ext} are certified in interval arithmetic from these formulas. None of the
evaluations has been checked by the authors of the criteria.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.31\textwidth}>{\raggedright\arraybackslash}p{0.33\textwidth}>{\raggedright\arraybackslash}p{0.28\textwidth}@{}}
\toprule
criterion & key quantity at $z_m$ & covers\\
\midrule
\cite[Thm.~1]{DHK2022b}, via $\Phi_2(\frac12,z^2)$ & $\log(1/z_m)-15.977968\ldots$ & $m\ge4\,346\,237$, with $\chi_2(z_m)\notin\KK$\\
\cite[Thm.~1]{DHK2022b}, via $\Li_2(\pm z)$ & $\frac12\log(1/z_m)-15.78$ & $m\gtrsim e^{31.5}/2$\\
\cite[Thm.~2.1]{DHK2020} (proof only outlined), via $\Phi_2(\frac12,z^2)$ & $\log(1/z_m)-15.431744\ldots$ & $m\ge2\,517\,046$, with $\chi_2(z_m)\notin\KK$\\
\cite[Thm.~2.2]{Kawashima2026} (unrefereed) & $\frac12\log(1/z_m)-26.84$ & $m\gtrsim e^{53.7}/2$\\
Bombieri--Andr\'e via \cite{Orr2026} (unrefereed) & height $\frac12\log(1/z_m)$ against about $1450$ & $m\gtrsim e^{2900}$\\
results at rational points & --- & none\\
\bottomrule
\end{tabular}
\caption{General criteria at $z_m$ (our evaluations).}\label{tab:lit}
\end{table}

At $m=4$ the first quantity is $-13.88$ and the third $-13.34$. The criterion of \cite{DHK2022b} gives the linear
independence of $1$, $\Phi_1(\frac12,z^2)$, $\Phi_2(\frac12,z^2)$ over $\KK$, hence $\chi_2(z_m)\notin\KK$, a stronger
conclusion than ours in its range. So the infinite tail $m\ge4\,346\,237$ of Theorem~\ref{thm:V} is due to
\cite{DHK2022b}. Theorem~2.1 of \cite{DHK2020}, as stated, has the same conclusion and would give it already for
$m\ge2\,517\,046$. Its proof, however, is given only in outline, with the details deferred to forthcoming articles;
\cite[Rem.~1(iii)]{DHK2022b} refers to it as the result announced without proof, says that the result of
\cite{DHK2022b} is better in general but not always, and its comparison \cite[Prop.~4]{DHK2022b} does not cover the case
$r=2$ with one point used here. What Theorem~\ref{thm:V} adds is therefore the range $2\le m\le2\,517\,045$ with
$m\notin\cE$, by one argument for all $m$, and, if the announced result of \cite{DHK2020} is set aside, the range
$2\le m\le4\,346\,236$. As far as our searches show, no result in the literature covers any $m$ with
$2\le m\le2\,517\,045$; for $m\ge3$ the searches were limited (Section~\ref{sec:context}), and a MathSciNet search and an
expert query are still owed.

\subsection{The extensions}\label{sec:closed-ext}
\emph{Odd $a$.} Proposition~\ref{prop:symbol} extends to every $a$.

\begin{proposition}\label{prop:symbolodd}
Let $a\ge1$, $\alpha=\alpha_a$ and $w:=(1-\alpha)/(1+\alpha)$. Then $aw^2+4w-a=0$, so $w$ is an algebraic integer if and
only if $a\mid4$. For $a\notin\{1,2,4\}$, in particular for every odd $a\ge3$, $\alpha\wedge w\ne0$ in
$\Lambda^2(\KK^\times)\otimes\QQ$.
\end{proposition}

\begin{proof}
From $\alpha^2+a\alpha-1=0$, $(1+\alpha)^2(aw^2+4w-a)=a(1-\alpha)^2+4(1-\alpha^2)-a(1+\alpha)^2=-4(\alpha^2+a\alpha-1)=0$.
The monic polynomial $X^2+(4/a)X-1$ has integer coefficients iff $a\mid4$, and its roots have product $-1$. If $w$ is not
integral, $v_\fp(w)<0$ at some prime $\fp$, while $\alpha$ is a unit; the rest is the proof of
Proposition~\ref{prop:symbol}.
\end{proof}

For $a=2m$ this is Proposition~\ref{prop:symbol}. So among the units $\alpha_a$ only $a=1$ ($\varphi^{-1}$), $a=2$
($\sqrt2-1$) and $a=4$ ($\sqrt5-2$) admit a Landen-type closed form; for odd $a\ge3$, $\chi_2(\alpha_a)$ has no expression
through $\pi^2$ and products of logarithms by symbol-preserving dilogarithm identities.

\emph{The inverse tangent integral.} With $\theta:=\arctan\beta_n$ we have $\sin2\theta=2\beta/(1+\beta^2)=2/n$, and
\[
  \Ti_2(\tan\theta)=\theta\log\tan\theta+\tfrac12\bigl(\Cl_2(2\theta)+\Cl_2(\pi-2\theta)\bigr),\qquad
  \Cl_2(x)=\sum_{k\ge1}\frac{\sin kx}{k^2},
\]
a classical formula (see \cite{Lewin1981}), which we checked numerically to $80$ digits at $n=5,8,12,22,71$. For $n\ge5$
the value $\sin2\theta=2/n$ is rational and not in $\{0,\pm\frac12,\pm1\}$, so $2\theta$ is not a rational multiple of
$\pi$ \cite[Cor.~3.12]{Niven1956}. Only $n=4$ gives a rational angle ($2\theta=\pi/6$), and there
$\Ti_2(2-\sqrt3)=\frac23G-\frac\pi{12}\log(2+\sqrt3)$.

\begin{proposition}\label{prop:symbolti}
Let $n\ge5$, $\zeta:=e^{2i\theta}=(\sqrt{n^2-4}+2i)/n$ and $\cF=\QQ(i,\sqrt{n^2-4})$. Then $\zeta$ is not an algebraic
integer, and $\bar\zeta\wedge\beta_n\ne0$ in $\Lambda^2(\cF^\times)\otimes\QQ$. Modulo torsion, $\bar\zeta\wedge\beta_n$
is the symbol of $\Ti_2(\beta_n)$.
\end{proposition}

\begin{proof}
$\zeta$ and $\bar\zeta=\zeta^{-1}$ are the roots of $X^2-bX+1$ with $b=2\sqrt{n^2-4}/n$, and $b^2=4-16/n^2\notin\ZZ$ for
$n\ge5$; so $b$, and hence $\zeta$, is not integral, $v_\fp(\zeta)\ne0$ at some prime $\fp$ of $\cF$, and $\zeta$ is
multiplicatively independent of the unit $\beta_n$. For the symbol, $\Ti_2(x)=(\Li_2(ix)-\Li_2(-ix))/(2i)$ and
$\delta\Li_2(u)=-(1-u)\wedge u$ give, modulo torsion, $\pm\frac{1-i\beta}{1+i\beta}\wedge\beta$, and
$(1-i\tan\theta)/(1+i\tan\theta)=e^{-2i\theta}=\bar\zeta$.
\end{proof}

So for $n\ge5$ no symbol-preserving identity expresses $\Ti_2(\beta_n)$ through $\pi^2$, $G$ and products of logarithms.
The symbol $\bar\zeta\wedge\beta_n$ lies in the part $S^1\wedge\RR_{>0}$ of $\Lambda^2(\mathbb C^\times)\otimes\QQ$, while the
symbols of the real values $\chi_2(\alpha_a)$ of Theorems~\ref{thm:V} and~\ref{thm:Vodd} do not; this suggests, but does
not prove, that the numbers of Theorem~\ref{thm:Vi} are not rational combinations of those of Theorems~\ref{thm:V}
and~\ref{thm:Vodd}. As a numerical check, PSLQ at $320$ digits with coefficients up to $10^{12}$ was run on the $20$
numbers $\Ti_2(\beta_n)$, $1$, $\pi^2$, $G$, $\pi\log\beta_n$, $\log^2\beta_n$, $\pi\log2$, $\log2\log\beta_n$, $\log^22$,
$\chi_2(\beta_n)$, $\Li_2(\beta_n)$, $\sqrt{|D|}\,L(2,\chi_D)$ (with $D$ the discriminant of $\QQ(\sqrt{-(n^2-4)})$),
$\theta\log\beta_n$, $\theta\pi$, $\theta^2$, $\theta\log n$, and four values $\chi_2(z_{m'})$ with $m'$ near $n/2$ and $m'=n$. It
found no relation at $n=5,8,9,10,12,22$. At $n=6$ it found only a relation without $\Ti_2$ among $\chi_2(\beta_6)$,
$\Li_2(\beta_6)$, $\pi^2$, $\log^2\beta_6$, as expected since $\beta_6=(\sqrt2-1)^2$, and none after removing $\Li_2$; as a
control, at $n=4$ it found $3\Ti_2(\beta_4)=2G+3\theta\log\beta_4$.

\emph{Known criteria.} The evaluations of \cite[Thm.~1]{DHK2022b} and \cite[Thm.~2.1]{DHK2020} in
Section~\ref{sec:lit} use only the real place and the height $\log(1/z)$ of $z^{-2}$ (the point $z^{-2}$ is an algebraic integer, so no
denominator enters), so they do not depend on the parity of $a$: since
$\log(1/\alpha_a)=\operatorname{arsinh}(a/2)$, the key quantity $\operatorname{arsinh}(a/2)-15.977968\ldots$ of
\cite{DHK2022b} changes sign between $a=8\,692\,473$ and $a=8\,692\,474$, and that of \cite{DHK2020},
$\operatorname{arsinh}(a/2)-15.431744\ldots$, between $a=5\,034\,091$ and $a=5\,034\,092$. So \cite{DHK2022b} gives the
stronger $\chi_2(\alpha_a)\notin\KK$ for $a\ge8\,692\,474$, and \cite{DHK2020}, as stated, for $a\ge5\,034\,092$. For the
inverse tangent integral, $\Ti_2(z)=z+\frac z4\Phi_2(\frac12,-z^2)$: the point $1$ is replaced by $-1$. Both criteria
depend on the points only through their absolute values $|\cdot|_v$, and $|-1|_v=1$ at every place, so every constant
is unchanged. With $\log(1/\beta_n)=\operatorname{arcosh}(n/2)$ this gives $\Ti_2(\beta_n)\notin\KK$ for
$n\ge8\,692\,474$ by \cite{DHK2022b}, and for $n\ge5\,034\,092$ by \cite{DHK2020} as stated (for even $n=2m$:
$m\ge4\,346\,237$ and $m\ge2\,517\,046$). These are our evaluations, not checked by the authors of the criteria. What
Theorems~\ref{thm:Vodd} and~\ref{thm:Vi} add is therefore the odd $a$ with $59\le a\le5\,034\,091$,
$a\notin\cE_{\mathrm{odd}}$; the odd $n$ with $71\le n\le5\,034\,091$, $n\notin\cE_i$; and the $m$ with
$4\le m\le2\,517\,045$, $m\notin\{5,7,9,15\}$. If the result announced in \cite{DHK2020} is set aside (see
Section~\ref{sec:lit}), the upper limits become $8\,692\,473$, $8\,692\,473$ and $4\,346\,236$.

\emph{Literature.} For odd $a$ we searched our own notes and the web (two queries); we found closed forms at
$\varphi^{-1}$ and $\varphi^{-3}$, results at rational points and identities, but no irrationality result for $\chi_2$ or
$\Li_2$ at the units $\alpha_a$ with odd $a$. For $\Ti_2$ we searched our own notes, which include an earlier sweep of
arXiv (2007--2026) for irrationality results on related values, and the web (two queries); we found only identities for
$\Ti_2$ and $\Cl_2$, and no irrationality result for $\Ti_2$ or $\Cl_2$ at points of this kind. These searches were
carried out by AI systems; a MathSciNet search and an expert query are still owed, so we make no claim beyond the
statement that we know of no earlier result in these ranges.

% ===========================================================================
\section{Two points}\label{sec:M1}
% ===========================================================================

\subsection{The statement}
Let $n\ge6$ be even and $P_n(X):=X^4+nX^3+2X^2-nX+1$. It is irreducible with four real roots: two in $(0,1)$, which we
call $z>w$, and $-1/z$, $-1/w$; moreover $w=(1-z)/(1+z)$, and $z\approx1-2/n$, $w\approx1/n$. Let $\cK:=\QQ(z)$, a totally
real biquadratic field with $\operatorname{Gal}(\cK/\QQ)=\{1,s,l,sl\}$, $s(z)=-1/z$, $l(z)=w$. Put $u:=z-1/z$; then
$u^2+nu+4=0$, and $\cF:=\cK^s=\QQ(u)=\QQ(\sqrt{n^2-16})$, on which $l$ acts as the nontrivial automorphism, with
$l(u)=4/u$. With $\eps_k:=(k+\sqrt{k^2-4})/2$ we have $zw=\eps_{n+2}^{-1}$ and $z/w=\eps_{n-2}$. Put $T_z:=\chi_2(z)$,
$T_w:=\chi_2(w)$; Landen's identity gives
\[
  T_n:=T_z+T_w=\frac{\pi^2}8-\frac12\log z\log w=\frac{\pi^2}8-\frac18\log^2\eps_{n+2}+\frac18\log^2\eps_{n-2}.
\]

\begin{definition}
$\mathrm{M1}(n)$ is the statement: $T_n\notin\QQ$, or $T_z-T_w\notin\sqrt{n^2-16}\,\QQ$.
\end{definition}

Equivalently, there is no $\alpha\in\cF$ with $T_z=\alpha$ and $T_w=l(\alpha)$: such an $\alpha$ would have
$\alpha+l(\alpha)\in\QQ$ and $\alpha-l(\alpha)\in\sqrt{n^2-16}\,\QQ$, and conversely. (Exchanging $z$ and $w$ only changes
the sign of $T_z-T_w$.)

\begin{theorem}[Theorem M1]\label{thm:M1}
$\mathrm{M1}(n)$ holds for every $n\in\mathcal N:=\{730,740,750,760,800,1000\}$.
\end{theorem}

The proof is computer-assisted: for each $n\in\mathcal N$ separately it uses two dual certificates checked in interval
arithmetic. It is a disjunction at six specific values of $n$, not a statement about a range of $n$, and it is not
formalised.

\emph{The case $n=730$} (Theorem~\ref{thm:M1-730}). Here $z=0.99726400650629232574\ldots$,
$w=0.0013698707255499998352\ldots$, $\eps_{732}=366+\sqrt{133955}=1/(zw)$, $\eps_{728}=364+11\sqrt{1095}=z/w$ and
$\sqrt{730^2-16}=22\sqrt{1101}$. Numerically $T_{730}=1.2246689334990568135\ldots$, $T_z=1.2232990624878816026\ldots$ and
$T_w=0.0013698710111752109\ldots$. The fields are $\cK=\QQ(\sqrt{133955},\sqrt{1095})$ and $\cF=\QQ(\sqrt{1101})$, and the
primes ramified in $\cK$ are $2,3,5,73,367$. The other instances are in Table~\ref{tab:M1fields}; in each case
$\cK=\QQ(\sqrt{d_+},\sqrt{d_-})$ with $d_\pm$ the squarefree parts of $(n\pm2)^2-4$.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}rllll@{}}
\toprule
$n$ & $\eps_{n+2}=1/(zw)$ & $\eps_{n-2}=z/w$ & $\sqrt{n^2-16}$ & ramified in $\cK$\\
\midrule
730 & $366+\sqrt{133955}$ & $364+11\sqrt{1095}$ & $22\sqrt{1101}$ & $2,3,5,73,367$\\
740 & $371+2\sqrt{34410}$ & $369+4\sqrt{8510}$ & $16\sqrt{2139}$ & $2,3,5,23,31,37$\\
750 & $376+5\sqrt{5655}$ & $374+5\sqrt{5595}$ & $2\sqrt{140621}$ & $2,3,5,13,29,373$\\
760 & $381+2\sqrt{36290}$ & $379+6\sqrt{3990}$ & $12\sqrt{4011}$ & $2,3,5,7,19,191$\\
800 & $401+20\sqrt{402}$ & $399+20\sqrt{398}$ & $4\sqrt{39999}$ & $2,3,67,199$\\
1000 & $501+10\sqrt{2510}$ & $499+10\sqrt{2490}$ & $4\sqrt{62499}$ & $2,3,5,83,251$\\
\bottomrule
\end{tabular}
\caption{The six instances of Theorem~\ref{thm:M1}.}\label{tab:M1fields}
\end{table}

\subsection{What changes at two points}
The machine is that of Section~\ref{sec:construction} with $z$ the root above: the same poles, atoms and functional,
now with $A,B\colon\QQ[t]\to\cK$ and $\Delta_h\in\cK[X]$. We write $y=z^2$; then $1-y=-uz$. Since $u$ is an algebraic integer
with $u\,l(u)=4$, $u$ divides $4$, and $z$, $w$ are units of $\cK$ (roots of a monic polynomial with constant term $1$).

\emph{Reflection.} Lemma~\ref{lem:R} holds with $\sigma=s$, the generator of $\operatorname{Gal}(\cK/\cF)$: its proof
used only $\sigma(z)=-1/z$ and that the coefficients are rational functions of $z$ with rational coefficients. So the
odd-index entries lie in $e\,\cF[X]$ with $e:=z+1/z$, $s(e)=-e$, $e^2=u^2+4=-nu\in\cF$, and the rescaled matrix
$E_{i+j}e^{\ind{i\text{ odd}}-\ind{j\text{ odd}}}$ shows $\Delta_h\in\cF[X]$. The reflection removes the conjugates
$-1/z$ and $-1/w$, where the series diverge.

\emph{The second place.} The remaining conjugate, $l$, is not removed but convergent: the coefficients of $A$ and $B$
are rational functions of $z$, so $l(\Delta_h)(T_w)=\det(\Lambda_w(t^{i+j}))$, the Hankel determinant of the same
machine at the weight $w$ (the series converge since $0<w<1$). The two embeddings of $\cF$ thus see the $z$-machine and
the $w$-machine, and the endgame uses the norm $\cF\to\QQ$.

\emph{Odd primes.} At every prime of $\cK$ above an odd $p$, $z$, $y$ and $1-y=-uz$ are units. These are the only
properties of $z$ that Lemmas~\ref{lem:atom}--\ref{lem:nine} and Theorem~\ref{thm:A} use, so they hold verbatim, with the
valuation normalised by $v(p)=1$; there are no special odd primes, including the ramified ones and those dividing
$n^2-16$. The bound is the same at every prime $\fp$ of $\cF$ above $p$.

\emph{The prime $2$.} Here Lemma~\ref{lem:ten} fails: at $n=400$, $h=48$, the exact $2$-adic content is $388.5$, above
$h\lfloor\log_2h\rfloor+3h=384$. It is replaced by the following weaker bound, which is the analogue over $\cK$ of the
case $\nu=1$ of Proposition~\ref{prop:ntwo}.

\begin{lemma}[Lemma~10$''$]\label{lem:tenpp}
Let $n$ be even and $\fP$ a prime of $\cK$ above $2$, with $v=v_\fP$ normalised by $v(2)=1$. Then
$-v(\Delta_h)\le(h-2)^2/4+3h$.
\end{lemma}

\begin{proof}
Since $n$ is even, $u/2$ is a root of $X^2+(n/2)X+1$, hence a unit; so
$\nu:=v(1-y)=v(u)=1$, instead of $2$. Follow the proof of Lemma~\ref{lem:tennu}, which up to the valuations does not
involve $z$. In (L), $y^b/(1-y)^{b+1}$ now has valuation $-(b+1)$, so
$v(G_{ij})\ge1-\pi+\min_{b<\pi}(v_2(b!)-1)=-\pi$. In (U), with $v(\eta)=1$, the first part has valuation $2+s_2(N_0)$ and
the second part valuation $\ge1+s_2(N_0)$, so $v(G_{ij})\ge2$ for $N_0\ge0$; the bound no longer grows with $N_0$. Hence
$v(G_{ij})\ge-f(i+j)$ with $f(s):=(s-K)_+$, a convex function, and $v(\tilde\Delta_h)\ge-\max_\sigma\sum_if(i+\sigma(i))$.
If $i<i'$ and $\sigma(i)>\sigma(i')$, put $c=i+\sigma(i)$, $d=i'+\sigma(i')$, $a=i+\sigma(i')$, $b=i'+\sigma(i)$; then
$a+b=c+d$ and $a<c,d<b$, so convexity gives $f(c)+f(d)\le f(a)+f(b)$, and removing inversions does not decrease the sum.
So the identity maximises, and $\sum_{i<h}f(2i)=1+3+\dots+(h-3)=(h-2)^2/4$. Finally $-v(\Delta_h)=3h-v(\tilde\Delta_h)$.
\end{proof}

So the prime $2$ costs $\frac14\log2=0.1733\ldots$ per $h^2$ instead of $0$. The mechanism that made it free in
Lemma~\ref{lem:ten} is not available anywhere in the family:

\begin{proposition}\label{prop:nu}
For every $n$ there is a prime $\fP$ of $\cK$ above $2$ with $v_\fP(1-y)\le1$ (normalised by $v_\fP(2)=1$). In particular
$v_2(1-y)=2$, which holds at $\sqrt5-2$ and makes the prime $2$ free there, cannot hold at every prime above $2$.
\end{proposition}

\begin{proof}
$z$ is a unit, so $v_\fP(1-y)=v_\fP(u)$. From $u\,l(u)=4$ we get $v_\fP(u)+v_\fP(l(u))=2$, and
$v_\fP(l(u))=v_{l^{-1}(\fP)}(u)$. If $v_\fP(u)\ge2$ for every $\fP\mid2$, then $v_\fP(l(u))\le0$ for every $\fP$, so
$v_{l^{-1}(\fP)}(u)\le0$, a contradiction.
\end{proof}

For even $n$, $\nu=1$ at every prime above $2$; for odd $n$, $\nu\in\{0,2\}$, and the prime with $\nu=0$ is worse, so odd
$n$ are not used. Proposition~\ref{prop:nu} does not show that the loss $\frac14\log2$ is necessary: exact profiles suggest
that the true $2$-adic cost is about $\frac18\log2$ per $h^2$, but we have not proved this.

\emph{The analytic part.} Theorem~\ref{thm:B} holds at a general weight $q\in\{z,w\}$, with $L:=\log(1/q)$, the field
$v_q(x):=-Lx-\Psi(x)$, and three changes. (a) $v_q$ is strictly decreasing on $(-\tanh L,\infty)$, which contains
$[-1/h,\infty)$ if and only if $h>\coth L$; this is the range of $h$ ($\coth L_z=364.9986\ldots$ at $n=730$, and
$\coth L_w<1.0001$). (b) The dual density is only assumed $\ge0$, of mass $1$, with $\operatorname{supp}\mu\subset[0,X_e]$
for some $X_e\ge4$ (at the $z$-place the support is long, $X_e\approx1300$), and $\Phi_q(\mu,\lambda):=-E(\mu)+\lambda+
\int_0^{X_e}(F_\mu-\lambda)_+\,dx$ with $F_\mu=2U^\mu+v_q$. (c) The tail condition becomes: with
$B(x):=2\log x-\log(x-1)-Lx$, both $\beta:=\lambda-B(X_e)$ and $\gamma:=L-(X_e-2)/(X_e(X_e-1))$ are positive. With
$M_0:=2\log(X_e+1)+1+L-\lambda$ and $\kappa:=2/(1-e^{-2\gamma})$, the proof of Theorem~\ref{thm:B} gives, for every even
$h>\coth L$,
\[
  \log\bigl|\det(\Lambda_q(t^{i+j}))_{i,j<h}\bigr|\le h^2\Phi_q(\mu,\lambda)+E_q(h),
\]
\begin{multline*}
  E_q(h):=2h\log(4h)+h\log4+(hX_e/2+2)\log3\\
  +h\,c_1(h)+2.362h-h\log h+h\max(M_0,0)+\kappa .
\end{multline*}
The pattern count below $X_eh$ replaces $(2h+1)\log3$, the cell $[-1/h,0]$ costs $h\max(M_0,0)$ (here $U^\mu\le\log(X_e+1)$
and $v_q\le L+1$ there), and the far nodes cost $\kappa$. Since $E_q(h)=O(h\log h)$, the $\limsup$ is again $\Phi_q$.

\emph{Nonvanishing.} Lemma~\ref{lem:P} holds over $\cF$ for $h=3\ell-1$ with $\ell\ge7$ prime and unramified in $\cK$.
Now $\zeta:=z^\ell\bmod\fl$ is $\operatorname{Frob}_\fl(z)$, one of four values:
\begin{center}
\begin{tabular}{@{}ccccc@{}}
\toprule
$\operatorname{Frob}_\fl$ & $1$ & $s$ & $l$ & $sl$\\
\midrule
$\zeta$ & $z$ & $-1/z$ & $w$ & $-1/w$\\
$1-\zeta^2$ & $-uz$ & $u/z$ & $-(4/u)w$ & $(4/u)/w$\\
$1-\zeta^{-2}$ & $u/z$ & $-uz$ & $(4/u)/w$ & $-(4/u)w$\\
\bottomrule
\end{tabular}
\end{center}
Every entry is an $\fl$-unit because $u\mid4$ and $\ell$ is odd, and steps 1--5 of Lemma~\ref{lem:P} use only these units
and $1-z^{-2}=u/z$. Since $\ell$ is unramified, $v_\fl$ restricts to $v_\fL$ on $\cF$ for $\fL=\fl\cap\cF$, and step~6
gives $\Delta_h(\alpha)\ne0$ for every $\alpha\in\cF$ with $v_\fL(\alpha)\ge-1$, whether $\ell$ is split or inert in $\cF$.

\begin{lemma}[Lemma~E$'$, the norm endgame]\label{lem:Eprime}
Let $n\ge6$ be even, and suppose that for each $q\in\{z,w\}$ there is a pair $(\mu_q,\lambda_q)$ as in~(b) above
($\mu_q\ge0$, mass $1$, $\operatorname{supp}\mu_q\subset[0,X_e]$ with $X_e\ge4$; the cap $\mu_q\le1$ is not required)
satisfying the tail condition~(c), with
\[
  M_1(n):=\tfrac12\bigl(\Phi_z(\mu_z,\lambda_z)+\Phi_w(\mu_w,\lambda_w)\bigr)+\tfrac43+\tfrac14\log2<0 .
\]
Then $\mathrm{M1}(n)$ holds.
\end{lemma}

\begin{proof}
Suppose $\alpha\in\cF$ has $T_z=\alpha$ and $T_w=l(\alpha)$, and fix $b\ge1$ with $b\alpha\in\cO_\cF$. Let
$\mathcal H:=\{3\ell-1:\ell\ge7\text{ prime, unramified in }\cK,\ \ell\nmid b,\ 3\ell-1>\coth L_z\}$, an infinite set; note
$\coth L_w<\coth L_z$. For $h\in\mathcal H$, Lemma~P$'$ over $\cF$ gives $\Delta_h(\alpha)\ne0$. For a prime $\fp$ of $\cF$
put $n_\fp:=-v_\fp(\Delta_h)$, which may be a half-integer at ramified primes, and $n_p:=\max(0,\max_{\fp\mid p}\lceil
n_\fp\rceil)$, $c_h:=\prod_pp^{n_p}$. Then $c_h\Delta_h\in\cO_\cF[X]$, and by the odd-prime lemmas and
Lemma~\ref{lem:tenpp},
\[
  \log c_h\le\sum_{3\le p<K}B_p\log p+\bigl((h-2)^2/4+3h\bigr)\log2+\theta(K)+\log2,
\]
where $B_p$ are the bounds used in Theorem~\ref{thm:A}; the term $\theta(K)=O(h)$ pays for all ceilings. So
$\limsup_{h\in\mathcal H}h^{-2}\log c_h\le\frac43+\frac14\log2$. The algebraic integer $\beta:=b^hc_h\Delta_h(\alpha)$ is
nonzero. Its two real embeddings are $b^hc_h\Delta_h(T_z)=b^hc_h\det(\Lambda_z(t^{i+j}))$ and
$b^hc_h\,l(\Delta_h)(T_w)=b^hc_h\det(\Lambda_w(t^{i+j}))$, so
$N_{\cF/\QQ}(\beta)=b^{2h}c_h^2\det(\Lambda_z(t^{i+j}))\det(\Lambda_w(t^{i+j}))$ is a nonzero integer. Taking logarithms,
dividing by $2h^2$, and applying the analytic bound at both places,
$0\le\frac43+\frac14\log2+\frac12(\Phi_z+\Phi_w)=M_1(n)<0$, a contradiction.
\end{proof}

\subsection{The certificates}
For each $n\in\mathcal N$ and $q\in\{z,w\}$ the certificate is a piecewise constant $\mu_q\ge0$ on a grid of $[0,X_e]$
with mass exactly $1$, a rational $\lambda_q$, a rigorous Arb upper bound for $\Phi_q(\mu_q,\lambda_q)$, and an Arb check
of the tail condition with $X_e\ge4$; the logarithm $L=\log(1/q)$ is an Arb ball computed from the quartic, so every bound
encloses the value at the true $L$. Two independent evaluators were used, and where both certified the same $(n,q)$ the
smaller bound is taken. Table~\ref{tab:M1cert} lists the results; $\frac43+\frac14\log2=1.50662012847331966\ldots$, and
every $M_1(n)$ is computed in Arb from the printed balls and lies entirely below $0$.

\begin{table}[ht]
\centering
\begin{tabular}{@{}rccr@{}}
\toprule
$n$ & $\Phi_z\le$ & $\Phi_w\le$ & $M_1(n)\le$\\
\midrule
730 & $0.97551590832772$ & $-3.98960878950$ & $-0.000426312$\\
740 & $0.98154355971108$ & $-3.99641267680$ & $-0.000814430$\\
750 & $0.98568546476333$ & $-4.00312517276$ & $-0.002099725$\\
760 & $0.98610919549783$ & $-4.00974867868$ & $-0.005199613$\\
800 & $1.00091072617$ & $-4.03494034059$ & $-0.010394678$\\
1000 & $1.05765433525$ & $-4.14651125316$ & $-0.037808330$\\
\bottomrule
\end{tabular}
\caption{Certified bounds for Theorem~\ref{thm:M1} (upper endpoints of Arb balls, rounded up). At the $z$-place
$X_e=1300$ for $n\le760$, and $X_e\approx1202$ and $1503$ for $n=800$, $1000$; at the $w$-place $X_e\approx4$.}\label{tab:M1cert}
\end{table}

The constant $\Phi_z$ is positive because $z\approx1-2/n$ gives the $z$-machine almost no decay; the $w$-place, with
$w\approx1/n$, pays for it. The side constants are comfortable: at $n=730$, for example, $\beta=0.5719$,
$\gamma=0.001971$, $M_0\le11.17$, $\kappa\le508.4$ at the $z$-place, and $\beta=16.41$, $\gamma=6.426$ at the $w$-place.
A third evaluator, written independently of both, confirms $M_1(n)<0$ for all six $n$ and gives
$M_1(730)\le-0.000452$. As a validation, the three codes applied at the weight $\sqrt5-2$ of Corollary~\ref{thm:U} give
$-1.35926599$, $-1.35939764$ and $-1.35939884$, consistent with Theorem~\ref{thm:cert} and the primal value
$-1.3594016$ of Remark~\ref{rem:equil}.

\subsection{Scope}
We state the limits of Theorem~\ref{thm:M1} explicitly.
\begin{itemize}
\item It is a disjunction. We do not know which of the two statements holds, and neither is known by other means:
  $T_n\notin\QQ$ is a statement of strong-four-exponentials type, and we know of no result on $T_z-T_w$.
\item For very large $n$ general criteria apply. Take the shift $\frac12$ at $w^2$ (the point $1$, $\beta=w^{-2}$), at
  the real place where $w$ is small; the conjugates of $w^{-2}$ are $w^{-2}$, $z^{-2}$, $w^2$, $z^2$. By our evaluation,
  the condition of \cite[Thm.~1]{DHK2022b}, $\frac12\log(1/w)-\log(1/z)-15.977968\ldots>0$, holds for every even
  $n\ge75\,559\,095\,378\,072\approx7.56\cdot10^{13}$, and that of \cite[Thm.~2.1]{DHK2020} (as stated, with its proof
  only outlined; see Section~\ref{sec:lit}), $2\log(1/w)-32-\log(5^4\cdot3^5\cdot13^4)-4\log(1/z)-2\log(4+9z^{-2})>0$,
  for every even $n\ge7\,608\,252\,420\,528\approx7.61\cdot10^{12}$. Either gives $\chi_2(w)\notin\cK$, and hence
  $\mathrm{M1}(n)$, for those $n$. The thresholds are certified in interval arithmetic from these formulas; our reading
  of the two statements has not been checked by a referee or by their authors. For $730\le n\le1000$ the two quantities
  (the second divided by $[\cK:\QQ]=4$) lie between $-12.7$ and $-12.5$, and between $-11.6$ and $-11.3$, so
  Theorem~\ref{thm:M1} is not implied.
\item It is proved for the six listed values of $n$ only, each with its own certificates. Even $n$ between them are not
  covered, and odd $n$ are not covered at all: Lemma~\ref{lem:tenpp} needs $n$ even, and for odd $n$ one prime above
  $2$ has $v(1-y)=0$.
\item For all even $n\ge730$ the statement is supported only numerically. A proof would need interval certificates in $n$
  (the dual bound is monotone in $L$, but this needs to be written) and an argument as $n\to\infty$; neither exists.
\item The method cannot reach $n=720$: there the primal value of the equilibrium problem gives $M_1(720)\ge+0.00098$
  (computed numerically, with a density admissible up to rounding of order $10^{-12}$), so no dual certificate can
  succeed. Numerically the threshold of the method lies in $(720,730)$.
\item The theorem is not formalised in Lean. Its proof was checked by two AI referees and has not been read by a human.
\end{itemize}

% ===========================================================================
\section{The formalisation}\label{sec:lean}
% ===========================================================================

\subsection{What is formalised}
The Lean project \cite{PiTwoRepo} proves Theorem~\ref{thm:V}, Theorem~\ref{thm:Vodd}, Theorem~\ref{thm:Vi},
Corollary~\ref{thm:U} and the identity \eqref{eq:closedform} in Lean~4 \cite{LeanFour} (version v4.35.0) with Mathlib \cite{Mathlib} (version v4.35.0
\cite{Mathlib4}). The machine is formalised once, with the trace $a$ of the unit $\alpha_a=(\sqrt{a^2+4}-a)/2$ as a
parameter, so that Corollary~\ref{thm:U} is the case $a=4$, Theorem~\ref{thm:V} the case $a=2m$ and
Theorem~\ref{thm:Vodd} the case of odd $a$. Theorem~U was proved first; Theorem~V adds the ingredients that depend on
$m$: Lemma~\ref{lem:tennu}, Lemma~\ref{lem:S}, the shift lemma, the margins, and Lemma~\ref{lem:P} for every $m$;
Theorem~\ref{thm:Vodd} adds Lemma~\ref{lem:tenzero}, eleven direct certificates and the margins at odd $a$.
Theorem~\ref{thm:Vi} uses a copy of the machine with the sign fixed, in the folder \lean{Ti\slash{}} (namespace
\lean{Chi2U.Ti}, $35$ modules), with the trace $n$ of $\beta_n$ as parameter; no file of the other theorems is changed.
The project has $130$ modules under \lean{Chi2U\slash{}}, with about $30{,}600$ lines, of which about $7{,}800$ are ported
verbatim from
the formalisation of \cite{Chi2Paper} \cite{Chi2Repo}: the prime number theorem, the interval arithmetic, the generic
analytic files, the criterion and the definition of $\chi_2$. All declarations are in the namespace \lean{Chi2U}. The
project is available at \url{https://github.com/telaviv/chi2-quadratic-units-irrationality} \cite{PiTwoRepo}, together with
a copy of this paper and the scripts of Section~\ref{sec:comp}. Theorem~\ref{thm:M1} is not formalised.
Corollary~\ref{cor:normminus} and the statement on the units of norm $+1$ after Theorem~\ref{thm:Vi} are not stated in
Lean; the first follows from Theorems~\ref{thm:V} and~\ref{thm:Vodd} as explained after its statement, the second from
Theorem~\ref{thm:Vi}, since every unit of norm $+1$ in $(0,1)$ is some $\beta_n$. The Clausen form of
Theorem~\ref{thm:Vi}, through the classical formula (see \cite{Lewin1981}), is not formalised either.

\subsection{The statement}
The definitions that the reader has to check are in \lean{Defs.lean}, \lean{Statement.lean},
\lean{V\slash{}Defs.lean}, \lean{VOdd\slash{}Defs.lean}, \lean{Ti\slash{}Defs.lean} and
\lean{Golden\slash{}Corollary.lean}:
\begin{quote}\ttfamily\footnotesize
noncomputable def chi2Term (z : $\mathbb{R}$) (n : $\mathbb{N}$) : $\mathbb{R}$ :=\\
\hspace*{2em}z \^{} (2 * n + 1) / (2 * (n : $\mathbb{R}$) + 1) \^{} 2\\[2pt]
noncomputable def chi2 (z : $\mathbb{R}$) : $\mathbb{R}$ := $\sum$' n : $\mathbb{N}$, chi2Term z n\\[2pt]
def V.TheoremV : Prop := $\forall$ m : $\mathbb{N}$, 2 $\le$ m $\to$ m $\notin$ (\char123 3, 5, 7, 9, 15\char125{} : Finset $\mathbb{N}$) $\to$\\
\hspace*{2em}Irrational (chi2 (Real.sqrt ((m : $\mathbb{R}$) \^{} 2 + 1) - m))\\[2pt]
theorem V.theoremV : V.TheoremV\\[2pt]
def VOdd.EOdd : Finset $\mathbb{N}$ := \char123 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35,\\
\hspace*{2em}37, 39, 41, 43, 45, 47, 49, 51, 53, 55, 57, 63, 65, 69, 75, 77, 81, 85, 87, 93,\\
\hspace*{2em}99, 105, 165\char125\\[2pt]
def VOdd.TheoremVOdd : Prop := $\forall$ a : $\mathbb{N}$, Odd a $\to$ 5 $\le$ a $\to$ a $\notin$ EOdd $\to$\\
\hspace*{2em}Irrational (chi2 ((Real.sqrt ((a : $\mathbb{R}$) \^{} 2 + 4) - a) / 2))\\[2pt]
theorem VOdd.theoremVOdd : VOdd.TheoremVOdd\\[2pt]
noncomputable def Ti.ti2Term (z : $\mathbb{R}$) (k : $\mathbb{N}$) : $\mathbb{R}$ :=\\
\hspace*{2em}(-1) \^{} k * z \^{} (2 * k + 1) / (2 * (k : $\mathbb{R}$) + 1) \^{} 2\\[2pt]
noncomputable def Ti.Ti2 (z : $\mathbb{R}$) : $\mathbb{R}$ :=\\
\hspace*{2em}$\sum$' k : $\mathbb{N}$, ti2Term z k\\[2pt]
def Ti.EOddI : Finset $\mathbb{N}$ := \char123 75, 77, 81, 85, 87, 91, 93,\\
\hspace*{2em}95, 99, 105, 111, 117, 123, 135, 147, 165, 195\char125\\[2pt]
def Ti.TheoremVi : Prop :=\\
\hspace*{2em}($\forall$ m : $\mathbb{N}$, 4 $\le$ m $\to$ m $\notin$ (\char123 5, 7, 9, 15\char125{} : Finset $\mathbb{N}$) $\to$\\
\hspace*{3em}Irrational (Ti2\\
\hspace*{4em}(m - Real.sqrt ((m : $\mathbb{R}$) \^{} 2 - 1)))) $\wedge$\\
\hspace*{2em}($\forall$ n : $\mathbb{N}$, Odd n $\to$ 71 $\le$ n $\to$ n $\notin$ EOddI $\to$\\
\hspace*{3em}Irrational (Ti2\\
\hspace*{4em}((n - Real.sqrt ((n : $\mathbb{R}$) \^{} 2 - 4)) / 2)))\\[2pt]
theorem Ti.theoremVi : Ti.TheoremVi\\[2pt]
def TheoremU : Prop := Irrational (chi2 (Real.sqrt 5 - 2))\\[2pt]
theorem chi2\_sqrt5\_sub\_two\_irrational : TheoremU\\
theorem chi2\_sqrt5\_sub\_two\_eq :\\
\hspace*{2em}chi2 (Real.sqrt 5 - 2) = Real.pi \^{} 2 / 24 - 3 / 4 * Real.log goldenRatio \^{} 2\\
theorem golden\_irrational' :\\
\hspace*{2em}Irrational (Real.pi \^{} 2 - 18 * Real.log goldenRatio \^{} 2)
\end{quote}
\lean{V.TheoremV} and \lean{V.theoremV} are in \lean{V\slash{}Defs.lean} and \lean{V\slash{}Interface.lean}, and
\lean{VOdd.EOdd}, \lean{VOdd.TheoremVOdd} and \lean{VOdd.theoremVOdd} in \lean{VOdd\slash{}Defs.lean} and
\lean{VOdd\slash{}Interface.lean}; \lean{EOdd} is the set $\cE_{\mathrm{odd}}$ written out. \lean{Ti.Ti2},
\lean{Ti.EOddI}, \lean{Ti.TheoremVi} and \lean{Ti.theoremVi} are in \lean{Ti\slash{}Defs.lean} and
\lean{Ti\slash{}Interface.lean}; \lean{Ti2} is the inverse tangent integral, it does not depend on \lean{chi2}, and
\lean{EOddI} is the set $\cE_i$ written out. Of the
other three theorems, the first is in \lean{Main.lean}, the second in \lean{Golden\slash{}ClosedForm.lean}, the third in
\lean{Golden\slash{}Corollary.lean}. The definition of $\chi_2$ is identical to that of \cite{Chi2Repo}, and
\lean{Defs.lean} proves summability for $|z|\le1$, so \lean{chi2 (Real.sqrt 5 - 2)} and, since
$0<\sqrt{m^2+1}-m<1$ and $0<(\sqrt{a^2+4}-a)/2<1$, the values of \lean{chi2} in \lean{V.TheoremV} and
\lean{VOdd.TheoremVOdd} are the genuine sums of the series. Likewise \lean{Ti\slash{}PoleExpansion.lean} proves
summability of the series of \lean{Ti2} for $|z|\le1$, and $0<\beta_n<1$, so the values of \lean{Ti2} in
\lean{Ti.TheoremVi} are the genuine sums. The internal point \lean{zT n} $=n/2-\sqrt{(n/2)^2-1}$ is rewritten into the
forms of the statement by proved lemmas.
\lean{goldenRatio} is Mathlib's $(1+\sqrt5)/2$ and \lean{Irrational} is Mathlib's predicate $x\notin\QQ$. The identity
\eqref{eq:closedform} is proved from Landen's identity for $\chi_2$, Euler's reflection formula and Landen's identity for
$\Li_2$ (\lean{Golden\slash{}Landen.lean}, \lean{Golden\slash{}Dilog.lean}), so the golden-ratio form is not a separate
assumption.

The command \lean{lake env lean Axioms.lean} prints, among its other lines,
\begin{quote}\ttfamily\small
'Chi2U.V.theoremV' depends on axioms:\\
\hspace*{2em}[propext, Classical.choice, Quot.sound]\\
'Chi2U.VOdd.theoremVOdd' depends on axioms:\\
\hspace*{2em}[propext, Classical.choice, Quot.sound]\\
'Chi2U.Ti.theoremVi' depends on axioms:\\
\hspace*{2em}[propext, Classical.choice, Quot.sound]\\
'Chi2U.chi2\_sqrt5\_sub\_two\_irrational' depends on axioms:\\
\hspace*{2em}[propext, Classical.choice, Quot.sound]\\
'Chi2U.golden\_irrational'' depends on axioms:\\
\hspace*{2em}[propext, Classical.choice, Quot.sound]
\end{quote}
and the same list for \lean{chi2\_sqrt5\_sub\_two\_eq} and for each of the main ingredients listed in \lean{Axioms.lean}.
These are Lean's three standard axioms. The development contains no \lean{sorry}, no added axiom, no
\lean{native\_decide}, no \lean{implemented\_by} and no \lean{@[extern]}, so no step relies on compiled code.

\subsection{Correspondence with the paper}
Table~\ref{tab:lean} lists the main formal counterparts. Paths are relative to \lean{Chi2U\slash{}}. The machine files
take the trace $a$ as a parameter, called \lean{az} there (\lean{Qd az} $=$ \lean{QuadraticAlgebra} $\QQ$
$((a/2)^2+1)$ $0$, \lean{zK az}, \lean{Delta az h}); Theorem~\ref{thm:V} uses $a=2m$, and the entries marked $m=2$ are
used only for Corollary~\ref{thm:U}. The files of Theorem~\ref{thm:Vi} take the trace $n$ of $\beta_n$ as a parameter
(\lean{Qt n} $=$ \lean{QuadraticAlgebra} $\QQ$ $((n/2)^2-1)$ $0$, \lean{zK n}, \lean{Delta n h}, in the namespace
\lean{Chi2U.Ti}); most of their declarations have the names of their $\chi_2$ counterparts.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.27\textwidth}>{\raggedright\arraybackslash}p{0.69\textwidth}@{}}
\toprule
paper & Lean declaration (file) \\
\midrule
$\KK$, $z$, $\sigma$ & \lean{Qd}, \lean{zK}, \lean{sig}, \lean{emb} (\lean{Field}); $m=2$: \lean{Q5} $=$ \lean{Qd 4}\\
Lemma~\ref{lem:pole}, \eqref{eq:mahler} & \lean{lemma1}, \lean{aeval\_chi2\_Delta} (\lean{PoleExpansion}); \lean{Lmom\_eq\_mahler} (\lean{Mahler})\\
Lemma~\ref{lem:R}, Cor.~\ref{cor:R} & \lean{eval$_2$\_Delta}, \lean{aeval\_Delta}, \lean{Delta\_map} (\lean{LemmaR})\\
Prop.~\ref{prop:criterion} & \lean{irrational\_of\_poly\_approx} (\lean{Criterion}); \lean{MachineBoundsU}, \lean{irrational\_of\_boundsU} (\lean{MainCond})\\
Lemma~\ref{lem:classcount} & \lean{AK\_eq} (\lean{Arith\slash{}ClassCount})\\
Lemma~\ref{lem:bordered} & \lean{lemmaB} (\lean{Arith\slash{}LemmaB})\\
Lemmas~\ref{lem:eight}, \ref{lem:nine} & \lean{lemma9} (\lean{Arith\slash{}OddPrimes}, \lean{Arith\slash{}Lemma9Levels}); \lean{Arith\slash{}Lemma8One}; \lean{padicNorm\_Delta\_odd} (\lean{Arith\slash{}OddExp})\\
Thm.~\ref{thm:A} & \lean{theoremA} (\lean{Arith\slash{}PrimeSums}); \lean{denAll\_int}, \lean{log\_denAll\_le} (\lean{Arith\slash{}Assembly})\\
Lemma~\ref{lem:ten} ($m=2$) & \lean{lemma10\_L}, \lean{lemma10\_U}, \lean{padicNorm\_Delta\_two} (\lean{Arith\slash{}TwoAdic})\\
Lemma~\ref{lem:tennu} & \lean{lemma10nu\_proof} (\lean{V\slash{}Lemma10nu}, \lean{V\slash{}TwoAdicNu}); \lean{lemma10nu\_size} (\lean{V\slash{}Defs})\\
Lemma~\ref{lem:S} & \lean{lemmaS\_proof} (\lean{V\slash{}LemmaS}, \lean{V\slash{}S*}); \lean{AK\_levels\_size\_proof} (\lean{V\slash{}AKSize})\\
Thm.~\ref{thm:B} (other route) & \lean{log\_abs\_Dpoly\_ge}, \lean{DualCertU}, \lean{DualCertU.analytic} (\lean{Analytic\slash{}TheoremBU})\\
Thm.~\ref{thm:cert} (coarser) & \lean{exists\_certU}, \lean{exists\_certU'} (\lean{Cert\slash{}CertU}); data \lean{Cert\slash{}DataU}, \lean{Cert\slash{}LogTab}; format \lean{LinCertU}, \lean{LinCertU.exists\_dual} (\lean{Cert\slash{}Lin}), \lean{CDataLin}, \lean{exists\_dual\_le} (\lean{Cert\slash{}LinInstance})\\
Lemma~\ref{lem:shift} & \lean{shift\_lemma\_proof} (\lean{V\slash{}Shift})\\
margins, Section~\ref{sec:margins} & \lean{margin\_V\_proof} (\lean{V\slash{}Margin})\\
Lemma~\ref{lem:P} & \lean{lemmaP}, \lean{nonvan\_frequently} (\lean{NonVan\slash{}LemmaP}); \lean{lemmaP\_m\_proof} (\lean{V\slash{}NonVan})\\
Section~\ref{sec:proof} & \lean{denV0\_int}, \lean{log\_denV\_le}, \lean{exists\_boundsV}, \lean{theoremV} (\lean{V\slash{}Interface}); $m=2$: \lean{boundsU}, \lean{chi2\_sqrt5\_sub\_two\_irrational} (\lean{Main})\\
\eqref{eq:closedform} & \lean{chi2\_landen}, \lean{Li2\_reflection}, \lean{Li2\_landen} (\lean{Golden\slash{}Landen}); \lean{chi2\_sqrt5\_sub\_two\_eq} (\lean{Golden\slash{}ClosedForm})\\
\midrule
Lemma~\ref{lem:tenzero} & \lean{lemma10\_0\_proof} (\lean{VOdd\slash{}TenZero}); \lean{lemma10\_0\_size} (\lean{VOdd\slash{}Defs})\\
Table~\ref{tab:certodd} (own values) & \lean{exists\_certOdd\_proof} (\lean{VOdd\slash{}CertOdd}); data \lean{VOdd\slash{}CertData\slash{}A$a$} for $11$ values of $a$\\
Prop.~\ref{prop:marginsodd} (``if'' part) & \lean{margin\_VOdd\_proof} (\lean{VOdd\slash{}Margin})\\
proof of Thm.~\ref{thm:Vodd} & \lean{denO0\_int}, \lean{log\_denO\_le}, \lean{exists\_boundsO}, \lean{theoremVOdd} (\lean{VOdd\slash{}Interface})\\
\midrule
$\Ti_2$, $\KK$, $\beta_n$, $\sigma$ & \lean{Ti2} (\lean{Ti\slash{}Defs}); \lean{Qt}, \lean{zK}, \lean{sig}, \lean{emb}, \lean{zT} (\lean{Ti\slash{}Field})\\
Lemma~\ref{lem:identity} (not used) & the $\chi_4$ machine directly: \lean{Ti\slash{}Machine}, \lean{Ti\slash{}LemmaR}; \lean{aeval\_Ti2\_Delta} (\lean{Ti\slash{}PoleExpansion})\\
valuations, Section~\ref{sec:Ti2} & \lean{padicNorm\_Delta\_odd\_proof} (\lean{Ti\slash{}OddExp}); \lean{lemmaS\_proof} (\lean{Ti\slash{}LemmaS}); \lean{lemma10nu\_proof} (\lean{Ti\slash{}Lemma10nu}); \lean{lemma10\_0\_proof} (\lean{Ti\slash{}TenZero})\\
size, Section~\ref{sec:Ti2} & \lean{DualCertT}, \lean{DualCertT.analytic} (\lean{Ti\slash{}Analytic\slash{}TheoremBT}); \lean{shift\_lemma\_proof} (\lean{Ti\slash{}Analytic\slash{}ShiftT}); \lean{analytic\_T\_proof} (\lean{Ti\slash{}Analytic})\\
Lemma~\ref{lem:Pti} & \lean{lemmaP\_n\_proof} (\lean{Ti\slash{}NonVan}, \lean{Ti\slash{}NonVan\slash{}*}); \lean{nonvan\_frequently\_T} (\lean{Ti\slash{}Interface})\\
Prop.~\ref{prop:marginsti} (``if'' part) & \lean{margin\_Vi\_proof} (\lean{Ti\slash{}Margin})\\
proof of Thm.~\ref{thm:Vi} & \lean{MachineBoundsT}, \lean{irrational\_of\_boundsT} (\lean{Ti\slash{}MainCond}); \lean{exists\_boundsT}, \lean{theoremVi} (\lean{Ti\slash{}Interface})\\
\bottomrule
\end{tabular}
\caption{Formal counterparts of the main steps.}\label{tab:lean}
\end{table}

\subsection{Differences from the written proof}
The formal proof establishes what the endgame needs, and in several places it takes a route that was shorter in Lean.
\begin{itemize}
\item \emph{The machine.} $\Delta_h$ is \emph{defined} as the determinant of the rational coordinates of the matrix
  $\tilde E$ of Corollary~\ref{cor:R}, so $\Delta_h\in\QQ[X]$ holds by definition; Lemma~\ref{lem:R} and
  Corollary~\ref{cor:R} then identify it with the Hankel determinant over $\KK$ and its value at $T$ with
  $\det(\Lambda(t^{i+j}))$.
\item \emph{Theorem B$'$.} The formal proof does not follow Section~\ref{sec:analytic}. It follows the lattice-energy
  route of the formal proof of Theorem~B in \cite{Chi2Paper}: the Andreief identity for the node expansion, the bound
  $h^h(1+2/h)^{h^2}$ for determinants with derivative rows via averages over roots of unity (instead of step~3), and a
  discrete P\'olya-type lattice energy inequality comparing the patterns, which live on the odd nodes, with a reference
  sequence on all of $\NN$ (instead of steps~5--6). The ingredient not present in \cite{Chi2Repo} is the two-sided Jensen
  bound of step~4
  (\lean{log\_abs\_Dpoly\_ge}), which gives the node weight \eqref{eq:nodeweight}. This route evaluates the dual at the
  nodes pointwise, so it never meets the cell $[-1/h,0]$ and does not use the monotonicity \eqref{eq:vmono} (which is
  nevertheless proved, as \lean{vU\_strictAntiOn}, on $[-\frac12,\infty)$). It is stated asymptotically, like Theorem~B of
  \cite{Chi2Paper}: the explicit $E_{\mathrm{an}}(h)$ is not formalised.
\item \emph{The certificate.} A formal dual certificate (\lean{DualCertU}) consists of a step density on cells of
  $[0,2]$, a grid of width $1/L$ on $[0,X]$ with $X=4$, rational cell bounds $S_k$ for $2U^\mu+v$, and the tail
  conditions; its exponent is $-E(\mu)+\lambda+\frac1L\sum_k(S_k-\lambda)_+$. The certificates are written in a
  linear-majorant form (\lean{LinCertU}, \lean{Cert\slash{}Lin.lean}): on the $k$-th grid cell, $2U^\mu+v$ is bounded by
  an affine function $\ell_k$ with endpoint values $e_{0,k}$, $e_{1,k}$, obtained from chords and tangents of each term,
  as in \cite{Chi2Paper}, which keeps the cancellation between neighbouring cells without the near/far split of
  Section~\ref{sec:cert}. The cell is charged $\frac1{2L}\bigl((e_{0,k}-\lambda)_++(e_{1,k}-\lambda)_+\bigr)$, the
  trapezoid rule, which by convexity is at least the integral of $(\ell_k-\lambda)_+$ over the cell. Splitting each cell
  into $r$ subcells and taking on each the larger endpoint value of $\ell_k$ gives a certificate of the first kind whose
  exponent exceeds the linear-majorant one by at most $B/(2Lr)$, $B=\sum_k|e_{1,k}-e_{0,k}|$
  (\lean{LinCertU.exists\_dual}), so the analytic theorem is applied unchanged. For Corollary~\ref{thm:U} the step
  density has $10$ cells of width $\frac15$ and the grid has $L=40$ ($160$ cells); the certified value is
  $\Phi_\QQ=-27083980489111/20000000000000\approx-1.3541990$, coarser than Theorem~\ref{thm:cert} but enough. The formal
  statements are $\Phi<\Phi_L:=-1.3538792$ (\lean{exists\_certU'}; the rounded constant $\Phi_L$ is the one used by
  the shift lemma below) and $\Phi<-27/20$ (\lean{exists\_certU}); the assembly (\lean{boundsU}) uses $\beta=-27/20$, so
  the formal margin is $\frac43-\frac{27}{20}=-\frac1{60}$.
\item \emph{Lemma 8$'$.} For the generic primes only the single-level range $K/3\le p$ used by Theorem~\ref{thm:A} is
  formalised, by a crude row bound on the Lagrange Gram matrix and Lemma~\ref{lem:bordered} instead of the atom
  expansion. The multi-level statement needed by Lemma~\ref{lem:S} is proved directly (\lean{V\slash{}LemmaS} and its
  helper files) instead of through the expansion of Lemma~7$'$: a Schur-complement form of the determinant, a
  multilinear expansion of its bottom rows, and a Newton (divided-difference) factorisation that extracts the squared
  Vandermonde factor. The polynomial factor enters through integer row and column exponents $(i-J)_+$, $(j-J-1)_+$ with
  the same total $(J-1)^2$. This proof does not use $p\mid m$.
\item \emph{Lemma $10_\nu$.} The Karamata step is replaced by a weighted Leibniz bound: by concavity
  $\hat g(2i)+\hat g(2j)\le2\hat g(i+j)$, so integer row weights $\lfloor\hat g(2i)/2\rfloor$ and column weights
  $\lceil\hat g(2j)/2\rceil$ give $v_2(\det G)\ge\sum_i\hat g(2i)$. Some entry bounds are coarser than in
  Lemma~\ref{lem:tennu}, where the slack of its final bound allows it. For odd $m$ no half-integral valuations occur:
  every bound is a rational power of $2$ times an element of the order.
\item \emph{The shift lemma} is applied to the formal certificate of Theorem~U, in its discrete format: each grid cell is
  split into $r$ subcells, and the left-endpoint sum loses $L(m)/(2rL)$, which is absorbed by taking $r$ large. So the
  formal analytic constant at $z_m$ is $\Phi_L-\frac12L(m)+\delta$ for any $\delta>0$, with
  $\Phi_L=-1.3538792$ in place of $\Phi(z_2)$ of Theorem~\ref{thm:cert}.
\item \emph{The margins} are proved with this coarser constant, and the exception set is still exactly $\cE$. Even
  $m\ge4$ and odd $m\ge69$ are handled by a closed form written with $\log m$ (the tightest case is $m=69$, with slack
  about $10^{-3}$), $m=2$ exactly, and the $28$ odd $m\in[11,67]\setminus\cE$ one by one with rational bounds on the
  logarithms (for instance $\log(2+\sqrt5)\le\frac{25}{12}\log2$).
\item \emph{Lemma P$'$.} Congruences are taken in a residue field of the order at a prime above $\ell$, with
  $\zeta:=z^\ell$ itself; no identification of $\zeta$ by Frobenius is needed, only
  $1-\bar z^{2\ell}=(2m\bar z)^\ell$. The formal Lemma~P$'$ (\lean{lemmaP}) needs only $\ell\nmid2m$, for every $m$; the
  instance used for Theorem~\ref{thm:V} (\lean{lemmaP\_m}) assumes $\ell\nmid2m(m^2+1)$, which still leaves infinitely
  many $\ell$. The progression sums are
  handled by an exact shift identity instead of the Newton form.
\item \emph{The endgame} uses only even $h$, through $P_h:=\Delta_{2\lfloor h/2\rfloor}$ in the criterion of
  \cite{Chi2Repo}.
\item \emph{Lemma $10_0$.} As for Lemma~$10_\nu$, the Karamata step is replaced by the weighted Leibniz bound: by
  concavity $g(2i)+g(2j)\le2g(i+j)$, and since $h$ is even every $g(2i)$ is even, so the integer row and column weights
  $\lfloor g(2i)/2\rfloor$, $\lceil g(2j)/2\rceil$ lose nothing and give $v(\tilde\Delta_h)\ge\sum_ig(2i)=2h-h^2/2$. The
  bound (U) is used in the weaker form $v(G_{ij})\ge2-N_0$, which is all the tent minorant needs.
\item \emph{The analytic constant at odd $a$} is $\Phi_L-\frac12L(a)$ (shift lemma), with $\Phi_L=-1.3538792$, which is
  $0.0053$ weaker than $\Phi_U$. So $a=123$, where the shift lemma alone gives $M_{\mathrm{odd}}(123)\le-0.000034$ in
  Proposition~\ref{prop:marginsodd}, has a positive formal shift margin and needs a direct certificate too: the formal
  proof uses eleven certificates, at $a=59,61,67,91,95,111,117,123,135,147,195$, against the ten of
  Table~\ref{tab:certodd}. They are Lean's own certificates in the linear-majorant form, on grids with $L$ between $20$
  and $100$ (against $N=1600$ in Table~\ref{tab:certodd}), and their values lie $0.0006$ to $0.015$ above those of
  Table~\ref{tab:certodd} (for example $-2.718256$ against $-2.730260$ at $a=59$). The formal margins are therefore
  thinner: the thinnest is at $a=135$, about $-0.00025$ (against $-0.000887$), followed by $a=59$, about $-0.0014$.
\item \emph{The margins at odd $a$.} Instead of the bound $C_0-\frac18\log a$ and the Arb table for $a\le5001$, the
  formal proof splits off the primes $3$, $5$, $7$ in $\sum_{p^e\parallel a}c_p(e)$, which gives a closed form negative
  for every odd $a\ge275$, and checks the $96$ odd $a<275$ outside $\cE_{\mathrm{odd}}$ one by one, with rational
  enclosures of the logarithms. Only the ``if'' part of Proposition~\ref{prop:marginsodd} is formalised; the ``only if''
  part is not needed for Theorem~\ref{thm:Vodd}.
\item \emph{Nonvanishing at odd $a$} uses \lean{lemmaP\_m} with $\ell\ge7$, $\ell\nmid a(a^2+4)$, along $h=3\ell-1$,
  instead of the set $\mathcal H$ of Section~\ref{sec:odd-a} with $\ell\ge37$; infinitely many $\ell$ remain.
\item \emph{Theorem~\ref{thm:Vi}: a copy of the machine.} Lemma~\ref{lem:identity} is not used. The $\chi_4$-twisted
  machine is defined directly over $\KK=\QQ(\sqrt{(n/2)^2-1})$ with the weights $\chi_4(t)\beta^t$, i.e.\ with $y=-\beta^2$,
  $1-y=n\beta$ and $\sigma(\beta)=1/\beta$, by a copy of the files of the $\chi_2$ machine with the sign fixed; each copied
  file names its original. Lemma~\ref{lem:R}, Corollary~\ref{cor:R}, the valuation lemmas and Lemma~\ref{lem:Pti} are
  proved again for this machine, with the proofs of the $\chi_2$ files and the departures listed above (Lemma~$8'$,
  Lemmas~$10_\nu$ and~$10_0$, Lemma~P$'$); the signs $\chi_4(t)=\pm1$ are units and do not change any bound. A sign
  parameter in the shared files would have touched every proof that unfolds a weight.
\item \emph{The prime $2$ at even $n$.} The valuations are taken in the order $\ZZ_{(2)}[\sqrt{d}]$, $d=(n/2)^2-1$,
  which is not the maximal order when $n\equiv2\bmod4$. Every bound is obtained from rational powers of $2$ times
  elements of this order, so it is a valid lower bound for the valuation at the prime above $2$.
\item \emph{Lemma P$'_n$} is stated for primes $\ell\ge7$ with $\ell\nmid n(n^2-4)$, as \lean{lemmaP\_m} for odd $a$,
  and used along $h=3\ell-1$ instead of the set $\mathcal H$ of Section~\ref{sec:Ti2}; the proof uses only $\ell\nmid n$,
  and infinitely many $\ell$ remain. It is read in $\KK$, in a residue field at a prime above $\ell$, so no case split by
  the Frobenius class of $\ell$ is needed.
\item \emph{The analytic constant for Theorem~\ref{thm:Vi}.} The formal Theorem~B$'$ above holds at $\beta_n$ with the
  signed weights, since only $|\chi_4(t)\beta^t|=\beta^t$ enters (\lean{DualCertT.analytic}). A copy of the shift lemma
  moves the formal certificate of Corollary~\ref{thm:U} to $\beta_n$, so the formal analytic constant is
  $\Phi_L-\frac12L_i(n)+\delta$ for any $\delta>0$. No further certificate is needed.
\item \emph{The margins of Theorem~\ref{thm:Vi}} are proved with $\Phi_L$, which is $0.0053$ weaker than $\Phi_U$; the
  exception set is still exactly that of Proposition~\ref{prop:marginsti}. The thinnest formal margins are at $n=115$,
  about $-0.00213$ (against $-0.007466$), and $n=71$, about $-0.0025$ (against $-0.007838$). Instead of the uniform tail
  and the Arb table for $n\le20\,000$, the formal proof uses the sharper bound $-\log\beta_n\ge\log n-1/(n-1)^2$, three
  closed forms, negative for $n\equiv0\bmod4$ with $n\ge8$, for $n\equiv2\bmod4$ with $n\ge138$ and for odd $n\ge275$,
  and checks the remaining $113$ values of $n$ ($28$ with $n\equiv2\bmod4$ and $85$ odd) one by one, with rational
  enclosures of the logarithms. Only the ``if'' part of Proposition~\ref{prop:marginsti} is formalised.
\end{itemize}

\subsection{How the certificates are checked}
The certificate data were produced by the scripts \lean{scripts\slash{}gen\_cert\_lin.py} (at any trace) and
\lean{scripts\slash{}gen\_cert\_u.py}, which runs it at $a=4$ and writes \lean{Cert\slash{}DataU.lean} and
\lean{Cert\slash{}LogTab.lean}; the eleven certificates of Theorem~\ref{thm:Vodd} are in
\lean{VOdd\slash{}CertData\slash{}A$a$.lean}, each with its generating command in its header. The scripts are not
trusted: every check is a decidable statement about the rational data, proved by \lean{decide +kernel}. For
Corollary~\ref{thm:U} these are the $160$ grid cells in $4$ chunks of $40$, the energy bound, the tail and the enclosure
of $\log z$ (\lean{Cert\slash{}DataU.lean}), together with a table of $1004$ logarithm enclosures
(\lean{Cert\slash{}LogTab.lean}) shared with the certificates at odd $a$. The dyadic enclosure of $\log2$ used by the
table, and the logarithm enclosures in the finite cases of the margins at odd $a$ (\lean{VOdd\slash{}Margin.lean}) and
of Theorem~\ref{thm:Vi} (\lean{Ti\slash{}Margin.lean}, generated by \lean{scripts\slash{}ti\slash{}margin\_ti\_cases.py}),
are also checked by \lean{decide +kernel}. Theorem~\ref{thm:Vi} uses no certificate of its own. A wrong value would make the build fail but
could not make a false statement provable.

\subsection{Cost}
The kernel check of the certificate of Corollary~\ref{thm:U}, with the logarithm table, takes about $71$ seconds. A build
of a fresh clone of the repository, with Mathlib's prebuilt cache and at most four parallel Lean processes, took
$9$ minutes $35$ seconds ($9110$ jobs, no errors) on a Windows~11 desktop with $32$ logical processors and $31.7$\,GB of
RAM, before the files for general $m$, for odd $a$ and for $\Ti_2$ were added; the complete project has $9178$ jobs, and
\lean{Axioms.lean} reports only the three standard axioms.

\subsection{What has to be trusted}
Beyond the Lean kernel and the three axioms, the reader has to trust that the definitions displayed above express
Theorem~\ref{thm:V}, Theorem~\ref{thm:Vodd}, Theorem~\ref{thm:Vi} and Corollary~\ref{thm:U}, and the Mathlib
definitions they use (real
numbers, \lean{tsum}, \lean{Real.sqrt}, \lean{Real.log}, \lean{Real.pi}, \lean{goldenRatio}, \lean{Irrational},
\lean{Odd}, \lean{Finset}). Nothing else, in particular no numerical data and no generating script, needs to be trusted.
To avoid trusting the elaborator's handling of the environment, every declaration of all $130$ project modules was
replayed through the kernel with \lean{leanchecker} (shipped with the Lean toolchain), each module against the compiled
environment of its imports, on 9 November 2026; all modules passed, in about $56$ minutes in total.
Mathlib itself was not replayed from scratch (\lean{--fresh}). Four AI referees, for Corollary~\ref{thm:U},
Theorem~\ref{thm:V}, Theorem~\ref{thm:Vodd} and Theorem~\ref{thm:Vi}, checked the fidelity of the statements (the
definitions above, traced to Mathlib, and the absence of hypotheses, custom axioms and compiler trust) and found them
faithful; the second also confirmed the exception set $\cE$ independently in interval arithmetic for $m\le3000$, the
third compared \lean{EOdd} with $\cE_{\mathrm{odd}}$ element by element and recomputed the exception set for the odd
$a\le6001$, with the formal constants and with those of Section~\ref{sec:odd-a}, and the fourth compared \lean{EOddI}
with $\cE_i$ element by element and recomputed the exception set for $5\le n\le5000$, with the formal constants and with
those of Section~\ref{sec:Ti2}. Apart from the check by the Lean kernel, all verification of
the formalisation so far was carried out by AI systems; no human expert has yet reviewed the Lean code.

% ===========================================================================
\section{Computations and reproducibility}\label{sec:comp}
% ===========================================================================

\subsection{Software}
The computations use python-flint~0.9.0 \cite{pythonflint}: exact arithmetic over $\QQ$ and $\QQ(\sqrt{d_m})$ for every
statement about valuations, and Arb ball arithmetic \cite{Arb} for every real number that feeds a claim. Hankel
determinants are evaluated at $T$ in ball arithmetic with working precision about $3.6h^2+8000$ bits at $m=2$, and at
least $2\cdot(\text{bits of the coefficients})+4000$ bits in the independent check for general $m$. The formalisation
uses Lean v4.35.0 and Mathlib v4.35.0.

\subsection{What each computation is used for}
\begin{itemize}
\item \emph{Proof inputs.} The certificate of Theorem~\ref{thm:cert} (\texttt{cert\_U.py}, run with arguments
  \texttt{1600 32 2 4}, $128$ bits, about one minute); the margin table for the odd $m\le65$ in the proof of
  Proposition~\ref{prop:margins} (\texttt{margins\_V.py}, Arb at $200$ bits, which also lists every $m<200$); the
  certificates of Theorem~\ref{thm:M1} (\texttt{dual\_ref.py}, and \texttt{dualcert\_arb2.py} with its library
  \texttt{dualcert.py}), the margins and the explicit numbers of Section~\ref{sec:M1} (\texttt{facts\_M1.py}, Arb at
  $3000$ bits). These are rigorous: floating point is used only to choose the density and $\lambda$, and any choice gives
  a valid bound.
\item \emph{Not used by the proof of Theorem~\ref{thm:V}.} The direct certificates of Table~\ref{tab:certV}
  (\texttt{cert\_V.py}, the program \texttt{cert\_U.py} with only $z$ changed); the effective thresholds
  (\texttt{h0\_U.py}, \texttt{h0\_scan.py} at $m=2$; \texttt{h0\_V.py}, \texttt{h0\_scan\_V.py} at $m=4$): exact sums,
  using the constants of Theorem~\ref{thm:B}; the identity at $m=4$ in Section~\ref{sec:closed}
  (\texttt{id17\_check.py}).
\item \emph{Checks of the lemmas} (not used by the proof). At $m=2$: the machine and the matrix $\tilde E$
  (\texttt{umach\_core.py}); the bordered identity at $h=2,\dots,12$ and $X\in\{0,1,-3/7\}$ (\texttt{bordered\_check.py});
  the row claim (\texttt{rowclaim\_check.py}); Lemmas~\ref{lem:eight}, \ref{lem:nine} on exact profiles up to $h=256$
  (\texttt{law\_check.py}, \texttt{u\_profile.py} with \texttt{fastcontent.py}); Lemma~\ref{lem:classcount} by brute
  force for every odd $d<K+40$ and $194$ values of $K$ (\texttt{law\_check.py}); Lemma~\ref{lem:ten} entrywise for $h\le64$
  (\texttt{lemma10\_check.py}); Lemma~\ref{lem:P} (\texttt{blocks\_check.py}, \texttt{lemmaP\_check.py}). An AI referee
  reimplemented the machine without sharing code and reproduced the numbers it checked; the certificate reproduced bit for
  bit at $N=100,200,1600$. For general $m$: Lemma~\ref{lem:tennu} entrywise (\texttt{lemma10nu\_check.py}),
  Lemmas~\ref{lem:eight}, \ref{lem:nine}, \ref{lem:S} and~\ref{lem:P} on exact data (\texttt{oddp\_check.py}), and the
  scores of Table~\ref{tab:evidenceV} (\texttt{vprofile.py}). The AI referee of Theorem~\ref{thm:V} wrote an independent
  implementation of the machine for general $m$, which checked these lemmas in $47$ pairs $(m,h)$ and reproduced the
  scores it recomputed; the referee also re-ran \texttt{cert\_V.py} at $m=4$ (same result bit for bit), compared it with
  an independent primal computation, and recomputed the margins with its own code.
\item \emph{The extensions} (Section~\ref{sec:ext}). Proof inputs: \texttt{cert\_za.py}, the program
  \texttt{cert\_V.py} with $z=\alpha_a$, for the ten certificates of Table~\ref{tab:certodd} (run with arguments
  \texttt{1600 32 2 4} and the value of $a$ in the environment variable \texttt{CERT\_A}; about ten seconds each);
  \texttt{margins\_odd.py} (Arb at $200$ bits) for the margin table of Proposition~\ref{prop:marginsodd} (odd $a\le5001$,
  with and without the certificates); \texttt{margins\_ti2.py} (Arb at $200$ bits) for the table $5\le n\le20\,000$ and the
  uniform tail of Proposition~\ref{prop:marginsti}. Checks, not used by the proofs: \texttt{vodd.py} (Lemma~\ref{lem:tenzero}
  entrywise, Lemma~\ref{lem:S} and Lemma~\ref{lem:P} on exact data at odd $a$); \texttt{sharpS\_check.py} (the sharper,
  unproved special-prime bound in the remark after Theorem~\ref{thm:Vodd}); \texttt{wlib.py} (exact library for the
  weighted machines, including the $\chi_4$ machine) with \texttt{wprofile.py} (exact contents and Arb scores, e.g.\ at
  $n=8$); \texttt{margins\_ti.py} (the first margin table for Theorem~\ref{thm:Vi}, up to $n\le2000$, and a check of the
  Clausen form; superseded by \texttt{margins\_ti2.py}); \texttt{lemmaP\_ti.py} (Lemma~\ref{lem:Pti} at $n=4,8,12$);
  \texttt{step1\_parity.py} (the exact check of the sign rule of Remark~\ref{rem:signrule}); \texttt{energy.py} (a
  floating-point model of the equilibrium problem, used only for the statement about $n=4$). The AI referees of the two
  extensions wrote independent implementations (the machine at odd $a$, the identity of Lemma~\ref{lem:identity} with its
  own arithmetic in $\QQ(i,\sqrt d)$, entrywise and Newton-polygon checks, interval margins with mpmath, the PSLQ runs);
  for this revision the ten certificates were re-run, bit for bit, and every number of Section~\ref{sec:ext} and
  Section~\ref{sec:closed-ext} was recomputed with separate code.
\end{itemize}
The scripts are in the folder \texttt{scripts/paper} of the repository \cite{PiTwoRepo} (those
for Section~\ref{sec:M1} in \texttt{scripts/paper/m1}), with a README that gives the command line for each of them and
the small result files quoted here. Not included are the referees' own check scripts (apart from \texttt{dual\_ref.py})
and the earlier script that produced the exact profiles for $h\le128$ in Table~\ref{tab:evidence}; those profiles are
included as data, and \texttt{u\_profile.py} computes the same quantities (checked at $h=16$). The scripts for general
$m$ named above are in \texttt{scripts/paper/v}.
The scripts of the extensions named above are in \texttt{scripts/paper/ext/vodd} and \texttt{scripts/paper/ext/ti2}.

\subsection{Numerical evidence}
Table~\ref{tab:evidence} shows exact scores at $m=2$, and Table~\ref{tab:evidenceV} at other $m$. The arithmetic column
is $h^{-2}\sum_pn_p\log p$ for the exact contents, so the score is the sum of the two previous columns. The values approach
the limits slowly, as $O(\log h/h)$.

\begin{table}[ht]
\centering
\begin{tabular}{@{}rcccr@{}}
\toprule
$h$ & score $h^{-2}\log|F_h(T)|$ & analytic & arithmetic & $n_2$\\
\midrule
16 & $-0.2930$ & $-1.4379$ & $1.1449$ & 54\\
32 & $-0.1734$ & $-1.4195$ & $1.2462$ & 142\\
64 & $-0.1147$ & $-1.4015$ & $1.2869$ & 350\\
96 & $-0.0951$ & $-1.3930$ & $1.2980$ & 576\\
128 & $-0.0764$ & $-1.3876$ & $1.3112$ & 830\\
192 & $-0.0659$ & $-1.3815$ & $1.3156$ & 1344\\
256 & $-0.0596$ & $-1.3781$ & $1.3185$ & 1918\\
\bottomrule
\end{tabular}
\caption{Exact scores for Corollary~\ref{thm:U} ($m=2$). At $h=192$ and $256$ the contents are proved lower bounds for
each $n_p$ (fast content computation), which can only make the score look worse.}\label{tab:evidence}
\end{table}

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}rrcccr@{}}
\toprule
$m$ & $h$ & score & analytic & arithmetic & $n_2$\\
\midrule
4 & 16 & $-0.5479$ & $-1.7948$ & $1.2469$ & 94\\
4 & 32 & $-0.3829$ & $-1.7739$ & $1.3910$ & 349\\
4 & 48 & $-0.3502$ & $-1.7637$ & $1.4135$ & 737\\
4 & 64 & $-0.3142$ & $-1.7572$ & $1.4429$ & 1277\\
4 & 96 & $-0.2903$ & $-1.7491$ & $1.4587$ & 2721\\
4 & 128 & $-0.2662$ & $-1.7443$ & $1.4781$ & 4733\\
6 & 32 & $-0.5176$ & $-1.9798$ & $1.4622$ & 142\\
6 & 64 & $-0.4434$ & $-1.9639$ & $1.5205$ & 350\\
8 & 32 & $-0.5976$ & $-2.1254$ & $1.5278$ & 558\\
8 & 64 & $-0.5096$ & $-2.1097$ & $1.6001$ & 2205\\
11 & 32 & $-0.5330$ & $-2.2865$ & $1.7534$ & 196\\
11 & 48 & $-0.4407$ & $-2.2769$ & $1.8362$ & 401\\
\midrule
3 & 32 & $-0.1326$ & $-1.6267$ & $1.4941$ & 196\\
3 & 48 & $-0.0734$ & $-1.6165$ & $1.5431$ & 401\\
\bottomrule
\end{tabular}
\caption{Exact scores at other $m$. The row $m=3$ is in $\cE$ and is not evidence for it (its score rises to $-0.0340$ at
$h=64$). At $m=4$, $h=96,128$, the first computation gave proved lower bounds for the contents; an independent exact
computation gave the same values.}\label{tab:evidenceV}
\end{table}

\subsection{Controls}
No false instance of the method is available, since no unit with rational $\chi_2$ is known. As substitutes: the proved
finite-$h$ bound of Remark~\ref{rem:effective} lies above the exact score at every tested $h$, and every per-prime
inequality holds on the exact profiles, often with equality; for a unit of norm $+1$ the reflection breaks (for the untwisted machine; with $\chi_4$ on the
atoms it holds again, Remark~\ref{rem:signrule}); with poles
on one side only the conjugate place costs $+0.50$ per $h^2$ at $h=16$; and at the points $\sqrt2-1$ and $\varphi^{-1}$ the
corresponding scores are positive (primal lower bounds $+0.3286$ and $+0.6572$ for the limiting exponent), so the
method does not conclude there. At $\sqrt2-1=z_1$ the exact scores are positive and rising (Section~\ref{sec:margins}),
and Lemma~\ref{lem:P} fails at $\ell\mid m$ (Section~\ref{sec:nonvan}), as it must. For Theorem~\ref{thm:M1}, the
method does not conclude at $n=6$ ($M_1(6)\approx+0.477$), $n=400$ ($M_1(400)\ge+0.070$) or $n=720$ (numerical values).

\section*{Acknowledgements and disclosure}
% Updated after the whole-paper referee of this revision (REFEREE_PAPER_V.md, 2026-11-08), and after the whole-paper
% referee of the extensions revision (REFEREE_PAPER_EXT.md, 2026-11-08).
The research, the construction, the proofs, the certificate programs, the Lean formalisation, the literature searches and
the text of this paper were produced largely by AI models (Claude, Anthropic), working under the direction of the author.
Apart from the check by the Lean kernel, all verification so far, including the internal reviews of the argument by AI
referees, was carried out by AI systems. The proof of Theorem~\ref{thm:V} for general $m$ was checked by one AI referee,
at a single gate, with an independent implementation of the machine, and it is formalised in Lean
(Section~\ref{sec:lean}). No MathSciNet search or expert query has been made for it. The text of this revision, which
adds Theorem~\ref{thm:V}, was reviewed as a whole by one further AI referee. The extensions of Section~\ref{sec:ext}
(Theorems~\ref{thm:Vodd} and~\ref{thm:Vi}) were each checked by one AI gate referee, with independent code, and both
are formalised in Lean (Section~\ref{sec:lean}); no human has checked them, and no MathSciNet search or expert query has been made for them. The text of the
present revision, which adds these extensions, was reviewed as a whole by one further AI referee. No human expert has yet reviewed the mathematics or the Lean code; we would be grateful for corrections. The
prime number theorem in the formalisation is ported from the PrimeNumberTheoremAnd project of A.~Kontorovich, T.~Tao and
collaborators \cite{PNTplus}, through the \lean{zeta5} repository of C\'esar Del Solar \cite{zeta5} and the formalisation
of \cite{Chi2Paper}.

\bibliographystyle{amsplain}
\bibliography{references}

\end{document}