Ground-State Zero Localization

Abstract

Vague residual-spectrum convergence forces eventual ground-transform zeros near each canonical zero ordinate.

Theorem 1.1 (Residual supports localize ground-transform zeros).

$$\begin{array}{r}\forall Z:\mathrm{ZeroData}(),n:\mathbb{N},\\ mu:\mathbb{N}\to \mathrm{Measure}(\mathbb{R}),F:\mathbb{N}\to \mathbb{R}\to \mathbb{C},\\ U:\mathrm{Set}(\mathbb{R}),\mathrm{IsOpen}(U)\wedge \mathrm{mem}(\mathrm{im}(\mathrm{zero}(Z,n)),U)\wedge \forall j\in \mathbb{N},\mathrm{support}(\mathrm{apply}(mu,j))\subseteq \left\{\mathrm{apply}(\mathrm{apply}(F,j),xi)=0\mid xi\in \mathbb{R}\right\}\wedge \\ \forall phi\in \mathbb{R}\to \mathbb{R},\mathrm{Continuous}(phi)\wedge \mathrm{HasCompactSupport}(phi)\wedge (\forall xi\in \mathbb{R},0\le \mathrm{apply}(phi,xi))\Rightarrow \mathrm{Tendsto}((j:\mathbb{N}\mapsto \mathrm{lintegral}(\mathrm{apply}(mu,j),(xi:\mathbb{R}\mapsto \mathrm{ofReal}(\mathrm{apply}(phi,xi))))),\mathrm{atTop}(),\mathrm{nhds}(\mathrm{lintegral}(\mathrm{zeroCountingMeasure}(Z),(xi:\mathbb{R}\mapsto \mathrm{ofReal}(\mathrm{apply}(phi,xi))))))\Rightarrow \\ \mathrm{EventuallyAtTop}((j:\mathbb{N}\mapsto \mathrm{Nonempty}(\mathrm{inter}(\left\{\mathrm{apply}(\mathrm{apply}(F,j),xi)=0\mid xi\in \mathbb{R}\right\},U)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/GroundStateZeroLocalization.ground_state_zero_localization (✓ std3). ∎

Source. Repository-derived.

Commentary.

The target is the canonical multiplicity-weighted real-ordinate measure constructed from ZeroData. Vague convergence is exposed publicly through convergence against every nonnegative compactly supported continuous real test.

A smooth bump supported in the chosen open neighborhood equals one at the selected ordinate. Its target integral is positive because that ordinate has positive canonical multiplicity.

Eventually the residual bump integral is positive, so the neighborhood meets the residual support. The public support inclusion then places a ground-transform zero there. The argument works for any open neighborhood, so a separate isolation premise is unnecessary.

References

• Truth anchor: D5/S3/Weil/Budget/GroundStateZeroLocalization.ground_state_zero_localization
• Dependency: D5/S3/Weil/ZetaAnalytic/RiemannPoissonDensity