Rational Contact Support

Abstract

A Gram-kernel contact polynomial vanishes on the positive residual support of a rational unit-circle completion.

Theorem 1.1 (Kernel contact polynomials vanish on residual support).

$$\begin{array}{r}\forall n:\mathbb{N},p:\mathrm{Fin}(n)\to \mathrm{Polynomial}(\mathbb{C}),\\ D:\mathrm{Polynomial}(\mathbb{C}),hD:\forall z\in Circle,\mathrm{eval}(D,z)\ne 0,\\ \alpha :{\mathbb{R}}_{\ge 0},tau:\mathrm{FiniteMeasure}(Circle),\\ \mathrm{let}(\psi :Circle\to \left(\mathrm{Fin}(n)\to \mathbb{C}\right),\forall z:Circle,i:\mathrm{Fin}(n),\psi (z)(i)=\frac{\mathrm{eval}(p(i),z)}{\mathrm{eval}(D,z)}muStar:\mathrm{FiniteMeasure}(Circle)=\alpha \cdot \mathrm{normalizedCircleHaar}()+tauG:\mathrm{Matrix}(\mathrm{Fin}(n),\mathrm{Fin}(n),\mathbb{C}),\forall i:\mathrm{Fin}(n),j:\mathrm{Fin}(n),G_{i,j}=\mathrm{integral}(muStar,(z:Circle\mapsto \psi (z)(i){\psi (z)(j)}^{\ast }))B:\mathrm{Matrix}(\mathrm{Fin}(n),\mathrm{Fin}(n),\mathbb{C}),\forall i:\mathrm{Fin}(n),j:\mathrm{Fin}(n),B_{i,j}=\mathrm{integral}(\mathrm{normalizedCircleHaar}(),(z:Circle\mapsto \psi (z)(i){\psi (z)(j)}^{\ast }))P:\left(\mathrm{Fin}(n)\to \mathbb{C}\right)\to \mathrm{Polynomial}(\mathbb{C}),\forall c:\mathrm{Fin}(n)\to \mathbb{C},P(c)=\sum _{i\in \mathrm{Fin}(n)}{c(i)}^{\ast }\cdot p(i))\\ \forall c:\mathrm{Fin}(n)\to \mathbb{C},\mathrm{mulVec}(G-\alpha \cdot B,c)=0\Rightarrow \\ \mathrm{support}(muStar-\alpha \cdot \mathrm{normalizedCircleHaar}())\subseteq \left\{\mathrm{eval}(P(c),z)=0\mid z\in Circle\right\}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Tomography/RationalContactSupport.rational_contact_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement constructs every source object. Polynomial numerators and a denominator without unit-circle zeros determine the rational feature vector, while normalized Haar and an arbitrary finite positive residual determine the completion.

Both complex Gram matrices are displayed entrywise as integrals on the exact unit-circle carrier. The contact polynomial is the conjugate-coefficient combination of the supplied polynomial numerators.

The completion Gram matrix splits into its normalized-Haar floor and residual Gram matrix. A kernel vector therefore has zero residual quadratic form, hence its squared contact function vanishes almost everywhere.

Polynomial evaluation is continuous, so its zero set is closed. The almost-everywhere vanishing statement therefore places the full support of the completion residual inside that zero set.

References

• Truth anchor: D5/S3/Observer/Tomography/RationalContactSupport.rational_contact_support
• Dependency: D5/S3/Weil/Budget/FullCirclePrimalAttainment