Structural arithmetic geometry

1.1. The fixed analytic target

We use the test algebra $\mathcal T=C_c^\infty(\mathbb R,\mathbb C)$, centered transform $F_f$, involution $f^*$, and Hermitian form $B_W$ defined in Part I. The convention is linear in the first argument. Thus the quadratic functional is $Q_W(f)=B_W(f,f)$. The underlying real vector space still contains every complex test function; realifying the scalar structure does not restrict the quantifier to real-valued tests.

For reference, the decisive distinction in the zero-side expression is $$\begin{equation} Q_W(f)=\sum_\rho F_f(\rho-\tfrac12) \overline{F_f(\tfrac12-\overline\rho)}.\tag{1}\end{equation}$$ Zeros are counted with multiplicity. A summand becomes an absolute square when the associated zero lies on the critical line. Replacing the second factor by the conjugate of the first before establishing that fact would assume the desired conclusion. The smoothness and compact support of $f$ give the decay needed for absolute convergence, with the explicit-formula convention of [3, Appendix B]. Convergence of this sum is consequently distinct from its nonnegativity.

The classical Weil criterion identifies nonnegativity of this exact functional on all of $\mathcal T$ with RH. It is a cited analytic theorem in this program, not a new theorem or an axiom introduced into the Lean library. The point of the formal work is to verify smaller transfers while exposing exactly where the arithmetic identification must enter.

1.2. Requirements for a structural explanation

A useful explanation should specify a source category, a realization functor, a positive or negative form in that category, and the comparison with the analytic target. It should also distinguish statements that are already known in that category from the construction still required for the arithmetic example. A Hodge index theorem on an available smooth projective surface is known mathematics. Producing an appropriate object associated to the arithmetic base, with the right correspondence algebra and archimedean terms, is a different task.

This separation prevents two common errors. One is to put the target identity into an opaque proposition named geometric realization and treat the name as a construction. The other is to demand so much structure that every later proof becomes formal, while leaving the existence of the structure unexamined. A sufficient package is useful when its fields identify independent construction problems. It becomes circular when a field is the original positivity statement with renamed variables.

2.1. Weaker certificates and their limits

If one asks only for a function $r:V\to\mathbb R$ with $B(x,x)=r(x)^2$, existence is again equivalent to nonnegativity: take the nonnegative square root pointwise. This certificate forgets addition, scalar multiplication, and the off-diagonal form. It is logically sufficient for the sign but structurally poor. The Lean library proves this equivalence explicitly so that an arbitrary norm-square representation is not mistaken for a new arithmetic construction.

Linearity of a realization restores the off-diagonal information through polarization. For a Hermitian form, the diagonal determines the form because the four values at $x+y$, $x-y$, $x+iy$, and $x-iy$ recover the real and imaginary cross terms. Consequently a linear map preserving every diagonal value preserves the entire form. This is a genuine additional property of the map, even though existence of a linear Hilbert realization remains equivalent to positivity.

A comparison order can be defined by forgetting structure. A geometric certificate may forget its cycle algebra, degrees, and pullback operations to become a positive realization. The existence of that forgetful map does not imply that every positive realization comes from geometry. Minimality in the category of Hilbert realizations therefore says nothing about initiality in a category of arithmetic spaces.

3.1. Logical strength of the image-restricted inequality

Suppose equation 3 has been proved, but the only proposed negativity theorem is $$I(\Gamma f,\Gamma f)\le0\qquad(f\in\mathcal T).$$ This statement is exactly Weil positivity after substitution. It can still be a useful reformulation, because the images $\Gamma f$ may admit geometric tools. It cannot be called an already established geometric input without a proof using those tools.

A negativity theorem for an independently constructed primitive space is stronger data. Its usefulness comes from the independent construction and its proof, not simply from the fact that the theorem quantifies over more vectors. One could always define $P$ using the Weil form and restate the same problem there. The source of the objects must therefore be recorded alongside the theorem signatures.

3.2. Composition and descent

Suppose another space $P'$ maps to $P$ by a linear map $u$ preserving intersection forms, and $\Gamma=u\Gamma'$ for a map $\Gamma':\mathcal T\to P'$. Then equation 3 pulls back along $u$. This is the basic compositional property APP needs: exact comparisons compose, and positivity pulls back along them.

If a pairing descends through a quotient, vectors killed by the quotient must pair to zero with every vector. For a nonnegative symmetric form the null-radical lemma provides precisely that condition. Thus the quotient construction can be formalized independently once positivity is given. It does not create a sign from an indefinite form. In a categorical setting, descent of the underlying object and descent of a positive form are different obligations; the compatibility equations must include the form and any operators that act on it.

For genuinely local geometric data, a descent assertion would have to specify the covering family, overlap maps, cocycle equations, and the topology used for completion. None of these is forced by the words condensed or cohomological. A general sheaf or condensed category may provide a useful home for analytic objects without proving the arithmetic comparison or the sign of a pairing in that category.

4.1. From purity to an invariant metric

A converse needs more care. In finite dimensions, a diagonalizable complex operator whose eigenvalues all have modulus one admits a positive invariant Hermitian form: choose an eigenbasis and make it orthonormal. The same conclusion fails without diagonalizability. It also does not extend verbatim to infinite-dimensional representations, where the choice of a complete norm and boundedness of the action matter.

This example refutes a proposed bridge from bare spectral purity to invariant polarisation. It does not refute stronger cohomological purity packages that include semisimplicity or a polarization theorem. Rather, it identifies which additional structure such a bridge must use. The Lean library verifies the shear obstruction in ordinary real linear algebra.

5.1. The radical and the intended carrier

The universal realization factors through the radical of the Weil form. A comparison with a wedge space must therefore explain whether that wedge space represents the full test space, its radical quotient, a completion, or another representation entirely. These choices are mathematically different even when their names suggest the same object.

A zero vector space has a vector, namely zero. It is not an empty type. Thus an assertion that a linear defect vanishes is ordinarily expressed by the space being the zero space, or by its nonzero-vector subtype being empty. Replacing this by emptiness of the full vector carrier changes the statement. This distinction already arises before any analytic positivity argument and is relevant to the context-repository audit in Part I.

An exact comparison with a positive target also identifies the source radical with the kernel of the realization map. Injectivity is therefore a substantive hypothesis when the desired conclusion is strict positivity on the source. A source vector killed by the map cannot acquire a strictly positive norm by pulling back the target metric. Quotienting it out may be correct, but the quotient has to match the intended arithmetic object.

6.1. The quantifier order

For the sign transfer, the needed order is $$\forall f\in\mathcal T\quad\forall\epsilon>0\quad \exists N\quad\forall n\ge N:\quad Q_W(f)\ge-\epsilon.$$ A common $N$ for every unit vector is unnecessary. Conversely, a calculation for finitely many chosen tests supplies only those finitely many inequalities. Increasing the number of tests in numerical experiments does not replace the all-test quantifier unless a density theorem and error estimate are proved.

One may work on a dense common core when the target quadratic form is continuous in the chosen topology. Here the topology must be named. Smooth compact tests have a natural test-function topology; an unbounded quadratic form on a Hilbert space is generally not continuous in the ambient Hilbert norm. A statement about a form core uses the form norm, not merely the norm in the surrounding $L^2$ space.

Finite-dimensional positivity is also basis-dependent in its interpretation. A positive semidefinite matrix representing the exact form on a finite span proves positivity on that span. A sampled kernel matrix may instead represent a quadrature approximation. In that case its positivity concerns the discretized form, and a quadrature error estimate is another comparison obligation. These are different applications of the same pullback principle.

6.2. Subtraction and normalization

A positive operator has a nonnegative ordinary trace whenever that trace is defined. A renormalized expression is often a difference of divergent or cutoff-dependent positive quantities. The sign of the difference does not follow from the signs of its summands.

This example applies to the logical form of a subtraction argument, not to a particular trace formula. It shows which inference needs justification. In the arithmetic explicit formula, the prime-power contribution and the archimedean subtraction have fixed signs and normalizations. A proposed positive compression must be compared with that entire expression, including all correction terms.

A related issue arises from shifting a lower-bounded self-adjoint operator, as in the localized constructions discussed by Suzuki [5]. If $A$ has lower bound $m$, then $A-cI$ is positive for $c<m$. This gives a useful Hilbert norm, but it says nothing about positivity of $A$ when $c$ is negative. The scalar operator $A=-I$ becomes positive after subtracting $-2I$. Returning to the unshifted arithmetic form is a separate step.

7.1. An explicit sufficient norm estimate

For a closed substrip $|\operatorname{Im}z|\le b$, a stronger but concrete estimate is $$\begin{equation} \int_\mathbb R|c_a\eta_a(t)-k_a(t)|e^{b|t|}\,dt\longrightarrow0.\tag{7}\end{equation}$$ Indeed, $|e^{izt}|\le e^{b|t|}$ on that substrip. Taking absolute values inside the Fourier integral bounds the left side of equation 6 by the integral in equation 7. This estimate supplies a direct map from an eigenfunction comparison to a holomorphic transform comparison.

If the difference is supported in $[-a,a]$, Cauchy-Schwarz gives the cruder sufficient bound $$\int_{-a}^{a}|c_a\eta_a-k_a|e^{b|t|}\,dt \le (2a)^{1/2}e^{ba}\|c_a\eta_a-k_a\|_{L^2}.$$ Therefore unweighted $L^2$ convergence with no rate is insufficient for this particular argument when $a\to\infty$. One can seek a sharper weighted estimate, a different transform bound, or a compactness argument with a normal-family hypothesis. What one cannot do is omit the growing weight while claiming uniform convergence on complex compact sets.

7.2. Rayleigh bounds and ground-state selection

Suppose an approximate vector has a small value of the Weil form. The ground-state Rayleigh quotient is no larger than that value, by the variational principle. This gives an upper bound for the lowest eigenvalue, whereas positivity requires a lower bound. A small trial value thus has the wrong inequality direction for proving positivity by itself.

Similarly, a small residual in an eigenvalue equation does not determine which eigenspace contains the approximate vector. Even after the intended eigenvalue has been correctly selected, a shrinking spectral gap can prevent residual convergence from controlling the vector.

For a self-adjoint operator with a simple ground eigenvalue $\lambda_0$ separated from the rest of its spectrum by $\delta>0$, the spectral theorem instead gives $$\|(1-P_0)v\|\le \delta^{-1}\|(A-\lambda_0)v\|.$$ The inequality follows by integrating $(t-\lambda_0)^2\ge\delta^2$ on the complement of the ground spectral projection. In a varying family, the useful condition is control of the residual divided by the gap, together with phase and normalization. Neither a vanishing residual alone nor a plausible trial eigenvalue supplies that condition.

7.3. The holomorphic zero-transfer obligation

Assume the transforms $c_a\widehat\eta_a$ are holomorphic on a connected open strip and have no zeros off the real axis. Suppose they converge uniformly on compact subsets to $\Xi$, which is not identically zero. Hurwitz’s theorem applied on each connected off-real component makes the limit either nowhere zero or identically zero there. The second possibility would make $\Xi$ vanish on an open subset of the connected strip, and hence on the whole strip by the identity theorem, contrary to the nonzero-limit hypothesis. Thus $\Xi$ has no zeros off the real axis in the strip. This is the precise complex-analytic transfer needed for the real-zero route.

The theorem requires holomorphic convergence, not agreement of sampled real values. Multiplication by a nonzero scalar does not change zeros, whereas a variable normalization must be holomorphic and nowhere zero on the domain. A meromorphic ratio requires restriction to domains avoiding its poles, and cannot be inserted into this argument as if it were an entire limit. These conditions become material when comparing alternative spectral determinant formulations.

The smaller residual for this route has two separate parts: the hypotheses ensuring the real-zero property for the actual ground-state transform throughout an exhausting family of intervals, and the normalized comparison in equation 6. General Hurwitz theory is already available. The missing theorem is the arithmetic and analytic identification of the family to which it is applied.

8.1. A disciplined meaning of the common obstruction

The common obstruction is not a newly proved universal object. It is the failure, so far, to construct a positive arithmetic realization together with an exact comparison to the Weil pairing. Each route makes a different part of that problem concrete. Geometry asks for the object, its primitive sign theorem, and its trace comparison. Finite positive models ask for a lower-defect bound on all tests. The ground-state route asks for selection and transform convergence. The spectral route asks for an actual zero realization in a positive space with the correct weight identity.

These are not automatically equivalent existence problems in their stated categories. Some packages may be strictly stronger than Weil positivity. Others, such as an existential Hilbert factorization of the exact form, are equivalent by construction. The comparison order and the source of each assumption must be included before making a minimality claim.

The user of a formal library should be able to locate the arithmetic obligation without unfolding an opaque proposition. In APP, the comparison fields are equalities or quantified eigenvector equations. No target theorem is declared as an axiom. The mathematical library verifies that these fields suffice, and the research notes record which concrete arithmetic instances remain absent.

9.1. Declarations versus theorem instances

A theorem parameterized by $Q$ and a comparison map proves a general implication for every valid instance. An arithmetic result requires a term of the relevant structure with $Q=Q_W$. The existence of the structure declaration is not evidence that such a term has been constructed. The distinction applies equally to a cohomology interface, a positive-kernel interface, and a convergence certificate.

The elementary nonzero examples in the library serve a narrower purpose. They establish that the interfaces have ordinary mathematical instances and that the transfer lemmas are not formulated with contradictory hypotheses. They do not test the arithmetic instance. A two-dimensional primitive form is an example of the mechanism, not a surrogate arithmetic surface.

The axiom audit records kernel dependencies of exported results. Standard logical axioms used by Lean and mathlib are distinguished from mathematical assumptions carried as explicit theorem parameters. A clean axiom audit says that the Lean proofs contain no newly postulated arithmetic theorem. It cannot establish that the user-facing identification of an abstract $Q$ with the classical Weil form is correct; that identification must be implemented and reviewed separately.

9.2. The next independently testable questions

For a geometric proposal, the first concrete questions concern the correspondence algebra and the exact arithmetic pairing. An independently proved negative intersection theorem is useful only after its primitive subspace and test-function map have been specified. At infinity, the chosen regularization must reproduce the completed-zeta term, including the subtraction at the identity.

For finite models, the first questions concern the finite form actually computed, the map from smooth tests to the model, and a one-sided comparison bound. It is often better to estimate a single scalar defect on a fixed test than to seek operator norm convergence on an entire ambient unit ball. This choice reduces the analytic burden without changing the all-test quantifier required at the end.

For the ground-state route, an informative calculation must distinguish the proxy, the exact ground state, and the gap above it. A rigorous bound on their normalized difference would connect two constructions that are presently related by evidence and conjecture. A small value of the quadratic form is not that bound. Nor does exact truncation of the prime sum identify the extremizing vector.

For the cohomological route, the first questions concern a nontrivial realization and a genuine weight identity. A predicate declaring a purity bound without referring to an action or eigenvalues does not answer them. The context audit shows why replacing such predicates by maps and identities is a substantive reformulation even when it does not yet prove the arithmetic theorem.

10.1. Consistent finite kernels

Suppose the label set is an increasing union $S=\bigcup_n S_n$ of finite sets, and each $K_n$ is a kernel on $S_n$. If $$K_{n+1}|_{S_n\times S_n}=K_n,$$ there is a well-defined kernel $K$ on $S$: choose an index containing both labels and use that value. The equality above makes the value independent of the choice. If each finite kernel is positive, every finite list lies in some $S_n$, and $K$ is positive.

This construction is exact descent of finite Gram data. It supplies the inner-product quotient and its completion by Theorem 2.3, applied to the free vector space on $S$. The construction is independent of RH as a general theorem. For an arithmetic application, however, one must prove that the resulting kernel is the kernel obtained from $B_W$ on the intended dictionary. Without that comparison, one has constructed a positive Hilbert space associated to other data.

A merely approximate consistency condition is more delicate. For each fixed pair of labels, a summable bound on successive entry differences makes the entries Cauchy. Positivity then passes to the resulting kernel by Proposition 10.2. This is an alternative intermediate structure: compatible finite Gram kernels can construct the positive target space rather than requiring a pre-existing common Hilbert space. The independent arithmetic comparison remains essential.

10.2. Direct limits of inner product spaces

The same idea can be expressed with finite-dimensional inner product spaces $H_n$ and isometric embeddings $u_n:H_n\to H_{n+1}$. A vector in the algebraic direct limit is represented by a pair $(n,x)$; two representatives agree if their images agree at a later stage. The inner product of two classes is computed after mapping both representatives into a common later space. Isometry makes the result independent of the stage.

This proposition describes a possible stronger intermediate structure for finite approximation programs. It includes actual transition maps and exact preservation of the pairing. A collection of finite self-adjoint matrices with no maps between their underlying spaces does not provide this system. Nor does convergence of a few eigenvalues specify transition maps preserving all cross terms.

10.3. Operators on the compatible limit

Suppose operators $J_n$ on $H_n$ commute with the transition maps, square to $-1$, and preserve the inner products. Then they define a linear isometry $J$ on the algebraic direct limit. In particular $\|Jx-Jy\|=\|x-y\|$, so $J$ is uniformly continuous and extends uniquely to the completion. The extension is linear and isometric, and satisfies $J^2=-1$ there by continuity. An action compatible at every stage and commuting with every $J_n$ also commutes with the limit operator, provided the action extends continuously.

This construction is a genuine descent mechanism for a polarisation already present at every stage. Its hypotheses are stronger than positivity of a scalar limit, because they prescribe compatible vectors and operators. That extra structure can be valuable: it controls the realized object, not just the sign of an arithmetic functional. It must nevertheless be supplied by the concrete approximation family. An isometry between successive abstract Hilbert spaces may exist without intertwining the required arithmetic maps or operators.

The direction of investigation depends on the available data. If exact isometric transitions are natural, the direct-limit construction is appropriate. If only scalar form comparisons are accessible, the one-sided residual of Proposition 6.1 asks for less. APP does not identify these routes as equivalent; it records a forgetful passage from a compatible positive system to positive scalar comparisons whenever the arithmetic realization maps commute.

A.1. Dropping the comparison

Take $V=\mathbb R$ with target $Q(x)=-x^2$ and a positive model $H=\mathbb R$ with $q(y)=y^2$. The model exists and is complete. No map $d$ can satisfy $Q(x)=q(dx)$ for every $x$, because the two sides have opposite signs at $x=1$. Thus existence of a positive model says nothing about the sign of an unrelated arithmetic expression.

A.2. Dropping injectivity

Take a nonzero vector space $V$ and the zero map into any positive inner product space. Its pulled-back quadratic form is identically zero and is nonnegative. It is not strictly positive on nonzero vectors. This is why a positivity certificate suffices for the Weil criterion but a positive definite metric on a specified source requires kernel information.

A.3. Dropping nonnegativity before quotienting

On $\mathbb R^2$ let $B((x_1,x_2),(y_1,y_2))=x_1y_1-x_2y_2$. The vector $(1,1)$ has zero diagonal value but pairs to $1$ with $(1,0)$. Its class cannot be killed while retaining this pairing. The null cone consists of two lines and is not a subspace. Quotienting the null cone is therefore not a general construction for indefinite forms.

A.4. Dropping semisimplicity

The shear of Example 4.3 has characteristic polynomial $(t-1)^2$. Its powers satisfy $S^n e_2=ne_1+e_2$, so they are unbounded in any norm on this finite-dimensional space. An invariant positive norm would keep $\|S^ne_2\|$ constant. This supplies a second proof of the obstruction and explains why a unit-circle eigenvalue condition does not control the representation.

A.5. Dropping continuity at a dense core

Define $q:\mathbb R\to\mathbb R$ by $q(x)=0$ for rational $x$ and $q(x)=-1$ otherwise. It is nonnegative on a dense subset and negative elsewhere. This function is not a quadratic form. It refutes the general continuity-free inference for arbitrary real-valued functions, not a theorem specifically asserting continuity of a finite-dimensional quadratic form. In applications to unbounded forms, the relevant continuity has to be proved in the form topology.

A.6. Dropping the gap scale

Example 7.1 has a positive spectral gap for every finite $n$, but no uniform lower bound. A claim that each approximation has a gap is weaker than a claim that the residual divided by that gap tends to zero. The distinction persists in infinite-dimensional problems and is especially relevant when a ground-state eigenvalue is numerically extremely small.

A.7. Dropping holomorphic control

For $n\ge1$, set $f_n(z)=1+z^2/n$ on the complex plane. The functions tend locally uniformly to the nonzero function $1$, while their zeros escape to infinity. This illustrates that local uniform convergence does not preserve the total number of zeros in the whole plane. Hurwitz applies on compact regions and transfers the absence of zeros there. A spectral determinant argument needs that local statement together with the specified arithmetic limit, rather than an informal matching of complete zero lists.