Irrationality of the dilogarithm at $-1/2$

Abstract.

We prove that $\operatorname{Li}_{2}(-1/2)$ is irrational. Irrationality of $\operatorname{Li}_{2}(1/s)$ was known for integers $s\leq-5$ and $s\geq 6$ by work of Hata and of Rhin and Viola, and Prellberg recently proved it for $s=-4,5,-3$. We define polynomials $G_{m}(T)$ with rational coefficients by an interpolation determinant. The rank of this determinant modulo primes $p$ with $m/5<p<5m/4$ bounds the denominators of the coefficients. A concavity inequality for a logarithmic energy bounds $G_{m}(\operatorname{Li}_{2}(-1/2))$. The only interval-arithmetic step is the potential certificate. The exact data in Table A.1, the coefficients of $G_{4}$, and the $9\times 9$ determinant modulo $11$ are printed and hand-checkable. A congruence modulo $11$ shows that $G_{m}$ has no rational zero for $m=4\cdot 11^{t}$.

1. Introduction

For $|z|\leq 1$ let $\operatorname{Li}_{2}(z)=\sum_{k\geq 1}z^{k}/k^{2}$. Hata [3, Theorem 1.1] proved that $\operatorname{Li}_{2}(1/s)$ is irrational for every integer $s\leq-5$ and every $s\geq 7$. Rhin and Viola settled $s=6$ by their permutation group method [7, Section 6], and later treated negative arguments [8, Theorem 2.1 and Section 4]. Viola and Zudilin [10] introduced a six-parameter family of double integrals for dilogarithmic values. In 2024 Calegari, Dimitrov and Tang [1, Remark 2.8.2 and Section 15.2] listed the integers still open: $s\in\{-4,-3,-2,2,3,4,5\}$. Prellberg’s 2026 preprint [6, Theorem 1.1] proves the cases $s=-4,5,-3$. We prove the case $s=-2$.

Theorem 1.

The number $\operatorname{Li}_{2}(-1/2)$ is irrational.

By Landen’s identity [2, (25.12.3)], $\operatorname{Li}_{2}(1/3)+\operatorname{Li}_{2}(-1/2)=-\frac{1}{2}\log^{2}(2/3)$, so the case $s=3$ does not follow from Theorem 1.

Put $\beta=\operatorname{Li}_{2}(-1/2)$ and $m=4n$. Section 2 defines $G_{m}(T)\in\mathbb{Q}[T]$ by an interpolation determinant. Sections 3 and 4 give, for all large $m$,

$$\deg G_{m}\leq m\ \text{by Lemma~{}\ref{lem:moment-identity}},\qquad D_{m}^{*}G_{m}(T)\in\mathbb{Z}[T],\qquad D_{m}^{*}\in\mathbb{Q}_{>0},$$

(1.1) $$\limsup_{\begin{subarray}{c}m\to\infty\\ 4\mid m\end{subarray}}\frac{\log D_{m}^{*}}{m^{2}}\leq\tau<4.33,\qquad\log|G_{m}(\beta)|\leq-4.36m^{2}+870m\log m,$$

$$\tau=\frac{1881503}{369600}-\frac{53}{48}\log 2,\qquad 4.36-\tau>0.0347.$$

If $\beta=u/q_{0}$ with $q_{0}>0$, then $q_{0}^{m}D_{m}^{*}G_{m}(\beta)\in\mathbb{Z}$. Section 5 shows that it is nonzero for $m=4\cdot 11^{t}$, $t\geq 1$, and (1.1) shows that it tends to zero.

Lemma 4.2 is computer-assisted: it uses interval arithmetic (Appendix F). The other finite data are printed in Tables 2.1, 5.1 and A.1 and in (5.2). They were also rechecked in exact rational arithmetic.

2. The determinant

Put $a=-2$. For $n\geq 1$ let

$$\begin{gathered}m=4n,\qquad\sigma=k=h=n,\qquad L=m+h,\\ I=\{\sigma+k,\ldots,\sigma+k+m-1\},\quad J=\{\sigma,\ldots,\sigma+2m+h-1\},\quad\Lambda=\{1,\ldots,h\},\end{gathered}$$

all ordered increasingly. For $j\geq 0$ put

$$t_{j}=\sum_{u=1}^{j}\frac{a^{j-u}}{u},\qquad b_{j}=\sum_{u=1}^{j}\frac{a^{j-u}}{u^{2}};\qquad t_{0}=b_{0}=0.$$

For $i\in I$, $j\in J$ and $\ell\in\Lambda$ let

$$\begin{gathered}C_{ij}=\begin{cases}(a^{i}-a^{j})/(j-i),&i\neq j,\\ 0,&i=j,\end{cases}\quad B_{ij}=\begin{cases}(t_{i}-t_{j})/(j-i),&i\neq j,\\ b_{i},&i=j,\end{cases}\\ A_{ij}=a^{i}\delta_{ij},\qquad V_{\ell j}=\frac{1}{j+\ell},\qquad M_{ij}=\int_{0}^{1}\!\int_{0}^{1}\frac{x^{i}y^{j}}{2+xy}\,dx\,dy,\end{gathered}$$

and put

(2.1) $$G_{m}(T)=\det\begin{pmatrix}C\\ B-TA\\ V\end{pmatrix},$$

a determinant of size $2m+h$. For an indeterminate $a$ the same formulas define

$$G_{m}(T;a)=\det\begin{pmatrix}C(a)\\ B(a)-TA(a)\\ V\end{pmatrix}\in\mathbb{Q}[a,T];\qquad G_{m}(T)=G_{m}(T;-2).$$

Lemma 2.1.

One has $G_{m}\in\mathbb{Q}[T]$, $\deg G_{m}\leq m$, and

(2.2) $$M=B+\log(3/2)C-\beta A,\qquad G_{m}(\beta)=\det\begin{pmatrix}C\\ M\\ V\end{pmatrix}.$$

Proof.

Write $\lambda=\log(3/2)$ and

$$\mathfrak{m}_{j}=\int_{0}^{1}\frac{u^{j}}{2+u}\,du,\qquad\mathfrak{n}_{j}=\int_{0}^{1}\frac{u^{j}\log(1/u)}{2+u}\,du.$$

Polynomial division and the geometric series give

$$\begin{gathered}\mathfrak{m}_{0}=\lambda,\quad\mathfrak{n}_{0}=-\beta,\qquad\mathfrak{m}_{j}=a\mathfrak{m}_{j-1}+\frac{1}{j},\quad\mathfrak{n}_{j}=a\mathfrak{n}_{j-1}+\frac{1}{j^{2}}\quad(j\geq 1),\\ \mathfrak{m}_{j}=a^{j}\lambda+t_{j},\qquad\mathfrak{n}_{j}=b_{j}-a^{j}\beta.\end{gathered}$$

The substitution $u=xy$ gives

$$M_{ij}=\frac{\mathfrak{m}_{i}-\mathfrak{m}_{j}}{j-i}\quad(i\neq j),\qquad M_{ii}=\mathfrak{n}_{i}.$$

Hence the first identity in (2.2). Add $\lambda$ times each $C$ row to the corresponding row of $B-\beta A$. Only the $m$ middle rows depend on $T$, and their coefficients are rational. ∎

Put $r=3/5$ and

$$\gamma_{+}(\theta)=re^{i\theta}\quad(0\leq\theta\leq\pi),\qquad\gamma_{-}(\theta)=re^{i\theta}\quad(\pi\leq\theta\leq 2\pi).$$

With the real intervals oriented increasingly, let

$$\Gamma=[-2,-r]+[r,1]+(c_{\Gamma}-1)\gamma_{+}+c_{\Gamma}\gamma_{-},\qquad c_{\Gamma}=\frac{\log 2+i\pi}{2\pi i},$$

a linear combination of paths. For every integer $d$,

(2.3) $$\int_{\Gamma}z^{d-1}\,dz=\begin{cases}(1-a^{d})/d,&d\neq 0,\\ 0,&d=0.\end{cases}$$

For $d\neq 0$ integrate $z^{d}/d$ on each path. For $d=0$ the real intervals give $-\log 2$ and the arcs give $i\pi(2c_{\Gamma}-1)=\log 2$.

For $u=(u_{1},\ldots,u_{d})$ put $\Delta(u)=\prod_{i<j}(u_{j}-u_{i})$. Use variables $x=(x_{1},\ldots,x_{m})$, $v=(v_{1},\ldots,v_{L})$ and $z=(z_{1},\ldots,z_{m})$.

Lemma 2.2.

With product differentials $dx\,dv\,dz$,

(2.4) $$G_{m}(\beta)=\frac{2^{3m^{2}/2-m}}{(m!)^{2}L!}\int_{[0,1]^{m}}\int_{[0,1]^{L}}\int_{\Gamma^{m}}\Phi(x,v,z)\,dz\,dv\,dx,$$

where

$$\Phi(x,v,z)=\frac{\Delta(x)^{2}\Delta(v)^{2}\Delta(z)^{2}\displaystyle\prod_{d=1}^{m}\prod_{b=1}^{L}(z_{d}-v_{b})\displaystyle\prod_{i^{\prime}=1}^{m}x_{i^{\prime}}^{\sigma+k+h}\prod_{b=1}^{L}v_{b}^{\sigma}\prod_{d=1}^{m}z_{d}^{-m-k}}{\displaystyle\prod_{i^{\prime}=1}^{m}\prod_{b=1}^{L}(2+x_{i^{\prime}}v_{b})}.$$

Proof.

By (2.3), $C_{ij}=a^{i}\int_{\Gamma}z^{j-i-1}\,dz$. Put $f_{i}(v)=\int_{0}^{1}x^{i}/(2+xv)\,dx$. Then

$$M_{ij}=\int_{0}^{1}f_{i}(v)v^{j}\,dv,\qquad V_{\ell j}=\int_{0}^{1}v^{\ell-1}v^{j}\,dv.$$

Set $e_{\Delta}=m(m-1)/2$ and $\mathbf{w}=(z_{1},\ldots,z_{m},v_{1},\ldots,v_{L})$. Multilinearity in the rows and antisymmetrization, applied to the $L$ rows $[M;V]$, then to the $m$ rows $C$, and then to the $m$ functions $f_{i}$, give

$$G_{m}(\beta)=\frac{1}{(m!)^{2}L!}\int_{[0,1]^{m}\times[0,1]^{L}\times\Gamma^{m}}D_{z}D_{zv}D_{x}D_{xv}\,dx\,dv\,dz,$$

where

$$D_{z} =\det(a^{i}z_{d}^{-i-1})_{i\in I,\,1\leq d\leq m}=(-1)^{e_{\Delta}}a^{m(\sigma+k)+e_{\Delta}}\Delta(z)\prod_{d}z_{d}^{-\sigma-k-m},$$

$$D_{zv} =\det(\mathbf{w}_{b}^{j})_{1\leq b\leq 2m+h,\,j\in J}=(-1)^{mL}\Delta(z)\Delta(v)\prod_{d}z_{d}^{\sigma}\prod_{b}v_{b}^{\sigma}\prod_{d,b}(z_{d}-v_{b}),$$

$$D_{x} =\det(x_{i^{\prime}}^{i})_{i\in I,\,1\leq i^{\prime}\leq m}=\Delta(x)\prod_{i^{\prime}}x_{i^{\prime}}^{\sigma+k},$$

$$D_{xv} =\det\begin{pmatrix}((2+x_{i^{\prime}}v_{b})^{-1})_{1\leq i^{\prime}\leq m,\,1\leq b\leq L}\\ (v_{b}^{\ell-1})_{1\leq\ell\leq h,\,1\leq b\leq L}\end{pmatrix}=\frac{a^{e_{\Delta}}\Delta(x)\Delta(v)\prod_{i^{\prime}}x_{i^{\prime}}^{h}}{\prod_{i^{\prime},b}(2+x_{i^{\prime}}v_{b})}.$$

The last equality follows from the Cauchy–Vandermonde identity. Explicitly, for $t_{i^{\prime}}=2/x_{i^{\prime}}$,

$$\det\begin{pmatrix}((2+x_{i^{\prime}}v_{b})^{-1})_{i^{\prime},b}\\ (v_{b}^{\ell-1})_{\ell,b}\end{pmatrix}=\prod_{i^{\prime}}x_{i^{\prime}}^{-1}\det\begin{pmatrix}((t_{i^{\prime}}+v_{b})^{-1})_{i^{\prime},b}\\ (v_{b}^{\ell-1})_{\ell,b}\end{pmatrix}.$$

The Cauchy–Vandermonde identity is

$$\det\begin{pmatrix}((t_{i^{\prime}}+v_{b})^{-1})_{i^{\prime},b}\\ (v_{b}^{\ell-1})_{\ell,b}\end{pmatrix}=\frac{\Delta(t)\Delta(v)}{\prod_{i^{\prime},b}(t_{i^{\prime}}+v_{b})}.$$

This is the Cauchy–Vandermonde identity [4]. With the preceding row-scaling identity it gives the displayed formula for $D_{xv}$, and continuity covers $x_{i^{\prime}}=0$. We verify the identity by induction on $m$. At the induction step fix $i^{\prime}$, let $v^{\prime}=(v_{1},\ldots,v_{L-1})$, and let $\widehat{t}_{i^{\prime}}$ denote $t$ with $t_{i^{\prime}}$ omitted. After multiplying by $v_{L}+t_{i^{\prime}}$, the residue of the quotient at $v_{L}=-t_{i^{\prime}}$ is

$$(-1)^{i^{\prime}+L}\frac{\Delta(\widehat{t}_{i^{\prime}})\Delta(v^{\prime})}{\prod_{j\neq i^{\prime}}\prod_{b<L}(t_{j}+v_{b})}.$$

By induction this is the signed complementary minor on the determinant side, so the residues agree. After subtracting them, the difference is a polynomial in $v_{L}$ of degree at most $h-1$ and vanishes at the other $L-1\geq h$ variables $v_{1},\ldots,v_{L-1}$. For $h=0$ it tends to zero at infinity. The case $m=0$ is the Vandermonde identity.

The product of the four factors is $(-1)^{e_{\Delta}+mL}a^{m(\sigma+k)+2e_{\Delta}}\Phi$. Since $m=4n$, both signs are positive and $m(\sigma+k)+2e_{\Delta}=3m^{2}/2-m$. ∎

An exact calculation gives

(2.5) $$16336404000000000\,G_{4}(T)=\sum_{j=0}^{4}p_{j}T^{j},$$

with the coefficients in Table 2.1.

Table 2.1. The integer coefficients in (2.5).

$j$	$p_{j}$
$0$	$1110544836657482146420241$
$1$	$9902753530700468230399560$
$2$	$33113649760730054563219200$
$3$	$49212514324793465856000000$
$4$	$27426807951407972352000000$

3. The divisor

Put

$$N_{\mathrm{den}}=10n-1,\qquad U=11n-1,\qquad d_{\ell}=\operatorname{lcm}(1,\ldots,\ell),\qquad\mathcal{D}_{m}=d_{N_{\mathrm{den}}}^{3m}d_{U}^{n}.$$

For $F\in\mathbb{Q}[T]$ let $v_{p}(F)=\min_{j}v_{p}([T^{j}]F)$.

Lemma 3.1.

For an indeterminate $a$,

(3.1) $$P_{m}(a,T):=\mathcal{D}_{m}G_{m}(T;a)\in\mathbb{Z}[a,T].$$

Proof.

The denominators of a $C$ entry divide $d_{N_{\mathrm{den}}}$. An off-diagonal $B$ entry is a difference of harmonic sums divided by $j-i$, so its denominator divides $d_{N_{\mathrm{den}}}^{2}$, and so does that of $b_{i}$. The denominators of a $V$ entry divide $d_{U}$. ∎

3.1. Residue classes

For $\rho>0$ and $0\leq x<\rho$ let

(3.2) $$K(x,\rho) =\{k\geq 0:1/2\leq x+k\rho<3/2\},$$

$$\mathcal{L}(x,\rho) =\{l\geq 0:1/4\leq x+l\rho<5/2\},$$

$$W(x,\rho) =\{w\geq 1:0<w\rho-x\leq 1/4\},$$

and

(3.3) $$\mathfrak{r}(x,\rho)=\min(2|K|+|W|,|\mathcal{L}|)-\mathbf{1}_{\{K=\{0\},\,\mathcal{L}=\{0,1\},\,W=\varnothing\}},\qquad\mathfrak{c}(\rho)=1+\int_{0}^{\rho}\mathfrak{r}(x,\rho)\,dx.$$

Lemma 3.2.

Let $p$ be an odd prime with $p^{2}>U$, and let $a=-2$. Then

(3.4) $$v_{p}(G_{m})\geq-m-\sum_{u=0}^{p-1}\mathfrak{r}(u/m,p/m)=-m\mathfrak{c}(p/m).$$

Proof.

Multiply the $C,B,V$ rows by $p,p^{2},p$. Write $i=u+kp$, $j=u+lp$ with $0\leq u<p$. Only the harmonic terms with $p$ in the denominator survive modulo $p$, and $a^{p}\equiv a\pmod{p}$, so

$$pt_{u+kp}\equiv a^{u}t_{k},\qquad p^{2}b_{u+kp}\equiv a^{u}b_{k}\pmod{p}.$$

The scaled $C$ and $B$ entries vanish modulo $p$ between distinct residue classes modulo $p$. For a cross-class $B$ entry, the numerator is $p$-integral after the row scaling and the remaining factor $p/(j-i)$ is zero modulo $p$. Within a class, for $j\neq i$, $j-i=p(l-k)$ with $0<|l-k|<p$, so the quotient denominator is a unit. Diagonal entries have their displayed separate values. Thus within a class they reduce to $a^{u}C_{kl}$ and $a^{u}B_{kl}$, and $-p^{2}TA\equiv 0$. A $V$ row reduces to zero unless $\ell+u=pw$. Then its entry is $1/(l+w)$, without the factor $a^{u}$. All displayed denominators are units because $p^{2}>U$. So, after permutations, the reduction has blocks with $2|K|+|W|$ rows and $|\mathcal{L}|$ columns.

For $K=\{0\}$, $\mathcal{L}=\{0,1\}$, $W=\varnothing$ the block, with its rows divided by the unit $a^{u}$, is

(3.5) $$\begin{pmatrix}0&1-a\\ 0&-1\end{pmatrix}=\begin{pmatrix}0&3\\ 0&-1\end{pmatrix},$$

of rank one for every odd $p$. Every other block has rank at most the minimum of its dimensions. So the rank is at most $R=\sum_{u}\mathfrak{r}(u/m,p/m)$. The matrix has $2m+n$ rows. Row operations over $\mathbb{Z}_{(p)}$, independent of $T$, make its last $2m+n-R$ rows divisible by $p$. Subtracting the scaling exponent $3m+n$ gives the first inequality in (3.4).

Every boundary in (3.2) has the form $x=c_{0}+b\rho$ with $4c_{0},b\in\mathbb{Z}$. At $\rho=p/m$, $m=4n$, it lies in $m^{-1}\mathbb{Z}$. The $K,\mathcal{L}$ conditions are closed on the left and open on the right in $x$, and the $W$ condition is $w\rho-1/4\leq x<w\rho$. So $\mathfrak{r}$ is constant on each $[u/m,(u+1)/m)$, and

(3.6) $$\sum_{u=0}^{p-1}\mathfrak{r}(u/m,p/m)=m\int_{0}^{p/m}\mathfrak{r}(x,p/m)\,dx.\qed$$

For $1/5<\rho<5/4$ only $0\leq k\leq 7$, $0\leq l\leq 12$ and $1\leq w\leq 2$ occur. The sets in (3.2) change only on the lines

(3.7) $$\begin{gathered}x=0,\quad x=\rho,\quad x=1/2-k\rho,\quad x=3/2-k\rho\quad(0\leq k\leq 7),\\ x=1/4-l\rho,\quad x=5/2-l\rho\quad(0\leq l\leq 12),\\ x=w\rho-1/4,\quad x=w\rho\quad(1\leq w\leq 2).\end{gathered}$$

Cut $(1/5,5/4)$ at the values of $\rho$ where two of these lines meet in $0\leq x\leq\rho$, and let $\mathcal{C}$ be the set of these cut points. On each resulting interval the order of the lines in $0<x<\rho$ is fixed, so the sets (3.2) are constant on each $x$-interval between consecutive lines, and $\mathfrak{c}$ is affine. At both endpoints of each row, its five printed lines $\ell_{1},\ldots,\ell_{5}$, in their printed order, satisfy

$$0\leq\ell_{1}(\rho)\leq\ell_{2}(\rho)\leq\cdots\leq\ell_{5}(\rho)\leq\rho.$$

Every other distinct line in (3.7) is $\leq 0$ at both endpoints or $\geq\rho$ at both endpoints. Affineness and distinctness make the ordering strict in the interior, apart from boundary lines. Hence no intersection in $0\leq x\leq\rho$ is omitted. Table A.1 lists the $44$ intervals, the five lines in $0<x<\rho$ in increasing order, the values of $\mathfrak{r}$ on the six $x$-intervals, $\mathfrak{c}(\rho)$ and $\int\mathfrak{c}$. Each row can be checked by hand from (3.3). The table was also rechecked in exact rational arithmetic (Appendix F). Summation gives

(3.8) $$\int_{1/5}^{5/4}\mathfrak{c}(\rho)\,d\rho=\frac{1121513}{369600}.$$

The configuration of (3.5) occupies $5/2-2\rho\leq x<\rho-1/4$ for $11/12<\rho<1$, and $1/2\leq x<\rho-1/4$ for $1\leq\rho<5/4$. Its contribution to (3.8) is

$$-\int_{11/12}^{1}(3\rho-11/4)\,d\rho-\int_{1}^{5/4}(\rho-3/4)\,d\rho=-\frac{5}{48}.$$

3.2. Larger primes

For $p>5n$ define row potentials $\lambda_{C}=0$, $\lambda_{B}(i)$, $\lambda_{V}(\ell)$ and column potentials $\chi(j)$ by

$$5n<p<6n: \quad(\lambda_{B},\lambda_{V},\chi)=(1+\mathbf{1}_{i\geq p},\,1,\,\mathbf{1}_{j\geq p+2n}),$$

$$6n\leq p<8n: \quad(\lambda_{B},\lambda_{V},\chi)=(\mathbf{1}_{i+p<10n},\,1,\,\mathbf{1}_{j\geq p}),$$

$$8n\leq p<10n: \quad(\lambda_{B},\lambda_{V},\chi)=(0,\,1,\,\mathbf{1}_{j\geq p}),$$

$$10n\leq p\leq 11n-1: \quad(\lambda_{B},\lambda_{V},\chi)=(0,\,\mathbf{1}_{p-\ell\in J},\,0),$$

and put

$$E_{p}^{\rm out}=\begin{cases}19n-2p,&5n<p<8n,\\ 11n-p,&8n\leq p\leq U.\end{cases}$$

Lemma 3.3.

For an odd prime $5n<p\leq U$ one has $v_{p}(G_{m})\geq-E_{p}^{\rm out}$.

Proof.

A $C$ entry has a pole only at $j=i+p$, of order at most one. A $B$ entry has pole order at most

$$\mathbf{1}_{\max(i,j)\geq p}+\mathbf{1}_{\{\max(i,j)\geq p,\ i\equiv j\pmod{p}\}},$$

including the double pole of $b_{i}$ for $i\geq p$. A $V$ entry has a simple pole when $p\mid j+\ell$. As $p^{2}>U$, there are no higher powers.

In the first range every $B$ row has potential at least one, and two if $i\geq p$. A collision $j=i+p$ has $j\geq p+2n$, and its column gives the second unit. In the second range all $i<p$. The columns $j\geq p$ cover the simple $B$ poles and the $C$ poles. A collision needs $i+p<10n$, and its row gives the other unit. In the third range $i<p$ and $i+p\geq 10n$, so only simple $B$ poles remain. In these three ranges every $V$ row has potential one, which covers $j+\ell=p$ and $j+\ell=2p$. In the fourth range $i,j<p$, only $V$ poles remain, and the rows with $\lambda_{V}=1$ are those containing one. So $\lambda_{\rm row}+\chi_{j}$ dominates every pole order. Multiply each row and column by $p$ to the power of its potential. The potentials add up to $(10n-p)+n+(8n-p)$, $(8n-p)+n+(10n-p)$, $n+(10n-p)$ and $11n-p$ in the four ranges. ∎

3.3. The factor at two

Lemma 3.4.

Let $N_{m}=\lceil 53m^{2}/48\rceil-m$. Then

(3.9) $$P_{m}(a,T)\in a^{N_{m}}\mathbb{Z}[a,T].$$

Proof.

Work in $\mathbb{Q}[[a]][T]$. Write

$$S_{j}(a)=\sum_{u\geq 1}\frac{a^{u}}{u^{j}},\qquad v_{k}(i)=\begin{cases}(i-k)^{-1},&i\neq k,\\ 0,&i=k,\end{cases}\quad z_{k}(i)=v_{k}(i)^{2},\quad e_{k}(i)=\mathbf{1}_{i=k}.$$

Subtract $S_{1}(a)$ times each $C$ row from the paired row of $B-TA$. Comparison of coefficients, including the diagonal, gives

(3.10) $$\begin{pmatrix}C\\ B-TA-S_{1}C\end{pmatrix} =\sum_{k\geq 0}a^{k}\binom{v_{k}(I)}{-z_{k}(I)-(T+S_{2})e_{k}(I)}e_{k}(J)^{t}$$

$$\quad+\sum_{k\geq 0}a^{k}\binom{e_{k}(I)}{v_{k}(I)}v_{k}(J)^{t}+\sum_{k\geq 0}a^{k}\binom{0}{-e_{k}(I)}z_{k}(J)^{t}.$$

For example, the off-diagonal lower entry is $\sum_{k\geq 0}a^{k}v_{k}(i)v_{k}(j)-(a^{i}+a^{j})/(i-j)^{2}$, and the diagonal entry is $\sum_{k\geq 0}a^{k}v_{k}(i)^{2}-a^{i}(T+S_{2})=b_{i}-Ta^{i}$. Each coefficient of $a$ involves finitely many terms.

Expand along the $n$ rows of $V$, and expand each remaining $2m$-row minor by the rank-one summands in (3.10). A nonzero term selects $2m=8n$ distinct rank-one summands. At weight $k$ at most

$$c_{k}=1+\mathbf{1}_{k\in J}+\mathbf{1}_{k\in I}$$

occur: the first summand needs $k\in J$, the third needs $k\in I$. All entries, including $T+S_{2}$, have nonnegative order in $a$. So every term has order at least the sum of the $8n$ smallest available weights. This use of the infinite expansion is coefficientwise: modulo $a^{N_{m}+1}$ only finitely many $k$ occur, so Cauchy–Binet applies to a finite truncation and then gives the asserted formal divisibility.

There is one weight at each $0\leq k<n$, two at each $n\leq k<2n$, and three at each $2n\leq k<6n$. Write $5n=3d+\epsilon_{0}$, $0\leq\epsilon_{0}<3$. The minimum available-weight sum is

$$\sum_{k=0}^{n-1}k+2\sum_{k=n}^{2n-1}k+3\sum_{k=2n}^{2n+d-1}k+\epsilon_{0}(2n+d) =\frac{53n^{2}}{3}-4n+\frac{\epsilon_{0}(3-\epsilon_{0})}{6}$$

$$=\left\lceil\frac{53n^{2}}{3}\right\rceil-4n=N_{m}.$$

The minors of $V$ do not depend on $a,T$, so $a^{N_{m}}\mid G_{m}(T;a)$ in $\mathbb{Q}[a,T]$. By (3.1), division by the monic $a^{N_{m}}$ gives (3.9). ∎

3.4. Summation over primes

Lemma 3.5.

For every $m=4n$, there is a rational number $D_{m}^{*}>0$ with $D_{m}^{*}G_{m}(T)\in\mathbb{Z}[T]$ and

$$\log D_{m}^{*}\leq\tau m^{2}+o(m^{2}),\qquad\tau=\frac{1881503}{369600}-\frac{53}{48}\log 2=4.325296633153372\ldots,$$

so that $4.36-\tau>0.0347$.

Proof.

Put $e_{0}(p)=3m\lfloor\log_{p}N\rfloor+n\lfloor\log_{p}U\rfloor=v_{p}(\mathcal{D}_{m})$. For odd $p$, with the first line taking precedence, let

(3.11) $$E_{p}=\begin{cases}e_{0}(p),&p\leq m/5\ \text{or}\ p^{2}\leq U\ \text{or}\ p/m\in\mathcal{C}\ \text{or}\ p=5m/4,\\ m\mathfrak{c}(p/m),&m/5<p<5m/4,\\ E_{p}^{\rm out},&5m/4<p\leq U,\\ 0,&p>U,\end{cases}$$

and

$$D_{m}^{*}=2^{e_{0}(2)-N_{m}}\prod_{p\ {\rm odd}}p^{E_{p}}.$$

By (3.6), $m\mathfrak{c}(p/m)\in\mathbb{Z}$. Lemmas 3.1, 3.2, 3.3 and 3.4 give $v_{p}(D_{m}^{*}G_{m})\geq 0$ for every $p$. The exponent at two may be negative.

For all sufficiently large $m$, $p>m/5$ implies $p^{2}>U$. Put

$$\vartheta(y)=\sum_{p\leq y}\log p,\qquad\eta_{\rm PNT}(X)=\sup_{y\geq X}|\vartheta(y)/y-1|.$$

By the prime number theorem, $\eta_{\rm PNT}(X)\to 0$. For an affine $f$ on $[t_{0},t_{1}]\subset[1/5,11/4]$, Stieltjes integration by parts gives

$$m\sum_{t_{0}m<p<t_{1}m}f(p/m)\log p=m^{2}\int_{t_{0}}^{t_{1}}f(\rho)\,d\rho+O\bigl{(}\eta_{\rm PNT}(m/5)m^{2}+m\log m\bigr{)}.$$

There are finitely many pieces, and the excluded primes at cut points contribute $O(m\log m)$. For $p\leq m/5$ the first powers contribute $(13m/4)\vartheta(m/5)=(13/20)m^{2}+o(m^{2})$, and the higher powers, including those of two,

$$O\Bigl{(}m\sum_{j=2}^{\lfloor\log_{2}U\rfloor}\vartheta(U^{1/j})\Bigr{)}=O(m^{3/2}\log(3m)).$$

Subtract $N_{m}\log 2$ once. For $p>5m/4$ the exponent is $m\mathfrak{c}_{\rm out}(p/m)$ with

$$\mathfrak{c}_{\rm out}(\rho)=\begin{cases}19/4-2\rho,&5/4<\rho<2,\\ 11/4-\rho,&2\leq\rho\leq 11/4,\end{cases}\qquad\int_{5/4}^{11/4}\mathfrak{c}_{\rm out}(\rho)\,d\rho=\frac{9}{8}+\frac{9}{32}=\frac{45}{32}.$$

With (3.8),

$$\frac{13}{20}+\frac{1121513}{369600}+\frac{45}{32}-\frac{53}{48}\log 2=\tau.$$

The total error is $O(\eta_{\rm PNT}(m/5)m^{2}+m^{3/2}\log(3m))=o(m^{2})$. ∎

4. Analytic estimate

In (2.4) there are $m$, $L=5m/4$ and $m$ variables $x$, $v$, $z$. Let

$$\mathcal{K}_{x}=\mathcal{K}_{v}=[0,1],\qquad\mathcal{K}_{z}=[-2,-r]\cup[r,1]\cup\{z:|z|=r\}.$$

For $i\in\{x,v,z\}$, let

$$\mathcal{K}_{i}^{+}=\{q\in\mathbb{C}:\operatorname{dist}(q,\mathcal{K}_{i})\leq 3/4096\}.$$

The sets $\mathcal{K}_{z}^{+}$ avoid zero, and $\log|2+xv|$ is bounded on $\mathcal{K}_{x}^{+}\times\mathcal{K}_{v}^{+}$. For positive measures $\mu=(\mu_{x},\mu_{v},\mu_{z})$ of masses $(1,5/4,1)$ put

$$I(\sigma,\sigma^{\prime}) =\iint\log|u-v|\,d\sigma(u)\,d\sigma^{\prime}(v),\qquad D(\sigma,\sigma^{\prime})=\iint\log|2+uv|\,d\sigma(u)\,d\sigma^{\prime}(v),$$

$$\mathcal{Q}(\mu) =I(\mu_{x},\mu_{x})+I(\mu_{v},\mu_{v})+I(\mu_{z},\mu_{z})+I(\mu_{v},\mu_{z})-D(\mu_{x},\mu_{v}),$$

$$\mathcal{E}(\mu) =\frac{3}{2}\log 2+\mathcal{Q}(\mu)+\frac{3}{4}\int\log|u|\,d\mu_{x}+\frac{1}{4}\int\log|u|\,d\mu_{v}-\frac{5}{4}\int\log|u|\,d\mu_{z}.$$

For a fixed $\nu$ let $\mathcal{U}_{i}(q)=\int\log|q-t|\,d\nu_{i}(t)$, $D_{i}(q)=\int\log|2+qt|\,d\nu_{i}(t)$, and

$$F_{x}(q) =2\mathcal{U}_{x}(q)-D_{v}(q)+\tfrac{3}{4}\log|q|,$$

$$F_{v}(q) =2\mathcal{U}_{v}(q)+\mathcal{U}_{z}(q)-D_{x}(q)+\tfrac{1}{4}\log|q|,$$

$$F_{z}(q) =2\mathcal{U}_{z}(q)+\mathcal{U}_{v}(q)-\tfrac{5}{4}\log|q|.$$

Lemma 4.1.

On triples of positive measures $\mu=(\mu_{x},\mu_{v},\mu_{z})$ of masses $(1,5/4,1)$ with finite absolute logarithmic self-integrals and $\operatorname{supp}\mu_{x}\subseteq\mathcal{K}_{x}^{+}$, $\operatorname{supp}\mu_{v}\subseteq\mathcal{K}_{v}^{+}$, and $\operatorname{supp}\mu_{z}\subseteq\mathcal{K}_{z}^{+}$, respectively, the functional $\mathcal{Q}$ is concave. The same statement applies when all supports lie in the smaller sets $\mathcal{K}_{x},\mathcal{K}_{v},\mathcal{K}_{z}$.

(4.1) $$\mathcal{E}(\mu)\leq\frac{3}{2}\log 2-\mathcal{Q}(\nu)+\int F_{x}\,d\mu_{x}+\int F_{v}\,d\mu_{v}+\int F_{z}\,d\mu_{z}.$$

Proof.

For positive compactly supported measures $\eta_{1},\eta_{2}$ in a disk $D$ strictly containing their supports, the Green kernel of $D$ is $-\log|u-v|$ plus a bounded term. Cauchy–Schwarz for its energy, together with the finite absolute self-integrals, gives absolute logarithmic cross-integrability. Thus signed differences of the measures used below have finite absolute logarithmic energy.

For a real signed measure $\sigma=\sigma_{+}-\sigma_{-}$ of mass zero, with positive compactly supported parts of finite absolute logarithmic self-integrals, write $I_{\rm ST}=-I$ for the sign convention in Saff–Totik. Their positivity lemma [9, Lemma I.1.8] gives

$$\|\sigma\|^{2}=-I(\sigma,\sigma)\geq 0.$$

For smooth $\sigma$, the identity

$$-I(\sigma,\sigma)=\frac{1}{2\pi}\int_{\mathbb{C}}|\nabla\mathcal{U}^{\sigma}|^{2}\,dA$$

follows from $\Delta\mathcal{U}^{\sigma}=2\pi\sigma$ and integration by parts. The boundary term vanishes because the mass is zero. Approximation extends this Dirichlet-integral formula to the stated finite-energy measures. Put $\langle\sigma,\sigma^{\prime}\rangle=-I(\sigma,\sigma^{\prime})$.

Let $(\sigma_{x},\sigma_{v},\sigma_{z})$ have mass zero in each coordinate, and first let the $v$-support avoid zero. Put $R(v)=-2/v$. Then

$$\log|2+xv| =\log|x-R(v)|+\log|v|,$$

$$\log|R(v)-R(z)| =\log 2+\log|v-z|-\log|v|-\log|z|,$$

and the one-variable terms integrate to zero. With $\sigma^{\prime}_{x}=\sigma_{x}$, $\sigma^{\prime}_{v}=R_{*}\sigma_{v}$ and $\sigma^{\prime}_{z}=-R_{*}\sigma_{z}$,

$$\mathcal{Q}(\sigma) =-\|\sigma^{\prime}_{x}\|^{2}-\|\sigma^{\prime}_{v}\|^{2}-\|\sigma^{\prime}_{z}\|^{2}+\langle\sigma^{\prime}_{x},\sigma^{\prime}_{v}\rangle+\langle\sigma^{\prime}_{v},\sigma^{\prime}_{z}\rangle$$

$$=-\tfrac{1}{2}\bigl{(}\|\sigma^{\prime}_{x}-\sigma^{\prime}_{v}\|^{2}+\|\sigma^{\prime}_{v}-\sigma^{\prime}_{z}\|^{2}+\|\sigma^{\prime}_{x}\|^{2}+\|\sigma^{\prime}_{z}\|^{2}\bigr{)}\leq 0.$$

The $z$-supports here avoid zero. In general fix a probability $\lambda$ with smooth density supported in $[1/2,3/4]$, and put

$$\sigma_{v,\zeta}=\sigma_{v}|_{\{|v|>\zeta\}}-\sigma_{v}(\{|v|>\zeta\})\lambda.$$

It has mass zero and support away from zero, so $\mathcal{Q}(\sigma_{x},\sigma_{v,\zeta},\sigma_{z})\leq 0$. Finite energy excludes an atom at zero, so the coefficient of $\lambda$ tends to zero as $\zeta\to 0$. The cross-integrability just proved makes the logarithmic kernels integrable against the total variations, and the potential of $\lambda$ is bounded on compact sets. Dominated convergence in the original coordinates gives

$$\mathcal{Q}(\sigma_{x},\sigma_{v,\zeta},\sigma_{z})\longrightarrow\mathcal{Q}(\sigma_{x},\sigma_{v},\sigma_{z})\leq 0.$$

The kernel $\log|2+xv|$ is bounded on the sets specified above. For the reference and the smoothed measures below also $\int|\log|v||\,d|\sigma_{v}|(v)<\infty$: the reference has bounded interval density, and the smoothed measures stay away from zero. With

$$|\log|R(v)-R(w)||\leq\log 2+|\log|v-w||+|\log|v||+|\log|w||$$

and the first kernel identity, dominated convergence also applies to the inverted pairings.

Expand $\mathcal{Q}(\nu+\sigma)$ with $\sigma=\mu-\nu$. The quadratic part is nonpositive and $d\mathcal{Q}_{\nu}(\nu)=2\mathcal{Q}(\nu)$. Adding the linear terms gives (4.1). ∎

Lemma 4.2 (computer-assisted).

There is a positive $\nu$ of masses $(1,5/4,1)$, with $50$, $52$, $62$ constant-density intervals on $[0,1]$, $[0,1]$, $[-2,-3/5]$ and $157$ Poisson kernels on $|z|=3/5$, all with rational data, such that

$$F_{x}\leq K_{x}=-4.626,\qquad F_{v}\leq K_{v}=-4.480,\qquad F_{z}\leq K_{z}=-0.090$$

on $[0,1]$, $[0,1]$ and $[-2,-3/5]\cup[3/5,1]\cup\{|z|=3/5\}$, $\mathcal{Q}(\nu)$ satisfies (B.1), and, on the disk $|q|\leq\delta=1/250$,

(4.2) $$F_{x}(q)<-6.2823007011,\qquad F_{v}(q)<-4.4935082437.$$

The interval densities are at most $131,153,43$, and the Poisson densities (4.4) add up to at most $24$.

Proof.

The rational data of $\nu$ are printed in Tables D.1 and D.2. An interval $[t_{0},t_{1}]$ of mass $w$ carries $w\,dt/(t_{1}-t_{0})$. A Poisson entry $(c,w)$, $|c|<r$, is

$$\frac{w(r^{2}-|c|^{2})}{2\pi|re^{i\theta}-c|^{2}}\,d\theta\qquad(0\leq\theta\leq 2\pi).$$

The file anc/analytic/reference.json repeats these tables for the verification program. The weights are positive, the three masses are exact, and the Poisson entries are invariant under conjugation. An interval has potential

$$\frac{w}{t_{1}-t_{0}}\operatorname{Re}\{f(q-t_{0})-f(q-t_{1})\},\qquad f(u)=u\log u-u,$$

with $u\log|u|-u$ on the real line. A Poisson entry has potential

(4.3) $$w\begin{cases}\log|r^{2}-q\overline{c}|-\log r,&|q|\leq r,\\ \log|q-c|,&|q|\geq r.\end{cases}$$

Let $U_{P}(q)$ denote the Poisson contribution to the $z$-potential. Put

$$M_{P}=\sum_{c}w_{c}=\frac{26460009509}{40000000000},\qquad W_{P}:=M_{P}\log(151/250).$$

Since $r+\delta=151/250$, the 157 Poisson rows give

$$\sup_{|q|\leq\delta}U_{P}(q)\leq W_{P}.$$

Real interval energies use $g(u)=\tfrac{1}{2}u^{2}\log|u|-\tfrac{3}{4}u^{2}$, with $g^{\prime\prime}(u)=\log|u|$. For the denominator,

$$\log(2+xv)=\log 2+\sum_{j=1}^{420}\frac{(-1)^{j+1}(xv/2)^{j}}{j}+R_{420},\qquad|R_{420}|\leq\frac{2(1/2)^{421}}{421}.$$

The pair decomposition and its outward enclosures are printed in Table C.1. Since the product mass of $\nu_{x}\otimes\nu_{v}$ is $1\cdot(5/4)$, the integrated remainder is at most

$$\frac{5}{4}\frac{2(1/2)^{421}}{421}=\frac{5}{2\cdot 421\cdot 2^{421}}<1.10\times 10^{-129}.$$

The bounds for $F_{x},F_{v},F_{z}$ are proved by subdivision in Arb ball arithmetic [5]. On a real subinterval, each interval-potential component is quasi-convex: away from $t_{0},t_{1}$, its derivative has the sign of $\log|q-t_{0}|-\log|q-t_{1}|$, which changes from negative to positive at $(t_{0}+t_{1})/2$, while the negative denominator term is convex. On each side of $|q|=r$ a Poisson-entry potential is the logarithm of the distance from $q$ to a fixed point, hence quasi-convex, and a row containing $r=3/5$ also evaluates $q=r$. Thus the component maximum is bounded by the relevant endpoint values. On a subarc of the circle, the largest distance to a pole is at an endpoint or at the antipodal point. Interval sign tests exclude the antipodal point when possible. If it lies on the subarc, or if a sign test is inconclusive, the full-circle upper bound is used. Otherwise the endpoint values suffice. Table B.1 covers the real paths and the upper semicircle, and conjugation covers the lower one. On the subintervals meeting zero the positive term $\frac{3}{4}\log|q|$ or $\frac{1}{4}\log|q|$ is increasing in $|q|$ and equals $-\infty$ at zero. For a real pole $t$ and $q=re^{i\theta}$, $|re^{i\theta}-t|^{2}=r^{2}+t^{2}-2rt\cos\theta$. This is monotone in $\theta\in[0,\pi]$ for each fixed sign of $t$, which justifies the endpoint or antipodal alternatives.

On $|q|\leq\delta$ use $|q-t|\leq|t|+\delta$, $|2+qt|\geq 2-\delta$ and $\log|r^{2}-q\overline{c}|-\log r\leq\log(r+\delta)$ with the same primitives. This gives (4.2). An interval has density $w/(t_{1}-t_{0})$. With respect to arclength, a Poisson entry has density at most

(4.4) $$H_{c}=\frac{w(r+|c|)}{2\pi r(r-|c|)}.$$

The endpoint majorants and disk bounds are printed in Table C.2 and the density checks in Table C.3. The density checks are rational, by an integer square-root bound for each $|c|^{2}$ and by $\pi>333/106$, which follows from Machin’s formula:

$$16\left(\frac{1}{5}-\frac{1}{3\cdot 5^{3}}+\frac{1}{5\cdot 5^{5}}-\frac{1}{7\cdot 5^{7}}\right)-\frac{4}{239}=\frac{333}{106}+\frac{3418213}{41563593750}.\qed$$

For this $\nu$ put

$$\alpha=\mathcal{Q}(\nu)-\tfrac{3}{2}\log 2-K_{x}-\tfrac{5}{4}K_{v}-K_{z};$$

by (B.2), $\alpha>4.365$.

Lemma 4.3.

Put $(H_{x},H_{v},H_{z})=(131,153,67)$. If $0<d=|q-q^{\prime}|\leq 1/16$, then

$$|\mathcal{U}_{i}(q)-\mathcal{U}_{i}(q^{\prime})|\leq 8H_{i}d(1+|\log d|).$$

Proof.

Let $E\subset\mathbb{R}$ be a measurable set of measure $\ell_{E}\leq 9/5$ containing the real support. By the triangle inequality,

$$|\log|q-t|-\log|q^{\prime}-t||\leq\log\Bigl{(}1+\frac{d}{|q-t|}\Bigr{)}+\log\Bigl{(}1+\frac{d}{|q^{\prime}-t|}\Bigr{)}.$$

Replacing $q$ or $q^{\prime}$ by its real part increases each integral. Symmetric decreasing rearrangement gives

$$\int_{E}\log\Bigl{(}1+\frac{d}{|q-t|}\Bigr{)}\,dt\leq 2\int_{0}^{\ell_{E}/2}\log(1+d/t)\,dt\leq 2d\Bigl{(}1+\log\Bigl{(}1+\frac{\ell_{E}}{2d}\Bigr{)}\Bigr{)},$$

so

$$\int_{E}|\log|q-t|-\log|q^{\prime}-t||\,dt\leq 4d\Bigl{(}1+\log\Bigl{(}1+\frac{\ell_{E}}{2d}\Bigr{)}\Bigr{)}\leq 4d\Bigl{(}1+\log\Bigl{(}1+\frac{9}{10d}\Bigr{)}\Bigr{)}<8d(1+|\log d|),$$

by $d^{2}+9d/5\leq 149/1280<1$. The interval components have disjoint interiors, so multiply by the density bound. By (4.3), a Poisson component is Lipschitz with constant at most $w/(r-|c|)$, and by (4.4)

$$\frac{w}{r-|c|}=\frac{2\pi r}{r+|c|}H_{c}\leq 2\pi H_{c}<8H_{c}.$$

Summation and $43+24=67$ give the bound for $\mathcal{U}_{z}$. ∎

Lemma 4.4.

If $m=4n\geq 64$, then

$$\log|G_{m}(\beta)|\leq-4.36m^{2}+870m\log m.$$

Proof.

Expand $\Gamma^{m}$ in (2.4) into products of its four oriented pieces. On each piece use normalized arclength, and keep its coefficient and tangent phase until taking absolute values. Since $|c_{\Gamma}-1|=|c_{\Gamma}|$, the absolute weights add up to

$$\varkappa=(2-r)+(1-r)+2\pi r|c_{\Gamma}|=\frac{9}{5}+\frac{3}{5}\sqrt{\pi^{2}+\log^{2}2},$$

so the paths contribute a factor at most $\varkappa^{m}$. Only positive measures enter Lemma 4.1.

Put $\epsilon=m^{-2}$ and $\eta=3\epsilon$. Replace every atom $u$ by the uniform measure of mass $1/m$ on the circle $u+2i\epsilon+\epsilon e^{i\theta}$. The resulting $\mu_{x},\mu_{v},\mu_{z}$ have masses $(1,5/4,1)$ and finite energy. The common translation preserves differences, so by subharmonicity in each variable averaging increases every positive logarithmic pair. Each circle has energy $\log\epsilon$, so removing the diagonal adds

$$-(m+5m/4+m)\log\epsilon=\frac{13}{2}m\log m.$$

The positive endpoint terms also increase, since

(4.5) $$\frac{1}{2\pi}\int_{0}^{2\pi}\log|u+2i\epsilon+\epsilon e^{i\theta}|\,d\theta=\log|u+2i\epsilon|\geq\log u\quad(u>0).$$

If an original factor vanishes, there is nothing to prove.

For $m\geq 64$ the negative kernels satisfy the derivative bounds

(4.6) $$L_{D}=\frac{101}{100},\qquad L_{z}=\frac{167}{100},\qquad\frac{1+\eta}{2-2\eta-\eta^{2}}<L_{D},\qquad\frac{1}{r-\eta}<L_{z},$$

since a displacement of at most $\eta$ in each coordinate gives $|2+xv|\geq 2-2\eta-\eta^{2}$ and $|z|\geq r-\eta$. So the negative terms contribute at most

$$A_{0}=6\cdot\frac{5}{4}L_{D}+3\cdot\frac{5}{4}L_{z}=\frac{1107}{80}.$$

Discard the factorials and $2^{-m}$ in (2.4). Then the logarithm of the integrand, with its prefactor, is at most

(4.7) $$m^{2}\mathcal{E}(\mu)+\frac{13}{2}m\log m+A_{0}.$$

We bound the three fields in (4.1) on the smoothed measures. Put $\omega=1+\log(m^{2}/3)$. Lemma 4.3 with $d\leq 3\epsilon$ gives the coefficients

$$C_{x}=16H_{x}=2096,\qquad C_{v}=16H_{v}+8H_{z}=2984,\qquad C_{z}=16H_{z}+8H_{v}=2296,$$

$$C_{x}+\tfrac{5}{4}C_{v}+C_{z}=8122,$$

and a weighted error at most $3\cdot 8122\,\epsilon\omega$.

For an $x$ or $v$ center $u<\delta-3\epsilon$ the whole circle lies in $|q|<\delta$, where (4.2) applies. Otherwise $u\geq\delta-3\epsilon\geq\delta/2$, and (4.5) gives

$$\log|u+2i\epsilon|-\log u=\frac{1}{2}\log(1+4\epsilon^{2}/u^{2})\leq\frac{8\epsilon^{2}}{\delta^{2}}.$$

So the positive terms add at most $(17/16)8\epsilon^{2}/\delta^{2}$. By (4.6), the negative terms in the three fields add at most $A_{0}\epsilon$. At $m=64$, and hence for all larger $m$,

$$\frac{17}{16}\frac{8\epsilon}{\delta^{2}}+A_{0}\leq\frac{265625}{2048}+\frac{1107}{80}<200.$$

So the total smoothing error is at most $(3\cdot 8122+200)\epsilon\omega=24566\epsilon\omega<26000\epsilon\omega$. Insert the lower endpoint $q_{-}$ of (B.1) in (4.1). As

$$-\alpha<\frac{3}{2}\log 2-q_{-}+K_{x}+\frac{5}{4}K_{v}+K_{z}<-4.36,$$

we get $m^{2}\mathcal{E}(\mu)\leq-4.36m^{2}+26000\omega$. With (4.7) and the path factor,

$$\log|G_{m}(\beta)|\leq-4.36m^{2}+26000(1+\log(m^{2}/3))+\frac{13}{2}m\log m+m\log\varkappa+A_{0}.$$

Divided by $m\log m$, no positive term increases for $m\geq 64$. At $m=64$ their sum is

$$C_{*}=\frac{26000(1+\log(64^{2}/3))}{64\log 64}+\frac{13}{2}+\frac{\log\varkappa}{\log 64}+\frac{1107}{80\cdot 64\log 64}<810<870.\qed$$

5. Nonvanishing

Let $\mathbb{Z}_{(11)}=\{u/v\in\mathbb{Q}:11\nmid v\}$, and let $v_{11}$ be the $11$-adic valuation, $v_{11}(0)=+\infty$.

Lemma 5.1.

For $m=4$,

(5.1) $$G_{4}(T)\equiv g(T):=4+2T+7T^{2}+3T^{3}+9T^{4}\pmod{11},$$

and $g$ has no root in $\mathbb{F}_{11}$.

Proof.

Here $I=\{2,\ldots,5\}$, $J=\{1,\ldots,9\}$, $\Lambda=\{1\}$, and all denominators are prime to $11$. Modulo $11$ the matrix (2.1) is

(5.2) $$\begin{pmatrix}5&0&1&5&1&7&0&2&3\\ 3&1&0&9&1&9&8&0&7\\ 5&5&9&0&4&9&4&6&0\\ 2&1&1&4&0&3&4&3&10\\ 8&1+7T&8&2&2&5&6&0&1\\ 8&8&3+8T&7&10&4&0&5&9\\ 4&2&7&3+6T&2&8&5&10&5\\ 9&2&10&2&9+10T&3&1&9&3\\ 6&4&3&9&2&8&7&5&10\end{pmatrix}.$$

Its determinant is $g(T)$. Reduction of (2.5), where $16336404000000000\equiv 4\pmod{11}$, gives the same polynomial. Table 5.1 lists the values of $g$. None is zero. ∎

Table 5.1. The polynomial $g$ over $\mathbb{F}_{11}$.

$w$	0	1	2	3	4	5	6	7	8	9	10
$g(w)$	4	3	6	3	2	7	7	9	5	5	4

Lemma 5.2.

For every $\xi\in\mathbb{Q}$ and every integer $t\geq 1$, $G_{4\cdot 11^{t}}(\xi)\neq 0$.

Proof.

Put $Q_{t}=11^{t}$, $m_{t}=4Q_{t}$ and $h=\sigma=k=Q_{t}$, and

(5.3) $$P_{t}(W)=Q_{t}^{3m_{t}+h}G_{m_{t}}(W/Q_{t}^{2}).$$

This is the determinant obtained after $T=W/Q_{t}^{2}$ by multiplying the $C$, $B$ and $V$ rows by $Q_{t}$, $Q_{t}^{2}$ and $Q_{t}$. Every nonzero index, difference and Cauchy denominator has absolute value less than $11Q_{t}$, hence $11$-adic valuation at most $t$. So $Q_{t}t_{i}$, $Q_{t}^{2}b_{i}$ and all entries of the scaled matrix lie in $\mathbb{Z}_{(11)}[W]$. Hence $P_{t}\in\mathbb{Z}_{(11)}[W]$ and $\deg P_{t}\leq m_{t}$.

Let $a=-2$ and $0\leq u<Q_{t}$. Only the summation indices divisible by $Q_{t}$ survive, and $a^{Q_{t}}\equiv a\pmod{11}$, so

$$Q_{t}t_{Q_{t}j+u}\equiv a^{u}t_{j},\qquad Q_{t}^{2}b_{Q_{t}j+u}\equiv a^{u}b_{j}\pmod{11}.$$

The scaled $C$ and $B$ entries vanish modulo $11$ between distinct residue classes modulo $Q_{t}$. In the class $u$ write $i=Q_{t}i_{0}+u$, $j=Q_{t}j_{0}+u$. Then $2\leq i_{0}\leq 5$ and $1\leq j_{0}\leq 9$. The only $V$ row in this class is $\ell=Q_{t}-u$, with

$$\frac{Q_{t}}{j+\ell}=\frac{1}{j_{0}+1}.$$

Cross-class $C$ and $B$ entries have $11$-adic valuation at least $1$. Within a class the nonzero differences $j_{0}-i_{0}$ satisfy $|j_{0}-i_{0}|\leq 7<11$ and are units. All other scaled $V$ entries vanish modulo $11$. So, after permutations, the matrix has $Q_{t}$ diagonal blocks

$$\begin{bmatrix}a^{u}C_{4}\\ a^{u}(B_{4}-WA_{4})\\ V_{4}\end{bmatrix},\qquad 0\leq u<Q_{t},$$

where the subscript $4$ refers to $G_{4}$. Each block has eight rows with the factor $a^{u}$. Hence

(5.4) $$P_{t}(W)\equiv\varepsilon_{t}(-2)^{4Q_{t}(Q_{t}-1)}g(W)^{Q_{t}}\pmod{11},\qquad\varepsilon_{t}\in\{1,-1\}.$$

The constant coefficient and the coefficient of $W^{m_{t}}$ are $11$-adic units, and $\deg P_{t}=m_{t}$.

Take $W=Q_{t}^{2}\xi$. If $v_{11}(W)>0$, the constant term is the unique term of least valuation in $P_{t}(W)$. If $v_{11}(W)=0$, then (5.4) and Lemma 5.1 give $P_{t}(W)\not\equiv 0\pmod{11}$. If $v_{11}(W)<0$, write $P_{t}(W)=\sum_{j=0}^{m_{t}}c_{j}W^{j}$. Here $v_{11}(c_{m_{t}})=0$ and $v_{11}(c_{j})\geq 0$, so

$$v_{11}(c_{j}W^{j})>m_{t}v_{11}(W)=v_{11}(c_{m_{t}}W^{m_{t}})\qquad(0\leq j<m_{t}),$$

and the leading term is the unique term of least valuation. In all three cases $P_{t}(W)\neq 0$, and by (5.3) $G_{m_{t}}(\xi)\neq 0$. ∎

6. Proof of Theorem 1

Suppose $\beta=u/q_{0}$ with $u\in\mathbb{Z}$ and $q_{0}\in\mathbb{Z}_{>0}$. By Lemmas 2.1 and 3.5,

$$Z_{m}:=q_{0}^{m}D_{m}^{*}G_{m}(u/q_{0})\in\mathbb{Z}.$$

By Lemma 5.2, $Z_{m}\neq 0$ for $m=4\cdot 11^{t}$, $t\geq 1$. By Lemmas 3.5 and 4.4,

$$\log|Z_{m}|\leq-(4.36-\tau)m^{2}+870m\log m+o(m^{2})+m\log q_{0}.$$

As $4.36-\tau>0.0347$, the right-hand side tends to $-\infty$ along this sequence. So $0<|Z_{m}|<1$ for large $t$, which is impossible. ∎

Appendix A Arithmetic integration

In Table A.1 the second column lists the lines (3.7) in $0<x<\rho$, in increasing order of $x$. The third column lists $\mathfrak{r}$ on the six $x$-intervals they cut from $[0,\rho)$. Then $\mathfrak{c}(\rho)=1+\sum\mathfrak{r}\cdot(\text{length})$. In the last three rows the fifth value includes the correction $-1$ of (3.3). By (3.11), the values of $\mathfrak{c}$ at the cut points are not used. Of the lines (3.7), $25$ meet $0<x<\rho$ for some $\rho\in(1/5,5/4)$, and $27$ meet the closed interval after adding $x=0$ and $x=\rho$. The table has $44\cdot 6=264$ regions and $66$ distinct triples $(K,\mathcal{L},W)$.

Table A.1. Exact arithmetic integration.

$\rho$	lines in $0<x<\rho$	$\mathfrak{r}$	$\mathfrak{c}(\rho)$	$\int\mathfrak{c}\,d\rho$
$(1/5,9/44)$	$1/4-\rho,\,5/2-12\rho,\,3/2-7\rho,\,1/2-2\rho,\,2\rho-1/4$	$11,11,11,9,11,11$	$3+\rho$	$1409/96800$
$(9/44,5/24)$	$5/2-12\rho,\,1/4-\rho,\,3/2-7\rho,\,1/2-2\rho,\,2\rho-1/4$	$11,10,11,9,11,11$	$21/4-10\rho$	$841/69696$
$(5/24,11/52)$	$3/2-7\rho,\,1/4-\rho,\,1/2-2\rho,\,2\rho-1/4,\,5/2-11\rho$	$10,9,9,11,11,10$	$4-4\rho$	$493/48672$
$(11/52,3/14)$	$3/2-7\rho,\,1/4-\rho,\,1/2-2\rho,\,5/2-11\rho,\,2\rho-1/4$	$10,9,9,11,10,10$	$4-4\rho$	$573/66248$
$(3/14,7/32)$	$1/4-\rho,\,1/2-2\rho,\,5/2-11\rho,\,2\rho-1/4,\,3/2-6\rho$	$9,9,11,10,10,10$	$5/2+3\rho$	$1411/100352$
$(7/32,2/9)$	$1/4-\rho,\,1/2-2\rho,\,5/2-11\rho,\,3/2-6\rho,\,2\rho-1/4$	$9,9,11,10,9,10$	$17/4-5\rho$	$1813/165888$
$(2/9,9/40)$	$1/4-\rho,\,5/2-11\rho,\,1/2-2\rho,\,3/2-6\rho,\,2\rho-1/4$	$9,9,9,10,9,10$	$9/4+4\rho$	$283/32400$
$(9/40,5/22)$	$5/2-11\rho,\,1/4-\rho,\,1/2-2\rho,\,3/2-6\rho,\,2\rho-1/4$	$9,9,9,10,9,10$	$9/4+4\rho$	$347/48400$
$(5/22,11/48)$	$1/4-\rho,\,1/2-2\rho,\,3/2-6\rho,\,2\rho-1/4,\,5/2-10\rho$	$9,9,10,9,10,9$	$19/4-7\rho$	$3329/557568$
$(11/48,1/4)$	$1/4-\rho,\,1/2-2\rho,\,3/2-6\rho,\,5/2-10\rho,\,2\rho-1/4$	$9,9,10,9,9,9$	$2+5\rho$	$307/4608$
$(1/4,11/40)$	$\rho-1/4,\,5/2-9\rho,\,3/2-5\rho,\,1/2-\rho,\,1/4$	$8,9,8,7,8,9$	$9/2-5\rho$	$51/640$
$(11/40,5/18)$	$5/2-9\rho,\,\rho-1/4,\,3/2-5\rho,\,1/2-\rho,\,1/4$	$8,8,8,7,8,9$	$7/4+5\rho$	$451/51840$
$(5/18,9/32)$	$\rho-1/4,\,3/2-5\rho,\,1/2-\rho,\,1/4,\,5/2-8\rho$	$8,8,7,8,9,8$	$17/4-4\rho$	$451/41472$
$(9/32,2/7)$	$\rho-1/4,\,3/2-5\rho,\,1/2-\rho,\,5/2-8\rho,\,1/4$	$8,8,7,8,7,8$	$17/4-4\rho$	$349/25088$
$(2/7,7/24)$	$\rho-1/4,\,3/2-5\rho,\,5/2-8\rho,\,1/2-\rho,\,1/4$	$8,8,7,7,7,8$	$9/4+3\rho$	$349/18816$
$(7/24,3/10)$	$3/2-5\rho,\,\rho-1/4,\,5/2-8\rho,\,1/2-\rho,\,1/4$	$8,6,7,7,7,8$	$4-3\rho$	$83/3200$
$(3/10,11/36)$	$\rho-1/4,\,5/2-8\rho,\,1/2-\rho,\,1/4,\,3/2-4\rho$	$6,7,7,7,8,7$	$5/2+2\rho$	$559/32400$
$(11/36,5/16)$	$5/2-8\rho,\,\rho-1/4,\,1/2-\rho,\,1/4,\,3/2-4\rho$	$6,6,7,7,8,7$	$5/2+2\rho$	$449/20736$
$(5/16,9/28)$	$\rho-1/4,\,1/2-\rho,\,3/2-4\rho,\,1/4,\,5/2-7\rho$	$6,7,7,7,7,7$	$5/4+6\rho$	$353/12544$
$(9/28,1/3)$	$\rho-1/4,\,1/2-\rho,\,3/2-4\rho,\,5/2-7\rho,\,1/4$	$6,7,7,7,6,7$	$7/2-\rho$	$533/14112$
$(1/3,11/32)$	$\rho-1/4,\,5/2-7\rho,\,3/2-4\rho,\,1/2-\rho,\,1/4$	$6,7,6,5,6,7$	$9/2-4\rho$	$151/4608$
$(11/32,7/20)$	$5/2-7\rho,\,\rho-1/4,\,3/2-4\rho,\,1/2-\rho,\,1/4$	$6,6,6,5,6,7$	$7/4+4\rho$	$251/12800$
$(7/20,5/14)$	$5/2-7\rho,\,3/2-4\rho,\,\rho-1/4,\,1/2-\rho,\,1/4$	$6,6,4,5,6,7$	$7/2-\rho$	$881/39200$
$(5/14,3/8)$	$3/2-4\rho,\,\rho-1/4,\,1/2-\rho,\,1/4,\,5/2-6\rho$	$6,4,5,6,7,6$	$6-8\rho$	$43/784$
$(3/8,11/28)$	$1/2-\rho,\,\rho-1/4,\,5/2-6\rho,\,1/4,\,3/2-3\rho$	$4,6,6,5,6,5$	$15/4-2\rho$	$167/3136$
$(11/28,2/5)$	$1/2-\rho,\,5/2-6\rho,\,\rho-1/4,\,1/4,\,3/2-3\rho$	$4,6,5,5,6,5$	$15/4-2\rho$	$207/9800$
$(2/5,5/12)$	$5/2-6\rho,\,1/2-\rho,\,\rho-1/4,\,1/4,\,3/2-3\rho$	$4,4,5,5,6,5$	$7/4+3\rho$	$119/2400$
$(5/12,7/16)$	$1/2-\rho,\,\rho-1/4,\,3/2-3\rho,\,1/4,\,5/2-5\rho$	$4,5,5,5,5,5$	$1/2+6\rho$	$49/768$
$(7/16,9/20)$	$1/2-\rho,\,3/2-3\rho,\,\rho-1/4,\,1/4,\,5/2-5\rho$	$4,5,4,5,5,5$	$9/4+2\rho$	$251/6400$
$(9/20,11/24)$	$1/2-\rho,\,3/2-3\rho,\,\rho-1/4,\,5/2-5\rho,\,1/4$	$4,5,4,5,4,5$	$9/2-3\rho$	$251/9600$
$(11/24,1/2)$	$1/2-\rho,\,3/2-3\rho,\,5/2-5\rho,\,\rho-1/4,\,1/4$	$4,5,4,4,4,5$	$7/4+3\rho$	$17/128$
$(1/2,11/20)$	$1/4,\,\rho-1/4,\,5/2-4\rho,\,3/2-2\rho,\,1/2$	$4,4,5,4,3,4$	$19/4-3\rho$	$127/800$
$(11/20,9/16)$	$1/4,\,5/2-4\rho,\,\rho-1/4,\,3/2-2\rho,\,1/2$	$4,4,4,4,3,4$	$2+2\rho$	$249/6400$
$(9/16,7/12)$	$5/2-4\rho,\,1/4,\,\rho-1/4,\,3/2-2\rho,\,1/2$	$4,3,4,4,3,4$	$17/4-2\rho$	$149/2304$
$(7/12,5/8)$	$5/2-4\rho,\,1/4,\,3/2-2\rho,\,\rho-1/4,\,1/2$	$4,3,4,2,3,4$	$6-5\rho$	$143/1152$
$(5/8,2/3)$	$3/2-2\rho,\,1/4,\,\rho-1/4,\,1/2,\,5/2-3\rho$	$3,2,2,3,4,3$	$19/4-3\rho$	$15/128$
$(2/3,11/16)$	$3/2-2\rho,\,1/4,\,\rho-1/4,\,5/2-3\rho,\,1/2$	$3,2,2,3,3,3$	$11/4$	$11/192$
$(11/16,3/4)$	$3/2-2\rho,\,1/4,\,5/2-3\rho,\,\rho-1/4,\,1/2$	$3,2,2,2,3,3$	$11/4$	$11/64$
$(3/4,5/6)$	$5/2-3\rho,\,1/4,\,1/2,\,\rho-1/4,\,3/2-\rho$	$2,2,2,3,3,3$	$1/2+3\rho$	$23/96$
$(5/6,7/8)$	$1/4,\,1/2,\,\rho-1/4,\,3/2-\rho,\,5/2-2\rho$	$2,2,3,3,3,2$	$3$	$1/8$
$(7/8,11/12)$	$1/4,\,1/2,\,3/2-\rho,\,\rho-1/4,\,5/2-2\rho$	$2,2,3,2,3,2$	$19/4-2\rho$	$71/576$
$(11/12,1)$	$1/4,\,1/2,\,3/2-\rho,\,5/2-2\rho,\,\rho-1/4$	$2,2,3,2,1,2$	$19/4-2\rho$	$17/72$
$(1,9/8)$	$1/4,\,5/2-2\rho,\,3/2-\rho,\,1/2,\,\rho-1/4$	$2,2,2,0,1,2$	$15/4-\rho$	$43/128$
$(9/8,5/4)$	$5/2-2\rho,\,1/4,\,3/2-\rho,\,1/2,\,\rho-1/4$	$2,1,2,0,1,2$	$6-3\rho$	$39/128$

$$\int_{1/5}^{5/4}\mathfrak{c}(\rho)\,d\rho =1121513/369600, \int_{5/4}^{11/4}\mathfrak{c}_{\rm out}(\rho)\,d\rho =45/32,$$

$$\frac{13}{4}\cdot\frac{1}{5} =13/20, =1881503/369600,$$ sum

$$\text{coefficient of }\log 2 =53/48, =-5/48.$$ contribution of (3.5)

Appendix B Numerical values

The bounds in Table B.1 are rounded upward. The rational enclosures are

(B.1) $$q_{-}:=-4.911220867982619 <\mathcal{Q}(\nu)<-4.911220867982618,$$

(B.2) $$4.365058361177462 <\alpha<4.365058361177465,$$

$$3.730290307027085 <\varkappa<3.730290307027087;$$

the lower bound for $\alpha$ holds with $q_{-}$ in place of $\mathcal{Q}(\nu)$.

Table B.1. Upper bounds for $F_{x},F_{v},F_{z}$ in Lemma 4.2.

support	subintervals	depth	upper bound	$K$
$x\in[0,1]$	1164	15	$-4.6260004267$	$-4.626$
$v\in[0,1]$	1272	16	$-4.4800027327$	$-4.480$
$z\in[-2,-3/5]$	658	14	$-0.0900423691$	$-0.090$
$z\in[3/5,1]$	4	2	$-0.3671210997$	$-0.090$
$|z|=3/5,\ \operatorname{Im}z\geq 0$	693	11	$-0.0900220839$	$-0.090$

Table B.2. Constants in Lemmas 4.2–4.4.

quantity	value
intervals on $x$, $v$, $z$; Poisson kernels	$(50,52,62,157)$
$(K_{x},K_{v},K_{z})$	$(-4.626,-4.480,-0.090)$
$\delta$	$1/250$
$\sup_{|q|\leq\delta}F_{x}(q)$	$<-6.2823007011$
$\sup_{|q|\leq\delta}F_{v}(q)$	$<-4.4935082437$
$(H_{x},H_{v},H_{z,\mathrm{real}},H_{z,\mathrm{circle}})$	$(131,153,43,24)$
subintervals in Table B.1	$3791$
precision (decimal digits)	$90$
series terms	$420$
series remainder per pair	$<8.78\times 10^{-130}$
$H_{z}$	$67$
$(C_{x},C_{v},C_{z})$	$(2096,2984,2296)$
$C_{x}+\tfrac{5}{4}C_{v}+C_{z}$	$8122$
$(L_{D},L_{z})$	$(101/100,167/100)$
$A_{0}$	$1107/80$
$\tfrac{17}{16}\cdot 8\epsilon/\delta^{2}+A_{0}$ at $m=64$	$<200$
$3(C_{x}+\tfrac{5}{4}C_{v}+C_{z})+200$	$24566$
$C_{*}$	$<810$
endpoint-disk precision (bits)	$100$

Appendix C Printed interval data

Tables C.1–C.3 give the numerical enclosures used in Lemma 4.2. Every displayed interval is outward rounded. The static row checks compare each upper endpoint with the printed bound.

Table C.1. The pair decomposition and its enclosures.

Here $I_{zr}$ is the energy of the real part of $\nu_{z}$, $I_{zp}$ the cross term of its real and Poisson parts, and $I_{pp}$ the Poisson self-energy. $I_{vz}=I(\nu_{v},\nu_{z})$ includes both the real and Poisson parts of $\nu_{z}$. term outward enclosure $I_{xx}$ [-1.546417482857900440,-1.546417482857900439] $I_{vv}$ [-2.239637943680446541,-2.239637943680446540] $I_{zr}$ [-0.162577112801730912,-0.162577112801730911] $I_{zp}$ [0.081132573652198143,0.081132573652198144] $I_{pp}$ [-0.272227665742282938,-0.272227665742282937] $I_{vz}$ [0.206849817575968853,0.206849817575968854] $D_{xv}$ [1.059475627780623120,1.059475627780623121] $\mathcal{Q}(\nu)=I_{xx}+I_{vv}+I_{zr}+2I_{zp}+I_{pp}+I_{vz}-D_{xv}$ [-4.911220867982618809,-4.911220867982618808]

For $i\in\{x,v\}$ put $A_{i}(\delta)=\int\log(|t|+\delta)\,d\nu_{i}(t)$, and put $A_{z,\mathrm{real}}(\delta)=\int\log(|t|+\delta)\,d\nu_{z,\mathrm{real}}(t)$. Put

$$D_{x,\mathrm{low}}=\log(2-\delta),\qquad D_{v,\mathrm{low}}=\tfrac{5}{4}\log(2-\delta).$$

Then $D_{i}(q)\geq D_{i,\mathrm{low}}$ for $i\in\{x,v\}$ and $|q|\leq\delta$. For $|q|\leq\delta$ the displayed endpoint calculation reads

$$F_{x}(q)\leq B_{x}:=2A_{x}(\delta)-D_{v,\mathrm{low}}+\tfrac{3}{4}\log\delta,\qquad F_{v}(q)\leq B_{v}:=2A_{v}(\delta)+A_{z,\mathrm{real}}(\delta)+W_{P}-D_{x,\mathrm{low}}+\tfrac{1}{4}\log\delta.$$

The denominator expansion retains $420$ terms. Since $0\leq xv/2\leq 1/2$ and the total $x$–$v$ mass is $1\cdot(5/4)$, the integrated remainder is bounded by

$$R_{xv}\leq\frac{5}{4}\,\frac{2(1/2)^{421}}{421}=\frac{5}{2\cdot 421\cdot 2^{421}}<1.10\times 10^{-129}.$$

Table C.2. Endpoint majorants and disk bounds for $\delta=1/250$.

quantity	outward enclosure
$A_{x}(\delta)$	[-0.638636770206138024,-0.638636770206138023]
$A_{v}(\delta)$	[-1.118528621477847036,-1.118528621477847035]
$A_{z,\mathrm{real}}(\delta)$	[0.148575311504214922,0.148575311504214923]
$W_{P}:=M_{P}\log(151/250)$	[-0.333515904969252,-0.333515904969250]
$M_{P}$ (sum of the 157 Poisson weights)	26460009509/40000000000
$D_{x,\mathrm{low}}$	[0.691145177889270,0.691145177889275]
$D_{v,\mathrm{low}}$	[0.863931472361588,0.863931472361593]
$B_{x}$	[-6.28230070117056,-6.28230070117054]
$B_{v}$	[-4.49350824377558,-4.49350824377554]

Table C.3. Rational density checks from the printed reference tables.

support	exact maximum used	integer upper bound
$x$	$1772217287/13581647$	$131$
$v$	$2076994349/13581647$	$153$
$z$ real	$4076507975/95071529$	$43$
$z$ circle	$\sum H_{c}<24$ by the integer square-root and $\pi>333/106$ checks	$24$

The first three bounds in Table C.3 are rational comparisons of rows in Table D.1. The fourth is the corresponding rational sum over Table D.2.

Appendix D Reference measure data

The two tables specify the reference measure $\nu$. All entries are exact terminating decimals.

Table D.1 lists the intervals of $\nu$ on each real support in increasing order of the index, and each line holds two consecutive entries (odd index left, even index right). Entry $(a,w)$ is the interval $[a,b]$ carrying $w\,dt/(b-a)$, where $b$ is the $a$ of the entry with the next index in the same block. The last $b$ of each block is given in its heading. Outside these intervals $\nu$ has no mass. For example, $\nu_{x}$ vanishes on $[0,0.02653493525245)$.

Table D.2 lists the circular part of $\nu_{z}$. Every row is a measure on the circle $|q|=r=3/5$, whose upper half is the support $z_{\circ}$ of Appendix E. It is the Poisson measure of the proof of Lemma 4.2 with center $c=\operatorname{Re}c+i\operatorname{Im}c$, $|c|<3/5$, and total mass $w$. Its logarithmic potential is (4.3). The $x$- and $v$-parts of $\nu$ have no Poisson rows.

Table D.1. Interval data for the reference measure: left endpoint $a$ and mass $w$ of each interval.

index	$a$	$w$	index	$a$	$w$
$x$-intervals on $[0,1]$: rows 1–50, last right endpoint $1$.
1	0.02653493525245	0.000000000011	2	0.03806023374436	0.000000000056
3	0.05156362923366	0.000000000066	4	0.06698729810778	0.009047636046
5	0.08426519384873	0.016164978747	6	0.10332332985438	0.019034345994
7	0.12408009626051	0.021065372172	8	0.14644660940673	0.022447569912
9	0.17032709244997	0.02345382024	10	0.19561928549564	0.024200308115
11	0.2222148834902	0.02476625456	12	0.25	0.025199538621
13	0.2788556548905	0.02553284359	14	0.30865828381746	0.025790757407
15	0.33928026734842	0.02598943694	16	0.37059047744874	0.026140976998
17	0.40245483899194	0.026255972454	18	0.43473690388997	0.026341379215
19	0.46729843538493	0.026402361973	20	0.5	0.026444293432
21	0.53270156461507	0.026470882322	22	0.56526309611003	0.026484444361
23	0.59754516100806	0.026487798034	24	0.62940952255126	0.026483565514
25	0.66071973265158	0.026473037339	26	0.69134171618254	0.026457122002
27	0.7211443451095	0.026437395821	28	0.75	0.026415300265
29	0.7777851165098	0.026391297706	30	0.80438071450436	0.026365737946
31	0.82967290755003	0.026339451805	32	0.85355339059327	0.026313133347
33	0.87591990373949	0.026286966515	34	0.89667667014562	0.026260716757
35	0.91573480615127	0.02623413097	36	0.93301270189222	0.026207204488
37	0.94843637076634	0.026178707612	38	0.96193976625564	0.026146051892
39	0.97346506474755	0.026100427024	40	0.98296291314453	0.026045558902
41	0.99039264020162	0.025800471869	42	0.99572243068691	0.02600510817
43	0.9989294616193	0.00101387447	44	0.9989702065603	0.001749595019
45	0.99908623833539	0.002577120956	46	0.99925989215865	0.003342459833
47	0.99946473080965	0.004008718139	48	0.99966956946065	0.004554823645
49	0.99984322328391	0.004774398867	50	0.999959255059	0.005316651861
$v$-intervals on $[0,1]$: rows 51–102, last right endpoint $1$.
51	0.00960735979838	0.013858434309	52	0.01703708685547	0.020659018632
53	0.02653493525245	0.022756374414	54	0.03806023374436	0.024040451088
55	0.05156362923366	0.024796480607	56	0.06698729810778	0.025298366124
57	0.08426519384873	0.025649764501	58	0.10332332985438	0.025910099392
59	0.12408009626051	0.026113452847	60	0.14644660940673	0.02628122952
61	0.17032709244997	0.026427269003	62	0.19561928549564	0.026561515238
63	0.2222148834902	0.026691316341	64	0.25	0.026821861266
65	0.2788556548905	0.026957166859	66	0.30865828381746	0.027100366588
67	0.33928026734842	0.027253308259	68	0.37059047744874	0.027416681441
69	0.40245483899194	0.027590343833	70	0.43473690388997	0.027773157352
71	0.46729843538493	0.027962829423	72	0.5	0.028155382615
73	0.53270156461507	0.028348951325	74	0.56526309611003	0.028512049639
75	0.59754516100806	0.028704024914	76	0.62940952255126	0.02895179599
77	0.66071973265158	0.029147228949	78	0.69134171618254	0.029330189043
79	0.7211443451095	0.029497893354	80	0.75	0.029651492159
81	0.7777851165098	0.029791323098	82	0.80438071450436	0.029918006281
83	0.82967290755003	0.030031872164	84	0.85355339059327	0.030133175201
85	0.87591990373949	0.030222548301	86	0.89667667014562	0.030300285976
87	0.91573480615127	0.030366116749	88	0.93301270189222	0.030419889284
89	0.94843637076634	0.030460392026	90	0.96193976625564	0.030485017656
91	0.97346506474755	0.030483706899	92	0.98296291314453	0.030461131797
93	0.99039264020162	0.030205136068	94	0.99572243068691	0.030465558928
95	0.9989294616193	0.001188270853	96	0.9989702065603	0.002050223725
97	0.99908623833539	0.003019909346	98	0.99925989215865	0.003916871095
99	0.99946473080965	0.004697775042	100	0.99966956946065	0.005337916652
101	0.99984322328391	0.005595394787	102	0.999959255059	0.006230983047
$z$-intervals on $[-2,-3/5]$: rows 103–164, last right endpoint $-3/5$.
103	-2	0.002445904785	104	-1.9999429570826	0.002196289941
105	-1.99978051259747	0.002095070288	106	-1.99953739724491	0.001843711398
107	-1.99925062313351	0.001537127441	108	-1.99896384902211	0.001185108178
109	-1.99872073366955	0.000804636229	110	-1.99855828918442	0.000466572663
111	-1.99850124626702	0.011949094627	112	-1.99401140296167	0.011829831253
113	-1.98654969628226	0.011904636078	114	-1.97614807840235	0.011879377704
115	-1.96285109064657	0.011837079332	116	-1.9467156727579	0.01177589427
117	-1.92781091907288	0.011699589994	118	-1.90621778264911	0.011609193707
119	-1.88202872861178	0.011505113623	120	-1.85534733820386	0.011387043787
121	-1.82628786523528	0.011255100131	122	-1.79497474683058	0.011109018301
123	-1.76154207057005	0.010947966233	124	-1.7261330003061	0.01077167805
125	-1.68889916311372	0.010579949336	126	-1.65	0.010372009648
127	-1.6096020831533	0.010147136288	128	-1.56787840265556	0.009904930406
129	-1.52500762571221	0.009644863536	130	-1.48117333157176	0.009366270662
131	-1.43656322541129	0.009068614306	132	-1.39136833455404	0.00875137721
133	-1.3457821904611	0.008414043831	134	-1.3	0.008056385332
135	-1.2542178095389	0.007678505629	136	-1.20863166544596	0.007280632319
137	-1.16343677458871	0.006863145229	138	-1.11882666842824	0.006426779891
139	-1.07499237428779	0.005972788018	140	-1.03212159734444	0.005503141876
141	-0.9903979168467	0.00502059841	142	-0.95	0.004528595244
143	-0.91110083688628	0.004031298216	144	-0.8738669996939	0.00353382249
145	-0.83845792942995	0.003042591462	146	-0.80502525316942	0.002564906577
147	-0.77371213476472	0.002108555487	148	-0.74465266179614	0.001681749548
149	-0.71797127138822	0.001293146877	150	-0.69378221735089	0.000950929581
151	-0.67218908092712	0.000661669911	152	-0.6532843272421	0.000429830492
153	-0.63714890935343	0.000257484313	154	-0.62385192159765	0.000143377053
155	-0.61345030371774	0.000084543242	156	-0.60598859703833	0.000061123507
157	-0.60149875373298	0.000001405548	158	-0.60144171081558	0.000003128248
159	-0.60127926633045	0.00000456608	160	-0.60103615097789	0.000005613821
161	-0.60074937686649	0.00000618074	162	-0.60046260275509	0.000006409107
163	-0.60021948740253	0.00000617203	164	-0.6000570429174	0.000006452761

Table D.2. Poisson data for the circular part of the reference measure: center $c$ and mass $w$ of each Poisson measure.

index	$\operatorname{Re}c$	$\operatorname{Im}c$	$w$
1	0.4913985408708	0.32834200771458	0.000000000005
2	0.48039239059364	0.34424431884887	0.000000000009
3	0.46887182411212	0.35977800454415	0.00000000001
4	0.45684917793738	0.37492643094071	0.000000000011
5	0.44433732622008	0.38967337672414	0.000638704082
6	0.43134966696442	0.40400305049552	0.002774568368
7	0.41790010768125	0.41790010768125	0.002648678352
8	0.40400305049552	0.43134966696442	0.003134952159
9	0.38967337672414	0.44433732622008	0.003371109225
10	0.37492643094071	0.45684917793738	0.00362052744
11	0.35977800454415	0.46887182411212	0.003823085588
12	0.34424431884887	0.48039239059364	0.004004693717
13	0.32834200771458	0.4913985408708	0.004164215022
14	0.31208809973437	0.50187848928221	0.004306593404
15	0.2955	0.5118210136366	0.004434028868
16	0.27859547146416	0.52121546722988	0.004548494496
17	0.26139261591943	0.53005179024582	0.004651574501
18	0.2439098546144	0.53832052052841	0.004744445721
19	0.22616590852777	0.54601280371417	0.004828370754
20	0.20817977832145	0.55312040271358	0.004904191893
21	0.18997072399417	0.55963570653161	0.004972725611
22	0.17155824425739	0.56555173841774	0.005034518792
23	0.15296205565559	0.57086216333684	0.005090055986
24	0.13420207145331	0.5755612947529	0.005139889582
25	0.11529838031153	0.57964410071831	0.005184386706
26	0.0962712247762	0.58310620926216	0.005223998617
27	0.07714097960205	0.58594391307192	0.005258940541
28	0.05792812993477	0.58815417346327	0.005289495695
29	0.03865324937501	0.58973462363401	0.005315860418
30	0.01933697794767	0.59068357119853	0.005338252913
31	0	0.591	0.005356869923
32	-0.01933697794767	0.59068357119853	0.005371839655
33	-0.03865324937501	0.58973462363401	0.00538329912
34	-0.05792812993477	0.58815417346327	0.005391294222
35	-0.07714097960205	0.58594391307192	0.005395976833
36	-0.0962712247762	0.58310620926216	0.005397361405
37	-0.11529838031153	0.57964410071831	0.005395592218
38	-0.13420207145331	0.5755612947529	0.005390634646
39	-0.15296205565559	0.57086216333684	0.005382588982
40	-0.17155824425739	0.56555173841774	0.005371424089
41	-0.18997072399417	0.55963570653161	0.005357167758
42	-0.20817977832145	0.55312040271358	0.005339817089
43	-0.22616590852777	0.54601280371417	0.005319360695
44	-0.2439098546144	0.53832052052841	0.005295824221
45	-0.26139261591943	0.53005179024582	0.005269193571
46	-0.27859547146416	0.52121546722988	0.005239457786
47	-0.2955	0.5118210136366	0.005206556882
48	-0.31208809973437	0.50187848928221	0.005170430831
49	-0.32834200771458	0.4913985408708	0.005131018794
50	-0.34424431884887	0.48039239059364	0.005088322391
51	-0.35977800454415	0.46887182411212	0.00504230892
52	-0.37492643094071	0.45684917793738	0.004992975694
53	-0.38967337672414	0.44433732622008	0.004940222961
54	-0.40400305049552	0.43134966696442	0.00488399491
55	-0.41790010768125	0.41790010768125	0.004824218204
56	-0.43134966696442	0.40400305049552	0.004760895309
57	-0.44433732622008	0.38967337672414	0.004694049607
58	-0.45684917793738	0.37492643094071	0.004623666088
59	-0.46887182411212	0.35977800454415	0.004549682725
60	-0.48039239059364	0.34424431884887	0.004472013635
61	-0.4913985408708	0.32834200771459	0.004390610978
62	-0.50187848928221	0.31208809973437	0.00430554631
63	-0.5118210136366	0.2955	0.004216885068
64	-0.52121546722988	0.27859547146416	0.004124710654
65	-0.53005179024582	0.26139261591943	0.004028997465
66	-0.53832052052841	0.2439098546144	0.003929757184
67	-0.54601280371417	0.22616590852777	0.003827028338
68	-0.55312040271358	0.20817977832145	0.003720966921
69	-0.55963570653161	0.18997072399417	0.003611737022
70	-0.56555173841774	0.17155824425739	0.00349933102
71	-0.57086216333684	0.15296205565559	0.003383865867
72	-0.5755612947529	0.13420207145331	0.003265638507
73	-0.57964410071831	0.11529838031153	0.003143389946
74	-0.58310620926216	0.0962712247762	0.003020584609
75	-0.58594391307192	0.07714097960205	0.002890212871
76	-0.58815417346327	0.05792812993477	0.002763390356
77	-0.58973462363401	0.03865324937501	0.002615447991
78	-0.59068357119853	0.01933697794767	0.002506482686
79	-0.591	0	0.002042234839
80	-0.59068357119853	-0.01933697794767	0.002506482686
81	-0.58973462363401	-0.03865324937501	0.002615447991
82	-0.58815417346327	-0.05792812993477	0.002763390356
83	-0.58594391307192	-0.07714097960205	0.002890212871
84	-0.58310620926216	-0.0962712247762	0.003020584609
85	-0.57964410071831	-0.11529838031153	0.003143389946
86	-0.5755612947529	-0.13420207145331	0.003265638507
87	-0.57086216333684	-0.15296205565559	0.003383865867
88	-0.56555173841774	-0.17155824425739	0.00349933102
89	-0.55963570653161	-0.18997072399417	0.003611737022
90	-0.55312040271358	-0.20817977832145	0.003720966921
91	-0.54601280371417	-0.22616590852777	0.003827028338
92	-0.53832052052841	-0.2439098546144	0.003929757184
93	-0.53005179024582	-0.26139261591943	0.004028997465
94	-0.52121546722988	-0.27859547146416	0.004124710654
95	-0.5118210136366	-0.2955	0.004216885068
96	-0.50187848928221	-0.31208809973437	0.00430554631
97	-0.4913985408708	-0.32834200771459	0.004390610978
98	-0.48039239059364	-0.34424431884887	0.004472013635
99	-0.46887182411212	-0.35977800454415	0.004549682725
100	-0.45684917793738	-0.37492643094071	0.004623666088
101	-0.44433732622008	-0.38967337672414	0.004694049607
102	-0.43134966696442	-0.40400305049552	0.004760895309
103	-0.41790010768125	-0.41790010768125	0.004824218204
104	-0.40400305049552	-0.43134966696442	0.00488399491
105	-0.38967337672414	-0.44433732622008	0.004940222961
106	-0.37492643094071	-0.45684917793738	0.004992975694
107	-0.35977800454415	-0.46887182411212	0.00504230892
108	-0.34424431884887	-0.48039239059364	0.005088322391
109	-0.32834200771458	-0.4913985408708	0.005131018794
110	-0.31208809973437	-0.50187848928221	0.005170430831
111	-0.2955	-0.5118210136366	0.005206556882
112	-0.27859547146416	-0.52121546722988	0.005239457786
113	-0.26139261591943	-0.53005179024582	0.005269193571
114	-0.2439098546144	-0.53832052052841	0.005295824221
115	-0.22616590852777	-0.54601280371417	0.005319360695
116	-0.20817977832145	-0.55312040271358	0.005339817089
117	-0.18997072399417	-0.55963570653161	0.005357167758
118	-0.17155824425739	-0.56555173841774	0.005371424089
119	-0.15296205565559	-0.57086216333684	0.005382588982
120	-0.13420207145331	-0.5755612947529	0.005390634646
121	-0.11529838031153	-0.57964410071831	0.005395592218
122	-0.0962712247762	-0.58310620926216	0.005397361405
123	-0.07714097960205	-0.58594391307192	0.005395976833
124	-0.05792812993477	-0.58815417346327	0.005391294222
125	-0.03865324937501	-0.58973462363401	0.00538329912
126	-0.01933697794767	-0.59068357119853	0.005371839655
127	0	-0.591	0.005356869923
128	0.01933697794767	-0.59068357119853	0.005338252913
129	0.03865324937501	-0.58973462363401	0.005315860418
130	0.05792812993477	-0.58815417346327	0.005289495695
131	0.07714097960205	-0.58594391307192	0.005258940541
132	0.0962712247762	-0.58310620926216	0.005223998617
133	0.11529838031153	-0.57964410071831	0.005184386706
134	0.13420207145331	-0.5755612947529	0.005139889582
135	0.15296205565559	-0.57086216333684	0.005090055986
136	0.17155824425739	-0.56555173841774	0.005034518792
137	0.18997072399417	-0.55963570653161	0.004972725611
138	0.20817977832145	-0.55312040271358	0.004904191893
139	0.22616590852777	-0.54601280371417	0.004828370754
140	0.2439098546144	-0.53832052052841	0.004744445721
141	0.26139261591943	-0.53005179024582	0.004651574501
142	0.27859547146416	-0.52121546722988	0.004548494496
143	0.2955	-0.5118210136366	0.004434028868
144	0.31208809973437	-0.50187848928221	0.004306593404
145	0.32834200771458	-0.4913985408708	0.004164215022
146	0.34424431884887	-0.48039239059364	0.004004693717
147	0.35977800454415	-0.46887182411212	0.003823085588
148	0.37492643094071	-0.45684917793738	0.00362052744
149	0.38967337672414	-0.44433732622008	0.003371109225
150	0.40400305049552	-0.43134966696442	0.003134952159
151	0.41790010768125	-0.41790010768125	0.002648678352
152	0.43134966696442	-0.40400305049552	0.002774568368
153	0.44433732622008	-0.38967337672414	0.000638704082
154	0.45684917793738	-0.37492643094071	0.000000000011
155	0.46887182411212	-0.35977800454415	0.00000000001
156	0.48039239059364	-0.34424431884887	0.000000000009
157	0.4913985408708	-0.32834200771458	0.000000000005

The interval and Poisson weights sum to masses $1$, $5/4$, and $1$ as stated in Lemma 4.2.

Appendix E Dyadic subdivisions

The supports are $x,v\in[0,1]$, $z_{-}=[-2,-3/5]$, $z_{+}=[3/5,1]$ and $z_{\circ}=\{|z|=3/5,\ \operatorname{Im}z\geq 0\}$ (by conjugation symmetry the upper half suffices). On each support $s$, the leaves are ordered from left to right. Their depths $d_{s,1},\ldots,d_{s,n_{s}}$ are listed in run-length form: an entry $d:r$ means that depth $d$ occurs on $r$ consecutive leaves. Set $t_{s,0}=0$ and $t_{s,j}=\sum_{i=1}^{j}2^{-d_{s,i}}$. The printed sequence satisfies $\sum_{j=1}^{n_{s}}2^{-d_{s,j}}=1$ for each support. On a real support $[A_{s},B_{s}]$ the $j$th interval is $[A_{s}+(B_{s}-A_{s})t_{s,j-1},A_{s}+(B_{s}-A_{s})t_{s,j}]$. On $z_{\circ}$ it is $q=(3/5)e^{i\pi t}$ for $t\in[t_{s,j-1},t_{s,j}]$. On each leaf, the Arb upper bound for $\sup F_{s}$ is strictly below its cap in Table B.1, and that table keeps the worst leaf for each support. The full leafwise Arb upper bounds are in anc/verification/analytic/leaves.json.gz.

Table E.1. Run-length encoded dyadic depths of the certificate partitions.

support	block	depth:repeat
$x$	1	5:1,6:1,7:1,8:1,9:3,10:14,11:14
$x$	2	10:18,11:4,10:19,11:4,10:21,11:4,10:22
$x$	3	11:4,10:24,11:4,10:26,11:2,10:27,11:4
$x$	4	10:28,11:2,10:29,11:4,10:30,11:2,10:31
$x$	5	11:2,10:32,11:2,10:32,11:2,10:32,11:2
$x$	6	10:32,11:4,10:32,11:2,10:32,11:2,10:32
$x$	7	11:2,10:32,11:2,10:31,11:2,10:30,11:4
$x$	8	10:29,11:2,10:28,11:4,10:26,11:4,10:25
$x$	9	11:6,10:23,11:6,10:21,11:8,10:18,11:10
$x$	10	10:15,11:14,10:12,11:16,10:9,11:18,10:6
$x$	11	11:12,12:2,11:11,10:1,11:13,12:4,11:21
$x$	12	12:4,11:15,12:10,11:9,12:10,13:2,12:3
$x$	13	11:4,12:8,13:6,12:3,11:1,12:3,13:4
$x$	14	14:22,15:2,14:2,15:2,14:1,15:2
$v$	1	8:1,9:1,10:2,11:17,12:6,11:18,12:2
$v$	2	11:11,10:1,11:20,10:6,11:14,10:9,11:12
$v$	3	10:12,11:10,10:15,11:8,10:18,11:6,10:20
$v$	4	11:4,10:23,11:2,10:25,11:2,10:26,11:2
$v$	5	10:27,11:4,10:28,11:2,10:30,11:2,10:30
$v$	6	11:2,10:31,11:2,10:65,11:2,10:32,11:2
$v$	7	10:66,11:2,10:32,11:2,10:32,11:2,10:32
$v$	8	11:2,10:31,11:2,10:30,11:4,10:29,11:2
$v$	9	10:28,11:4,10:26,11:4,10:25,11:6,10:23
$v$	10	11:6,10:21,11:8,10:18,11:10,10:15,11:14
$v$	11	10:12,11:16,10:8,11:20,10:6,11:12,12:2
$v$	12	11:26,12:4,11:20,12:8,11:14,12:10,11:9
$v$	13	12:10,13:2,12:3,11:4,12:7,13:8,12:3
$v$	14	11:1,12:3,13:4,14:22,15:2,14:2,15:2
$v$	15	14:1,16:2,15:1
$z_{-}$	1	14:4,13:10,12:2,11:4,12:4,11:9,12:2
$z_{-}$	2	11:6,10:3,11:8,10:6,11:6,10:9,11:4
$z_{-}$	3	10:12,11:2,10:15,11:2,10:45,9:3,10:16
$z_{-}$	4	9:4,10:14,9:6,10:10,9:8,10:10,9:9
$z_{-}$	5	10:8,9:11,10:6,9:12,10:4,9:13,10:4
$z_{-}$	6	9:14,10:4,9:14,10:4,9:14,10:4,9:15
$z_{-}$	7	10:2,9:16,10:2,9:15,10:4,9:15,10:2
$z_{-}$	8	9:16,10:2,9:32,10:2,9:15,10:2,9:173
$z_{+}$	1	2:4
$z_{\circ}$	1	3:1,5:1,6:2,7:1,8:3,9:4,10:6
$z_{\circ}$	2	11:30,10:313,9:1,10:8,9:1,10:20,9:1
$z_{\circ}$	3	10:8,9:1,10:20,9:1,10:8,9:1,10:20
$z_{\circ}$	4	9:1,10:8,9:1,10:8,9:2,10:8,9:1
$z_{\circ}$	5	10:8,9:1,10:8,9:2,10:8,9:1,10:8
$z_{\circ}$	6	9:2,10:6,9:2,10:6,9:2,10:8,9:2
$z_{\circ}$	7	10:6,9:2,10:6,9:3,10:4,9:3,10:6
$z_{\circ}$	8	9:3,10:4,9:3,10:4,9:4,10:2,9:4
$z_{\circ}$	9	10:2,9:93

Appendix F Computer checks

Lemma 4.2 is proved by the interval computation of check_analytic.py, in Arb ball arithmetic [5] through python-flint 0.9.0. The other scripts recheck printed data in exact rational arithmetic. Times are for Python 3.12.3 on one core of an ARM64 Linux server.

Table F.1. Scripts in anc/ and their running times in seconds.

script	statements checked	time
check_determinant.py	(2.5) and Table 2.1; (2.3) for $d\neq 0$ and the four determinant evaluations in Lemma 2.2 for small sizes.	$<1$
check_arith.py	the cut points and every entry of Table A.1; (3.8), $5/48$, $45/32$ and $\tau$; $N_{m}$ in Lemma 3.4; the potentials of Lemma 3.3 for $n\leq 12$.	$<10$
check_analytic.py	Lemma 4.2: Tables B.1, B.2, D.1 and D.2, (B.1), (B.2), (4.2); the constants of Lemma 4.4.	$<90$
check_mod11.py	(5.2), (5.1) and Table 5.1.	$<1$

Statements and declarations

Competing interests. The author has no competing interests.

Funding. No funding was received for this work.

Data availability. The scripts of Appendix F, the data of the measure $\nu$ and the outputs of the scripts are included in the anc/ attachment accompanying this manuscript.