\documentclass[11pt]{amsart}

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

% ---------------------------------------------------------------------------
% 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{\CC}{\mathbb{C}}
\newcommand{\cN}{\mathcal{N}}
\newcommand{\cE}{\mathcal{E}}
\newcommand{\cF}{\mathcal{F}}
\newcommand{\Acert}{A_{\mathrm{cert}}}
\newcommand{\Abody}{A_{\mathrm{body}}}
\newcommand{\etafar}{\eta_{\mathrm{far}}}
\newcommand{\xtop}{x_{\mathrm{top}}}
\renewcommand{\Re}{\operatorname{Re}}
\renewcommand{\Im}{\operatorname{Im}}
\newcommand{\eps}{\varepsilon}
\newcommand{\ind}[1]{[\,#1\,]}
\newcommand{\lean}[1]{{\def\_{\textunderscore\allowbreak}\texttt{#1}}}

\begin{document}

\title{One of $\beta(4),\beta(6),\dots,\beta(36)$ is irrational}

\author{Shawn Krisman}

\subjclass[2020]{Primary 11J72; Secondary 11M06, 41A60, 68V20}
\keywords{Dirichlet beta function, irrationality, linear forms in zeta-type values,
saddle-point method, formal verification, Lean}

\date{\today}

\begin{abstract}
Let $\beta(s)=\sum_{m\ge 0}(-1)^m(2m+1)^{-s}$ be Dirichlet's beta function. We prove that at
least one of the seventeen numbers $\beta(4),\allowbreak \beta(6),\allowbreak \dots,\allowbreak \beta(36)$ is irrational. All
previous explicit results of this kind that we know of include $\beta(2)$, Catalan's constant; our statement does
not involve $\beta(2)$ at all. The proof uses the linear forms
$L_n=\sum_{t\ge0}(-1)^tR_n''(t)$ attached to a very-well-poised rational function $R_n$ with
triple integer zeros and half-integer poles. The second derivative, a $\beta$-analogue of a device
of Rivoal, removes $\beta(2)$, and a symmetry removes the odd values. The zeros of $R_n$ run
through the region of its poles, which makes every prime $p>n$ harmless. The common denominators
are controlled by a $p$-adic analysis and an arithmetic integral that we bound with an exact
rational certificate. The size of $L_n$ is bounded by an elementary estimate on the real axis,
and its nonvanishing for infinitely many $n$ follows from a saddle-point analysis along a
certified contour. The whole proof, including every numerical certificate, has been formalised
in Lean~4 with Mathlib and checked by the Lean kernel, using only Lean's three standard axioms.
\end{abstract}

\maketitle

\tableofcontents

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

For $s>0$ let
\[
  \beta(s)=\sum_{m=0}^{\infty}\frac{(-1)^m}{(2m+1)^s}
\]
be Dirichlet's beta function, the $L$-function of the non-principal character modulo $4$.

\begin{theorem}\label{thm:main}
At least one of the seventeen numbers $\beta(4),\allowbreak \beta(6),\allowbreak \beta(8),\allowbreak \dots,\allowbreak \beta(36)$ is irrational.
\end{theorem}

\subsection{Context}
The values of $\beta$ at odd integers are classical: if $E_m$ denotes the Euler numbers, defined by
$\operatorname{sech}x=\sum_{m\ge0}E_mx^m/m!$ (so $E_2=-1$), then $\beta(2k+1)=(-1)^kE_{2k}\pi^{2k+1}/(4^{k+1}(2k)!)$. For example $\beta(1)=\pi/4$ and
$\beta(3)=\pi^3/32$. So the odd values are nonzero rational multiples of odd powers of $\pi$, and
they are transcendental by Lindemann's theorem. Nothing comparable is known for the even values.
The first one, $\beta(2)$, is Catalan's constant. Our argument never uses the arithmetic nature of
$\beta(2)$.

The explicit irrationality results for even beta values that we know of all include $\beta(2)$:
\begin{itemize}
\item Rivoal and Zudilin \cite[Thm.~2]{RivoalZudilin2003} proved that at least one of
  $\beta(2),\allowbreak \beta(4),\allowbreak \dots,\allowbreak \beta(14)$ is irrational;
\item Zudilin \cite[Thm.~1]{Zudilin2019} proved the same for $\beta(2),\allowbreak \dots,\allowbreak \beta(12)$;
\item Lai and Zhou \cite[Thm.~6.1]{LaiZhou2021} proved it for $\beta(2),\allowbreak \dots,\allowbreak \beta(10)$.
\end{itemize}
Such a statement holds as soon as $\beta(2)$ is irrational, and then it says nothing about
$\beta(4),\allowbreak \beta(6),\dots$. A proof that $\beta(2)$ is irrational has recently been claimed in an
AI-generated preprint with an accompanying Lean formalisation \cite{OpenAICatalan2026}; it has not
been refereed, and we have not checked it. Theorem~\ref{thm:main} does not depend on the arithmetic
nature of $\beta(2)$ in any way. Rivoal and Zudilin \cite[Thm.~1]{RivoalZudilin2003} also proved a lower
bound of order $\log a$ for the dimension of the $\QQ$-vector space spanned by $1$ and the even
values $\beta(2),\allowbreak \dots,\allowbreak \beta(a)$; Fischler \cite{Fischler2020} proved results of the same type for
general Dirichlet $L$-values of a fixed parity. A dimension at least $3$ forces one of
$\beta(4),\allowbreak \dots,\allowbreak \beta(a)$ to be irrational, so these results give a $\beta(2)$-free statement
qualitatively, for some computable $a$. We have not found an explicit value of $a$ in the
literature. Even ignoring error terms, the constant $1/(2+\log 2)$ of \cite{RivoalZudilin2003}
would require $\log a\ge 3(2+\log2)$, that is, $a\approx3\cdot10^3$, and the constant
$1/(1+\log2)$ of \cite{Fischler2020} would require $\log a\ge3(1+\log2)$, that is, $a\approx160$.

To our knowledge, Theorem~\ref{thm:main} is the first explicit irrationality statement about the
even values of $\beta$ that does not involve $\beta(2)$. Our literature search covered arXiv and
the web, but not MathSciNet or zbMATH; we would be grateful to hear of prior work.

\subsection{The method}
We follow the now standard approach of Ball and Rivoal \cite{BallRivoal2001} through linear forms
with rational coefficients. The new
features are the following.
\begin{enumerate}
\item \emph{Removing $\beta(2)$.} We use $L_n=\sum_{t\ge0}(-1)^tR_n''(t)$, where $R_n$ has triple zeros
  at the integers of $\Lambda_n=[-(1+r)n-1,\,rn]$ and poles at half-integers. This adapts to alternating sums and half-integer
  poles the second-derivative device of Rivoal \cite{Rivoal2002} (see also
  \cite[\S8, Lemma~19]{Zudilin2004}), which was introduced for odd zeta values. Differentiating twice
  raises every exponent by $2$, so $\beta(2)$ cannot occur, and a reflection symmetry kills the
  odd-index values (Section~\ref{sec:algebra}).
\item \emph{Zeros through the pole region.} As in the constructions of Zudilin \cite{Zudilin2019}
  and Lai--Zhou \cite{LaiZhou2021}, the integer zeros of $R_n$ run through the whole region
  $[-n-\frac12,-\frac12]$ where the poles $-k-\frac12$ ($0\le k\le n$) lie; $[-n,-1]$ is the set of
  integers in that region. For the second-derivative form this
  requires triple zeros there. Its effect (Lemma~\ref{lem:C}) is that the primes $p>n$ do not
  contribute to the denominators at all.
\item \emph{An optimised block profile.} The denominator of $R_n$ is a product of $35$ ``blocks''
  $\prod_{k=\delta n}^{(1-\delta)n}(t+k+\frac12)$ counted with multiplicity ($28$ distinct offsets;
  $\delta=0$ occurs $8$ times). The other offsets have spacing $\frac1{160}$ on $(0,\frac1{20}]$ and
  $\frac1{80}$ on $[\frac1{16},\frac{23}{80}]$ (Table~\ref{tab:blocks}). The profile was found by a numerical search.
\item \emph{Certified numerics.} The arithmetic integral that governs the denominators is a sum
  over $62{,}131$ intervals. We evaluate it exactly in rational arithmetic
  (Section~\ref{sec:A}). The size of $L_n$ is bounded on the real axis (Section~\ref{sec:size}).
  Its nonvanishing comes from a saddle point whose location, value and steepest-descent contour
  are certified by interval arithmetic (Section~\ref{sec:nonvan}).
\item \emph{Formalisation.} Every step, including all the computations, has been formalised in
  Lean~4 \cite{LeanFour} and Mathlib \cite{Mathlib} (Section~\ref{sec:lean}).
\end{enumerate}
The numerical margin is small: the exponent that must be negative is
$Q=V+\Acert+20\log2<-0.0714$, see \eqref{eq:Q}. Here $V$ bounds the size of $L_n$
(Proposition~\ref{prop:Phi}), $\Acert$ is the arithmetic integral (Proposition~\ref{prop:certA}), and
$20\log2$ is the $2$-adic cost of the denominators (Proposition~\ref{prop:smallprimes}).

\subsection{The formalisation}
The statement of Theorem~\ref{thm:main} and its complete proof, including the prime number theorem,
complex Stirling bounds, the contour-integral representation, the arithmetic certificate and the
interval-arithmetic saddle-point certificate, are formalised in Lean~4 with Mathlib and checked by
the Lean kernel. The proof depends only on Lean's three standard axioms (\lean{propext},
\lean{Classical.choice}, \lean{Quot.sound}). It contains no \lean{sorry} and no \lean{native\_decide}:
every proof, including every computation, is checked by the kernel. The formal statement and what it means are described in
Section~\ref{sec:lean}. The repository is \url{https://github.com/telaviv/beta-irrationality}.

The prose proof below is self-contained and can be read without the formalisation, except that
certain finite computations are only described, not reproduced: the exact value of a rational sum
with $62{,}131$ terms (Proposition~\ref{prop:certA}), $58$ logarithm enclosures
(Proposition~\ref{prop:Phi}), and the interval-arithmetic checks of the saddle-point data
(Theorem~\ref{thm:saddle}). The arithmetic certificate and the saddle certificate are decidable
statements about rational data, proved by \lean{decide +kernel}; the $58$ logarithm enclosures of
Proposition~\ref{prop:Phi} are proved by \lean{norm\_num} from Mathlib's series bounds for $\log$. All
proofs are checked by the Lean kernel.

\subsection{Organisation and notation}
Section~\ref{sec:construction} defines $R_n$ and $L_n$. Section~\ref{sec:algebra} shows that
$L_n\in\QQ+\QQ\beta(4)+\dots+\QQ\beta(36)$. Section~\ref{sec:arith} constructs a common denominator
$D_n$, and Section~\ref{sec:A} bounds its size through the arithmetic integral. Section~\ref{sec:size}
bounds $|L_n|$, and Section~\ref{sec:nonvan} proves that $L_n\ne0$ for infinitely many $n$.
Section~\ref{sec:proof} combines these results. Section~\ref{sec:lean} describes the formalisation,
and Section~\ref{sec:remarks} contains remarks on limits of the method.

Throughout, $p$ denotes a prime and $v_p$ the $p$-adic valuation on $\QQ$, with $v_p(0)=+\infty$. $\lfloor\cdot\rfloor$,
$\lceil\cdot\rceil$ and $\{\cdot\}$ are the floor, ceiling and fractional part; $\ind{P}$ is $1$ if
$P$ holds and $0$ otherwise; $\#$ denotes cardinality; intervals $[a,b]$ of integers are written in
the same way as real intervals when no confusion can arise. $F(y):=y\log y$ with the principal branch
of the logarithm, and $F(0):=0$. We write $\theta(y)=\sum_{p\le y}\log p$ for Chebyshev's function.
For a power series $g$ in $\eps$, $[\eps^M]g$ is the coefficient of $\eps^M$.

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

\subsection{Parameters}
Fix the following data.
\begin{itemize}
\item $r=7/6$, and $n$ runs through the multiples of $q=480$: $n=480N_0$ with $N_0\in\NN$, $N_0\ge1$.
  Then $rn=560N_0$ and $(1+r)n=1040N_0$ are integers, and $n$ is even.
\item Twenty-eight \emph{blocks} $j=1,\allowbreak \dots,28$ with offsets $\delta_j$ and multiplicities $m_j$:
  $(\delta_1,m_1)=(0,8)$, and $(\delta_j,m_j)=(\kappa/160,1)$ for the $27$ values
  \[
    \kappa\in\{1,2,3,4,5,6,7,8\}\cup\{10,12,14,\allowbreak \dots,46\}.
  \]
  We write $a_j:=\delta_jn=3\kappa N_0$ (with $\kappa=0$ for $j=1$), $b_j:=n-a_j$ and $I_j:=[a_j,b_j]\cap\ZZ$. Since
  $\delta_j\le 46/160<\frac12$, each $I_j$ is a nonempty integer interval, symmetric under
  $k\mapsto n-k$, and $\#I_j=(1-2\delta_j)n+1$.
\end{itemize}

\begin{table}[ht]
\centering
\begin{tabular}{@{}p{0.36\textwidth}p{0.58\textwidth}@{}}
\toprule
quantity & value\\
\midrule
$r$, $q$ & $7/6$, $480$\\
blocks $(\delta_j,m_j)$ & $(0,8)$; $(\kappa/160,1)$ for $\kappa=1,\allowbreak \dots,8$ and $\kappa=10,12,\allowbreak \dots,46$\\
number of blocks & $28$\\
$S=\sum_jm_j$ & $35$\\
$\sum_jm_j(1-2\delta_j)$ & $279/10$\\
$G=\sum_jm_j(1-2\delta_j)-6r-3$ & $179/10$\\
zero set $\Lambda_n$ & $[-(1+r)n-1,\,rn]\cap\ZZ=[-1040N_0-1,\,560N_0]$, each of order $3$\\
$Z=3\#\Lambda_n$ & $10n+6$\\
$\cN=2(2+r)n+3$ & $\frac{19}{3}n+3=3040N_0+3$\\
\bottomrule
\end{tabular}
\caption{The parameters.}\label{tab:blocks}
\end{table}

For $0\le k\le n$ put
\[
  B_k:=\sum_{j=1}^{28}m_j\,\ind{k\in I_j}.
\]
The block $j=1$ is $[0,n]$, so $8\le B_k\le 35$ for all $0\le k\le n$, and $B_{n-k}=B_k$. The
constants
\begin{equation}\label{eq:G}
  S:=\sum_jm_j=35,\qquad G:=\sum_jm_j(1-2\delta_j)-6r-3=\frac{279}{10}-10=\frac{179}{10}
\end{equation}
will appear throughout. (Here $\sum_jm_j(1-2\delta_j)=8+27-\frac{1}{80}\sum\kappa=35-\frac{568}{80}$.)
We also put
\[
  \cN:=2(2+r)n+3=\tfrac{19}{3}n+3=3040N_0+3;
\]
in Section~\ref{sec:arith} every integer whose $p$-adic valuation we need has absolute value $<\cN$.

\subsection{The rational function and the linear form}
Let $\Lambda_n:=[-(1+r)n-1,\,rn]\cap\ZZ$; it has $(1+2r)n+2=1600N_0+2$ elements. Define
\begin{equation}\label{eq:R}
  R_n(t):=\frac{(2t+n+1)\prod_{l\in\Lambda_n}(t-l)^3}{\prod_{j=1}^{28}\prod_{k\in I_j}(t+k+\tfrac12)^{m_j}}
  =\frac{(2t+n+1)\prod_{l\in\Lambda_n}(t-l)^3}{\prod_{k=0}^{n}(t+k+\tfrac12)^{B_k}},
\end{equation}
and
\begin{equation}\label{eq:L}
  L_n:=\sum_{t=0}^{\infty}(-1)^tR_n''(t).
\end{equation}

\begin{lemma}\label{lem:counts}
Put $Z:=3\#\Lambda_n=10n+6$. Then $\sum_{k=0}^nB_k=\sum_jm_j\#I_j=(G+10)n+35$, and
\[
  \deg R_n=1+Z-\sum_kB_k=-Gn-28 .
\]
In particular $R_n(t)=O(t^{-3})$, $R_n''(t)=O(t^{-5})$ as $t\to\infty$, and the series \eqref{eq:L}
converges absolutely.
\end{lemma}

\begin{proof}
$\#\Lambda_n=(1+2r)n+2$ and $3(1+2r)=10$ give $Z=10n+6$. Next,
$\sum_jm_j\#I_j=\sum_jm_j((1-2\delta_j)n+1)=\frac{279}{10}n+35=(G+10)n+35$. The degree is
$1+10n+6-(G+10)n-35$. The asymptotics follow because $Gn+28\ge 3$.
\end{proof}

The factor $2t+n+1$ (``the $e$-factor'') fixes the parity needed in Lemma~\ref{lem:sym}. Its zero
$t=-\frac{n+1}{2}=-\frac n2-\frac12$ coincides with the central pole, where $B_{n/2}=35$; so the pole at $-\frac{n+1}2$ has order $34$,
and $a_{35,n/2}=0$ in Lemma~\ref{lem:pf} below. This causes no difficulty.

\begin{lemma}\label{lem:sym}
$R_n(-n-1-t)=R_n(t)$.
\end{lemma}

\begin{proof}
The map $l\mapsto -n-1-l$ is a bijection of $\Lambda_n$ onto itself, because
$-n-1-(-(1+r)n-1)=rn$. Hence
$\prod_{l\in\Lambda_n}(-n-1-t-l)^3=(-1)^{3\#\Lambda_n}\prod_{l\in\Lambda_n}(t-l)^3$, and
$3\#\Lambda_n=10n+6$ is even. The $e$-factor becomes $2(-n-1-t)+n+1=-(2t+n+1)$. In the denominator,
$-n-1-t+k+\frac12=-(t+(n-k)+\frac12)$ and $B_{n-k}=B_k$, so the denominator is multiplied by
$(-1)^{\sum_kB_k}=(-1)^{(G+10)n+35}=-1$, since $(G+10)n=13392N_0$ is even. The two signs cancel.
\end{proof}

Lemma~\ref{lem:sym} is what makes $R_n$ \emph{very-well-poised}, in the terminology of
\cite{Zudilin2004}: in the term ratio $R_n(t+1)/R_n(t)$ every upper parameter pairs with a lower one
with sum $n+2$, the factor $2t+n+1$ supplying the very-well-poised pair.

\begin{remark}
Consider more generally a function of the same shape, with arbitrary parameters $r$ and blocks, triple
zeros at every integer of the pole region, and the $e$-factor raised to a power $e\in\{0,1\}$. For
such parameters the symmetry reads $R_n(-n-1-t)=(-1)^nR_n(t)$, which needs
$(-1)^{\deg R_n}=(-1)^n$, i.e.\ $e\equiv(G+1)n+S\pmod2$. Since $q(G+1)=9072$ is even, $e=1$ works for
all $n\in480\NN$. Only the specific parameters of Table~\ref{tab:blocks} are used below.
\end{remark}

% ===========================================================================
\section{\texorpdfstring{The linear form lies in $\QQ+\QQ\beta(4)+\dots+\QQ\beta(36)$}{The linear form lies in Q + Q beta(4) + ... + Q beta(36)}}\label{sec:algebra}
% ===========================================================================

For $k\ge0$ and $j\ge1$ put
\[
  \sigma_k^{(j)}:=\sum_{m=0}^{k-1}\frac{(-1)^m}{(2m+1)^j}\in\QQ .
\]
For $0\le k\le n$ define the power series in $\QQ[[\eps]]$
\begin{equation}\label{eq:fk}
  f_k(\eps):=(n-2k+2\eps)\prod_{l\in\Lambda_n}(u_{k,l}+\eps)^3\prod_{\substack{0\le k'\le n\\k'\ne k}}(k'-k+\eps)^{-B_{k'}},
\end{equation}
where
\[
  u_{k,l}:=-k-\tfrac12-l=-\tfrac{w_{k,l}}{2},\qquad w_{k,l}:=2k+1+2l,
\]
and $(d+\eps)^{-1}=\sum_{M\ge0}(-1)^Md^{-M-1}\eps^M$ for $d\ne0$. Note that $w_{k,l}$ is an odd
integer. When $k$ is fixed we write simply $u_l$ and $w_l$. If $t_0:=-k-\frac12$, then $f_k(\eps)$ is the Taylor expansion at $\eps=0$ of
$R_n(t_0+\eps)(t_0+\eps+k+\frac12)^{B_k}$.

\begin{lemma}[Partial fractions]\label{lem:pf}
Put $a_{i,k}:=[\eps^{B_k-i}]f_k$ for $0\le k\le n$, $1\le i\le B_k$, and $a_{i,k}:=0$ for
$i>B_k$. Then $a_{i,k}\in\QQ$ and, for every $t\in\CC\setminus\{-k-\frac12:0\le k\le n\}$,
\[
  R_n(t)=\sum_{k=0}^{n}\sum_{i=1}^{35}\frac{a_{i,k}}{(t+k+\frac12)^i} .
\]
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:counts} the numerator of \eqref{eq:R} has smaller degree than the denominator, so
$R_n$ equals the sum of its principal parts at the distinct points $-k-\frac12$. The principal part at
$t_0=-k-\frac12$ is $\sum_{i=1}^{B_k}a_{i,k}(t-t_0)^{-i}$, where $a_{i,k}$ is the coefficient of
$(t-t_0)^{B_k-i}$ in the Taylor expansion of $R_n(t)(t-t_0)^{B_k}$, which is $f_k$. Since $B_k\le 35$,
all $i\le 35$ are covered.
\end{proof}

\begin{lemma}\label{lem:altsum}
For integers $j\ge2$ and $k\ge0$,
\[
  \sum_{t=0}^{\infty}\frac{(-1)^t}{(t+k+\frac12)^j}=(-1)^k2^j\bigl(\beta(j)-\sigma_k^{(j)}\bigr).
\]
\end{lemma}

\begin{proof}
$(t+k+\frac12)^{-j}=2^j(2(t+k)+1)^{-j}$. Substituting $m=t+k$ gives
$(-1)^k2^j\sum_{m\ge k}(-1)^m(2m+1)^{-j}$, and the series converges absolutely.
\end{proof}

\begin{proposition}[Expansion]\label{prop:expansion}
Define
\begin{gather*}
  \tau_i:=\sum_{k=0}^{n}(-1)^k\,2^{i+2}\,i(i+1)\,a_{i,k},\\
  \rho_n:=-\sum_{k=0}^{n}\sum_{i=1}^{35}(-1)^k\,2^{i+2}\,i(i+1)\,a_{i,k}\,\sigma_k^{(i+2)} .
\end{gather*}
Then $\rho_n,\tau_i\in\QQ$ and $L_n=\rho_n+\sum_{i=1}^{35}\tau_i\,\beta(i+2)$.
\end{proposition}

\begin{proof}
For real $t>-\frac12$, Lemma~\ref{lem:pf} may be differentiated termwise:
$R_n''(t)=\sum_{k,i}a_{i,k}\,i(i+1)(t+k+\frac12)^{-i-2}$. Multiply by $(-1)^t$ and sum over $t\ge0$.
This is a finite sum of absolutely convergent series, so the order of summation may be exchanged,
and Lemma~\ref{lem:altsum} with $j=i+2\ge3$ gives the claim.
\end{proof}

\begin{lemma}[Symmetry]\label{lem:tau-odd}
$a_{i,n-k}=(-1)^ia_{i,k}$ for all $i,k$. Consequently $\tau_i=0$ for every odd $i$.
\end{lemma}

\begin{proof}
By Lemmas~\ref{lem:sym} and~\ref{lem:pf},
\[
  R_n(t)=R_n(-n-1-t)=\sum_{k,i}\frac{a_{i,k}}{(-n-1-t+k+\frac12)^i}
  =\sum_{k,i}\frac{(-1)^ia_{i,k}}{(t+(n-k)+\frac12)^i}.
\]
Uniqueness of the partial-fraction decomposition gives $a_{i,n-k}=(-1)^ia_{i,k}$. For odd $i$,
substituting $k\mapsto n-k$ in the definition of $\tau_i$ and using that $n$ is even gives
$\tau_i=\sum_k(-1)^{n-k}2^{i+2}i(i+1)(-1)^ia_{i,k}=-\tau_i$.
\end{proof}

\begin{corollary}\label{cor:form}
$L_n=\rho_n+\sum_{j=2}^{18}\tau_{2j-2}\,\beta(2j)\in\QQ+\QQ\beta(4)+\QQ\beta(6)+\dots+\QQ\beta(36)$.
In particular $\beta(2)$ does not occur.
\end{corollary}

\begin{proof}
In Proposition~\ref{prop:expansion} only $\beta(i+2)$ with $1\le i\le35$ occurs. By
Lemma~\ref{lem:tau-odd} only even $i=2j-2$ with $2\le j\le18$ survive.
\end{proof}

% ===========================================================================
\section{Denominators}\label{sec:arith}
% ===========================================================================

Recall $\cN=2(2+r)n+3=\frac{19}{3}n+3$. For $k\in[0,n]$ and $l\in\Lambda_n$ we have
$|w_l|=|2k+1+2l|\le 2(1+r)n+1<\cN$, and for $k,k'\in[0,n]$ we have $|k'-k|\le n<\cN$.

\subsection{Valuations of the Taylor coefficients}

\begin{definition}
Let $p$ be a prime and $e,\lambda\in\ZZ$. A power series $g\in\QQ[[\eps]]$ is
\emph{$(e,\lambda)$-bounded at $p$} if $v_p([\eps^M]g)\ge e-\lambda M$ for all $M\ge0$.
\end{definition}

\begin{lemma}\label{lem:psge}
Let $p$ be a prime and $\lambda\in\ZZ$.
\begin{enumerate}
\item If $g_1$ is $(e_1,\lambda)$-bounded and $g_2$ is $(e_2,\lambda)$-bounded at $p$, then $g_1g_2$ is
  $(e_1+e_2,\lambda)$-bounded at $p$.
\item If $u,c\in\QQ$ with $v_p(u)\ge e$ and $v_p(c)\ge e-\lambda$, then $u+c\eps$ is
  $(e,\lambda)$-bounded at $p$.
\item If $d\in\QQ\setminus\{0\}$ with $v_p(d)\le\lambda$ and $e\le -v_p(d)$, then $(d+\eps)^{-1}$
  is $(e,\lambda)$-bounded at $p$.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) $[\eps^M](g_1g_2)=\sum_{a+b=M}[\eps^a]g_1\,[\eps^b]g_2$, and each term has valuation
$\ge e_1-\lambda a+e_2-\lambda b=e_1+e_2-\lambda M$. (2) is immediate. (3) The coefficient of
$\eps^M$ is $(-1)^Md^{-M-1}$, of valuation $-v_p(d)-Mv_p(d)\ge e-\lambda M$.
\end{proof}

\begin{lemma}[Lemma A]\label{lem:A}
Let $p$ be a prime, $\lambda\ge0$ an integer and $0\le k\le n$. Let $e_E\in\ZZ$, $e_l\in\ZZ$
$(l\in\Lambda_n)$ and $e_{k'}\in\ZZ$ $(k'\in[0,n]\setminus\{k\})$ satisfy
\begin{itemize}
\item $v_p(n-2k)\ge e_E$ and $v_p(2)\ge e_E-\lambda$;
\item $v_p(u_l)\ge e_l$ and $e_l\le\lambda$ for every $l\in\Lambda_n$;
\item $v_p(k'-k)\le\lambda$ and $e_{k'}\le -v_p(k'-k)$ for every $k'\ne k$.
\end{itemize}
Put $\nu:=e_E+3\sum_{l\in\Lambda_n}e_l+\sum_{k'\ne k}B_{k'}e_{k'}$. Then $f_k$ is
$(\nu,\lambda)$-bounded at $p$, and $v_p(a_{i,k})\ge \nu-\lambda(B_k-i)$ for $1\le i\le B_k$.
\end{lemma}

\begin{proof}
Apply Lemma~\ref{lem:psge}(2) to $n-2k+2\eps$ and to each $u_l+\eps$ (here $v_p(1)=0\ge e_l-\lambda$),
Lemma~\ref{lem:psge}(3) to each $(k'-k+\eps)^{-1}$, and Lemma~\ref{lem:psge}(1) to the product
\eqref{eq:fk}. The bound for $a_{i,k}=[\eps^{B_k-i}]f_k$ follows.
\end{proof}

For an odd prime $p$ and $0\le k\le n$ define
\begin{gather*}
  c_p(k):=3\,\#\{l\in\Lambda_n:p\mid w_l\}+\ind{p\mid n-2k},\\
  P_{p,j}(k):=\#\{k'\in I_j\setminus\{k\}:p\mid k'-k\},\\
  \eps_p(k):=c_p(k)-\sum_jm_jP_{p,j}(k),\\
  \nu_p(k):=3\sum_{l\in\Lambda_n}v_p(w_l)-\sum_{k'\ne k}B_{k'}\,v_p(k'-k),
\end{gather*}
and for $p=2$
\[
  \nu_2(k):=1-Z-\sum_{k'\ne k}B_{k'}\,v_2(k'-k).
\]
Note $\sum_{k'\ne k}B_{k'}g(k')=\sum_jm_j\sum_{k'\in I_j\setminus\{k\}}g(k')$ for any $g$. Put
$\lambda_p:=\lfloor\log_p\cN\rfloor$ for odd $p$, and $\lambda_2:=\lfloor\log_2n\rfloor$.

\begin{corollary}\label{cor:A}
Let $0\le k\le n$ and $1\le i\le B_k$.
\begin{enumerate}
\item[(a)] If $p$ is odd and $p>n$, then $a_{i,k}\in\ZZ_{(p)}$, i.e.\ $v_p(a_{i,k})\ge0$.
\item[(b)] If $p$ is odd and $p^2>\cN$, then $v_p(a_{i,k})\ge \eps_p(k)-(B_k-i)$.
\item[(c)] If $p$ is odd, then $v_p(a_{i,k})\ge \nu_p(k)-\lambda_p(B_k-i)$.
\item[(d)] $v_2(a_{i,k})\ge \nu_2(k)-\lambda_2(B_k-i)$.
\end{enumerate}
\end{corollary}

\begin{proof}
We apply Lemma~\ref{lem:A}. Since $p$ is odd in (a)--(c), $v_p(u_l)=v_p(w_l)\ge0$ and $v_p(2)=0$.
\begin{enumerate}
\item[(a)] Take $\lambda=0$ and all exponents $0$. For $k'\ne k$, $0<|k'-k|\le n<p$, so
  $v_p(k'-k)=0$.
\item[(b)] Take $\lambda=1$, $e_E=\ind{p\mid n-2k}$, $e_l=\ind{p\mid w_l}$ and
  $e_{k'}=-\ind{p\mid k'-k}$. Since $0<|k'-k|<\cN<p^2$, $v_p(k'-k)=\ind{p\mid k'-k}\le1$. When
  $n=2k$ the condition $v_p(n-2k)\ge e_E$ holds trivially, as $v_p(0)=+\infty$. Here $\nu=\eps_p(k)$.
\item[(c)] Take $\lambda=\lambda_p$, $e_E=0$, $e_l=v_p(w_l)$ and $e_{k'}=-v_p(k'-k)$. Since
  $0<|w_l|,|k'-k|<\cN<p^{\lambda_p+1}$, both valuations are $\le\lambda_p$. Here $\nu=\nu_p(k)$.
\item[(d)] Take $\lambda=\lambda_2$, $e_E=1$ (as $n$ is even, $v_2(n-2k)\ge1$, and
  $v_2(2)=1\ge1-\lambda_2$), $e_l=-1$ (as $w_l$ is odd, $v_2(u_l)=-1$) and $e_{k'}=-v_2(k'-k)$,
  which is admissible because $|k'-k|\le n<2^{\lambda_2+1}$. Here $\nu=1-3\#\Lambda_n-\sum
  B_{k'}v_2(k'-k)=\nu_2(k)$.\qedhere
\end{enumerate}
\end{proof}

\subsection{Partial sums}

\begin{lemma}[Lemma B]\label{lem:B}
Let $p$ be a prime, $\lambda\ge0$ and $k\ge0$, and suppose $v_p(2m+1)\le\lambda$ for all $0\le m<k$.
Then $v_p(\sigma_k^{(j)})\ge -j\lambda$. In particular, for $0\le k\le n$:
$v_p(\sigma_k^{(j)})\ge -j$ if $p$ is odd and $p^2>\cN$; $v_p(\sigma_k^{(j)})\ge-j\lambda_p$ if $p$ is odd; and
$v_2(\sigma_k^{(j)})\ge0$.
\end{lemma}

\begin{proof}
Each term $(-1)^m(2m+1)^{-j}$ has valuation $\ge-j\lambda$. For $m<k\le n$ we have
$0<2m+1<2n<\cN$, which gives the three special cases.
\end{proof}

\subsection{\texorpdfstring{The primes $p>n$}{The primes p > n}}

\begin{lemma}[Lemma C]\label{lem:C}
Let $p$ be an odd prime with $p>n$. Then $\rho_n\in\ZZ_{(p)}$.
\end{lemma}

\begin{proof}
For $j\ge1$ and $k\ge0$, substituting $l=k-m$ gives
\begin{equation}\label{eq:Bexpand}
  (-1)^k2^j\sigma_k^{(j)}=\sum_{l=1}^{k}\frac{(-1)^l}{(k-l+\frac12)^j}.
\end{equation}
For $1\le l\le n$ and $0\le k\le n$ put
$T(l,k):=\sum_{i}a_{i,k}\,i(i+1)\,(k-l+\frac12)^{-i-2}$. By \eqref{eq:Bexpand},
\[
  \rho_n=-\sum_{k=0}^{n}\sum_{l=1}^{k}(-1)^lT(l,k)=-\sum_{l=1}^{n}(-1)^l\sum_{k=l}^{n}T(l,k).
\]
It suffices to show that $\sum_{k\ge l}T(l,k)\in\ZZ_{(p)}$ for each $1\le l\le n$.

By Lemma~\ref{lem:pf}, $\sum_{k=0}^nT(l,k)=R_n''(-l)$. Since $-l\in[-n,-1]\subset\Lambda_n$, the
point $-l$ is a zero of order $3$ of $R_n$ and is not a pole, so $R_n''(-l)=0$. Hence
\begin{equation}\label{eq:Csplit}
  \sum_{k=l}^{n}T(l,k)=-\sum_{k=0}^{l-1}T(l,k).
\end{equation}
By Corollary~\ref{cor:A}(a), $a_{i,k}\in\ZZ_{(p)}$, and $(k-l+\frac12)^{-1}=2/(2(k-l)+1)$. So $T(l,k)$
is $p$-integral unless $p\mid 2(k-l)+1$. Suppose that $p\mid 2(k_1-l)+1$ for some $k_1\ge l$ and
$p\mid 2(k_2-l)+1$ for some $k_2<l$. Then $p\mid 2(k_1-k_2)$, so $p\mid k_1-k_2$, which is impossible
because $0<k_1-k_2\le n<p$. Hence one of the two sides of \eqref{eq:Csplit} is a sum of $p$-integral
terms, and so both sides are $p$-integral.
\end{proof}

\subsection{The common denominator}

\begin{definition}\label{def:Ep}
For a prime $p$ define the integer $E_p$ by
\[
  E_p:=\begin{cases}
  \max_{0\le k\le n}\bigl(-\nu_2(k)\bigr)+35\lambda_2, & p=2,\\
  0, & p \text{ odd},\ p>n,\\
  \max_{0\le k\le n}\bigl(B_k+2-\eps_p(k)\bigr), & p \text{ odd},\ p\le n,\ p^2>\cN,\\
  \max_{0\le k\le n}\bigl(-\nu_p(k)\bigr)+37\lambda_p, & p \text{ odd},\ p^2\le\cN,
  \end{cases}
\]
(the cases are applied in this order), and put $D_n:=\prod_{p\le n}p^{E_p}\in\QQ_{>0}$.
\end{definition}

Thus $v_p(D_n)=E_p$ for every prime $p$. We do not need $E_p\ge0$ in the third range, so we only
assert $D_n\in\QQ_{>0}$.

\begin{proposition}[Integrality]\label{prop:integral}
$D_n\rho_n\in\ZZ$ and $D_n\tau_i\in\ZZ$ for all $i$.
\end{proposition}

\begin{proof}
It suffices to show $v_p(\rho_n)\ge -E_p$ and $v_p(\tau_i)\ge-E_p$ for every prime $p$. Both $\tau_i$
and $\rho_n$ are $\ZZ$-linear combinations of the numbers $a_{i,k}2^{i+2}$ and
$a_{i,k}2^{i+2}\sigma_k^{(i+2)}$ respectively, with $0\le k\le n$ and $1\le i\le B_k\le 35$. We bound these
numbers.
\begin{itemize}
\item $p$ odd, $p>n$: $a_{i,k}2^{i+2}\in\ZZ_{(p)}$ by Corollary~\ref{cor:A}(a), so $\tau_i$ is
  $p$-integral; $\rho_n$ is $p$-integral by Lemma~\ref{lem:C}.
\item $p$ odd, $p\le n$, $p^2>\cN$: by Corollary~\ref{cor:A}(b) and Lemma~\ref{lem:B},
  \[
    v_p\bigl(a_{i,k}2^{i+2}\sigma_k^{(i+2)}\bigr)\ge \eps_p(k)-(B_k-i)-(i+2)=\eps_p(k)-B_k-2\ge-E_p,
  \]
  and $v_p(a_{i,k}2^{i+2})\ge\eps_p(k)-B_k+1\ge -E_p$.
\item $p$ odd, $p^2\le\cN$: by Corollary~\ref{cor:A}(c) and Lemma~\ref{lem:B},
  \[
    v_p\bigl(a_{i,k}2^{i+2}\sigma_k^{(i+2)}\bigr)\ge\nu_p(k)-\lambda_p(B_k-i)-\lambda_p(i+2)
    \ge\nu_p(k)-37\lambda_p\ge-E_p,
  \]
  and the same bound holds without the factor $\sigma_k^{(i+2)}$.
\item $p=2$: by Corollary~\ref{cor:A}(d) and Lemma~\ref{lem:B},
  \[
    v_2\bigl(a_{i,k}2^{i+2}\sigma_k^{(i+2)}\bigr)\ge\nu_2(k)-\lambda_2(B_k-i)+i+2\ge\nu_2(k)-35\lambda_2\ge-E_2,
  \]
  and similarly without $\sigma_k^{(i+2)}$.\qedhere
\end{itemize}
\end{proof}

\begin{corollary}\label{cor:intform}
$D_nL_n=D_n\rho_n+\sum_{j=2}^{18}(D_n\tau_{2j-2})\,\beta(2j)$ is a linear form in
$1,\allowbreak \beta(4),\allowbreak \dots,\allowbreak \beta(36)$ with integer coefficients.
\end{corollary}

\subsection{\texorpdfstring{The size of $D_n$ at $p=2$ and at small primes}{The size of D\_n at p = 2 and at small primes}}

Let $s_p(N)$ denote the sum of the base-$p$ digits of $N\ge0$, and $\ell_p(N):=\lfloor\log_pN\rfloor$
for $N\ge1$, $\ell_p(0):=0$.

\begin{lemma}[Legendre-type bounds]\label{lem:legendre}
Let $p$ be a prime.
\begin{enumerate}
\item For $N\ge0$: $(p-1)v_p(N!)=N-s_p(N)$ and $0\le s_p(N)\le(p-1)(\ell_p(N)+1)$.
\item For integers $1\le A\le B+1$:
  $(p-1)\sum_{d=A}^{B}v_p(d)\le(B-A+1)+(p-1)(\ell_p(A-1)+1)$.
\item If $p$ is odd and $A\ge0$: $(p-1)\sum_{0\le m<A}v_p(2m+1)\ge A-(p-1)(\ell_p(2A)+1)$.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) is Legendre's formula, and each of the at most $\ell_p(N)+1$ digits is $\le p-1$.
(2) The sum equals $v_p(B!)-v_p((A-1)!)$; multiply by $p-1$ and use (1).
(3) Since $(2A)!=\prod_{m<A}(2m+1)\cdot2^AA!$ and $p$ is odd, the sum equals
$v_p((2A)!)-v_p(A!)$. By (1), $(p-1)$ times it is $A-s_p(2A)+s_p(A)\ge A-s_p(2A)$.
\end{proof}

\begin{lemma}\label{lem:polesum}
Let $p$ be a prime, $N\ge n$, $0\le k\le n$ and $1\le j\le 28$. Then
\[
  (p-1)\sum_{k'\in I_j\setminus\{k\}}v_p(k'-k)\le \#I_j+2(p-1)(\ell_p(N)+1).
\]
\end{lemma}

\begin{proof}
The numbers $|k'-k|$ with $k'\in I_j$, $k'>k$ form an interval $[A_1,B_1]$ of positive integers, and
those with $k'<k$ form another interval $[A_2,B_2]$; their total length is at most $\#I_j$ and
$A_i-1\le n\le N$. Apply Lemma~\ref{lem:legendre}(2) to each (an empty interval contributes $0$).
\end{proof}

\begin{proposition}\label{prop:smallprimes}
\begin{enumerate}
\item For odd $p$ with $p^2\le\cN$: $E_p-G\,v_p(n!)\le156(\lambda_p+1)$.
\item $\sum_{3\le p\le\sqrt{\cN}}(E_p-G\,v_p(n!))\log p\le 312\lfloor\sqrt\cN\rfloor\log\cN$.
\item $E_2-G\,v_2(n!)\le 20n+40+123(\lambda_2+1)$.
\end{enumerate}
\end{proposition}

\begin{proof}
(1) Fix $k$. As $l$ runs through $\Lambda_n$, $w_l=2k+1+2l$ runs through the consecutive odd integers
from $-(2((1+r)n-k)+1)$ to $2(k+rn)+1$. Its positive values are $2m+1$, $0\le m<A_1:=k+rn+1$, and its
negative values are $-(2m+1)$, $0\le m<A_2:=(1+r)n-k+1$. Here $A_1+A_2=(1+2r)n+2=Z/3$ and
$2A_1,2A_2\le\cN$. By Lemma~\ref{lem:legendre}(3),
\[
  (p-1)\cdot3\sum_{l\in\Lambda_n}v_p(w_l)\ge Z-6(p-1)(\lambda_p+1).
\]
By Lemma~\ref{lem:polesum} with $N=\cN$, and $\sum_jm_j=35$,
\[
  (p-1)\sum_jm_j\sum_{k'\in I_j\setminus\{k\}}v_p(k'-k)\le\sum_jm_j\#I_j+70(p-1)(\lambda_p+1).
\]
With Lemma~\ref{lem:counts}, $\sum_jm_j\#I_j-Z=Gn+29$. Hence
$(p-1)(-\nu_p(k))\le Gn+29+76(p-1)(\lambda_p+1)$. On the other hand, by Lemma~\ref{lem:legendre}(1),
$(p-1)v_p(n!)\ge n-(p-1)(\lambda_p+1)$. Therefore
\begin{align*}
  (p-1)\bigl(E_p-Gv_p(n!)\bigr)&\le 29+76(p-1)(\lambda_p+1)+37(p-1)\lambda_p\\
  &\qquad+G(p-1)(\lambda_p+1)\\
  &\le 29+131(p-1)(\lambda_p+1).
\end{align*}
Divide by $p-1\ge2$ and use $14.5\le 25(\lambda_p+1)$.

(2) By (1) each term is at most $156(\lambda_p\log p+\log p)\le312\log\cN$, since
$p^{\lambda_p}\le\cN$ and $p\le\cN$. There are at most $\lfloor\sqrt\cN\rfloor$ primes in the range.

(3) Fix $k$. By Lemma~\ref{lem:polesum} with $p=2$, $N=n$,
\begin{align*}
  -\nu_2(k)&=Z-1+\sum_jm_j\sum_{k'\in I_j\setminus\{k\}}v_2(k'-k)\\
  &\le Z-1+(G+10)n+35+70(\lambda_2+1)\\
  &=(G+20)n+40+70(\lambda_2+1).
\end{align*}
By Lemma~\ref{lem:legendre}(1), $v_2(n!)\ge n-\lambda_2-1$. Hence
\begin{align*}
  E_2-Gv_2(n!)&\le 20n+40+70(\lambda_2+1)+35\lambda_2+G(\lambda_2+1)\\
  &\le 20n+40+123(\lambda_2+1).
\end{align*}
\end{proof}

The main term $20n$ of (3), essentially $2Z$, comes from the $Z$ zero factors $u_l+\eps$, each of
which has $v_2(u_l)=-1$, together with a loss of the same size from the pole factors. It is the
source of the term $20\log2$ in \eqref{eq:Q}.

\subsection{\texorpdfstring{Decomposition of $\log D_n$}{Decomposition of log D\_n}}

\begin{proposition}\label{prop:decomp}
For every $n\in480\NN$,
\begin{multline*}
  \log D_n-G\log n!\le\bigl(20n+40+123(\lambda_2+1)\bigr)\log2+312\lfloor\sqrt\cN\rfloor\log\cN\\
  +\sum_{\substack{p\le n\\p^2>\cN}}\bigl(E_p-G\lfloor n/p\rfloor\bigr)\log p .
\end{multline*}
\end{proposition}

\begin{proof}
By definition and Legendre's formula, $\log D_n-G\log n!=\sum_{p\le n}(E_p-Gv_p(n!))\log p$. Split the
sum into $p=2$, the odd $p$ with $p^2\le\cN$ (note $p^2\le\cN$ implies $p\le n$), and the odd $p\le n$
with $p^2>\cN$. Apply Proposition~\ref{prop:smallprimes} to the first two parts. In the third part
$p^2>\cN>n$, so $v_p(n!)=\lfloor n/p\rfloor$.
\end{proof}

% ===========================================================================
\section{The arithmetic integral}\label{sec:A}
% ===========================================================================

In this section we bound the last sum in Proposition~\ref{prop:decomp} by $n(\Acert+o(1))$, where
\begin{equation}\label{eq:Acert}
  \Acert:=\frac{12507029707866288048422972493354331}{790300921079786767495600904601600}
  =15.8256549806\ldots
\end{equation}

\subsection{Residue-class counts}
For a prime $p$, $0\le k\le n$ and a block $I_j$ put
$N_{p,j}(k):=\#\{k'\in I_j:\ k'\equiv k\pmod p\}$. Counting $k'=k$ separately,
\begin{equation}\label{eq:Nidentity}
\begin{gathered}
  \ind{k\in I_j}+P_{p,j}(k)=N_{p,j}(k),\quad\text{hence}\\
  B_k+2-\eps_p(k)=2+\sum_jm_jN_{p,j}(k)-c_p(k).
\end{gathered}
\end{equation}

\begin{definition}\label{def:f}
For real $x\ge1$ and $y\in\RR$ put
\begin{align*}
  N_j(x,y)&:=\#\{m\in\ZZ:\ \delta_jx\le y+m\le(1-\delta_j)x\}\\
          &\phantom{:}=\lfloor y-\delta_jx\rfloor-\lceil y-(1-\delta_j)x\rceil+1,\\
  c(x,y)&:=3\,\#\{o\in\ZZ\text{ odd}:\ 2y-2(1+r)x<o\le 2y+2rx\},\\
  f(x,y)&:=2+\sum_jm_jN_j(x,y)-c(x,y)-G\lfloor x\rfloor .
\end{align*}
Since $f(x,y+1)=f(x,y)$ and $f(x,\cdot)$ takes finitely many values on $[0,1]$, we may define
\[
  e^*(x):=\max_{y\in\RR}f(x,y)=\max_{0\le y<1}f(x,y).
\]
\end{definition}

\begin{remark}
The formalisation (and the informal write-up it was ported from) defines $f$ by cases, with the block
indicator $\ind{\delta_jx\le y\le(1-\delta_j)x}$ and the three expressions for $P_j(x,y)$ according to
whether $y$ lies in, to the left of, or to the right of the block; it takes the maximum over
$0\le y\le x$. For $x\ge1$ and every $y$,
$\ind{\delta_jx\le y\le(1-\delta_j)x}+P_j(x,y)=N_j(x,y)$ (use
$\lceil a\rceil=\lfloor a\rfloor+1-\ind{a\in\ZZ}$ in the two out-of-block cases), so the two
definitions of $f$ agree identically; as $[0,x]$ contains a period, the two $e^*$ agree.
\end{remark}

\begin{proposition}[Pointwise bound]\label{prop:pointwise}
Let $p$ be a prime with $p\le n$ and $p^2>\cN$. Then $E_p-G\lfloor n/p\rfloor\le e^*(n/p)$.
\end{proposition}

\begin{proof}
Here $p$ is odd. Let $0\le k\le n$, $x:=n/p\ge1$ and $y:=k/p$. Then
$N_{p,j}(k)=\#\{m\in\ZZ:a_j\le k+mp\le b_j\}=N_j(x,y)$, because $a_j/p=\delta_jx$ and
$b_j/p=(1-\delta_j)x$. Next, the values $w_l$ $(l\in\Lambda_n)$ are all the odd integers in
$[2k-2(1+r)n-1,\ 2k+2rn+1]$. An odd multiple $op$ of $p$ (necessarily with $o$ odd) with
$2k-2(1+r)n<op\le 2k+2rn$ lies in that interval, and these $o$ are exactly the odd $o$ with
$2y-2(1+r)x<o\le2y+2rx$. Hence $c_p(k)\ge c(x,y)$. (This is usually strict: $c(x,y)$ drops the
$e$-factor indicator $\ind{p\mid n-2k}$ and the two odd endpoints $2k-2(1+r)n-1$ and $2k+2rn+1$ of the
range of $w_l$, so the bound may lose up to $1+3+3=7$ here; in exact computations at
$n=480,960,1440$ the total loss in $E_p-G\lfloor n/p\rfloor\le e^*(n/p)$ was at most $2$.) By \eqref{eq:Nidentity},
$B_k+2-\eps_p(k)-G\lfloor n/p\rfloor\le f(x,y)\le e^*(x)$. Take the maximum over $k$.
\end{proof}

\begin{lemma}[Uniform bound]\label{lem:tail}
For $x\ge1$, $e^*(x)\le 40+G\{x\}$.
\end{lemma}

\begin{proof}
$N_j(x,y)$ counts the integers in an interval of length $(1-2\delta_j)x$, so
$N_j\le(1-2\delta_j)x+1$. The number of odd integers in a half-open interval $(u,v]$ is
$\lfloor\frac{v+1}2\rfloor-\lfloor\frac{u+1}2\rfloor\ge\frac{v-u}2-1$, so
$c(x,y)\ge3((1+2r)x-1)=10x-3$. Using \eqref{eq:G},
$f(x,y)\le 2+35+(G+10)x-10x+3-G\lfloor x\rfloor=40+G\{x\}$.
\end{proof}

\subsection{Step structure}
By the odd-integer count in the proof of Lemma~\ref{lem:tail}, for all $x\ge1$ and $y\in\RR$,
\begin{multline}\label{eq:flooroffsets}
  f(x,y)=2+\sum_jm_j\bigl(1+\lfloor y-\delta_jx\rfloor-\lceil y-(1-\delta_j)x\rceil\bigr)\\
   -3\bigl(\lfloor y-(-rx-\tfrac12)\rfloor-\lfloor y-((1+r)x-\tfrac12)\rfloor\bigr)-G\lfloor x\rfloor;
\end{multline}
this is Definition~\ref{def:f} with the count of odd integers written out. So $f(x,y)$ depends on $y$
only through the floors and ceilings of $y-c_o(x)$ for the $58$ \emph{offsets}
$c_o(x)=s_ox+t_o$ with
\[
  (s_o,t_o)\in\{(\delta_j,0),\ (1-\delta_j,0):1\le j\le28\}\cup\{(-r,-\tfrac12),\ (1+r,-\tfrac12)\}.
\]
The pairs $(0,0)$ and $(1,0)$ are among these offsets (block $j=1$, $\delta_1=0$). Let $\cF$ be this
set of $58$ pairs together with $(0,\frac12)$, so $\#\cF=59$. (The extra pair is not needed for the
argument below; it is included because the certificate uses it, and it only refines the partition.) Define the \emph{event set} $\cE\subset[1,400]$ as the union of
\begin{itemize}
\item the points $1+j/20$ $(0\le j<40)$ and $3+j/2$ $(0\le j\le 794)$, which include every integer in
  $[1,400]$;
\item all $x\in(1,400)$ of the form $x=(t_2-t_1+m)/(s_1-s_2)$ with $(s_1,t_1),(s_2,t_2)\in\cF$,
  $s_1>s_2$ and $m\in\ZZ$.
\end{itemize}
This is a finite set of rational numbers. It has $62{,}132$ elements
$1=x_0<x_1<\dots<x_L=400$, $L=62{,}131$.

\begin{lemma}\label{lem:step}
$e^*$ is constant on each open interval $(x_{\ell-1},x_\ell)$.
\end{lemma}

\begin{proof}
Let $J=(x_{\ell-1},x_\ell)$ and $x,x'\in J$. Consider the discrete set
$C(x):=\{c_o(x)+m:\ o\text{ an offset},\ m\in\ZZ\}$. For two of its elements, the difference
$c_o(x)-c_{o'}(x)+m-m'=(s_o-s_{o'})x+(t_o-t_{o'})+(m-m')$ is an affine function of $x$. If it is not
identically zero, its only zero is an event point, or lies outside $(1,400)$; in either case it does not
vanish on $J$. Hence the map $c_o(x)+m\mapsto c_o(x')+m$ is well defined, bijective and strictly
increasing from $C(x)$ onto $C(x')$. Since $C(x)$ is a locally finite union of translates of $\ZZ$, the
map extends to an increasing bijection $\pi:\RR\to\RR$. For every offset $o$ and every $y$,
$c_o(x)+m\le y\iff c_o(x')+m\le\pi(y)$, so $\lfloor\pi(y)-c_o(x')\rfloor=\lfloor y-c_o(x)\rfloor$, and
likewise for ceilings. Also $\lfloor x\rfloor=\lfloor x'\rfloor$, since $\cE$ contains every integer of
$[1,400]$. By \eqref{eq:flooroffsets}, $f(x',\pi(y))=f(x,y)$ for all $y$, and therefore
$e^*(x')=e^*(x)$.
\end{proof}

The proof also shows how $e^*$ is computed exactly at a rational point $\xi$. The function
$f(\xi,\cdot)$ is constant on each open interval between consecutive points of $C(\xi)$. So $e^*(\xi)$
is the maximum, over the $58$ offsets $o$, of the value of $f(\xi,\cdot)$ at $c_o(\xi)$ and of its
right limit there. Each such value is an integer combination of floors of rational numbers, minus
$G\lfloor\xi\rfloor$.

\subsection{The certificate}

\begin{proposition}[Certified computation]\label{prop:certA}
Let $\xi_\ell:=(x_{\ell-1}+x_\ell)/2$ and
\[
  \Abody:=\sum_{\ell=1}^{L}e^*(\xi_\ell)\Bigl(\frac1{x_{\ell-1}}-\frac1{x_\ell}\Bigr).
\]
Then
\[
  \sum_{\ell=1}^{L}\Bigl\lceil 2^{96}e^*(\xi_\ell)\Bigl(\frac1{x_{\ell-1}}-\frac1{x_\ell}\Bigr)\Bigr\rceil
  =U:=1243345293752876677540040193981 .
\]
Consequently $\Abody\le U/2^{96}=15.6932239\ldots$ and
\[
  \frac{U}{2^{96}}+\frac{44}{400}+\frac{G}{2\cdot 399}=\Acert ,
\]
with $\Acert$ as in \eqref{eq:Acert}. (Note $44/400+G/798=1321/9975$.)
\end{proposition}

\begin{proof}
This is a finite computation with explicit rational numbers: enumerate $\cE$, evaluate $e^*(\xi_\ell)$
exactly by the recipe after Lemma~\ref{lem:step}, round each term up to a multiple of $2^{-96}$, and
add. The last identity is exact rational arithmetic. The computation has been carried out
independently by an exact-rational Python implementation and by the Lean kernel; see
Section~\ref{sec:lean-cert}.
\end{proof}

\subsection{From primes to the integral}

\begin{lemma}[Tail]\label{lem:pnt-tail}
Let $X\ge2$ be an integer, $C,G'\ge0$, and $h:[X,\infty)\to\RR$ with $h(y)\le C+G'\{y\}$. For every
$\eps>0$, for all sufficiently large $n$,
\[
  \sum_{p\le n/X}h(n/p)\log p\le n\Bigl(\frac CX+\frac{G'}{2(X-1)}\Bigr)+\eps n .
\]
\end{lemma}

\begin{proof}
Choose an integer $K_0\ge1$ with $G'/(2K_0(X-1))\le\eps/4$ and an integer $M>X$ with
$(C+G')\log4/M\le\eps/4$. The primes $p\le n/M$ contribute at most $(C+G')\theta(n/M)\le
(C+G')(\log4)\,n/M\le\eps n/4$, by Chebyshev's bound $\theta(y)\le y\log4$. Cut $[X,M)$ into the
$K_0(M-X)$ half-open cells $[\,m+\frac{i-1}{K_0},\,m+\frac i{K_0})$, $X\le m<M$, $1\le i\le K_0$. On
such a cell $h\le C+G'i/K_0$. The primes with $n/p$ in the cell $[a,b)$ are those in $(n/b,n/a]$, and
by the prime number theorem $\theta(n/a)-\theta(n/b)=n(1/a-1/b)+o(n)$. Since there are finitely many
cells, for large $n$ the primes $n/M<p\le n/X$ contribute at most
\[
  n\sum_{m=X}^{M-1}\sum_{i=1}^{K_0}\Bigl(C+\frac{G'i}{K_0}\Bigr)
  \Bigl(\frac1{m+\frac{i-1}{K_0}}-\frac1{m+\frac i{K_0}}\Bigr)+\frac{\eps n}4 .
\]
The $C$-part telescopes to $C(1/X-1/M)\le C/X$. In the $G'$-part each bracket is at most
$1/(K_0m^2)$, so the inner sum is at most $G'(K_0+1)/(2K_0m^2)$. Since
$\sum_{m\ge X}m^{-2}\le1/(X-1)$, the $G'$-part is at most
$\frac{G'}{2(X-1)}+\frac{G'}{2K_0(X-1)}\le\frac{G'}{2(X-1)}+\frac\eps4$.
\end{proof}

\begin{proposition}\label{prop:lemma5}
There are $\eps_n\to0$ such that, for all large $n\in480\NN$,
\[
  \sum_{\substack{p\le n\\p^2>\cN}}\bigl(E_p-G\lfloor n/p\rfloor\bigr)\log p\le n(\Acert+\eps_n).
\]
\end{proposition}

\begin{proof}
Fix $\eps>0$ and define $h$ on $[1,\infty)$ by $h(x):=e^*(x)$ for $x<400$ and
$h(x):=\max(e^*(x),0)$ for $x\ge400$. Let $n$ be large; in particular $n/\sqrt\cN\ge400$, which holds as
soon as $n\ge 7\cdot400^2$ because $\cN\le7n$.
\begin{enumerate}
\item By Proposition~\ref{prop:pointwise}, each term of the sum is at most $h(n/p)\log p$. Every prime
  $p\le n$ not in the sum has $p^2\le\cN$, hence $n/p\ge n/\sqrt\cN\ge400$ and $h(n/p)\ge0$. So the sum
  is at most $\sum_{p\le n}h(n/p)\log p$.
\item \emph{Primes $n/400<p\le n$}, i.e.\ $n/p\in[1,400)$. Let $v_\ell:=e^*(\xi_\ell)$. By
  Lemma~\ref{lem:step}, $h(n/p)=v_\ell$ when $n/p\in(x_{\ell-1},x_\ell)$. By the prime number
  theorem, $\sum_{x_{\ell-1}<n/p<x_\ell}\log p=n(1/x_{\ell-1}-1/x_\ell)+o(n)$ for each of the finitely
  many $\ell$. At most $L+1$ primes have $n/p\in\cE$, and each contributes at most
  $(40+G)\log n$ by Lemma~\ref{lem:tail}. Hence this part is at most $n\Abody+\eps n/2$ for large $n$.
\item \emph{Primes $p\le n/400$.} By Lemma~\ref{lem:tail}, $h(x)\le40+G\{x\}\le44+G\{x\}$ for
  $x\ge400$. We use $44=S+9$, the constant of the formal certificate; $40$ would lower $\Acert$ by
  $0.01$. Lemma~\ref{lem:pnt-tail} with $X=400$, $C=44$, $G'=G$ bounds this part by
  $n(44/400+G/798)+\eps n/2$.
\end{enumerate}
Adding up and using Proposition~\ref{prop:certA}, the sum is at most $n(\Acert+\eps)$ for large $n$.
\end{proof}

\begin{corollary}\label{cor:logD}
There are $\eps'_n\to0$ with $\log D_n\le G\log n!+n(\Acert+20\log2+\eps'_n)$ for all large
$n\in480\NN$.
\end{corollary}

\begin{proof}
Combine Propositions~\ref{prop:decomp} and~\ref{prop:lemma5}. The remaining error terms
$(40+123(\lambda_2+1))\log2$ and $312\lfloor\sqrt\cN\rfloor\log\cN$ are $O(\sqrt n\log n)=o(n)$.
\end{proof}

% ===========================================================================
\section{\texorpdfstring{The size of $L_n$}{The size of L\_n}}\label{sec:size}
% ===========================================================================

Put
\begin{equation}\label{eq:Phi}
  \Phi(x):=3\bigl[F(x+\tfrac{13}6)-F(x-\tfrac76)\bigr]-\sum_{j=1}^{28}m_j\bigl[F(x+1-\delta_j)-F(x+\delta_j)\bigr]
  \qquad(x\ge\tfrac76),
\end{equation}
and $V:=-29.76$. (Note $\frac{13}6=1+r$ and $\frac76=r$.)

\begin{lemma}\label{lem:vanish}
$R_n''(t)=0$ for every integer $t\in[0,rn]$.
\end{lemma}
(The same argument works at every integer of $\Lambda_n$; only $t\in[0,rn]$ is used below, and this is
the case that is formalised.)

\begin{proof}
Near such $t$, $R_n(s)=(s-t)^3g(s)$ with $g$ holomorphic at $t$, since the poles of $R_n$ are at
half-integers. Hence $R_n''=6(s-t)g+6(s-t)^2g'+(s-t)^3g''$ vanishes at $s=t$.
\end{proof}

\begin{lemma}\label{lem:logderiv}
For real $t\ge rn+1$, $|R_n''(t)|\le|R_n(t)|(M^2+M)$ with $M:=21642N_0$.
\end{lemma}
(The formalisation uses the cruder count $\sum_jm_j\#I_j\le35(n+1)$, which gives
$M_0\le21600N_0+42\le21642N_0$ in the proof below; this is the origin of the constant.)

\begin{proof}
On $(rn+\frac12,\infty)$, $R_n'=R_ng$ with
$g(t)=\frac{2}{2t+n+1}+\sum_{l\in\Lambda_n}\frac{3}{t-l}-\sum_{k=0}^{n}\frac{B_k}{t+k+\frac12}$.
At $t\ge rn+1$ every $|t-l|$, $|t+k+\frac12|$ and $|t+\frac{n+1}2|$ is at least $1$, so both $|g(t)|$
and $|g'(t)|$ are at most $M_0:=1+Z+\sum_kB_k=1+(10n+6)+(G+10)n+35=18192N_0+42\le M$. Then
$R_n''=R_n(g^2+g')$.
\end{proof}

\begin{lemma}\label{lem:runs}
\begin{enumerate}
\item If $a\le b$ are integers and $t>b$ is real, then
  $\sum_{l=a}^{b}\log(t-l)\le F(t-a+1)-F(t-b)-(b-a+1)$.
\item If $A\le B$ are integers and $t+A\ge\frac12$, then
  $\sum_{k=A}^{B}\log(t+k+\frac12)\ge F(t+B+\frac12)-F(t+A-\frac12)-(B-A+1)$.
\item $\log N!\le N\log N-N+\log(N+1)+1$ for $N\ge1$, and $F(Ny)=NF(y)+Ny\log N$ for $N,y>0$.
\end{enumerate}
\end{lemma}

\begin{proof}
$F$ is convex with $F'(y)=\log y+1$. Hence $\log c\le F(c+1)-F(c)-1$ for $c>0$ and
$F(c)-F(c-1)-1\le\log c$ for $c\ge1$. Telescoping gives (1) and (2). (3): (1)-type telescoping gives
$\log N!\le F(N+1)-N$, and $F(N+1)\le F(N)+\log(N+1)+1$ by the mean value theorem. The scaling identity
is immediate.
\end{proof}

\begin{proposition}\label{prop:logR}
For real $t\ge rn+1$ and $x=t/n$: $R_n(t)>0$ and
\begin{align*}
  \log R_n(t)&\le n\Phi(x)-Gn(\log n-1)+34\\
  &\le -G\log n!+n\Phi(x)+G(\log(n+1)+1)+34 .
\end{align*}
\end{proposition}

\begin{proof}
All factors in \eqref{eq:R} are positive for $t>rn$. By Lemma~\ref{lem:runs}(1) with
$a=-(1+r)n-1$, $b=rn$, and $F(y+2)\le F(y)+2(\log(y+2)+1)$,
\[
  \sum_{l\in\Lambda_n}\log(t-l)\le F(t+(1+r)n)-F(t-rn)-(1+2r)n+2\log(t+(1+r)n+2).
\]
By the scaling identity the right side is
$n[F(x+\frac{13}6)-F(x-\frac76)]+\frac{10}3n(\log n-1)+2\log(t+1040N_0+2)$. For the block $I_j$,
Lemma~\ref{lem:runs}(2), the inequalities $F(Y+\frac12)-F(Y)\ge\frac12(\log Y+1)$ and
$F(X)-F(X-\frac12)\ge\frac12(\log(X-\frac12)+1)$ with $Y=n(x+1-\delta_j)$, $X=n(x+\delta_j)$, and
$Y\ge t/2$, $X-\frac12\ge t/2$ (as $t\ge1$) give
\begin{multline*}
  \sum_{k\in I_j}\log(t+k+\tfrac12)\ge n[F(x+1-\delta_j)-F(x+\delta_j)]\\
  +n(1-2\delta_j)(\log n-1)+\log t-\log2 .
\end{multline*}
Combining with weights $3$ and $-m_j$, the $n(\log n-1)$ terms add up to
$(10-\sum_jm_j(1-2\delta_j))n(\log n-1)=-Gn(\log n-1)$, and the remaining terms are
$\log(2t+n+1)+6\log(t+1040N_0+2)-35\log t+35\log2$. Since $2t+n+1\le3t$ and $t+1040N_0+2\le 3t$, this is
at most $7\log3+35\log2-28\log t\le7\log3+35\log2<34$ (as $\log t\ge0$). The second inequality follows from Lemma~\ref{lem:runs}(3).
\end{proof}

\begin{proposition}[Real-axis maximum]\label{prop:Phi}
$\Phi(x)\le V=-29.76$ for all $x\ge\frac76$, and $\Phi(x)\le V-4\log(x/3)$ for $x\ge3$.
\end{proposition}

\begin{proof}
For $x>\frac76$,
\begin{align*}
  \Phi'(x)&=3\log\frac{x+13/6}{x-7/6}-\sum_jm_j\log\frac{x+1-\delta_j}{x+\delta_j},\\
  \Phi''(x)&=\frac3{x+13/6}-\frac3{x-7/6}-\sum_jm_j\Bigl(\frac1{x+1-\delta_j}-\frac1{x+\delta_j}\Bigr).
\end{align*}
\emph{Step 1: $\Phi''\le0$ on $(\frac76,\frac43]$.} On an interval $[a,b]$ with $a\ge\frac76$, each
term of $\Phi''$ is monotone, so
\[
  \Phi''(x)\le\frac3{a+13/6}-\frac3{b-7/6}-\sum_jm_j\Bigl(\frac1{b+1-\delta_j}-\frac1{a+\delta_j}\Bigr).
\]
For $[a,b]=[\frac76,\frac65],[\frac65,\frac54],[\frac54,\frac43]$ the right side is a rational number,
approximately $-78.1$, $-24.4$ and $-6.81$ respectively.

\emph{Step 2: the tangent at $x_0=58911/50000$.} Certified enclosures of the $58$ logarithms
$\log(x_0+s)$ that occur in $\Phi(x_0)$ and $\Phi'(x_0)$ give
\[
  \Phi(x_0)\le-29.7613,\qquad -0.002\le\Phi'(x_0)\le0 .
\]
Each enclosure writes $x_0+s=2^a3^b5^cz$ with $|1-z|<0.015$, uses $8$ terms of the Taylor series of
$\log z$ with an explicit remainder, and uses Mathlib's enclosures of $\log2$, $\log3$ and $\log5$.
(The true values are $\Phi(x_0)=-29.76132763\ldots$ and $\Phi'(x_0)=-0.00148021\ldots$.) $\Phi$ is
continuous on $[\frac76,\infty)$ and concave on $(\frac76,\frac43]$, so for $\frac76\le x\le\frac43$,
\[
  \Phi(x)\le\Phi(x_0)+\Phi'(x_0)(x-x_0)\le-29.7613+0.002\,(x_0-\tfrac76)<-29.76 .
\]
\emph{Step 3: $\Phi'\le0$ on $[\frac43,\infty)$.} Since $\log(Y/X)\ge(Y-X)/Y$ for $Y\ge X>0$, the
block sum in $\Phi'$ is at least $S_b(x):=\sum_jm_j(1-2\delta_j)/(x+1-\delta_j)$, which is decreasing
in $x$. On $[\frac43,2]$, $(x+\frac{13}6)/(x-\frac76)\le21\le 24$ and $S_b(x)\ge S_b(2)\ge9.55$, while
$3\log24<9.54$ (we use $24$ rather than $21$ because $\log24=3\log2+\log3$ is directly bounded by
the enclosures of $\log2$ and $\log3$). On $[2,3]$, the ratio is $\le5\le6$, $S_b(x)\ge S_b(3)\ge7$ and $3\log6<5.4$.

\emph{Step 4: $\Phi'(x)\le-4/x$ for $x\ge3$.} Here $3\log\frac{x+13/6}{x-7/6}\le\frac{10}{x-7/6}\le
\frac{180}{11x}$ (using $\log y\le y-1$ and $x\ge3$), and $\frac1{x+1-\delta_j}\ge\frac3{4x}$, so $S_b(x)\ge\frac{279}{10}\cdot\frac3{4x}$.
Hence $\Phi'(x)\le(\frac{180}{11}-\frac{837}{40})/x=-\frac{2007}{440x}\le-4/x$.

So $\Phi$ is nonincreasing on $[\frac43,\infty)$, and $\Phi(x)\le\Phi(\frac43)<V$ there; with Step 2,
$\Phi\le V$ on $[\frac76,\infty)$. By Step 4, $x\mapsto\Phi(x)+4\log x$ is nonincreasing on
$[3,\infty)$, so $\Phi(x)\le\Phi(3)-4\log(x/3)\le V-4\log(x/3)$.
\end{proof}

Numerically, the maximum of $\Phi$ on $[\frac76,\infty)$ is $-29.7613276\ldots$, attained at
$x^*=1.1782140\ldots$.

\begin{proposition}\label{prop:size}
For every $n=480N_0\in480\NN$ with $L_n\ne0$,
\[
  \log|L_n|\le-G\log n!+n\bigl(V+\eps''_n\bigr),\qquad
  \eps''_n:=\frac{A_{\mathrm{size}}+22\log N_0}{480N_0}\to0,
\]
where $A_{\mathrm{size}}:=G(\log481+1)+34+2\log2+2\log21642+2\log1441$.
\end{proposition}

\begin{proof}
By Lemma~\ref{lem:vanish}, $L_n=\sum_{t\ge rn+1}(-1)^tR_n''(t)$. By Lemma~\ref{lem:logderiv} and
Proposition~\ref{prop:logR}, $|R_n''(t)|\le(M^2+M)e^{C_n}e^{n\Phi(t/n)}$ with
$C_n:=-G\log n!+G(\log(n+1)+1)+34$. Put $T:=3n$ and $w(t):=1/((t+1)(t+2))$, so that $\sum_{t\ge0}w(t)=1$.
We claim $e^{n\Phi(t/n)}\le e^{nV}\cdot2(T+1)^2w(t)$ for integers $t\ge rn+1$. For $t\le T$ this follows
from Proposition~\ref{prop:Phi} and $(t+1)(t+2)\le2(T+1)^2$. For $t>T$, Proposition~\ref{prop:Phi}
gives $e^{n\Phi(t/n)}\le e^{nV}(T/t)^{4n}\le e^{nV}(T/t)^2$, and
$(T/t)^2(t+1)(t+2)\le2T^2$ for $t\ge T\ge4$. Therefore
\[
  |L_n|\le(M^2+M)\,e^{C_n+nV}\,2(T+1)^2 .
\]
Taking logarithms, with $M^2+M\le2M^2$, $T+1\le1441N_0$ and $n+1\le481N_0$,
\begin{align*}
  \log|L_n|&\le-G\log n!+nV+A_{\mathrm{size}}+(4+G)\log N_0\\
  &\le -G\log n!+nV+A_{\mathrm{size}}+22\log N_0.\qedhere
\end{align*}
\end{proof}

\begin{remark}
On the real axis $x>r$, the function $\Phi$ is the real part of the boundary value of the phase $\Psi$ of
Section~\ref{sec:nonvan} from the upper half-plane: the factor $3F(r-x)$ of $\Psi$ has real part $-3F(x-r)$. The saddle point
gives the better exponent $\Re\Omega\approx-29.7790$ in place of $V$ (see Remark~\ref{rem:saddlesize}),
but the elementary bound of Proposition~\ref{prop:size} suffices, and it is the one used in the proof.
\end{remark}

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

We extend $R_n$ to the rational function of $z\in\CC$ given by \eqref{eq:R}. It has real coefficients,
and its poles are the points $-k-\frac12$ ($0\le k\le n$), all with real part $\le-\frac12$. Put
\[
  F_n(z):=R_n''(z)\,\frac{\pi}{\sin\pi z}.
\]
Recall that $|\sin\pi(x+iy)|^2=\sin^2\pi x+\sinh^2\pi y$, so $|\sin\pi z|\ge\sinh(\pi|\Im z|)$, and
$|\sin\pi z|=\cosh(\pi\Im z)\ge1$ when $\Re z\in\frac12+\ZZ$.

\subsection{An integral representation}

\begin{lemma}\label{lem:decay}
Let $c>-\frac12$. There is $C=C(n,c)$ such that $|R_n''(z)|\le C(1+|z|^2)^{-1}$ whenever $\Re z\ge c$.
Moreover $R_n''(\bar z)=\overline{R_n''(z)}$.
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:counts}, $|R_n(w)|\le C_1|w|^{-3}$ for $|w|\ge R_1$. If $|z|\ge 2R_1+2$, Cauchy's
estimate on the circle $|w-z|=\frac12$ gives
\[
  |R_n''(z)|\le 8\max_{|w-z|=1/2}|R_n(w)|\le C_1'|z|^{-3}.
\] On the compact set $\{\Re z\ge c,\ |z|\le 2R_1+2\}$, which contains no pole, $R_n''$ is
bounded. The symmetry holds because $R_n$ has real coefficients.
\end{proof}

\begin{proposition}\label{prop:contour}
For every real $c\in(0,rn+1)\setminus\ZZ$,
\[
  L_n=-\frac1{2\pi i}\int_{c-i\infty}^{c+i\infty}F_n(z)\,dz=-\frac1\pi\,\Re\int_0^\infty F_n(c+iy)\,dy .
\]
\end{proposition}

\begin{proof}
Let $N>c$ be an integer and $Y>0$, and integrate $F_n$ counterclockwise around the rectangle with
vertices $c\pm iY$, $N+\frac12\pm iY$. Inside, $F_n$ is meromorphic with simple poles at the integers
$t\in(c,N]$, with residue $(-1)^tR_n''(t)$. On the horizontal sides $|F_n|\le\pi C\sinh(\pi Y)^{-1}$ by
Lemma~\ref{lem:decay}, so they vanish as $Y\to\infty$. On the line $\Re z=N+\frac12$ we have
$|F_n(z)|\le\pi C/(1+|z|^2)$, so its integral is at most $\pi^2C(1+(N+\frac12)^2)^{-1/2}\to0$ as
$N\to\infty$. On the line $\Re z=c$, $|\sin\pi z|\ge\max(|\sin\pi c|,\sinh\pi|y|)$, so the integral
converges absolutely. Hence
\[
  -\int_{c-i\infty}^{c+i\infty}F_n(z)\,dz=2\pi i\sum_{t>c}(-1)^tR_n''(t)=2\pi i\,L_n ,
\]
where the last equality uses Lemma~\ref{lem:vanish}: every integer $0\le t<c$ satisfies $t\le rn$.
(The rectangle is traversed upwards on $\Re z=N+\frac12$ and downwards on $\Re z=c$; the residue sum
converges absolutely.) Finally $F_n(c-iy)=\overline{F_n(c+iy)}$, because $R_n''$ and $\sin$ commute with
complex conjugation. Hence
$\int_{c-i\infty}^{c+i\infty}F_n\,dz=i\int_{\RR}F_n(c+iy)\,dy=2i\Re\int_0^\infty F_n(c+iy)\,dy$.
\end{proof}

\subsection{Gamma factorisation}

We use the following $58$ factors $(c_i,s_i,u_i,\beta_i)$, $0\le i\le57$:
\begin{gather*}
  (3,+1,\tfrac{13}6,2),\qquad(3,-1,\tfrac76,1),\\
  \text{and for each block } j:\quad
  (m_j,+1,\delta_j,\tfrac12),\ (-m_j,+1,1-\delta_j,\tfrac32).
\end{gather*}
Put $\alpha_i(x):=s_ix+u_i$. One checks directly:
\begin{equation}\label{eq:factorid}
\begin{gathered}
  \sum_ic_is_i=0,\quad\sum_ic_iu_i=-G,\quad\sum_ic_i(\beta_i-\tfrac12)=-29,\\
  \sum_ic_i=6,\quad\sum_i|c_i|=76,\quad\sum_i|c_i(\beta_i-\tfrac12)|=41 .
\end{gathered}
\end{equation}
In particular $\sum_ic_i\alpha_i(x)=-G$ for all $x$.

\begin{lemma}\label{lem:gamma}
For $z\in\CC\setminus(\ZZ\cup(\ZZ+\frac12))$,
\[
  R_n(z)=P_n(z)\,\frac{\sin^3\pi z}{\pi^3},\qquad
  P_n(z):=(2z+n+1)\prod_{i=0}^{57}\Gamma(s_iz+nu_i+\beta_i)^{c_i}.
\]
\end{lemma}

\begin{proof}
Write $p_0:=(1+r)n+1$ and $q_0:=rn$, which is even. Then
$\prod_{l=-p_0}^{q_0}(z-l)=\Gamma(z+p_0+1)/\Gamma(z-q_0)$, and by the reflection formula
$1/\Gamma(z-q_0)=(-1)^{q_0}\Gamma(q_0+1-z)\sin(\pi z)/\pi$. Cubing, and using $(-1)^{3q_0}=1$, gives the
first two factors. For a block, $\prod_{k=a_j}^{b_j}(z+k+\frac12)=\Gamma(z+b_j+\frac32)/\Gamma(z+a_j+\frac12)$,
which gives the factors $(m_j,\allowbreak \dots,\frac12)$ and $(-m_j,\allowbreak \dots,\frac32)$ since $a_j=\delta_jn$ and
$b_j=(1-\delta_j)n$.
\end{proof}

For $\Im z>0$, every argument $s_iz+nu_i+\beta_i$ has nonzero imaginary part, so $P_n$ is holomorphic
and zero-free there. Put
\begin{align*}
  \mu&:=\frac{P_n'}{P_n}=\frac2{2z+n+1}+\sum_ic_is_i\,\psi(s_iz+nu_i+\beta_i),\\
  \mu'&=-\frac4{(2z+n+1)^2}+\sum_ic_is_i^2\,\psi'(s_iz+nu_i+\beta_i),
\end{align*}
where $\psi=\Gamma'/\Gamma$.

\begin{lemma}\label{lem:FPH}
For $\Im z>0$,
\[
  F_n(z)=\frac{P_n(z)H_n(z)}{\pi^2},
\]
where
\[
  H_n:=\sin^2(\pi z)(\mu^2+\mu')+6\pi\mu\sin(\pi z)\cos(\pi z)+3\pi^2(2\cos^2\pi z-\sin^2\pi z),
\]
and, with $\mathbf q:=e^{2\pi iz}$,
\begin{equation}\label{eq:qform}
  \mathbf qH_n=\tfrac14\Bigl[(-1+2\mathbf q-\mathbf q^2)(\mu^2+\mu')+6\pi i\mu(1-\mathbf q^2)
  +3\pi^2(3+2\mathbf q+3\mathbf q^2)\Bigr].
\end{equation}
\end{lemma}

\begin{proof}
Write $\sigma=\sin\pi z$, $\gamma=\cos\pi z$. From $R_n=P_n\sigma^3/\pi^3$ and $P_n'=\mu P_n$,
$P_n''=(\mu^2+\mu')P_n$,
\[
  R_n''=\frac{P_n}{\pi^3}\bigl[(\mu^2+\mu')\sigma^3+6\pi\mu\sigma^2\gamma+6\pi^2\sigma\gamma^2-3\pi^2\sigma^3\bigr].
\]
Multiply by $\pi/\sigma$. For \eqref{eq:qform} use $\mathbf q\sigma^2=-(1-\mathbf q)^2/4$,
$\mathbf q\sigma\gamma=i(1-\mathbf q^2)/4$ and $\mathbf q\gamma^2=(1+\mathbf q)^2/4$.
\end{proof}

\subsection{Stirling's formula in sectors}

Let $\log\Gamma$ denote the branch of the logarithm of $\Gamma$ on $\CC\setminus(-\infty,0]$ that is real
on $(0,\infty)$.

\begin{theorem}[{cf.~\cite[\S5.11(ii)]{DLMF}}]\label{thm:stirling}
Let $0<\varphi\le\pi$ and put $\varsigma:=\sin(\varphi/2)$. For $w\ne0$ with $|\arg w|\le\pi-\varphi$,
\begin{gather*}
  \Bigl|\log\Gamma(w)-\bigl((w-\tfrac12)\log w-w+\tfrac12\log2\pi\bigr)\Bigr|\le\frac1{12\varsigma^2|w|},\\
  \Bigl|\psi(w)-\log w+\frac1{2w}\Bigr|\le\frac1{8\varsigma^3|w|^2},\qquad
  \Bigl|\psi'(w)-\frac1w-\frac1{2w^2}\Bigr|\le\frac1{4\varsigma^4|w|^3}.
\end{gather*}
\end{theorem}

The first bound is \cite[\S5.11(ii)]{DLMF} with $K=1$; the other two follow from the same
representation and are proved below.

\begin{proof}
We recall the argument, which is also the one formalised. Let $Q_1(t):=\frac12\{t\}(1-\{t\})$, so
$0\le Q_1\le\frac18$. For $w\in\CC\setminus(-\infty,0]$ one has the Stieltjes representation
\[
  \log\Gamma(w)=(w-\tfrac12)\log w-w+\tfrac12\log2\pi+J(w),\quad J(w):=\int_0^\infty\frac{Q_1(t)}{(t+w)^2}\,dt
\]
(in the formalisation it is derived from Euler's limit formula and an exact Euler--Maclaurin identity
for $\sum_{j\le N}\log(w+j)$). If $|\arg w|\le\pi-\varphi$ and $t\ge0$, then
$|t+w|\ge\varsigma(t+|w|)$: indeed
$|t+w|^2-\varsigma^2(t+|w|)^2\ge 2t|w|(\cos\varphi+\cos\arg w)\ge0$. For $x>0$,
\begin{align*}
  \int_0^1\frac{u(1-u)/2}{(u+x)^2}\,du&=(x+\tfrac12)\log(1+\tfrac1x)-1\\
  &=\sum_{k\ge1}\frac{1}{(2k+1)(2x+1)^{2k}}\le\frac1{12x(x+1)},
\end{align*}
so for $\varrho>0$
\[
  \int_0^\infty\frac{Q_1(t)}{(t+\varrho)^{2}}\,dt\le\sum_{k\ge0}\frac1{12}\Bigl(\frac1{k+\varrho}-\frac1{k+1+\varrho}\Bigr)
  =\frac1{12\varrho}.
\]
With $\varrho=|w|$ this gives $|J(w)|\le1/(12\varsigma^2|w|)$. Differentiating under the integral,
$\psi(w)=\log w-\frac1{2w}-2\int_0^\infty Q_1(t)(t+w)^{-3}dt$ and
$\psi'(w)=\frac1w+\frac1{2w^2}+6\int_0^\infty Q_1(t)(t+w)^{-4}dt$; the bounds follow from $Q_1\le\frac18$
and $\int_0^\infty(t+|w|)^{-m}dt=|w|^{1-m}/(m-1)$.
\end{proof}

\begin{corollary}\label{cor:stirling}
Let $0<\varphi\le\pi$, $\varsigma=\sin(\varphi/2)$, $a>0$, and let $\alpha\in\CC$ with $|\alpha|\ge a$,
$|\arg\alpha|\le\pi-\varphi$. Let $\beta\in(0,2]$ and $n\ge4/a$. Then
\begin{gather*}
  \Bigl|\log\Gamma(n\alpha+\beta)-\bigl[n\alpha\log n+n(\alpha\log\alpha-\alpha)\\
   +(\beta-\tfrac12)(\log n+\log\alpha)+\tfrac12\log2\pi\bigr]\Bigr|
   \le\frac{9+1/(6\varsigma^2)}{an},\\
  \bigl|\psi(n\alpha+\beta)-\log n-\log\alpha\bigr|\le\frac{4+1/(8\varsigma^3)}{an},\\
  |\psi'(n\alpha+\beta)|\le\frac{3+1/\varsigma^4}{an}.
\end{gather*}
\end{corollary}

\begin{proof}
Put $w=n\alpha+\beta$ and $u=\beta/(n\alpha)$, so $|u|\le2/(an)\le\frac12$ and $|w|\ge an-2\ge an/2$.
Adding the positive real number $\beta$ moves the argument towards $0$, so $|\arg w|\le|\arg\alpha|$.
Since $\arg(1+u)$ is $0$ or of sign opposite to $\arg\alpha$ and $|\arg(1+u)|<\pi/2$, the principal
logarithms satisfy $\log w=\log n+\log\alpha+\log(1+u)$. Insert this into Theorem~\ref{thm:stirling}
and use $|\log(1+u)-u|\le|u|^2$, $|\log(1+u)|\le\frac32|u|$ for $|u|\le\frac12$:
the extra terms are $n\alpha(\log(1+u)-u)$, of size $\le n|\alpha||u|^2\le4/(an)$, and
$(\beta-\frac12)\log(1+u)$, of size $\le\frac32\cdot\frac32|u|\le4.5/(an)$, while
$1/(12\varsigma^2|w|)\le1/(6\varsigma^2an)$. The bounds for $\psi$ and $\psi'$ follow in the same way from
the second and third bounds of Theorem~\ref{thm:stirling}, using $|w|\ge an/2\ge2$.
\end{proof}

\subsection{The phase and the certified saddle data}

On the set $\mathcal D$ of $x\in\CC$ with $\alpha_i(x)\notin(-\infty,0]$ for all $i$ (this contains the
open upper half-plane and the real interval $(0,\frac76)$) define, with principal logarithms,
\begin{gather*}
  \Psi(x):=\sum_ic_i\,\alpha_i(x)\log\alpha_i(x),\qquad f(x):=\Psi(x)-2\pi ix,\\
  \psi_\flat(x):=\sum_ic_i(\beta_i-\tfrac12)\log\alpha_i(x),\\
  A(x):=\frac{(2x+1)\,e^{\psi_\flat(x)}}{\pi^2}\cdot\Bigl(-\frac{(\Psi'(x)-3\pi i)^2}{4}\Bigr).
\end{gather*}
By \eqref{eq:factorid}, $\Psi'(x)=\sum_ic_is_i\log\alpha_i(x)$, $\Psi''(x)=\sum_ic_i/\alpha_i(x)$ and
$\Psi'''(x)=-\sum_ic_is_i/\alpha_i(x)^2$. We say that the \emph{sector condition $(a,\eta)$ holds at $x$}
if $|\alpha_i(x)|\ge a$ and $|\arg\alpha_i(x)|\le\pi-\eta$ for every $i$.

\begin{theorem}[Certified saddle data]\label{thm:saddle}
Put $a:=10^{-3}$, $\eta:=\pi-2.76$, $\rho:=1/250$, $M_3:=56746$, $\delta_0:=10^{-7}$ and
$\etafar:=9.727\cdot10^{-4}$, and let
\[
  c_0:=1.1719231074608510827430178+0.0099732253713548444658806\,i .
\]
There are $x_0\in\CC$, $d\in\CC$ with $|d|=1$, and $v_0,\allowbreak \dots,v_{46}\in\CC$ such that the following
hold, where $\Omega:=f(x_0)$ and $K_\star:=|\Psi''(x_0)|$.
\begin{enumerate}
\item[(S0)] $|x_0-c_0|\le10^{-12}$, and $x_0$ is the unique zero of $\Psi'-2\pi i$ in this disc. Moreover
  \begin{gather*}
    -29.7790173\le\Re\Omega\le-29.7790172,\\
    -7.301075589\le\Im\Omega\le-7.301075587,\qquad\sin(480\,\Im\Omega)>0.99 .
  \end{gather*}
\item[(S1)] $K_\star\ge260$, $\Psi''(x_0)d^2=-K_\star$, $|\Psi'''(x)|\le M_3$ for $|x-x_0|\le\rho$, and
  $M_3\rho\le\frac32K_\star$.
\item[(S1$'$)] $\rho<\Im x_0$; in particular the closed disc $|x-x_0|\le\rho$ lies in $\Im x>0$.
\item[(P)] $v_0=x_c:=1.161975915052$, so $\delta_0\le x_c<\frac76$; $v_5=x_0-\rho d$, $v_6=x_0+\rho d$;
  $v_{46}=\xtop:=9.211726243607+60.012047688088\,i$; $\Re v_k\ge0$ for all $k$; and
  $\Im(v_k+t(v_{k+1}-v_k))>0$ for $0\le k<46$ and $0<t\le1$.
\item[(S2)] For $1\le k<46$, $k\ne5$, and every $x\in[v_k,v_{k+1}]$: $\Re f(x)\le\Re\Omega-\etafar$ and
  the sector condition $(a,\eta)$ holds at $x$. The same holds for every $x\ne v_0+e$ on the segment
  $[v_0+e,v_1]$, for every real $e$ with $|e|\le\delta_0$.
\item[(S3)] For every $y\ge0$: $\Re f(\xtop+iy)\le\Re\Omega-\etafar-(7-2\pi)y$, and the sector condition
  $(a,\eta)$ holds at $\xtop+iy$.
\item[(S4)] The sector condition $(a,\eta)$ holds at $x_0+sd$ for $|s|\le\rho$.
\end{enumerate}
\end{theorem}

\begin{proof}[Method of proof]
All statements are verified by exact rational interval arithmetic, with verified enclosures of $\pi$,
$\log$, $\arctan$ and $\arg$ (series with explicit tail bounds, after argument reduction) and complex
boxes. The verification is carried out by the Lean kernel; see Section~\ref{sec:lean}.
\begin{itemize}
\item (S0): with $Y\approx1/\Psi''(c_0)$, a box evaluation shows $|1-Y\Psi''(z)|\le\kappa_c<1$ on the disc
  $B_0=\{|z-c_0|\le10^{-12}\}$ and $|Y(\Psi'(c_0)-2\pi i)|\le\eps$ with $\eps+\kappa_c10^{-12}\le10^{-12}$.
  Then $z\mapsto z-Y(\Psi'(z)-2\pi i)$ is a contraction of $B_0$ into itself, and the Banach fixed point
  theorem gives existence and uniqueness. $\Omega$ is enclosed by evaluating $f(c_0)$ on a box and adding
  a mean-value bound for $|f(x_0)-f(c_0)|$. For the sine, one checks
  $480\Im\Omega=u+\frac\pi2-558\cdot2\pi$ with $|u|\le0.07$, so $\sin(480\Im\Omega)=\cos u\ge1-u^2/2$.
\item (S1), (S1$'$): $\Psi''(x_0)$ is enclosed in a box; $d:=v/|v|$ with $v:=1-\overline{\Psi''(x_0)}/K_\star$
  satisfies $\Psi''(x_0)d^2=-K_\star$; and $M_3$ bounds $\sum_i|c_i|/|\alpha_i|^2$ on a box containing the disc.
\item (P), (S2): the vertices $v_k$ other than $v_5,v_6$ are explicit rational points with $12$ decimals,
  obtained from a Runge--Kutta trace of the steepest-descent curves of $\Re f$ from $x_0\pm\rho d$. On
  each segment $[v_k,v_{k+1}]$, a second-order Taylor bound
  $\Re f(v_k+t(v_{k+1}-v_k))\le\Re f(v_k)+t\Re(f'(v_k)(v_{k+1}-v_k))+C t^2|v_{k+1}-v_k|^2$, with $C$ an
  upper bound of $|\Psi''|$ on a box containing the segment, is applied from both ends and shows
  $\Re f\le T_0:=-29.78$. Here $T_0$ is the lower end $-29.7790173$ of the enclosure of $\Re\Omega$
  in (S0) minus $9.827\cdot10^{-4}$, so $T_0\le\Re\Omega-9.827\cdot10^{-4}$; this
  gives (S2) with margin $9.827\cdot10^{-4}$. The two short connectors $[v_4,v_5]=[v_4,x_0-\rho d]$ and
  $[v_6,v_7]=[x_0+\rho d,v_7]$ lie in discs of radius $10^{-9}$ around the rational points $v_4,v_7$, on
  which $\Re f\le T_0$ is checked directly. Moving the start point by $|e|\le\delta_0$ changes $f$ by at most
  $\delta_0\sup|f'|\le10^{-5}$ on the first segment, which costs $10^{-5}$ of the margin; hence
  $\etafar=9.727\cdot10^{-4}$. The sector condition is checked on boxes covering all segments.
\item (S3): $\partial_y\Re f(\xtop+iy)=2\pi-\Im\Psi'(\xtop+iy)$. Box evaluations give
  $\Im\Psi'(\xtop+iy)\ge7$ for $0\le y\le900.19-\Im\xtop$, and for $Y:=\Im\xtop+y\ge900.19$ the bound
  \[
    \Im\Psi'(X+iY)\ge\frac\pi2\sum_ic_i-\sum_i\frac{|c_i||s_iX+u_i|}{Y}=3\pi-\frac{738.09\ldots}{Y}\ge8.6
  \]
  applies, with $X:=\Re\xtop$. The sector
  condition on the ray follows from $|\alpha_i|\ge\Im\xtop\ge60$ and
  $|\arg\alpha_i|\le\frac\pi2+\frac{13}{60}$.\qedhere
\end{itemize}
\end{proof}

At the saddle, $\Psi'(x_0)=2\pi i$, so $-(\Psi'(x_0)-3\pi i)^2/4=\pi^2/4$ and
\begin{equation}\label{eq:Ax0}
  A(x_0)=\tfrac14(2x_0+1)e^{\psi_\flat(x_0)}\ne0,
\end{equation}
since $\Re x_0\ge0$. The numerical values are $x_0\approx1.17192+0.00997i$, $K_\star\approx260.8$ and
$\sin(480\Im\Omega)\approx0.99757$. The contour from $x_c$ to $\xtop$ has $46$ segments: $4$ on the
lower steepest-descent curve, a connector, the Taylor segment $[v_5,v_6]$, a connector, and $39$ on the
upper curve.

\subsection{The integrand along the contour}

Put
\[
  \lambda_n:=-Gn\log n+Gn-29\log n+3\log2\pi .
\]

\begin{proposition}\label{prop:integrand}
Let $a>0$ and $0<\eta\le\pi$. There are $n_1$ and $C$, depending only on $a$ and $\eta$, with the following property.
Let $n\ge n_1$, and let $x$ satisfy $\Im x>0$, $\Re x\ge0$ and the sector condition $(a,\eta)$. Then
\[
  F_n(nx)=n\,e^{\lambda_n+nf(x)}A_n(x)
\]
for a number $A_n(x)$ with
\begin{enumerate}
\item[(U)] $|A_n(x)|\le C(|x|+3)^{164}$;
\item[(M)] $|A_n(x)-A(x)|\le C(|x|+3)^{164}\bigl(n^{-1}+e^{-2\pi n\Im x}\bigr)$.
\end{enumerate}
\end{proposition}

\begin{proof}
Let $\varsigma=\sin(\eta/2)$. Apply Corollary~\ref{cor:stirling} to each factor, with
$\alpha=\alpha_i(x)$ and $\beta=\beta_i$; note $s_i(nx)+nu_i+\beta_i=n\alpha_i(x)+\beta_i$. Summing with
weights $c_i$ and using \eqref{eq:factorid}, the main terms add up to
\[
  -Gn\log n+n\Psi(x)+Gn-29\log n+\psi_\flat(x)+3\log2\pi=\lambda_n+n\Psi(x)+\psi_\flat(x).
\]
Hence $P_n(nx)=n(2x+1+\frac1n)\exp(\lambda_n+n\Psi(x)+\psi_\flat(x)+e_n)$ with
$|e_n|\le76(9+1/(6\varsigma^2))/(an)$. Similarly, since $\sum_ic_is_i\log n=0$ and
$|2nx+n+1|\ge n\Re(2x+1)\ge n$,
\[
  |\mu(nx)-\Psi'(x)|\le\frac2n+\frac{76(4+1/(8\varsigma^3))}{an},\qquad
  |\mu'(nx)|\le\frac4{n^2}+\frac{76(3+1/\varsigma^4)}{an}.
\]
With $\mathbf q=e^{2\pi inx}$ and Lemma~\ref{lem:FPH},
$F_n(nx)=P_n(nx)\mathbf q^{-1}(\mathbf qH_n(nx))/\pi^2$, and $\mathbf q^{-1}e^{n\Psi(x)}=e^{nf(x)}$. So the
claimed formula holds with
\[
  A_n(x):=\frac{(2x+1+\frac1n)e^{\psi_\flat(x)+e_n}}{\pi^2}\,\mathbf qH_n(nx).
\]
Since $a\le|\alpha_i(x)|\le|x|+3$, we have $|\log\alpha_i(x)|\le\log(|x|+3)+|\log a|+\pi$. By
\eqref{eq:factorid} this gives $|\Psi'(x)|\le C_1(|x|+3)$ and
$|e^{\psi_\flat(x)}|\le e^{41(|\log a|+\pi)}(|x|+3)^{41}$. Let $B$ be the largest of $1$, $2|x|+2$ and these
two bounds, so $B\le C_2(|x|+3)^{41}$. For $n\ge n_1$ the errors $e_n$, $\mu(nx)-\Psi'(x)$ and $\mu'(nx)$
are at most $1$ in modulus. Since $|\mathbf q|\le1$, \eqref{eq:qform} gives $|\mathbf qH_n|\le C_3B^2$, and
(U) follows. For (M), write \eqref{eq:qform} as
$\mathbf qH_n=-\frac14[(\mu-3\pi i)^2+\mu']+\mathbf q\,\Xi$ with $|\Xi|\le C_4B^2$, and compare with
$-\frac14(\Psi'-3\pi i)^2$: the difference is $O(B/n)+O(B^2|\mathbf q|)$, with
$|\mathbf q|=e^{-2\pi n\Im x}$. Also $|(2x+1+\frac1n)e^{\psi_\flat+e_n}-(2x+1)e^{\psi_\flat}|=O(B^2/n)$. Combining
these gives (M).
\end{proof}

\subsection{Deformation of the contour}

\begin{lemma}\label{lem:deform}
Let $c\in(0,rn+1)\setminus\ZZ$, and let $w_0=c,w_1,\allowbreak \dots,w_{K'}\in\CC$ be such that every point of every
segment $[w_k,w_{k+1}]$ other than $w_0$ has positive imaginary part, and $\Re w_k\ge0$ for all $k$.
Then
\[
  i\int_0^\infty F_n(c+iy)\,dy=\sum_{k=0}^{K'-1}\int_{[w_k,w_{k+1}]}F_n(z)\,dz+i\int_0^\infty F_n(w_{K'}+iy)\,dy .
\]
\end{lemma}

\begin{proof}
Let $\delta:=\min_{m\in\ZZ}|c-m|\in(0,\frac12]$; note $\delta\le c$. On
$U:=\{\Im z>0\}\cup\{|z-c|<\delta\}$, $F_n$ is holomorphic: $U$ contains no integer and no pole of
$R_n''$. $U$ is star-shaped with respect to $c+i\delta/2$ (both pieces are convex and contain this
point), so $F_n$ has a primitive on $U$. For $Y>\Im w_{K'}$ consider the closed polygon
$c\to c+iY\to\Re w_{K'}+iY\to w_{K'}\to w_{K'-1}\to\dots\to w_0=c$, which lies in $U$; the integral of
$F_n$ around it is $0$. The horizontal side lies in $\Re z\ge0$, where $|F_n(z)|\le\pi C\sinh(\pi Y)^{-1}$
by Lemma~\ref{lem:decay}, so its contribution tends to $0$ as $Y\to\infty$. The two vertical
integrals converge absolutely, again by Lemma~\ref{lem:decay}.
\end{proof}

\subsection{Laplace's method}

\begin{lemma}\label{lem:laplace}
Let $K_1,\rho_1>0$, $M_1\ge0$ with $M_1\rho_1\le\frac32K_1$. Let $\phi,g:[-\rho_1,\rho_1]\to\CC$ be
continuous, with $|\phi(s)+K_1s^2/2|\le M_1|s|^3/6$, $|g|\le A_0$ and $|g(s)-g(0)|\le A_1|s|$. Then
for $n>0$
\[
  \Bigl|\int_{-\rho_1}^{\rho_1}e^{n\phi(s)}g(s)\,ds-g(0)\sqrt{\frac{2\pi}{nK_1}}\Bigr|
  \le\frac1n\Bigl(\frac{8A_0M_1}{3K_1^2}+\frac{2A_1}{K_1}\Bigr)+A_0e^{-nK_1\rho_1^2/4}\sqrt{\frac{4\pi}{nK_1}} .
\]
Moreover $\Re\phi(s)\le0$.
\end{lemma}

(The formalisation proves the same estimate with the larger constants
$(16\sqrt{2\pi}/3)\cdot A_0M_1/K_1^2$ and $2\sqrt{2\pi}\cdot A_1/K_1$; only the order $O(1/n)$ is used.)

\begin{proof}
Write $\phi(s)=-K_1s^2/2+T(s)$. Then $|T(s)|\le M_1|s|^3/6\le M_1\rho_1s^2/6\le K_1s^2/4$, so
$\Re\phi\le-K_1s^2/4\le0$ and
\begin{align*}
  |e^{n\phi}-e^{-nK_1s^2/2}|&=e^{-nK_1s^2/2}|e^{nT}-1|\le e^{-nK_1s^2/2}n|T|e^{n|T|}\\
  &\le\frac{nM_1|s|^3}6e^{-nK_1s^2/4}.
\end{align*}
Split
\begin{multline*}
  \int e^{n\phi}g=g(0)\int e^{-nK_1s^2/2}+\int e^{-nK_1s^2/2}(g(s)-g(0))\\
  +\int(e^{n\phi}-e^{-nK_1s^2/2})g.
\end{multline*}
The second integral is at most $A_1\int_\RR|s|e^{-nK_1s^2/2}ds=2A_1/(nK_1)$, and the third at most
\[
  \frac{nM_1A_0}6\int_\RR|s|^3e^{-nK_1s^2/4}ds=\frac{8A_0M_1}{3nK_1^2}.
\]
Finally
$\int_{|s|>\rho_1}e^{-nK_1s^2/2}ds\le e^{-nK_1\rho_1^2/4}\int_\RR e^{-nK_1s^2/4}ds$.
\end{proof}

\subsection{The asymptotic formula and nonvanishing}

\begin{proposition}\label{prop:asymp}
Let $\theta:=\Im\Omega$ and $C_0:=d\,A(x_0)\sqrt{2\pi/K_\star}$, so $C_0\ne0$ by \eqref{eq:Ax0}; write
$C_0=|C_0|e^{i\phi_0}$. Then, as $n\to\infty$ in $480\NN$,
\[
  L_n=-\frac1\pi\,n^{3/2}e^{\lambda_n+n\Re\Omega}\Bigl(|C_0|\sin(n\theta+\phi_0)+o(1)\Bigr).
\]
\end{proposition}

\begin{proof}
Let $c_n:=\lfloor nx_c\rfloor+\frac12$. Since $0<x_c<r$, we have $0<c_n<rn+1$ and $c_n\notin\ZZ$, and
$\chi_n:=c_n/n-x_c$ satisfies $|\chi_n|\le\frac1{2n}\le\delta_0$ for large $n$. Let
$J_n:=i\int_0^\infty F_n(c_n+iy)\,dy$. By Proposition~\ref{prop:contour}, $L_n=-\frac1\pi\Im J_n$. Apply
Lemma~\ref{lem:deform} with $w_0=c_n$ and $w_k=nv_k$ $(1\le k\le46)$; the hypotheses hold by (P), since
$\Im(c_n+t(nv_1-c_n))=tn\Im v_1>0$ for $t>0$. Thus $J_n$ is the sum of the $46$ segment integrals and
the integral over the vertical ray from $n\xtop$.

\emph{The Taylor segment.} Parametrising $[nv_5,nv_6]$ by $z=n(x_0+sd)$, $|s|\le\rho$, and using
Proposition~\ref{prop:integrand} (applicable by (S1$'$), (S4) and $\Re(x_0+sd)\ge0$, which holds since
$\Re v_5,\Re v_6\ge0$),
\[
  \int_{[nv_5,nv_6]}F_n(z)\,dz=n^2d\,e^{\lambda_n+n\Omega}\mathcal D_n,\qquad
  \mathcal D_n:=\int_{-\rho}^{\rho}e^{n\phi(s)}A_n(x_0+sd)\,ds,
\]
where $\phi(s):=f(x_0+sd)-\Omega$.
Since $f'(x_0)=\Psi'(x_0)-2\pi i=0$, $f''(x_0)d^2=\Psi''(x_0)d^2=-K_\star$ and $|f'''|=|\Psi'''|\le M_3$ on the
disc, Taylor's formula gives $|\phi(s)+K_\star s^2/2|\le M_3|s|^3/6$. By Lemma~\ref{lem:laplace}, $\Re\phi\le0$.
By (M) with $\Im(x_0+sd)\ge\Im x_0-\rho>0$,
$|\mathcal D_n-\int_{-\rho}^{\rho}e^{n\phi(s)}A(x_0+sd)\,ds|=O(n^{-1})$. The function $A$ is holomorphic on
$\Im x>0$, hence bounded and Lipschitz on the disc, and Lemma~\ref{lem:laplace} (with $K_1=K_\star$,
$M_1=M_3$, $\rho_1=\rho$) gives
\[
  \mathcal D_n=A(x_0)\sqrt{2\pi/(nK_\star)}+O(n^{-1}).
\]
\emph{The far part.} Let $E_n$ be the sum of the other $45$ segment integrals and the ray integral. On
each of these segments, (S2) and (U) give $|F_n(z)|\le Cn\,e^{\lambda_n+n(\Re\Omega-\etafar)}$; the
segments have length $O(n)$. (For the first segment, $z=n((x_c+\chi_n)+t(v_1-x_c-\chi_n))$ with
$|\chi_n|\le\delta_0$.) On the ray, $z=n(\xtop+iu)$, $u\ge0$, and (S3), (U) give
$|F_n(z)|\le Cn\,e^{\lambda_n+n(\Re\Omega-\etafar)}e^{-n(7-2\pi)u}(|\xtop|+u+3)^{164}$, whose integral
over $dz=in\,du$ is $O(n^2e^{\lambda_n+n(\Re\Omega-\etafar)})$ because $n(7-2\pi)\ge 1$. (The
formalisation uses the cruder bound $B\le Ce^{41|x|}$ in the proof of
Proposition~\ref{prop:integrand}, and accordingly needs $n(7-2\pi)\ge165$.) Hence
$|E_n|=O(n^2e^{\lambda_n+n\Re\Omega-n\etafar})$.

\emph{Conclusion.} Combining,
\begin{align*}
  n^{-3/2}e^{-\lambda_n}J_n&=e^{n\Omega}\bigl(C_0+O(n^{-1/2})\bigr)+O\bigl(n^{1/2}e^{-n\etafar}\bigr)e^{n\Re\Omega}\\
  &=C_0e^{n\Omega}+o(e^{n\Re\Omega}),
\end{align*}
and $\Im(C_0e^{n\Omega})=|C_0|e^{n\Re\Omega}\sin(n\theta+\phi_0)$.
\end{proof}

\begin{lemma}\label{lem:sines}
For real $u,v$: $|\sin u|+|\sin(u+v)|\ge|\sin v|$.
\end{lemma}

\begin{proof}
$\sin v=\sin(u+v)\cos u-\cos(u+v)\sin u$.
\end{proof}

\begin{corollary}\label{cor:nonvan}
For all sufficiently large $n\in480\NN$, $L_n\ne0$ or $L_{n+480}\ne0$. In particular $L_n\ne0$ for
infinitely many $n\in480\NN$.
\end{corollary}

\begin{proof}
By Lemma~\ref{lem:sines} with $v=480\theta$ and (S0), for every $n$,
$\max(|\sin(n\theta+\phi_0)|,|\sin((n+480)\theta+\phi_0)|)\ge\frac12\sin(480\theta)>0.49$. By
Proposition~\ref{prop:asymp}, once the $o(1)$ terms are below $0.49|C_0|$, the corresponding $L$ is
nonzero.
\end{proof}

\begin{remark}\label{rem:saddlesize}
Proposition~\ref{prop:asymp} also gives $\log|L_n|\le\lambda_n+n\Re\Omega+O(\log n)
=-G\log n!+n\Re\Omega+O(\log n)$, with $\Re\Omega\le-29.7790172$. This is better than
Proposition~\ref{prop:size} by about $0.019$ per unit of $n$. We do not use it, and it is not part of the
formalisation.
\end{remark}

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

Put
\begin{equation}\label{eq:Q}
\begin{split}
  Q:=V+\Acert+20\log2&=-29.76+15.8256549806\ldots+13.8629436111\ldots\\
  &=-0.0714014\ldots<0 .
\end{split}
\end{equation}
Let $\ell_n:=D_nL_n$, $n\in480\NN$. By Corollary~\ref{cor:intform},
$\ell_n=a_n+\sum_{j=2}^{18}c_{n,j}\beta(2j)$ with $a_n,c_{n,j}\in\ZZ$. If $L_n\ne0$, Corollary~\ref{cor:logD} and Proposition~\ref{prop:size} give,
for large $n$,
\[
  \log|\ell_n|=\log D_n+\log|L_n|\le n\bigl(Q+\eps'_n+\eps''_n\bigr),
\]
the terms $\pm G\log n!$ cancelling. Since $Q<0$ and $\eps'_n,\eps''_n\to0$, it follows that
$|\ell_n|\le e^{nQ/2}$ for all large $n$ (trivially when $L_n=0$), so $\ell_n\to0$. On the other hand $D_n>0$, so by
Corollary~\ref{cor:nonvan}, $\ell_n\ne0$ for infinitely many $n$.

Suppose now that $\beta(4),\allowbreak \beta(6),\allowbreak \dots,\allowbreak \beta(36)$ are all rational, and let $\Delta\ge1$ be a common
denominator. Then $\Delta\ell_n\in\ZZ$ for every $n$. For the infinitely many $n$ with $\ell_n\ne0$ this
gives $|\Delta\ell_n|\ge1$, which contradicts $\ell_n\to0$. Hence at least one of
$\beta(4),\allowbreak \dots,\allowbreak \beta(36)$ is irrational. \qed

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

\subsection{What is formalised}
The repository \url{https://github.com/telaviv/beta-irrationality} \cite{BetaRepo}, at release tag
\lean{v1.0} (commit \lean{f8df497}), contains a proof of Theorem~\ref{thm:main} in Lean~4
\cite{LeanFour} (version v4.35.0) with Mathlib \cite{Mathlib} (version v4.35.0 \cite{Mathlib4}).
All declaration names and file paths in this section refer to that release. The formalisation covers
every step of the proof of Theorem~\ref{thm:main},
including the parts that a written proof would cite:
the prime number theorem, Stirling's formula with explicit remainder in sectors, the
contour-integral representation, the deformation of contours, and all numerical certificates. Paths
below are relative to the repository root, and declaration names refer to the version described here.

\subsection{The statement}
The two definitions that the reader has to check are, in
\lean{BetaIrrational\slash{}Defs.lean} and \lean{BetaIrrational\slash{}Statement.lean} (in namespace
\lean{BetaIrr}, after unfolding the auxiliary definition \lean{betaTerm}; \lean{dirichletBeta} is
\lean{noncomputable}):
\begin{quote}\ttfamily\small
def dirichletBeta (s : $\mathbb{N}$) : $\mathbb{R}$ :=\\
\hspace*{2em}$\sum$' m : $\mathbb{N}$, (-1 : $\mathbb{R}$)\^{}m / (2 * (m : $\mathbb{R}$) + 1)\^{}s\\[2pt]
def OneOfBeta4To36 : Prop :=\\
\hspace*{2em}$\exists$ j $\in$ Finset.Icc 2 18, Irrational (dirichletBeta (2 * j))\\[2pt]
theorem BetaIrr.I3.oneOfBeta4To36 : OneOfBeta4To36
\end{quote}
The theorem is in the file \lean{BetaIrrational\slash{}I3\slash{}MainUnconditional.lean}. Here $\sum'$ is
Mathlib's unconditional sum (\lean{tsum}); the file \lean{BetaIrrational\slash{}Defs.lean} proves that the
series is summable for $s\ge2$, so \lean{dirichletBeta s} is the genuine value $\beta(s)$.
\lean{Finset.Icc 2 18} is $\{2,\allowbreak \dots,18\}$, so the statement says that $\beta(2j)$ is irrational for
some $2\le j\le18$. \lean{Irrational x} is Mathlib's predicate $x\notin\QQ$.

The command \lean{lake env lean Axioms.lean} prints
\begin{quote}\ttfamily\small
'BetaIrr.I3.oneOfBeta4To36' depends on axioms:\\
\hspace*{2em}[propext, Classical.choice, Quot.sound]
\end{quote}
and it prints the same axiom list for each of the main ingredients listed in \lean{Axioms.lean}. These are Lean's
three standard axioms, which Mathlib also uses. The development contains no
\lean{sorry}, no added axiom and no \lean{native\_decide}, so no step relies on compiled code.

\subsection{Correspondence with the paper}
Table~\ref{tab:lean} lists the main formal counterparts.\footnote{\raggedright Files, relative to
\lean{BetaIrrational\slash{}}: \lean{Expansion.lean} (\lean{PFData}); \lean{I3\slash{}Concrete\slash{}Expansion.lean}
(\lean{R\_eq\_pfR}, \lean{pf\_symmetric}, \lean{expansion\_I3}, \lean{pf\_R2\_inner\_zero});
\lean{Arith\slash{}PSVal.lean} (\lean{psge\_*}); \lean{I3\slash{}Arith\slash{}LemmaA.lean}; \lean{I3\slash{}Arith\slash{}Integrality.lean};
\lean{Arith\slash{}LemmaBC.lean} (\lean{vge\_Bq}, \lean{vge\_rho\_of\_R2\_zero}); \lean{I3\slash{}Arith\slash{}Lemma4.lean}
(\lean{int\_*}, \lean{log\_D\_sub\_le}); \lean{I3\slash{}Arith\slash{}Size.lean}; \lean{I3\slash{}CertA\slash{}Pointwise.lean},
\lean{Tail.lean}, \lean{Attain.lean}, \lean{Cert.lean}; \lean{I3\slash{}CertAK\slash{}CertCompute.lean}
(\lean{bodyUnits\_400}); \lean{PNT\slash{}PrimeSums.lean}; \lean{PNT\slash{}Theta.lean}; \lean{I3\slash{}Glue\slash{}Sharp.lean};
\lean{I3\slash{}Glue\slash{}Main.lean} (\lean{arith\_I3}, \lean{oneOfBeta4To36\_of\_parts});
\lean{I3\slash{}Size\slash{}RBound.lean}, \lean{PhiBound.lean}, \lean{Main.lean}; \lean{Analytic\slash{}Contour.lean};
\lean{I3\slash{}Analytic\slash{}Gamma.lean}, \lean{LogDeriv.lean}, \lean{Deform.lean}, \lean{NonvanI3.lean};
\lean{Stirling\slash{}Bound.lean}, \lean{Scaled.lean}, \lean{Digamma.lean}, \lean{ScaledDigamma.lean};
\lean{I3\slash{}Interval\slash{}SaddleDataI3.lean}; \lean{Analytic\slash{}Laplace.lean}; \lean{Criterion.lean};
\lean{I3\slash{}MainCond.lean}; \lean{I3\slash{}MainUnconditional.lean}.} The theorem is
\lean{oneOfBeta4To36\_of\_certUnits} applied to the kernel-checked sum \lean{CertA.bodyUnits\_400}. It
goes through \lean{oneOfBeta4To36\_of\_parts}, whose inputs are the certificate inequality,
Proposition~\ref{prop:size} and Corollary~\ref{cor:nonvan}, and through the criterion
\lean{exists\_irrational\_of\_small\_forms}, which formalises Section~\ref{sec:proof}.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.3\textwidth}>{\raggedright\arraybackslash}p{0.66\textwidth}@{}}
\toprule
paper & Lean declaration (namespace \lean{BetaIrr}) \\
\midrule
Lemma~\ref{lem:pf}, Cor.~\ref{cor:form} & \lean{I3.R\_eq\_pfR}, \lean{I3.pf\_symmetric}, \lean{PFData.tsum\_alt\_R2\_even}, \lean{I3.expansion\_I3}\\
Lemmas~\ref{lem:psge}, \ref{lem:A}, Cor.~\ref{cor:A} & \lean{Arith.psge\_mul}, \lean{Arith.psge\_inv}, \lean{I3.Arith.vge\_a}, \lean{I3.Arith.a\_bound\_sharp}\\
Lemma~\ref{lem:B} & \lean{Arith.vge\_Bq}\\
Lemma~\ref{lem:C} & \lean{Arith.vge\_rho\_of\_R2\_zero}, \lean{I3.pf\_R2\_inner\_zero}\\
Prop.~\ref{prop:integral} & \lean{I3.Arith.int\_rho\_I3}, \lean{I3.Arith.int\_tau\_I3}\\
Props.~\ref{prop:smallprimes}, \ref{prop:decomp} & \lean{I3.Arith.small\_primes\_sum\_le}, \lean{I3.Arith.E2\_sub\_le}, \lean{I3.Arith.log\_D\_sub\_le}\\
Prop.~\ref{prop:pointwise}, Lemma~\ref{lem:tail} & \lean{I3.CertA.pointwise\_le\_eStar\_prime}, \lean{I3.CertA.eStar\_le\_tail}\\
Lemma~\ref{lem:step} & \lean{I3.CertA.eStar\_eq\_mid}, \lean{I3.CertA.eStar\_isGreatest}\\
Prop.~\ref{prop:certA} & \lean{I3.CertA.bodyUnits\_400}, \lean{I3.CertA.certFact\_of\_units}\\
Lemma~\ref{lem:pnt-tail}, Prop.~\ref{prop:lemma5} & \lean{PNT.eventually\_primeSum\_lemma5\_le}, \lean{I3.sharp\_of\_pointwise}, \lean{I3.arith\_I3}\\
prime number theorem & \lean{PNT.theta\_div\_tendsto}\\
Props.~\ref{prop:logR}, \ref{prop:Phi}, \ref{prop:size} & \lean{I3.Size.log\_R\_le\_fact}, \lean{I3.Size.Phi\_le\_V}, \lean{I3.size\_I3}\\
Prop.~\ref{prop:contour} & \lean{Analytic.hasSum\_alternating\_eq\_half\_line}\\
Lemmas~\ref{lem:gamma}, \ref{lem:FPH} & \lean{I3.Analytic.RC\_eq\_Pfun}, \lean{I3.Analytic.Fn\_eq\_PH}\\
Thm.~\ref{thm:stirling}, Cor.~\ref{cor:stirling} & \lean{Stirling.stirling\_sector}, \lean{Stirling.stirling\_scaled};
for $\psi$, $\psi'$: \lean{Stirling.digamma\_sector}, \lean{Stirling.deriv\_digamma\_sector}, \lean{Stirling.digamma\_scaled}, \lean{Stirling.deriv\_digamma\_scaled}\\
Thm.~\ref{thm:saddle} & \lean{I3.Interval.I3\_saddleData}\\
Lemmas~\ref{lem:deform}, \ref{lem:laplace} & \lean{I3.Analytic.contour\_eq\_polyline\_Fn}, \lean{Analytic.laplace\_bound}\\
Prop.~\ref{prop:asymp}, Cor.~\ref{cor:nonvan} & \lean{I3.Analytic.nonvan\_of\_saddleData}\\
Section~\ref{sec:proof} & \lean{exists\_irrational\_of\_small\_forms}, \lean{I3.oneOfBeta4To36\_of\_parts}, \lean{I3.oneOfBeta4To36\_of\_certUnits}, \lean{I3.oneOfBeta4To36}\\
\bottomrule
\end{tabular}
\caption{Formal counterparts of the main steps.}\label{tab:lean}
\end{table}

A few arguments are organised differently in the formalisation, because Mathlib (at the version used)
lacks some standard tools.
\begin{itemize}
\item Mathlib has no residue theorem. Proposition~\ref{prop:contour} is proved by subtracting the
  principal parts $(-1)^tR_n''(t)\bigl((z-t)^{-1}-(z-c+1)^{-1}\bigr)$ at the integers $c<t\le N$,
  removing the resulting removable singularities, applying Cauchy's theorem for rectangles, and
  evaluating the model integrals explicitly.
\item The deformation (Lemma~\ref{lem:deform}) uses primitives of holomorphic functions on unions of
  discs, extended to the upper half-plane together with a small disc around $c$.
\item Stirling's formula (Theorem~\ref{thm:stirling}) is proved from Euler's limit formula for $\Gamma$,
  an exact Euler--Maclaurin identity and Mathlib's Stirling formula for $n!$; this yields the
  constant $1/12$ of \cite[\S5.11(ii)]{DLMF}.
\item The prime number theorem in the form $\theta(y)/y\to1$ is ported from the PrimeNumberTheoremAnd
  project \cite{PNTplus} (Wiener--Ikehara route), through the port in the \lean{zeta5} repository of
  C\'esar Del Solar (GitHub \lean{domino14}) \cite{zeta5}. Only the \lean{PNTPort\slash{}} folder of that
  repository carries the Apache License~2.0, and the ported files keep it. Chebyshev's bound
  $\theta(y)\le y\log4$ is in Mathlib.
\item All error terms are explicit, except those coming from the prime number theorem and the
  compactness arguments in Section~\ref{sec:nonvan} (the amplitude bounds $A_0,A_1$ of
  Lemma~\ref{lem:laplace}, applied to $g(s)=A(x_0+sd)$ in the proof of Proposition~\ref{prop:asymp}).
\item Some explicit constants in the formal statements are weaker than in the text (e.g.\
  Lemma~\ref{lem:laplace}); only their finiteness is used.
\end{itemize}

\subsection{How the certificates are checked}\label{sec:lean-cert}
The arithmetic certificate and the saddle certificate are decidable statements about rational data,
proved by \lean{decide +kernel}, i.e.\ by evaluation in the Lean kernel; the $58$ logarithm enclosures
of Proposition~\ref{prop:Phi} are proved by \lean{norm\_num} from Mathlib's series bounds for $\log$.
All proofs are checked by the kernel. The data (event lists, polyline vertices, rational enclosures)
were produced by scripts that are not trusted: a wrong value would make the build fail, but could not
make a false statement provable. The generators of the arithmetic certificate and of the $\Phi$
enclosures are in the repository (\lean{scripts\slash{}certA\slash{}}, \lean{scripts\slash{}size\slash{}}); the ad hoc Python
generator of the polyline and the saddle boxes is not.

\emph{The arithmetic certificate} (Proposition~\ref{prop:certA}). The specification of $e^*$ and of the
event list (built with \lean{List.mergeSort}) is what the soundness proofs use, but the kernel cannot
evaluate it efficiently. The proof therefore passes through equivalent forms, each with a general proof
of equivalence: a closed form of $e^*$ that uses only natural-number arithmetic (it rests on the
observation behind \eqref{eq:Nidentity} that each block contributes $m_j(1+\lfloor y-\delta_jx\rfloor
-\lceil y-(1-\delta_j)x\rceil)$ in all cases); a structural merge sort; a decomposition of the event
list into $133$ windows, each sorted in the kernel and compared with literal data, together with a
check that their concatenation is strictly increasing; and a decomposition of the sum into $1{,}995$
chunks, each checked separately. The resulting value of the rounded body sum, $U$, agrees exactly with
an independent exact-rational Python implementation.

\emph{The saddle certificate} (Theorem~\ref{thm:saddle}). This uses a verified interval arithmetic with
rational endpoints (rounded outwards to the grid $2^{-p}\ZZ$), complex boxes, verified enclosures of
$\log$, $\arctan$, $\pi$ and $\arg$, the contraction lemma for (S0), and segment, disc and ray checks
as described in the proof of Theorem~\ref{thm:saddle}. The certified value of $\Re\Omega$ agrees with
two independent ball-arithmetic (Arb) implementations.

\emph{Caveat.} Two helper functions in the arithmetic-certificate code carry \lean{@[implemented\_by]}
attributes. These affect only compiled code (used by the scripts that generate the data); the kernel
never uses them, and they add no axiom.

\subsection{Cost}
A cold build takes more than an hour on a desktop computer. The arithmetic certificate dominates: about
$2.6$ CPU-hours for the chunk sums and about $1$ CPU-hour for the window checks, run as three parallel
import chains, with up to about $4$\,GB resident memory per process ($16$\,GB of RAM recommended). The
interval certificate takes about $30$ CPU-minutes.

\subsection{What has to be trusted}
Beyond the Lean kernel and the three axioms, the reader has to trust that the two definitions displayed
above express Theorem~\ref{thm:main}, and the Mathlib definitions they use (real numbers, \lean{tsum},
\lean{Irrational}, \lean{Finset.Icc}). Nothing else, in particular no numerical data and no generating
script, needs to be trusted. A reader who does not want to trust the elaborator's environment
handling can replay the environment with \lean{lean4checker}. 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{Remarks}\label{sec:remarks}
% ===========================================================================

\subsection{The margin}
The proof needs $Q=V+\Acert+20\log2<0$, and $Q\approx-0.0714$. The three terms are of size $30$, $16$
and $14$, so the margin is about $0.2\%$ of the largest term. It is thin, but each of the three numbers
is certified: $V$ by Proposition~\ref{prop:Phi}, $\Acert$ by exact rational arithmetic, and $\log2$ by
Mathlib's bounds. With the saddle-point exponent of Remark~\ref{rem:saddlesize} in place of $V$ one
would get $\Re\Omega+\Acert+20\log2\le-0.0904$.

\subsection{Effectivity}
The theorem is proved for $n\ge n_0$ with an unspecified $n_0$, because the prime number theorem is
used without an error term. This does not affect the irrationality statement. The other error terms
are explicit but large: for instance the small-prime term $312\sqrt\cN\log\cN$ of
Proposition~\ref{prop:decomp} falls below $0.0714\,n$ only for $n$ of order $10^{11}$ [numerical
estimate]. An effective version would need an explicit form of the prime number theorem and a sharper
count at the small primes.

\subsection{\texorpdfstring{Why $\beta(36)$}{Why beta(36)}}
The parameters were found by a numerical search over the block profile (offsets on the grid
$\frac1{160}\ZZ$) and over $r$ [numerical, not part of the proof]. The optimum found is a nearly uniform
density of offsets on $(0,0.29]$, with about a quarter of the multiplicity on $\delta=0$. For the same
type of construction (triple zeros at every integer of the pole region) with total multiplicity
$S=33$ (which would give $\beta(4),\allowbreak \dots,\allowbreak \beta(34)$), the best value of $Q$ in the coarse model of the
search (offsets on $\frac1{80}\ZZ$, $r=13/12$) was $\approx+1.18$, against about $-0.15$ needed in that
model. Halving the grid gained about $0.06$, with decreasing returns, so $\beta(34)$ appears out of
reach for this family [heuristic].

\subsection{\texorpdfstring{Comparison with constructions that include $\beta(2)$}{Comparison with
constructions that include beta(2)}}
The construction of Zudilin \cite[\S3]{Zudilin2019}, with the parameters of Lai--Zhou
\cite[Thm.~6.1]{LaiZhou2021}, which reaches $\beta(2),\allowbreak \dots,\allowbreak \beta(10)$, uses simple zeros. For the
second-derivative form the zeros in the pole region must be triple (the proof of Lemma~\ref{lem:C}
needs $R_n''=0$ there), and differentiating twice raises every pole order by $2$, so each denominator
exponent grows by $2$. We believe that these two costs, three times the zero density and the shift
by $2$, account for the much larger number of values needed here [heuristic]; in exchange the form
never involves $\beta(2)$.

\section*{Acknowledgements and disclosure}
The construction, the proofs, the parameter search, the certificate programs, the Lean formalisation
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 this manuscript, was carried out by AI systems. 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, through the \lean{zeta5} repository of C\'esar Del Solar.

\bibliographystyle{amsplain}
\bibliography{references}

\end{document}