Complementary Contact Support

Abstract

A zero complementary gap localizes residual support on entire contact zeros.

Theorem 1.1 (Complementary contact support).

$$\forall a\in \mathrm{Real}\left(\right),theta\in \mathrm{Real}\left(\right),phi\in \mathrm{WeilTestFunction}\left(\right),mu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\left(\left(\left(\left(\left(0<a\wedge 0\le theta\right)\wedge \left(\forall x\in \mathrm{Real}\left(\right),\mathrm{conj}\left(phi\left(x\right)\right)=phi\left(x\right)\right)\right)\wedge \left(\forall xi\in \mathrm{Real}\left(\right),0\le \mathrm{realPart}\left(\mathrm{fourierLaplace}\left(phi,xi\right)\right)+\frac{theta}{x{i}^2+a^2}\right)\right)\wedge \mathrm{Integrable}\left((xi:\mathrm{Real}\left(\right)\mapsto \mathrm{realPart}\left(\mathrm{fourierLaplace}\left(phi,xi\right)\right)+\frac{theta}{x{i}^2+a^2}),mu\right)\right)\wedge \mathrm{integral}\left(xi,\mathrm{Real}\left(\right),\mathrm{realPart}\left(\mathrm{fourierLaplace}\left(phi,xi\right)\right)+\frac{theta}{x{i}^2+a^2},mu\right)=0\right)\Rightarrow \mathrm{let}S=(xi:\mathrm{Real}\left(\right)\mapsto \mathrm{realPart}\left(\mathrm{fourierLaplace}\left(phi,xi\right)\right)+\frac{theta}{x{i}^2+a^2});\mathrm{let}G=(z:\mathrm{Complex}\left(\right)\mapsto \left(z^2+a^2\right)\cdot \mathrm{fourierLaplace}\left(phi,z\right)+theta);\left(\left(\mathrm{support}\left(mu\right)\subseteq \left\{S\left(xi\right)=0\mid xi\in \mathrm{Real}\left(\right)\right\}\wedge \mathrm{Differentiable}\left(\mathrm{Complex}\left(\right),G\right)\right)\wedge \left(\exists C\in \mathrm{Real}\left(\right),tau\in \mathrm{Real}\left(\right),\left(0\le C\wedge 0\le tau\right)\wedge \left(\forall z\in \mathrm{Complex}\left(\right),\mathrm{norm}\left(G\left(z\right)\right)\le C\cdot \exp \left(tau\cdot \mathrm{norm}\left(z\right)\right)\right)\right)\right)\wedge \mathrm{support}\left(mu\right)\subseteq \left\{G\left(xi\right)=0\mid xi\in \mathrm{Real}\left(\right)\right\}$$

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

Source. Repository-derived.

Commentary.

The contact gap is constructed from the canonical Fourier-Laplace transform and the positive resolvent denominator. Pointwise nonnegativity and a zero integral force it to vanish throughout the residual support.

Clearing the denominator constructs the complex contact function. Compact support makes the transform entire and supplies an explicit finite exponential bound after multiplication by the quadratic factor.

Reality of the even test makes the transform real on the real axis, so the first support localization transfers to the real zeros of the entire contact function.

References

• Truth anchor: D5/S3/Weil/TestFunctions/ComplementaryContactSupport.complementary_contact_support