Finite Weil approximations

1. Finite objects and common tests

The limit of positive real numbers is nonnegative. In a finite approximation approach to Weil positivity, the difficult question is which real numbers have been proved positive and whether their limit is the intended arithmetic functional. A positive matrix, a signed explicit formula, and the Fourier transform of a ground state need not be approximations of the same object. A useful comparison specifies a common test space and the maps by which every finite object is evaluated on it.

Part I fixes the classical Weil pairing and studies geometric sufficient structures [6]. Part III organizes realizations and their morphisms [7]. The present paper concerns the analytic passage from finite data. Its results are elementary reductions with explicit estimates. They separate known convergence facts from the arithmetic sign problem and identify the additional estimates needed in two current operator constructions.

Four parameters occur repeatedly. A zero height $T$ selects a finite portion of the zero divisor. A support radius $a$ restricts the test functions. A dimension $N$ selects a finite dimensional subspace of a Hilbert or form domain. A finite set of places $S$ selects a semilocal arithmetic model. A statement involving one parameter should not silently be used as a statement about another. For instance, a compact support condition makes the prime term finite but leaves infinitely many zero terms on the other side of the explicit formula.

We use real nonnegativity for diagonal values and complex sesquilinearity for the arithmetic pairing. A general positivity transfer needs only a real-valued functional. The stronger algebraic structures become relevant when the transfer is required to preserve pairings, kernels, actions, or spectral data. The accompanying Lean module keeps this distinction visible: its approximation certificate records linear comparison maps and real values, while sesquilinear and geometric structures are treated elsewhere in the program.

Definition 1.1. Let $X$ be a real vector space, $Y_n$ real vector spaces, $d_n:X\to Y_n$ linear maps, and $q_n:Y_n\to\mathbb R$ functions. The values compared with a target $Q:X\to\mathbb R$ are $p_n(x)=q_n(d_nx),\qquad e_n(x)=p_n(x)-Q(x).$ The maps $d_n$ are called comparison maps. This terminology does not assert that they are injective, surjective, isometric, or compatible with transitions between the $Y_n$ .

This modest definition is useful because each stronger property can be requested where needed. If the only conclusion is $Q(x)\ge0$ , pointwise convergence of $p_n(x)$ suffices. If the conclusion concerns a Hilbert norm or an unbounded operator, one must specify more: an ambient topology, a domain, and suitable continuity or resolvent estimates. These requirements are not consequences of positivity alone.

The distinction also constrains claims of mathematical novelty. Closedness of the nonnegative cone and continuity of finite sums are standard facts. Their formal implementation checks the transfer without constructing an arithmetic model. The construction problem begins where a concrete $q_n$ must be proved nonnegative and its defect $e_n$ must be estimated. An unrestricted certificate can always be made tautological by choosing $q_n=Q$ and $d_n=\operatorname{id}$ .

2. The centered zero sum

2.1. The transform convention

Write $\mathcal T=C_c^\infty(\mathbb R,\mathbb C)$ . For $f,g\in\mathcal T$ , let $\begin{equation} \begin{split} (f*g)(t)&=\int_\mathbb Rf(u)g(t-u)\,du,\\ f^*(t)&=\overline{f(-t)},\qquad F_f(z)=\int_\mathbb Rf(t)e^{zt}\,dt. \end{split}\tag{1}\end{equation}$ Compact support makes $F_f$ entire. Fubini’s theorem and a change of variables give $\begin{equation} F_{f*g}(z)=F_f(z)F_g(z),\qquad F_{f^*}(z)=\overline{F_f(-\overline z)}.\tag{2}\end{equation}$ No spectral assertion is used in either identity.

For a nontrivial zero $\rho$ of the Riemann zeta function, put $z_\rho=\rho-\tfrac12$ . With multiplicities understood, the Weil pairing and its diagonal are $\begin{equation} \begin{split} B_W(f,g)&=\sum_\rho F_f(z_\rho) \overline{F_g(-\overline{z_\rho})},\\ Q_W(f)&=B_W(f,f). \end{split}\tag{3}\end{equation}$ The functional equation and conjugation symmetry preserve the zero multiset under $z\mapsto-\overline z$ . Once absolute convergence is established, reindexing by this involution proves that $B_W$ is Hermitian. It is linear in the first argument under our convention.

The two arguments of $F_f$ in a diagonal summand coincide precisely when $\operatorname{Re}z_\rho=0$ . Hence an on-axis zero contributes $|F_f(z_\rho)|^2$ , while an arbitrary zero contributes a product of evaluations at different points. Replacing that product by an absolute square before proving the axis condition would change the functional. This algebraic distinction persists at finite height.

2.2. Uniform decay on the critical strip

For $a>0$ , let $\mathcal T_a$ consist of smooth functions supported in $[-a,a]$ , and define $p_M(f)=\max_{0\le j\le M}\sup_{t\in\mathbb R}|f^{(j)}(t)|.$ These seminorms give the usual fixed-support test topology. The next estimate is proved directly because the width of the strip matters in the later comparison.

Lemma 2.1. For every $a,b>0$ and integer $M\ge0$ , there is a constant $C_{a,b,M}$ such that $\begin{equation} |F_f(\sigma+i\tau)|\le C_{a,b,M}p_M(f)(1+|\tau|)^{-M}\tag{4}\end{equation}$ for $f\in\mathcal T_a$ and $|\sigma|\le b$ .

Proof. Set $u_\sigma(t)=e^{\sigma t}f(t)$ . Its support is in $[-a,a]$ , and Leibniz’s formula yields $u_\sigma^{(M)}(t)=e^{\sigma t} \sum_{j=0}^M\binom Mj\sigma^{M-j}f^{(j)}(t).$ The $L^1$ norm of this derivative is at most $2ae^{ab}(1+b)^M p_M(f)$ . For $\tau\ne0$ , integration by parts $M$ times gives $F_f(\sigma+i\tau)=(-i\tau)^{-M} \int_\mathbb Ru_\sigma^{(M)}(t)e^{i\tau t}\,dt.$ All boundary terms vanish because $f$ is smooth with compact support. When $|\tau|\ge1$ , this proves the required estimate after changing the constant. For $|\tau|\le1$ , use $|F_f(\sigma+i\tau)|\le2ae^{ab}p_0(f)$ and enlarge the same constant. ◻

Only the unconditional location $0<\operatorname{Re}\rho<1$ is needed to apply this lemma to the zero sum. The further input is a zero-counting bound. We use $\begin{equation} \#\{\rho:|\operatorname{Im}\rho|\le T\}\le C T\log(2+T) \qquad(T\ge1),\tag{5}\end{equation}$ with multiplicities. Classical zero counting gives considerably more; an explicit modern bound is available in Trudgian’s work [9]. No improvement conditional on RH is required here.

Theorem 2.2. For $f,g\in\mathcal T_a$ and an integer $M\ge1$ , the sum in (3) converges absolutely. If $B_{W,T}$ denotes the sum over $|\operatorname{Im}\rho|\le T$ , then for $T\ge1$ , $\begin{equation} |B_W(f,g)-B_{W,T}(f,g)| \le C_{a,M}p_M(f)p_M(g) T^{1-2M}\log(2+T).\tag{6}\end{equation}$ In particular, the convergence is uniform when $p_M(f)$ and $p_M(g)$ are bounded at fixed support.

Proof. Both $z_\rho$ and $-\overline{z_\rho}$ have real part in $[-\tfrac12,\tfrac12]$ and imaginary part $\operatorname{Im}\rho$ . By lemma 2.1, the absolute value of a summand is at most $C_{a,M}p_M(f)p_M(g)(1+|\operatorname{Im}\rho|)^{-2M}.$ Partition the remaining zeros into shells $2^kT<|\operatorname{Im}\rho|\le2^{k+1}T$ , $k\ge0$ . By (5), their total contribution is at most a constant times $p_M(f)p_M(g)\sum_{k\ge0} (2^kT)^{-2M}2^{k+1}T\log(2+2^{k+1}T).$ Since $\log(2+2^{k+1}T)\le\log(2+T)+(k+1)\log2$ , this is bounded by the right side of (6). The sums of $2^{k(1-2M)}$ and $(k+1)2^{k(1-2M)}$ converge. The finitely many zeros below height one cause no difficulty. ◻

Corollary 2.3. The pairing $B_W$ is continuous on $\mathcal T_a\times\mathcal T_a$ , and $Q_W$ is continuous on $\mathcal T_a$ . These assertions do not assume nonnegativity.

Proof. The proof gives a bound $|B_W(f,g)|\le C_a p_1(f)p_1(g)$ after adding the finitely many low zeros. This is joint continuity of the sesquilinear pairing. Its diagonal is continuous by composition with $f\mapsto(f,f)$ . ◻

The tail estimate resolves a convergence question but does not bound the finite value from below. It is also a fixed-support estimate. If $a$ grows with the approximation index, the constants and the seminorms can grow. An argument using (6) on changing tests must track that dependence instead of citing convergence for each fixed test.

3. Finite Hermitian blocks

3.1. Reflected pairs

Let $z\notin i\mathbb R$ and write $z^\dagger=-\overline z$ . A reflected pair with equal multiplicity $m$ contributes $\begin{equation} m\bigl(u\overline v+v\overline u\bigr) =2m\operatorname{Re}(u\overline v),\qquad u=F_f(z),\quad v=F_f(z^\dagger).\tag{7}\end{equation}$ Here the tests are complex-valued, and the interpolation map below is complex linear with target $\mathbb C^r$ . No real-valuedness constraint is imposed on its independently prescribed values. For a real-valued test the centered transform instead satisfies $F_f(\overline z)=\overline{F_f(z)}$ , directly by conjugating its defining integral. This identity does not identify the reflected arguments $z$ and $-\overline z$ .

The corresponding Hermitian matrix is $m\begin{pmatrix}0&1\\1&0\end{pmatrix}.$ Its eigenvalues are $m$ and $-m$ . At $(u,v)=(1,1)$ its value is $2m$ ; at $(1,-1)$ its value is $-2m$ . These two scalar evaluations for $m=1$ are checked in Lean. The calculation does not claim that an off-axis zeta zero exists.

To turn this coefficient calculation into a statement about test functions, one must know that the evaluation data can be realized. The following finite interpolation lemma supplies that step and states its test-space scope explicitly.

Lemma 3.1. Let $I\subset\mathbb R$ be a nonempty open interval and $z_1,\dots,z_r$ distinct complex numbers. The map $\mathcal E:C_c^\infty(I,\mathbb C)\longrightarrow\mathbb C^r, \qquad f\longmapsto(F_f(z_1),\dots,F_f(z_r))$ is surjective.

Proof. If its image were a proper subspace, a nonzero complex linear functional on $\mathbb C^r$ would annihilate it. Thus there would be coefficients $c_j$ , not all zero, such that $\int_I f(t)\sum_{j=1}^r c_j e^{z_jt}\,dt=0 \qquad\text{for all }f\in C_c^\infty(I,\mathbb C).$ The continuous function $u(t)=\sum c_je^{z_jt}$ must then vanish on $I$ . For completeness, if $u(t_0)\ne0$ , multiply by a constant phase so that its real part is positive at $t_0$ . It remains positive in a small interval. A nonnegative smooth bump supported there gives a nonzero integral, a contradiction.

Choose $t_0\in I$ and differentiate $u=0$ for orders $0,\dots,r-1$ . The resulting linear system is $\sum_{j=1}^r(c_je^{z_jt_0})z_j^k=0, \qquad 0\le k<r.$ Its Vandermonde determinant is nonzero because the $z_j$ are distinct. Hence all $c_j$ vanish, contradicting their choice. ◻

Proposition 3.2. Let $Z$ be a finite multiset of complex numbers invariant under $z\mapsto-\overline z$ . Give each distinct point its positive multiplicity and define $Q_Z(f)=\sum_{z\in Z}F_f(z)\overline{F_f(-\overline z)}.$ On $C_c^\infty(I,\mathbb C)$ , this form is nonnegative for every $f$ if and only if every point of $Z$ lies on $i\mathbb R$ .

Proof. If all points are on the axis, the formula is a sum of positive multiples of absolute squares. Conversely, choose an off-axis pair $z,z^\dagger$ . By lemma 3.1, there is a test with values $1,-1$ on this pair and zero on every other distinct point of $Z$ . Formula (7) gives a strictly negative value. ◻

Nonnegativity here means positive semidefiniteness. The finite form is not positive definite on the full test space: its kernel contains the infinite-dimensional subspace of tests whose transforms vanish at all the finitely many arguments. For $N$ linearly independent bumps, the $r$ homogeneous evaluation conditions have a nullspace of dimension at least $N-r$ ; $N$ can be arbitrarily large.

The proposition concerns a finite multiset and arbitrary complex tests. It does not give a negative value of the complete Weil form from this particular interpolating test: zeros outside the finite set still contribute. The usual global criterion requires additional analytic reasoning. The proposition does establish that positivity of all spectral-height truncations is already a strong zero-location condition, not an automatic property of truncation.

3.2. Coefficient norms and test norms

Finite interpolation is qualitative. Its proof supplies no bound independent of $r$ , the locations $z_j$ , or the interval length. A solution realizing prescribed coefficients may have very large derivatives. Consequently the negative value of a finite block and the tail estimate in theorem 2.2 cannot be combined without controlling the interpolating test’s seminorms.

This is one example of a recurring distinction between finite and uniform constructions. Surjectivity for each $r$ does not provide uniformly bounded right inverses. In finite dimensions, one may choose a right inverse after selecting bases, but its norm depends on the smallest singular value of the evaluation map in the chosen norms. When evaluation points coalesce, that value can become small. A statement about all heights must estimate this dependence.

The same issue appears when a finite Gram matrix is written in a poorly scaled basis. Congruence by an invertible matrix preserves the sign of the quadratic form, while the numerical eigenvalues and the operator norm depend on the reference inner product. A stable comparison therefore records both the coefficient map and the norm. Reporting a small minimum eigenvalue without those choices does not identify an invariant error estimate.

4. Finite prime evaluation

The centered explicit formula makes the finite prime parameter precise. With $\gamma$ the Euler constant and $\Lambda$ the von Mangoldt function, write $\begin{equation} \begin{split} W(h)={}&F_h(\tfrac12)+F_h(-\tfrac12) -\sum_{n\ge2}\frac{\Lambda(n)}{\sqrt n} \bigl(h(\log n)+h(-\log n)\bigr)\\ &-(\log(4\pi)+\gamma)h(0)\\ &-\int_0^\infty \frac{e^{-u/2}(h(u)+h(-u))-2e^{-u}h(0)}{1-e^{-2u}}\,du. \end{split}\tag{8}\end{equation}$ This is the additive centered form of the convention in Connes and Consani’s Appendix B [2]. The numerator in the integral has cancellation at zero. The pole, prime, and archimedean terms belong to one identity; they are not separate nonnegative contributions.

Proposition 4.1. If $f\in\mathcal T_a$ and $h=f*f^*$ , then every nonzero term in the prime sum of (8) satisfies $n\le e^{2a}$ . A cutoff including all such prime powers evaluates the full prime term exactly.

Proof. The support of a convolution is contained in the sum of the supports. Both $f$ and $f^*$ are supported in $[-a,a]$ , so $h$ is supported in $[-2a,2a]$ . If $\log n>2a$ , both $h(\log n)$ and $h(-\log n)$ vanish. The von Mangoldt coefficient further restricts the sum to prime powers. ◻

At a fixed support radius there is no infinite prime tail to estimate once the cutoff is large enough. This observation is useful computationally, but it leaves the sign of the exact expression unchanged. In particular, adding primes is not generally an order-increasing operation: the new contribution has a minus sign, and the correlation values $h(\log n)+h(-\log n)$ can have either sign.

One can see this dependence directly. For $h=f*f^*$ , $h(u)=\int_\mathbb Rf(t)\overline{f(t-u)}\,dt, \qquad h(-u)=\overline{h(u)}.$ Thus the prime term is a real weighted sum of translated correlations. Cauchy-Schwarz gives $|h(u)|\le\|f\|_2^2$ , but this absolute bound does not determine the sign of $\operatorname{Re}h(u)$ . Even a positive semidefinite correlation kernel can take negative values at individual nonzero arguments.

Example 4.2. Let $\phi$ be a real smooth bump with sufficiently small support, let $s$ exceed twice that support radius, and put $f(t)=\phi(t)-\phi(t-s)$ . The translated supports are disjoint. At displacement $s$ , the surviving cross term in $h(s)$ is $-\|\phi\|_2^2$ . Replacing the minus sign in $f$ by a plus sign gives $+\|\phi\|_2^2$ . The sign of an individual prime correlation therefore cannot be read from the fact that $h$ is a convolution square.

The prime formula and the zero formula nevertheless describe the same $W(h)$ on their common test class. The value of the explicit formula is precisely this equality. For a positivity proof, one must further organize the signed arithmetic expression into a controlled quadratic structure. A proof of the formula does not supply that organization.

5. Positivity through comparison maps

5.1. Pointwise error estimates

Theorem 5.1. Let $X$ be a set and $p_n,Q,\epsilon_n:X\to\mathbb R$ . Suppose that for each $x\in X$ , $p_n(x)\ge-\epsilon_n(x),\qquad \epsilon_n(x)\longrightarrow0,\qquad p_n(x)\longrightarrow Q(x).$ Then $Q(x)\ge0$ for all $x$ .

Proof. Fix $x$ . The sequence $p_n(x)+\epsilon_n(x)$ is nonnegative and converges to $Q(x)$ . The interval $[0,\infty)$ is closed, so its limit belongs to that interval. ◻

The quantifier order is part of the conclusion’s strength. The theorem requires convergence for every fixed test. It does not require a single error bound valid over a unit ball of tests. In applications, uniform estimates can help prove the pointwise hypotheses, but demanding them without a further reason makes the residual stronger than necessary.

Corollary 5.2. For the spaces and comparison maps of definition 1.1, suppose $\begin{equation} q_n(y)\ge0,\qquad |q_n(d_nx)-Q(x)|\le\epsilon_n(x),\qquad \epsilon_n(x)\longrightarrow0\tag{9}\end{equation}$ for all applicable $n,y,x$ . Then $Q\ge0$ .

Proof. The first two inequalities imply $Q(x)\ge-\epsilon_n(x)$ . Passing to the limit gives the assertion. Alternatively, the absolute comparison proves $q_n(d_nx)\to Q(x)$ , and theorem 5.1 applies with zero lower-bound error. ◻

The Lean structure records exactly the data in this corollary, including the dependent family of spaces $Y_n$ and linear maps $d_n$ . The forms in this interface are real functions. Their quadratic laws are not needed by the proof and are not inferred from the field name. A use that also needs sesquilinearity must provide that structure separately.

5.2. Dense cores and form topology

Proposition 5.3. Let $X$ be a topological space, $e:D\to X$ have dense image, and $Q:X\to\mathbb R$ be continuous. If $Q(eu)\ge0$ for every $u\in D$ , then $Q\ge0$ on $X$ . In particular, the hypotheses of theorem 5.1 may be verified only on $D$ if their limit there is $Q\circ e$ .

Proof. The set $\{x:Q(x)\ge0\}$ is closed by continuity and contains the dense image of $e$ . It therefore equals $X$ . Apply theorem 5.1 to $Q\circ e$ for the last assertion. ◻

For $Q_W$ on $\mathcal T_a$ , corollary 2.3 supplies an appropriate topology. For the closed extension of a lower-bounded unbounded form on $L^2$ , the relevant domain carries a form norm. These settings should not be conflated. A densely defined closed form need not extend to a continuous finite-valued functional on all of $L^2$ .

To describe the form norm, let $q$ be a closed Hermitian form with lower bound $q(u)\ge-c\|u\|^2$ . On its domain set $\|u\|_q^2=q(u)+(c+1)\|u\|^2.$ The shifted form is a positive inner product, and its Cauchy-Schwarz inequality makes $q$ continuous in $\|\cdot\|_q$ . If a subspace is dense in this norm, positivity established there passes to the full form domain. Density only in the ambient $L^2$ norm does not provide this argument, since it gives no control of the form values.

5.3. Finite Gram limits

Proposition 5.4. Let $G_n$ and $G$ be real matrices indexed by a fixed finite set. Suppose $G_n(i,j)\to G(i,j)$ for every entry and $\sum_{i,j}x_iG_n(i,j)x_j\ge0 \qquad\text{for every real vector }x.$ Then the same inequality holds with $G$ in place of $G_n$ .

Proof. For a fixed $x$ , each summand converges. There are only finitely many summands, so their sum converges to the quadratic value for $G$ . Apply theorem 5.1 with zero error. ◻

The symmetry of the matrices is unnecessary for this order statement, although it is normally present in a Gram interpretation. The analogous complex Hermitian statement follows by applying the same continuity argument to real diagonal values. The Lean theorem implements the real finite-sum version.

If the dimensions vary, entrywise convergence has no meaning until the indices are compared. One option is a nested sequence of finite dimensional subspaces with restrictions of a common form. Another is the common-test construction of definition 1.1. Both provide actual maps. Equality of dimensions, or a list of similar-looking matrices, does not.

Example 5.5. On $X=\mathbb N$ , define $p_n(x)=1$ when $x=n$ and $p_n(x)=0$ otherwise. Each fixed $x$ has $p_n(x)=0$ eventually, so $p_n\to0$ pointwise. For every $n$ , however, $\sup_x|p_n(x)|=1$ . Thus the convergence is not uniform. Both conclusions are proved in Lean.

This example explains why a fixed-test theorem cannot be applied to a test $x_n$ moving with the cutoff. To control $p_n(x_n)$ one needs an estimate valid on that moving family, compactness and equicontinuity, or some other additional structure. Merely renaming $x_n$ as a test does not preserve the order of the quantifiers.

6. Continuous kernels and finite matrices

6.1. The mean-zero comparison

An explicit operator identity makes the comparison more informative than an abstract existence statement. Suzuki proves that the localized Weil operator is the Friedrichs extension of $D^*G_aD$ , with $D=i\,d/dx$ on $H_0^1(-a,a)$ and $G_a$ the compression of the screw-function kernel to the mean-zero subspace [8, Theorem 1.1]. Write $Q_W^a$ for the closed localized extension of the smooth-test form. The source establishes on the full Sobolev core, rather than only on smooth tests, that $\begin{equation} Q_W^a(v)=\langle G_aDv,Dv\rangle,\qquad v\in H_0^1(-a,a).\tag{10}\end{equation}$ The domain and the mean-zero compression are essential parts of this statement; the Sobolev identity is the source’s Lemma 3.1.

Let $I=(-a,a)$ , $L=2a$ , and $L_0^2(I)=\left\{u\in L^2(I):\int_Iu=0\right\}.$ The orthogonal projection onto this closed subspace is $(P_0u)(x)=u(x)-L^{-1}\int_Iu(t)\,dt.$ We regard functions as complex-valued and use the $L^2$ inner product linear in the first argument.

Proposition 6.1. The map $D:H_0^1(I)\longrightarrow L_0^2(I),\qquad Dv=iv',$ is a linear bijection. Its inverse is $\begin{equation} (Ku)(x)=-i\int_{-a}^xu(t)\,dt.\tag{11}\end{equation}$ Moreover, $\|Ku\|_2\le L\|u\|_2$ and $\|(Ku)'\|_2=\|u\|_2$ . Thus $D$ and $K$ are continuous for the derivative graph norm on $H_0^1(I)$ .

Proof. The one-dimensional Sobolev representative of $v\in H_0^1(I)$ is absolutely continuous and vanishes at both endpoints. Hence $\int_Iiv'=0$ , so $D$ has the asserted range. If $Dv=0$ , the representative is constant and its boundary value forces it to vanish.

For $u\in L_0^2(I)$ , the function in (11) is absolutely continuous, has derivative $-iu\in L^2(I)$ , and vanishes at $-a$ . Its value at $a$ also vanishes because $u$ has mean zero. It belongs to $H_0^1(I)$ and satisfies $DKu=u$ . The fundamental theorem of calculus gives $KDv=v$ .

Cauchy-Schwarz gives $|Ku(x)|\le\sqrt L\|u\|_2$ for every $x\in I$ . Integrating its square over an interval of length $L$ proves $\|Ku\|_2\le L\|u\|_2$ . The derivative identity proves the remaining norm assertion. ◻

Corollary 6.2. Suppose a form $q$ on $H_0^1(I)$ satisfies $q(v)=\langle GDv,Dv\rangle$ for a bounded self-adjoint operator $G$ on $L_0^2(I)$ . Then $q\ge0$ on $H_0^1(I)$ if and only if $G\ge0$ on $L_0^2(I)$ . If $H_0^1(I)$ is a form core for a closed extension of $q$ , the same condition gives positivity on the full form domain.

Proof. Positivity of $G$ passes along $D$ . Conversely, for $u\in L_0^2(I)$ set $v=Ku$ . Surjectivity gives $\langle Gu,u\rangle=q(v)\ge0$ . The final assertion follows by continuity in the form norm, as in proposition 5.3. ◻

This equivalence contains a concrete map and a concrete inverse. It does not prove positivity of $G_a$ . Applied for every $a$ to (10), it is another presentation of the full arithmetic sign problem. Its advantage is that $G_a$ has a continuous kernel on a compact interval, which permits explicit finite approximations and a precise norm error.

6.2. Cell averages and the comparison matrix

Let $\kappa$ be a continuous Hermitian kernel on $\overline I\times\overline I$ , meaning $\kappa(x,y)=\overline{\kappa(y,x)}$ . Define $(Au)(x)=\int_I\kappa(x,y)u(y)\,dy, \qquad G=P_0AP_0\big|_{L_0^2(I)}.$ Both are bounded self-adjoint operators. For the screw-function application, $\kappa(x,y)=g(x-y)$ is real and symmetric. All assertions in this subsection concern an arbitrary continuous Hermitian kernel.

Choose a partition $I=I_1\cup\cdots\cup I_m$ up to endpoints, with cell lengths $\ell_j>0$ and maximal length $h_m$ . Let $E_m$ be orthogonal projection onto the functions constant on each cell. The normalized indicators $e_j=\ell_j^{-1/2}\mathbf1_{I_j}$ form an orthonormal basis of its range. Since $E_m1=1$ , the projection preserves mean zero and commutes with $P_0$ .

In this basis, the matrix of $E_mAE_m$ is $\begin{equation} B_m(i,j)=\frac{1}{\sqrt{\ell_i\ell_j}} \int_{I_i}\int_{I_j}\kappa(x,y)\,dy\,dx.\tag{12}\end{equation}$ The mean-zero constraint for a coefficient vector $c$ is $\begin{equation} \sum_{j=1}^m c_j\sqrt{\ell_j}=0.\tag{13}\end{equation}$ These integration weights matter. For nonuniform cells, replacing this condition by $\sum c_j=0$ changes the subspace on which positivity is being checked.

For a general $u\in L_0^2(I)$ , the comparison map is $\begin{equation} d_m(u)_j=\langle u,e_j\rangle =\ell_j^{-1/2}\int_{I_j}u(t)\,dt.\tag{14}\end{equation}$ It satisfies the constraint, and $E_mu=\sum_jd_m(u)_je_j$ . The diagonal value of the matrix is $\langle AE_mu,E_mu\rangle =\sum_{i,j}\overline{d_m(u)_i}\,B_m(i,j)d_m(u)_j.$ Thus the finite model is evaluated on the same test through a declared linear map.

6.3. A quantitative kernel estimate

Define a modulus of continuity by $\omega_\kappa(\delta)= \sup\{|\kappa(x,y)-\kappa(x',y')|: |x-x'|+|y-y'|\le\delta\}.$ All points in the supremum lie in $\overline I^2$ . Compactness and continuity imply $\omega_\kappa(\delta)\to0$ as $\delta\downarrow0$ .

Theorem 6.3. For the preceding partition and kernel, $\begin{equation} \|A-E_mAE_m\|\le L\omega_\kappa(2h_m).\tag{15}\end{equation}$ Consequently, for $u\in L_0^2(I)$ , $\begin{equation} \left|\langle Gu,u\rangle- \sum_{i,j}\overline{d_m(u)_i}B_m(i,j)d_m(u)_j\right| \le L\omega_\kappa(2h_m)\|u\|_2^2.\tag{16}\end{equation}$ If $h_m\to0$ and there are $\delta_m\ge0$ with $\delta_m\to0$ such that $\begin{equation} \sum_{i,j}\overline c_i B_m(i,j)c_j \ge-\delta_m\sum_j|c_j|^2 \quad\text{whenever \href{#eq:approx:constraint}{(13)} holds},\tag{17}\end{equation}$ then $G\ge0$ on $L_0^2(I)$ .

Proof. For $x\in I_i$ and $y\in I_j$ , the kernel of $E_mAE_m$ is the cell average $\kappa_m(x,y)=\frac1{\ell_i\ell_j} \int_{I_i}\int_{I_j}\kappa(s,t)\,dt\,ds.$ Every pair $(s,t)$ in this average differs from $(x,y)$ by total distance at most $2h_m$ . Therefore $|\kappa(x,y)-\kappa_m(x,y)|\le\omega_\kappa(2h_m)$ . For $u\in L^2(I)$ this gives $|((A-E_mAE_m)u)(x)| \le\omega_\kappa(2h_m)\int_I|u(y)|\,dy \le\omega_\kappa(2h_m)\sqrt L\|u\|_2.$ Taking the $L^2(I)$ norm in $x$ introduces another factor of $\sqrt L$ , since the right side is constant on an interval of length $L$ . This gives (15). Since $P_0u=u$ , the value $\langle Gu,u\rangle$ equals $\langle Au,u\rangle$ . Cauchy-Schwarz and the operator norm bound prove (16).

Finally, $\sum|d_m(u)_j|^2=\|E_mu\|_2^2\le\|u\|_2^2$ . Combining the two inequalities yields $\langle Gu,u\rangle\ge- \bigl(\delta_m+L\omega_\kappa(2h_m)\bigr)\|u\|_2^2.$ The coefficient on the right tends to zero. Fix $u$ and pass to the limit. ◻

For a fixed interval, the modulus term is automatic. The remaining estimate is (17). Positivity of $G$ would imply this estimate with $\delta_m=0$ , because the finite form is an actual restriction. Thus the theorem is an explicit analytic reduction of the sign problem; it does not generate a sign from continuity.

For $u=Dv$ , the error becomes $\begin{equation} |q(v)-q_m(d_mDv)|\le L\omega_\kappa(2h_m)\|v'\|_2^2.\tag{18}\end{equation}$ This is a graph-norm estimate. It is enough for convergence on each fixed Sobolev test and does not claim a bound by $\|v\|_2^2$ uniform over the form core. High-frequency tests can have a large derivative norm while their $L^2$ norm stays fixed.

When $a$ also varies, both $L=2a$ and the modulus of the restricted kernel vary. A two-parameter argument must choose the mesh so that the displayed product tends to zero in the regime under consideration. The fixed-interval theorem does not specify such a choice uniformly over all $a$ .

7. Compression, subtraction, and changing spaces

7.1. Positive compressions

Let $H$ be a Hilbert space, $P_n$ orthogonal projections, and $B_f$ operators for which the following traces are finite. The quantity $p_n(f)=\operatorname{Tr}(B_fP_nB_f^*)$ is nonnegative, since $B_fP_nB_f^*=(B_fP_n)(B_fP_n)^*$ . If $B_fP_n$ is Hilbert-Schmidt, this trace is its squared Hilbert-Schmidt norm. This is a genuine positivity mechanism.

To identify an arithmetic form, however, a trace formula may subtract another term: $\begin{equation} Q_n(f)=p_n(f)-c_n(f).\tag{19}\end{equation}$ The sign of $p_n$ says nothing by itself about the difference. One needs a bound on the whole subtraction, an exact positive factorization of the difference, or an error small enough to use theorem 5.1.

Example 7.1. For $x\in\mathbb R$ , put $p_n(x)=(n+1)x^2$ and $c_n(x)=(n+2)x^2$ . Both are nonnegative quadratic forms, but $p_n(x)-c_n(x)=-x^2$ at every stage. The difference is already convergent and strictly negative at $x=1$ . Lean checks the positivity of the two sequences and their negative difference.

Connes and Consani’s archimedean comparison controls the discrepancy between a Sonin trace and the Weil distribution under specified support and vanishing conditions [2]. The discrepancy estimate is the part that connects the compression to arithmetic. Compactness of an error operator alone cannot determine its sign: a rank-one negative operator is compact.

Proposition 7.2. If $c_n(f)\le p_n(f)+\epsilon_n(f)$ , $\epsilon_n(f)\to0$ , and $p_n(f)-c_n(f)\to Q(f)$ for every fixed $f$ , then $Q\ge0$ .

Proof. The displayed inequality gives $p_n(f)-c_n(f)\ge-\epsilon_n(f)$ . Apply theorem 5.1. ◻

This proposition names the estimate that is actually needed. Assuming only that both $p_n$ and $c_n$ are traces of positive operators would omit it. In an arithmetic application, the subtraction can encode pole or cutoff terms, so it cannot be dropped without changing the target.

7.2. Shifted form norms

For a lower-bounded self-adjoint operator $A$ , choose $\lambda<\inf\operatorname{Spec}A$ . Then $A-\lambda I$ is positive and defines a form norm. This construction is available even when $A$ has negative spectrum.

Example 7.3. On $\mathbb R$ , take $q(x)=-x^2$ and $\lambda=-2$ . The shifted form $q(x)-\lambda x^2=x^2$ is positive, although $q(1)=-1$ . This implication failure is proved in Lean.

In the finite spectral construction of Connes, Consani and Moscovici, the quotient inner product uses the form shifted by its smallest eigenvalue; the stated real-zero result includes simplicity and evenness assumptions [4, Theorem 1.1]. Positivity of that quotient is a property of the shifted form. Removing the shift requires information about the original smallest eigenvalue or a separate arithmetic comparison.

There is a useful one-sided sufficient condition. If $q(x)-\lambda\|x\|^2\ge0$ and $\lambda\ge0$ , then $q(x)\ge0$ . If $\lambda<0$ , the same algebra gives only $q(x)\ge\lambda\|x\|^2$ . A limiting argument can still work when the negative lower bound tends to zero on each fixed test. The sign and size of the shift must therefore remain in the statement.

7.3. Semilocal comparison maps

Changing arithmetic spaces require more than a common name for their vectors. Connes, Consani and Moscovici construct specific Hilbert-space isomorphisms between semilocal Sonin spaces and identify a common entire-function carrier, with inner products depending on the set of places [3, Theorem 4.6 and following discussion]. This gives substantive comparison data. It does not by itself provide uniform norm constants as the set of places grows.

An elementary example shows the distinction. Let $H_n=\mathbb R$ as a vector space but give it the norm $\|x\|_n=n|x|$ for $n\ge1$ . The identity map $H_n\to H_{n+1}$ is an isomorphism for each $n$ . A fixed coordinate $1$ has norm tending to infinity. The underlying vector space can remain unchanged while the family of Hilbert norms has no finite limiting value on that vector.

For a common-space limit, one may seek maps $U_n:H_n\to H$ into a fixed Hilbert space with controlled norms, or specify a directed system whose completion is part of the construction. For positivity on common tests, it is often enough to provide $d_n:\mathcal T\to H_n$ and compare $q_n(d_nf)$ with $Q_W(f)$ . The latter approach avoids demanding an unnecessary global Hilbert-space limit. It still requires the arithmetic identity or error estimate.

8. Ground states and spectral gaps

8.1. Selection of the lowest eigenspace

A small eigenvector residual is useful only relative to spectral information. If $\|(A-\mu)v\|$ is small, the vector may concentrate near any spectral value close to $\mu$ . To compare it with the ground state, $\mu$ must be identified with, or quantitatively related to, the bottom eigenvalue and separated from the remaining spectrum.

The following estimate states the exact dependence. Let $A$ be self-adjoint on a Hilbert space, let $\lambda_0$ be a simple isolated lowest eigenvalue with normalized eigenvector $\eta$ , and let $P$ be the projection onto $\mathbb C\eta$ . Suppose the remainder of the spectrum lies in $[\lambda_0+\gamma,\infty)$ for $\gamma>0$ .

Theorem 8.1. For every $v\in\operatorname{Dom}A$ , $\begin{equation} \|(I-P)v\|\le\gamma^{-1}\|(A-\lambda_0)v\|.\tag{20}\end{equation}$ If $\|v\|=1$ , one can choose $c\in\mathbb C$ , $|c|=1$ , such that $\begin{equation} \|v-c\eta\|\le\sqrt2\,\gamma^{-1} \|(A-\lambda_0)v\|.\tag{21}\end{equation}$

Proof. Set $w=(I-P)v$ . The spectral projection preserves $\operatorname{Dom}A$ and commutes with $A$ , so $(A-\lambda_0)v=(A-\lambda_0)w$ . The spectral gap gives $\gamma\|w\|^2\le\langle (A-\lambda_0)w,w\rangle \le\|(A-\lambda_0)v\|\,\|w\|.$ The last inequality is Cauchy-Schwarz; the middle expression is real and nonnegative. If $w=0$ , (20) is immediate. Otherwise divide by $\gamma\|w\|$ .

Write $v=\alpha\eta+w$ with $w\perp\eta$ . Choose the phase $c$ so that $\overline c\alpha=|\alpha|$ when $\alpha\ne0$ , and any unit phase when $\alpha=0$ . Orthogonality gives $1=\|v\|^2=|\alpha|^2+\|w\|^2$ , so $|\alpha|\le1$ and $\|v-c\eta\|^2=2(1-|\alpha|) \le2(1-|\alpha|^2)=2\|w\|^2.$ Combine this with (20). ◻

The proof only needs the lower bound on the orthogonal complement and the reducing property of the projection. The spectral theorem is one way to obtain them. In finite dimensions they can be certified by a matrix gap estimate. The phase choice is necessary because an eigenspace does not specify a preferred unit vector.

Corollary 8.2. Suppose $v_n\in\operatorname{Dom}A_n$ , $\|v_n\|=1$ , $r_n=\|(A_n-\mu_n)v_n\|$ , and $\lambda_{0,n}$ is the actual simple lowest eigenvalue with gap $\gamma_n>0$ . If $\frac{r_n+|\mu_n-\lambda_{0,n}|}{\gamma_n}\longrightarrow0,$ then, after phase choices, $v_n$ approaches the normalized ground state in norm.

Proof. The triangle inequality gives $\|(A_n-\lambda_{0,n})v_n\|\le r_n+|\mu_n-\lambda_{0,n}|$ . Apply (21). ◻

An estimate for $r_n$ alone does not certify the eigenvalue difference in this corollary. In particular, a variational upper bound identifies a trial energy above the ground-state energy; a lower bound or a suitable enclosure is still needed to show that the trial vector is near the bottom rather than an excited level.

8.2. A shrinking-gap counterexample

Example 8.3. On $\mathbb R^2$ with its Euclidean inner product, let $A_n=\begin{pmatrix}0&0\\0&(n+1)^{-1}\end{pmatrix}, \qquad v_n=e_2.$ The operator is positive and self-adjoint. Its minimum is the simple eigenvalue zero with ground-state line $\mathbb Re_1$ , and its gap is $\gamma_n=(n+1)^{-1}$ . The residual $\|A_nv_n\|$ tends to zero. Nevertheless, $\operatorname{dist}(v_n,\mathbb Re_1)=1$ for every $n$ . The ratio of residual to gap equals one.

The Lean implementation defines the same diagonal linear map and proves residual convergence, separation from every vector on the first-coordinate line, and the exact zero-energy condition. The default product norm in the code is the maximum norm. The asserted residual and separation statements hold in that norm as well. A bundled self-adjoint Euclidean operator is not part of the formal declaration.

This example isolates the missing hypothesis without an arithmetic assumption. Every finite minimum is simple, each operator is positive, and the residual tends to zero. Even this combination does not force convergence of the trial vectors to the corresponding ground states. A uniform gap is sufficient, but the weaker and more precise requirement is a vanishing residual-to-gap ratio.

8.3. Parity and normalization

Suppose an involution $R$ commutes with $A$ and the lowest eigenspace is one-dimensional. Then $R$ acts on that eigenspace by a scalar whose square is one. The ground state is therefore even or odd. Simplicity alone does not determine which parity occurs. A comparison with an even proxy needs evenness, or another argument showing a nonzero even component in the lowest eigenspace.

Normalization also affects a proposed transform limit. If $\eta_n$ is an eigenvector, so is $c_n\eta_n$ for any nonzero scalar. The zeros of its transform do not change under this scalar multiplication, but the transform can tend to zero or diverge. To identify a nonzero limiting function, one must fix the scalar using a norm, a linear functional, or a specified coefficient and prove that the chosen normalization is defined.

For example, a normalization $\ell_n(\eta_n)=1$ requires $\ell_n(\eta_n)\ne0$ . If one first estimates normalized vectors in $L^2$ and then renormalizes by $\ell_n$ , the continuity bounds for $\ell_n$ and a lower bound on its values enter the error estimate. A phase chosen for $L^2$ closeness may not coincide with the normalization used by an arithmetic formula. Both choices must be related explicitly.

9. Transform comparison on complex strips

9.1. A weighted integral bound

For $b\ge0$ , define the closed vertical strip $S_b=\{z\in\mathbb C:|\operatorname{Re}z|\le b\}$ . For a measurable function $h:\mathbb R\to\mathbb C$ , set $\|h\|_{1,b}=\int_\mathbb Re^{b|t|}|h(t)|\,dt$ when the integral is finite. This is the quantity naturally controlling a centered Laplace transform on $S_b$ .

Theorem 9.1. Let $b\ge0$ and let $h:\mathbb R\to\mathbb C$ be measurable with $\|h\|_{1,b}<\infty$ . Then $\begin{equation} \sup_{z\in S_b}\left|\int_\mathbb Rh(t)e^{zt}\,dt\right| \le\|h\|_{1,b}.\tag{22}\end{equation}$ If measurable functions $h_n$ have finite weighted integrals and satisfy $\|h_n\|_{1,b}\to0$ , their error transforms converge uniformly to zero on $S_b$ .

Proof. Since $b\ge0$ , the weight is at least one, so the hypothesis already implies $h\in L^1(\mathbb R)$ . For real $t$ and $z\in S_b$ , $|e^{zt}|=e^{(\operatorname{Re}z)t}\le e^{|\operatorname{Re}z||t|} \le e^{b|t|}.$ The same bound proves integrability of $h(t)e^{zt}$ by domination. The triangle inequality for the integral gives $\left|\int h(t)e^{zt}\,dt\right| \le\int|h(t)|\,|e^{zt}|\,dt \le\int e^{b|t|}|h(t)|\,dt.$ The right side is independent of $z$ . Given $\epsilon>0$ , choose $n$ large enough that it is less than $\epsilon$ for $h_n$ . This is uniform convergence on the entire strip. ◻

All three steps are implemented in Lean: the complex exponential bound, the Bochner integral comparison, and uniform convergence on the subtype representing the strip. The formal theorem is stated for an error function $h_n$ . If $h_n=f_n-g_n$ , identification of the error integral with $F_{f_n}-F_{g_n}$ uses integrability of the individual transforms. In the compact-support case that integrability follows directly. The error theorem does not silently provide it for arbitrary measurable functions.

For the Fourier convention $\widehat f(w)=\int f(t)e^{-iwt}\,dt$ , the same estimate controls the horizontal strip $|\operatorname{Im}w|\le b$ . The substitution $z=-iw$ relates the conventions. Suzuki uses the sign $+iwt$ , so the two Fourier transforms are related by $w\mapsto-w$ . This reflection preserves real-zero statements and leaves the even target $\Xi$ unchanged. A fixed convention is still needed for the comparison maps and normalization.

9.2. Expanding support

An $L^2$ estimate implies a weighted $L^1$ estimate on a fixed compact interval. Its dependence on that interval is explicit.

Proposition 9.2. If $h$ is supported in $[-R,R]$ and belongs to $L^2$ , then $\begin{equation} \|h\|_{1,b}\le C_b(R)\|h\|_2, \qquad C_b(R)= \begin{cases} \sqrt{(e^{2bR}-1)/b},&b>0,\\ \sqrt{2R},&b=0. \end{cases}\tag{23}\end{equation}$

Proof. Apply Cauchy-Schwarz to $e^{b|t|}$ and $|h(t)|$ on $[-R,R]$ . The squared norm of the first factor is $\int_{-R}^R e^{2b|t|}\,dt$ , which equals the displayed expression squared. ◻

For a ground-state comparison on expanding intervals, (23) must be combined with (21). A sufficient condition is $\begin{equation} C_b(R_n)\, \frac{\|(A_n-\lambda_{0,n})v_n\|}{\gamma_n} \longrightarrow0,\tag{24}\end{equation}$ after the required transport and normalization. This condition is stronger than norm convergence of the eigenvectors if $R_n\to\infty$ . It is also only one sufficient route; separate control of weighted tails can avoid the crude factor $C_b(R_n)$ .

Example 9.3. Fix $b>0$ and a nonnegative nonzero $\phi\in C_c^\infty(0,1)$ . Let $h_n(t)=e^{-bn}\phi(t-n)$ . Then $\|h_n\|_2=e^{-bn}\|\phi\|_2\to0$ , but $F_{h_n}(b)=\int_0^1\phi(u)e^{bu}\,du>0$ for every $n$ . Thus $L^2$ convergence alone does not give transform convergence on a strip with nonzero width when supports escape.

A useful alternative is to split the weighted error into a compact part and a tail. For every fixed $R$ , suppose $h_n\to0$ in $L^1([-R,R])$ , and assume $\begin{equation} \lim_{R\to\infty}\sup_n \int_{|t|>R}e^{b|t|}|h_n(t)|\,dt=0.\tag{25}\end{equation}$ The compact contribution to $\|h_n\|_{1,b}$ is at most $e^{bR}\|h_n\|_{L^1([-R,R])}$ , while the tail is uniformly small. Choosing $R$ first and $n$ second proves $\|h_n\|_{1,b}\to0$ . This order of choices is essential; a tail estimate only for each fixed $n$ would not suffice.

9.3. Transport between intervals

Suppose $\eta_n$ is defined on an interval $I_n$ and a proxy $k_n$ is written in a scaled coordinate. Before taking their difference, define the transport. For example, for $r_n>0$ the $L^2$ -isometric dilation is $(U_n\eta_n)(t)=r_n^{1/2}\eta_n(r_nt),$ with support dilated by $r_n^{-1}$ . Its transform is $F_{U_n\eta_n}(z)=r_n^{-1/2}F_{\eta_n}(z/r_n).$ The scalar factor and argument scaling are part of the formula. A dilation used to normalize support therefore changes the region on which a transform comparison is asserted.

One can instead use a nonisometric dilation if that is the normalization supplied by the source. Then its norm change must be recorded. In either case, set $h_n=c_nU_n\eta_n-k_n$ only after the scalar $c_n$ and the embedding by zero extension have been fixed. The weighted estimate applies to this actual function. It cannot compare unnamed vectors in different Hilbert spaces.

10. Ground-state transform limits

10.1. Known zero-location input

Connes and van Suijlekom prove a real-zero theorem for the Fourier transform of a simple isolated even ground state of a specified distributional quadratic form [5, Theorem 6.1]. Their precise statement includes lower boundedness and essential self-adjointness on the trigonometric-polynomial domain. A merely formal kernel expression does not supply that domain hypothesis. The theorem is an available analytic input once its assumptions have been checked for the proposed operator.

Connes’s later construction distinguishes the explicit proxy $k_\lambda$ from the actual normalized ground state. The proxy transform has a proved limit equal to $\Xi$ on closed substrips, while simplicity and evenness of the actual minimum and comparison with the proxy remain stated tasks [1, Sections 6.5 and 6.6]. These are separate statements about different functions. A known limit for the proxy cannot be substituted into the ground-state theorem without a comparison estimate.

The following abstract statement describes the required final analytic passage. It is not a new zeta-function theorem.

Proposition 10.1. Let $\Omega\subset\mathbb C$ be a connected open set and $L\subset\Omega$ a relatively closed set. Let $H_n$ be holomorphic on $\Omega$ with no zeros in $\Omega\setminus L$ . Suppose $H_n\to H$ uniformly on compact subsets of $\Omega$ , where $H$ is not identically zero. Then every zero of $H$ in $\Omega$ belongs to $L$ .

Proof. If $z_0\in\Omega\setminus L$ , choose a disk around $z_0$ whose closure lies in $\Omega\setminus L$ . The functions $H_n$ are nonvanishing on this disk. Hurwitz’s theorem says that the limit is either nonvanishing there or identically zero there. The second case would make $H$ identically zero on connected $\Omega$ by the identity theorem. Thus $H(z_0)\ne0$ . ◻

The elementary content of this proposition is the way the zero-free region is chosen. The holomorphic convergence must hold in a neighborhood of a proposed off-axis zero, not just at real arguments. A nonzero limit is also necessary: the functions $H_n=1/n$ are nonvanishing and converge to the zero function, whose zero set is the entire domain.

Corollary 10.2. In a horizontal strip $\Omega=\{w:|\operatorname{Im}w|<b_0\}$ , let $\eta_n$ and $k_n$ be integrable functions whose Fourier transforms are holomorphic. Suppose the transforms of $\eta_n$ have only real zeros in $\Omega$ , and for every $0<b<b_0$ , $\|\eta_n-k_n\|_{1,b}\longrightarrow0.$ If $\widehat{k_n}\to H$ locally uniformly in $\Omega$ and $H\not\equiv0$ , then every zero of $H$ in $\Omega$ is real.

Proof. The weighted comparison implies uniform convergence of $\widehat{\eta_n}-\widehat{k_n}$ on each closed substrip by theorem 9.1. Hence $\widehat{\eta_n}\to H$ locally uniformly. Apply proposition 10.1 with $L=\Omega\cap\mathbb R$ . ◻

10.2. Holomorphic normalization

Multiplication by a nonzero scalar does not alter zeros. More generally, a holomorphic nowhere-zero factor $a_n(w)$ preserves the zero set of a holomorphic function on its domain. Therefore a renormalized family $a_n\widehat{\eta_n}$ can enter proposition 10.1 if its convergence and holomorphy are proved.

A pointwise finite expression for a normalizing exponent does not alone establish this condition. If $a_n=e^{\phi_n}$ , holomorphy of $\phi_n$ is a sufficient way to ensure a holomorphic nowhere-zero factor. If the proposed limit is a quotient, one must also specify a domain where it is holomorphic or account for removable singularities. Hurwitz in the stated form is not a theorem about arbitrary meromorphic limits with unexamined poles.

Suzuki’s nonlocal spectral construction produces real-zero entire functions after choosing a positive shifted form. Its proposed large-interval limit is conditional, and the small-interval positivity, simplicity, and evenness theorem does not cover arbitrary large intervals [8, Theorems 1.4 and 1.5, Corollary 1.6]. For a use of that proposal, the shift, boundary parameter, normalization, and domain of the limiting function must be retained. None is removed by the existence of self-adjoint extensions at finite size.

The weighted comparison gives a concrete sufficient replacement for an informal approximation assertion. It does not claim that the replacement estimate is necessary or already known for the arithmetic family. A local uniform transform estimate could be proved directly without going through weighted $L^1$ . The stronger spatial estimate is valuable when it can be derived from a spectral gap and explicit tails.

11. The remaining arithmetic estimates

The preceding results distinguish two precise residual problems. For a continuous kernel on a fixed interval, the finite matrices and the error bound are explicit. The unresolved input is a lower bound on the mean-zero matrix form that tends to zero with refinement. For a ground-state transform construction, the unresolved inputs concern the selected eigenfunction and its comparison with a known proxy.

The kernel route asks for a concrete arithmetic $\kappa_a$ , partitions with mesh tending to zero, and numbers $\delta_{a,m}\ge0$ such that (17) holds and $\delta_{a,m}\to0$ for each fixed $a$ . The remaining analytic error $2a\omega_{\kappa_a}(2h_m)$ already tends to zero. Composing theorem 6.3 with corollary 6.2 then proves local Weil positivity. To cover all compactly supported tests, this construction is required for every interval size.

The ground-state route asks for operators satisfying the precise real-zero theorem, simple isolated even minimum eigenvectors with a declared normalization, and explicit transports to the proxy coordinate. One then seeks either local uniform transform comparison or the weighted errors in corollary 10.2. An approximate eigenvector method must estimate the residual relative to the actual minimum and divide by the spectral gap. If only an $L^2$ error is available, its conversion to weighted $L^1$ must account for growing support.

Neither package is certified by a successful finite computation at a bounded collection of parameters. A rigorous matrix calculation can prove (17) for its particular interval and partition, with a certified error for the continuum kernel at that scale. It does not establish the estimate for every interval. Likewise, a ground-state plot or small residual at finitely many parameters does not prove the asymptotic gap ratio or the weighted comparison.

There are useful intermediate outcomes short of the global target. A finite matrix lower bound plus (15) yields a quantitative lower bound for the localized continuous kernel. A gap estimate plus a certified residual gives an error bar for a normalized ground state. A weighted spatial error gives a uniform error bar for its transform on a chosen strip. Each is an independent theorem with specified inputs and a conclusion that can be reused without assuming global Weil positivity.

11.1. Circularity boundaries

Several apparently stronger structures can be equivalent presentations of the target. A positive Hilbert realization whose squared norm is exactly $Q_W(f)$ proves positivity immediately; constructing that realization from the assumption $Q_W\ge0$ is the standard quotient-and-completion construction. Similarly, positivity of the screw-function compression for every interval is equivalent to positivity of its pullback along the derivative map. An explicit equivalence is mathematically useful, but it does not make either side an independently established input.

A finite approximation certificate has the same boundary. If one sets $q_n=Q_W$ on the test space, the certificate’s positivity field is the original problem. To avoid this substitution, a proposed model must have an independently given formula or construction. Its positivity proof must use that construction, and the arithmetic comparison must be checked afterward. The quantifiers over all tests and all scales must remain visible throughout.

The analysis also excludes a different error: treating the absence of a proof in a Lean library as evidence of a new mathematical theorem. The positivity transfer and weighted transform estimate are standard analysis and have formal proofs here. The zero-counting input, operator realization, and real-zero theorem are known external mathematics with nontrivial formalization work remaining. The unresolved arithmetic lower bounds and ground-state comparisons are mathematical obligations, not missing import statements.

A. Formal statements and coverage

The module contains twenty theorem declarations in the namespace . It was checked with Lean and mathlib revision . Every printed theorem dependency is contained in the standard set , , and . There are no additional mathematical axioms or proof placeholders in this module.

The formal statements concern supplied functions, maps, matrices, and integrals. They do not define the zeta zero divisor or assert that a concrete arithmetic approximation certificate exists. This scope matters when a general theorem is applied to the Weil form: the application must still construct the relevant arguments and discharge its hypotheses.

A.1. Order and dense-image results

The main scalar limit theorem has the following mathematical signature: $\begin{gathered} q:\mathbb N\to X\to\mathbb R,\quad Q:X\to\mathbb R,\quad \epsilon:\mathbb N\to X\to\mathbb R,\\ (\forall n,x,\ -\epsilon_n(x)\le q_n(x)),\quad (\forall x,\ \epsilon_n(x)\to0),\quad (\forall x,\ q_n(x)\to Q(x))\\ \Longrightarrow\quad\forall x,\ 0\le Q(x). \end{gathered}$ It is . Its proof uses closedness of the real order through the library’s limit-of-inequalities theorem. The comparison version is ; it first derives $-\epsilon_n(x)\le Q(x)$ from the absolute defect.

The theorem takes an arbitrary topological space, a dense-range map, and a continuous real functional. It uses the closed set where the functional is nonnegative. The composed result is . Neither declaration assumes that the topology is a Hilbert norm, so an application can choose the test-function or form topology that its continuity proof actually supports.

A.2. Changing spaces and finite sums

The structure includes a dependent family $Y_n$ , real module instances on each $Y_n$ , and linear maps from a common real module $X$ . Its fields are the model values, the comparison error, nonnegativity of each model, the absolute comparison bound, and pointwise convergence of the error to zero. The theorem is corollary 5.2 for these fields.

The declaration treats a fixed finite index type and real matrix entries. Its proof passes limits through two finite sums and multiplication by fixed coefficients. The finite index type is part of the statement; the theorem does not compare matrices of different dimensions. The complex Hermitian version and the operator kernel approximation of theorem 6.3 are mathematical arguments in this paper, not declarations in this module.

The elementary pullback statement is . The separate declaration takes the actual bound $c(x)\le q(x)$ and concludes $q(x)-c(x)\ge0$ . It is deliberately stronger in its premise than positivity of either separate term, which the counterexample shows is insufficient.

A.3. Transform estimates

The theorem states $|\operatorname{Re}z|\le b\quad\Longrightarrow\quad \|\exp(zt)\|\le\exp(b|t|)$ for real $t$ . The proof uses the exact complex exponential norm formula and a real product estimate. The parameter $b$ need not be separately declared nonnegative in the formal statement: existence of a $z$ satisfying the premise already implies that fact.

The next theorem, , assumes integrability of $t\mapsto e^{b|t|}\|h(t)\|$ and proves the Bochner integral bound in theorem 9.1. Its final consumer, , uses the subtype $\{z:\mathbb C\mid |z.\mathrm{re}|\le b\}$ as the domain of uniform convergence. Its conclusion concerns the entire closed strip, including unbounded imaginary parts. This is stronger than the local uniform convergence required for a holomorphic limit argument.

The module does not prove holomorphy of an arbitrary transform, integration by parts for smooth tests, or the zero-counting estimate. In the paper, these are separate mathematical steps. The formal transform estimate can nevertheless be used immediately when a later module provides the actual error functions and the weighted integral convergence.

A.4. Counterexamples

The declarations and encode examples 7.1 and 7.3. The function computes the real diagonal value of the reflected Hermitian block. Its positive and negative evaluations are and . Finite interpolation at actual transform arguments is not formalized by these two scalar calculations.

The moving-spike example uses a function on $\mathbb N\times\mathbb N$ . The declarations and prove the two convergence claims in example 5.5. This example is about arbitrary functions; it is not presented as a sequence of continuous quadratic forms.

The final countermodel defines as a real linear map on $\mathbb R\times\mathbb R$ . The declarations , , and verify the residual, separation, and zero-energy assertions. The general spectral-gap theorem theorem 8.1, Sobolev inverse proposition 6.1, and escaping-support example are proved in prose. Their absence from this module is a formalization boundary, not an extra assumption in the scalar countermodel.

B. Finite certificates with explicit errors

A finite certificate becomes useful when its numerical or symbolic inequalities have a stated relation to the continuum object. The kernel estimate provides a simple example with no appeal to an unspecified limit theorem. Let $B_m$ be the cell-average matrix from (12), and let $V_m$ be the weighted mean-zero coefficient space from (13). Suppose a rigorous finite calculation proves $c^*B_mc\ge\beta_m\|c\|^2\qquad(c\in V_m).$ If $\beta_m<0$ , the continuum lower bound supplied by this information is $\langle Gu,u\rangle\ge \bigl(\beta_m-L\omega_\kappa(2h_m)\bigr)\|u\|^2.$ If $\beta_m\ge0$ , the directly valid conclusion is $\langle Gu,u\rangle\ge-L\omega_\kappa(2h_m)\|u\|^2$ . The two cases combine as $\begin{equation} \langle Gu,u\rangle\ge \bigl(\min\{\beta_m,0\}-L\omega_\kappa(2h_m)\bigr)\|u\|^2.\tag{26}\end{equation}$ The minimum is necessary because a positive bound for the finite projection does not control vectors in its orthogonal complement.

To verify (26), start from $\langle Gu,u\rangle\ge\beta_m\|E_mu\|^2-L\omega_\kappa(2h_m)\|u\|^2$ . When $\beta_m<0$ , the contraction property gives $\beta_m\|E_mu\|^2\ge\beta_m\|u\|^2$ ; when $\beta_m\ge0$ , discard the nonnegative term. This elementary sign split avoids an incorrect inference of strict continuum coercivity from a positive finite matrix.

If the computed matrix is an approximation $\widetilde B_m$ rather than the exact cell-average matrix, one also needs a certified bound $\|B_m-\widetilde B_m\|\le\eta_m$ . Then a lower bound $\widetilde\beta_m$ for $\widetilde B_m$ gives $\beta_m=\widetilde\beta_m-\eta_m$ for the exact finite matrix. The total error has two distinct origins: matrix evaluation and continuum projection. Both are displayed before taking a limit.

An analogous finite ground-state certificate begins with an interval enclosure for the actual lowest eigenvalue and a positive lower bound on the next spectral level. If the enclosing intervals are disjoint, their separation gives a certified gap. A residual bound for a normalized trial vector then enters corollary 8.2. To reach a transform certificate, multiply by the support-dependent factor in (23) or prove the weighted error directly.

These constructions identify what a finite calculation can establish. They also identify which constants must be controlled in an asymptotic theorem. The passage from a verified finite certificate to all interval sizes is an additional mathematical assertion, not an automatic consequence of refining the matrix at one fixed size.

References

A. Connes, The Riemann Hypothesis: Past, Present and a Letter Through Time, 2026. arXiv:2602.04022. https://arxiv.org/abs/2602.04022.
A. Connes and C. Consani, Weil positivity and Trace formula, the archimedean place, 2020. arXiv:2006.13771. https://arxiv.org/abs/2006.13771.
A. Connes, C. Consani, and H. Moscovici, Zeta zeros and prolate wave operators, 2023, revised 2024. arXiv:2310.18423. https://arxiv.org/abs/2310.18423.
A. Connes, C. Consani, and H. Moscovici, Zeta Spectral Triples, 2025. arXiv:2511.22755. https://arxiv.org/abs/2511.22755.
A. Connes and W. D. van Suijlekom, Quadratic Forms, Real Zeros and Echoes of the Spectral Action, 2025. arXiv:2511.23257. https://arxiv.org/abs/2511.23257.
M. Long and The YonedaAI Collaboration, Arithmetic Positivity Structures, Arithmetic Positivity Program, Part I, 2026. Companion preprint.
M. Long and The YonedaAI Collaboration, Structural Arithmetic Geometry, Arithmetic Positivity Program, Part III, 2026. Companion preprint.
M. Suzuki, Weil’s quadratic form via the screw function, 2026, version dated August 24, 2026. arXiv:2606.09096. https://arxiv.org/abs/2606.09096.
T. S. Trudgian, An improved upper bound for the argument of the Riemann zeta-function on the critical line II, 2012. arXiv:1208.5846. https://arxiv.org/abs/1208.5846.