Arithmetic State Positivity

Abstract

The normalized zeta state induces a positive arithmetic seminorm and its Hilbert completion.

Theorem 1.1 (The arithmetic state is positive and completes to a Hilbert space).

$$\forall s\in \mathbb{R},F\in C_b(\mathbb{N},\mathbb{C}),1<s\Rightarrow \left(0\le \frac{1}{\Re (\mathrm{riemannZeta}\left(s\right))}\times \sum _{n\in \mathbb{N}}{\Vert F\left(n\right)\Vert }^2\times n^{-s}\wedge \left(\mathrm{arithmeticState}\left(s,\overline{F}\times F\right)=\mathrm{ofReal}\left(\frac{1}{\Re (\mathrm{riemannZeta}\left(s\right))}\times \sum _{n\in \mathbb{N}}{\Vert F\left(n\right)\Vert }^2\times n^{-s}\right)\wedge \left(\mathrm{ofReal}\left({\Vert \mathrm{toArithmeticPreHilbert}\left(s,F\right)\Vert }^2\right)=\mathrm{arithmeticState}\left(s,\overline{F}\times F\right)\wedge \left(\left(\mathrm{CompletionCoe}\left(\mathrm{toArithmeticPreHilbert}\left(s,F\right)\right)=0\iff \Vert \mathrm{toArithmeticPreHilbert}\left(s,F\right)\Vert =0\right)\wedge \left(\mathrm{DenseRange}\left((x:\mathrm{ArithmeticPreHilbert}\left(s\right)\mapsto \mathrm{CompletionCoe}\left(x\right))\right)\wedge \left(\mathrm{CompleteSpace}\left(\mathrm{ArithmeticHilbertSpace}\left(s\right)\right)\wedge \left(\forall x\in \mathrm{ArithmeticHilbertSpace}\left(s\right),{\Vert x\Vert }^2=\Re (\mathrm{inner}\left(\mathbb{C},x,x\right))\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ZetaObservation/ArithmeticStatePositivity.arithmetic_positivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

A bounded complex observable is integrated against the repository’s normalized zeta distribution at a real parameter above one. The zeroth natural-number term has zero mass, so the displayed natural sum is the source sum over positive integers.

The first three conjuncts state positivity, the exact normalized weighted integer expansion, and the induced seminorm-square identity. The normalized series is nonnegative, the full complex state value equals its real coercion, and the real seminorm square equals that complex state value after coercion.

The remaining conjuncts expose the canonical separation and completion: an observable maps to zero exactly when its seminorm vanishes, the canonical range is dense, the completion is complete, and its norm square is its self inner product.

The construction uses the existing zeta distribution together with the pinned library’s pre-inner-product core and uniform completion. No conjectural positivity principle is assumed.

References

• Truth anchor: D5/S3/Analytic/ZetaObservation/ArithmeticStatePositivity.arithmetic_positivity