Finite Stieltjes Operator Realization
Abstract
Finite positive atomic Stieltjes moments have positive Hankel truncations and an explicit positive diagonal operator realization.
Theorem 1.1 (Positive atomic moments generate Hankel and operator positivity).
Proof. Machine-checked in Lean as D5/S3/Constants/FiniteStieltjesOperatorRealization.finite_stieltjes_operator_realization (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let I be finite, and let x and w be nonnegative real node and weight families. Define mu at n as the finite sum of w(i) times x(i) to the n-th power, and define the order-k Hankel matrix by the moment at p+q. Every such truncation is positive semidefinite; its zero coefficient vector explicitly attains equality.
On the real Euclidean space indexed by I, multiplication by x is an explicit diagonal nonnegative operator U. The vector v has coordinates sqrt(w(i)). Every moment is the inner product of U to the n-th power applied to v with v, and the zero state attains equality in operator nonnegativity.
The proof identifies each Hankel truncation with the Gram matrix of the vectors sqrt(w(i)) x(i)^p and applies Mathlib’s Gram positivity theorem. It formalizes the unconditional finite positive-atomic core only; no Riemann-hypothesis or square-folded-xi representation is assumed or claimed.
References
- Truth anchor:
D5/S3/Constants/FiniteStieltjesOperatorRealization.finite_stieltjes_operator_realization