Toeplitz Contact Support

Abstract

A contact eigenvector localizes a Toeplitz residual on finitely many polynomial zeros.

Theorem 1.1 (Toeplitz contact support).

$$\forall N\in \mathbb{N},mu\in \mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right),sigma\in \mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right),alpha\in \mathrm{NonnegativeReal}\left(\right),v\in \mathrm{Fin}\left(N+1\right)\to \mathbb{C},\left(\left(\left(\left(\left(mu=\mathrm{smul}\left(alpha,\mathrm{normalizedCircleHaar}\left(\right)\right)+sigma\wedge \mathrm{let}m=(ell:\mathbb{Z}\mapsto \mathrm{integral}\left(z,\mathrm{Circle}\left(\right),\mathrm{zpow}\left(z,\mathrm{neg}\left(ell\right)\right),mu\right))\right)\wedge \mathrm{let}T=\mathrm{Matrix}\left((j,k\in \mathrm{Fin}\left(N+1\right)\mapsto m\left(j-k\right))\right)\right)\wedge \mathrm{let}q=\mathrm{sum}\left(j,\mathrm{Fin}\left(N+1\right),\mathrm{monomial}\left(v\left(j\right),j\right)\right)\right)\wedge \mathrm{dotProduct}\left(\mathrm{star}\left(v\right),v\right)=1\right)\wedge \mathrm{mulVec}\left(T,v\right)=\mathrm{smul}\left(\mathrm{toComplex}\left(alpha\right),v\right)\right)\Rightarrow \left(\left(\mathrm{support}\left(sigma\right)\subseteq \left\{\mathrm{eval}\left(q,z\right)=0\mid z\in \mathrm{Circle}\left(\right)\right\}\wedge \mathrm{natDegree}\left(q\right)\le N\right)\wedge \left(\exists M\in \mathbb{N},point\in \mathrm{Fin}\left(M\right)\to \mathrm{Circle}\left(\right),weight\in \mathrm{Fin}\left(M\right)\to \mathrm{ExtendedNonnegativeReal}\left(\right),\left(\left(\left(M\le \mathrm{natDegree}\left(q\right)\wedge \left(\forall r\in \mathrm{Fin}\left(M\right),\mathrm{eval}\left(q,point\left(r\right)\right)=0\right)\right)\wedge \left(\forall r\in \mathrm{Fin}\left(M\right),weight\left(r\right)\ne \mathrm{infinity}\left(\right)\right)\right)\wedge sigma=\mathrm{sum}\left(r,\mathrm{Fin}\left(M\right),\mathrm{smul}\left(weight\left(r\right),\mathrm{dirac}\left(point\left(r\right)\right)\right)\right)\right)\wedge mu=\mathrm{smul}\left(alpha,\mathrm{normalizedCircleHaar}\left(\right)\right)+\mathrm{sum}\left(r,\mathrm{Fin}\left(M\right),\mathrm{smul}\left(weight\left(r\right),\mathrm{dirac}\left(point\left(r\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/ToeplitzContactSupport.toeplitz_contact_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Fourier moments, Toeplitz matrix, and analytic contact polynomial are constructed from the supplied completion measure and coefficient vector.

Normalized-Haar monomial orthogonality turns the contact eigenvector equation into a zero residual quadratic integral. The residual support is therefore contained in the contact zero set.

The polynomial is nonzero because the coefficient vector is unit. Its circle roots are finite, have cardinality at most its degree, and enumerate both the residual Dirac sum and the full optimizer decomposition.

References

• Truth anchor: D5/S3/Weil/TestFunctions/ToeplitzContactSupport.toeplitz_contact_support
• Dependency: D5/S3/Weil/Budget/FullCirclePrimalAttainment