Finite Zero Gram Hierarchy
Abstract
A finite positive-weighted zero-resolvent kernel is a Gram matrix whose determinant is one exact nonnegative Cauchy–Binet contribution.
Theorem 1.1 (Finite zero-resolvent Gram determinants are nonnegative).
Proof. Machine-checked in Lean as D5/S3/Weil/FiniteZeroGramHierarchy.finite_zero_gram_hierarchy (✓ std3). ∎
Source. Repository-derived.
Commentary.
The sampling nodes lie in the open upper half-plane, so no real ordinate can make a resolvent denominator zero. Nonnegative real weights define the diagonal middle factor of the Gram matrix.
Mathlib’s positive-semidefinite diagonal and congruence lemmas prove positivity. Multiplicativity of the determinant, the diagonal determinant formula, and conjugate-transpose compatibility give the displayed weighted determinant square.
The source’s infinite subset expansion is not asserted because it omits enumeration and convergence hypotheses. The reverse implication to the Riemann hypothesis is also omitted: a Gram construction is positive for every real ordinate family and therefore cannot locate zeta zeros on the critical line.
A companion Lean theorem shows sharpness at determinant zero using two distinct ordinates, positive weights, and a repeated upper-half-plane sampling node.
References
- Truth anchor:
D5/S3/Weil/FiniteZeroGramHierarchy.finite_zero_gram_hierarchy