Contact-Zero Localization

Abstract

Vague convergence of finite contact spectra localizes an indexed positive atom near every enumerated zero ordinate.

Theorem 1.1 (Finite contact spectra localize positive atoms).

$$\begin{array}{r}\forall Z:\mathrm{ZeroData}(),n0:\mathbb{N},\\ M:\mathbb{N}\to \mathbb{N},G:\mathbb{N}\to \mathbb{R}\to \mathbb{C},\\ tau:\forall n:\mathbb{N},\mathrm{Fin}(\mathrm{apply}(M,n))\to \mathrm{Subtype}(xi:\mathbb{R},\mathrm{apply}(\mathrm{apply}(G,n),xi)=0),\\ c:\forall n:\mathbb{N},\mathrm{Fin}(\mathrm{apply}(M,n))\to ENNReal,\\ U:\mathrm{Set}(\mathbb{R}),\mathrm{IsOpen}(U)\wedge \mathrm{mem}(\mathrm{im}(\mathrm{zero}(Z,n0)),U)\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}((n:\mathbb{N}\mapsto \mathrm{lintegral}(\mathrm{sumMeasure}((j:\mathrm{Fin}(\mathrm{apply}(M,n))\mapsto \mathrm{apply}(\mathrm{apply}(c,n),j)\cdot \mathrm{dirac}(\mathrm{val}(\mathrm{apply}(\mathrm{apply}(tau,n),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}((n:\mathbb{N}\mapsto \exists j\in \mathrm{Fin}(\mathrm{apply}(M,n)),0<\mathrm{apply}(\mathrm{apply}(c,n),j)\wedge \mathrm{mem}(\mathrm{val}(\mathrm{apply}(\mathrm{apply}(tau,n),j)),U))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaAnalytic/ContactZeroLocalization.contact_zero_localization (✓ std3). ∎

Source. Repository-derived.

Commentary.

The signed contact atoms are indexed directly. Their subtype records the transform-zero equation, and the residual measure is the corresponding finite positive Dirac sum.

A compactly supported smooth bump at the selected ordinate has positive integral against the multiplicity-weighted target measure. Vague convergence makes its residual integral eventually positive.

Expanding that residual integral as a finite sum produces an indexed positive-weight atom in the bump support and hence in the chosen open neighborhood. No separate isolation premise is needed.

References

• Truth anchor: D5/S3/Weil/ZetaAnalytic/ContactZeroLocalization.contact_zero_localization
• Dependency: D5/S3/Weil/Budget/GroundStateZeroLocalization