Archimedean Jump Decomposition

Abstract

The completed-zeta Archimedean term is its mass contribution plus a nonnegative continuous translation energy.

Theorem 1.1 (Archimedean jump decomposition).

$$\forall f\in \mathcal{W},hArch:\mathrm{ArchimedeanConvergent}(\mathrm{convolutionSquare}\left(f\right))\Rightarrow \mathrm{archimedeanTerm}\left(\mathrm{convolutionSquare}\left(f\right),hArch\right)=\mathrm{archimedeanConstant}\cdot l2Mass\left(f\right)+\mathrm{archimedeanJumpEnergy}\left(f\right)\wedge 0\le \mathrm{archimedeanJumpEnergy}\left(f\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaGamma/ArchimedeanJumpDecomposition.archimedean_jump_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

The test function lies in the canonical carrier of even smooth compactly supported complex-valued functions. The displayed hArch premise is the exact integrability witness consumed by archimedeanTerm.

The jump density is exp(-x/2)/(1-exp(-2x)) on positive scales, and the jump energy integrates the squared displacement of f by translation against that density. The proof derives its Levy representation from the frozen digamma series and applies Fourier inversion and Tonelli.

The first public conjunct is the exact complex identity. The second public conjunct records positivity of the independently constructed continuous jump energy.

References

• Truth anchor: D5/S3/Weil/ZetaGamma/ArchimedeanJumpDecomposition.archimedean_jump_decomposition
• Dependency: D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity