Finite Atomic Budgeted Completion

Abstract

An active complementary gap forces an even optimizer to be finite atomic.

Theorem 1.1 (Active budget gives a finite symmetric atomic completion).

$$\forall a\in \mathrm{Real}\left(\right),theta\in \mathrm{Real}\left(\right),lambda\in \mathrm{NNReal}\left(\right),phi\in \mathrm{WeilTestFunction}\left(\right),residual\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),completion\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\left(0<a\wedge \left(0<theta\wedge \left(\left(\forall x\in \mathrm{Real}\left(\right),\mathrm{conj}\left(phi\left(x\right)\right)=phi\left(x\right)\right)\wedge \left(\left(\forall xi\in \mathrm{Real}\left(\right),0\le \mathrm{realPart}\left(\mathrm{fourierLaplace}\left(phi,xi\right)\right)+\frac{theta}{(xi{)}^2+(a{)}^2}\right)\wedge \left(\mathrm{Integrable}\left((xi:\mathrm{Real}\left(\right)\mapsto \mathrm{realPart}\left(\mathrm{fourierLaplace}\left(phi,xi\right)\right)+\frac{theta}{(xi{)}^2+(a{)}^2}),residual\right)\wedge \left(\mathrm{Integrable}\left((xi:\mathrm{Real}\left(\right)\mapsto \frac{1}{(xi{)}^2+(a{)}^2}),residual\right)\wedge \left(\mathrm{integral}\left(xi,\mathrm{Real}\left(\right),\mathrm{realPart}\left(\mathrm{fourierLaplace}\left(phi,xi\right)\right)+\frac{theta}{(xi{)}^2+(a{)}^2},residual\right)=0\wedge \left(\mathrm{map}\left((xi:\mathrm{Real}\left(\right)\mapsto -xi),residual\right)=residual\wedge completion=\mathrm{smul}\left(\mathrm{ofReal}\left(\frac{\mathrm{toReal}\left(lambda\right)}{2\cdot \mathrm{pi}\left(\right)}\right),\mathrm{volume}\left(\mathrm{Real}\left(\right)\right)\right)+residual\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists I\in Type,finiteI\in \mathrm{Fintype}\left(I\right),point\in I\to \mathrm{Real}\left(\right),weight\in I\to \mathrm{ENNReal}\left(\right),weightZero\in \mathrm{ENNReal}\left(\right),\left(\forall r\in I,weight\left(r\right)\ne \mathrm{infinity}\left(\right)\right)\wedge \left(weightZero\ne \mathrm{infinity}\left(\right)\wedge \left(\left(\forall r\in I,\left((point\left(r\right){)}^2+(a{)}^2\right)\cdot \mathrm{fourierLaplace}\left(phi,point\left(r\right)\right)+theta=0\wedge \left((-point\left(r\right){)}^2+(a{)}^2\right)\cdot \mathrm{fourierLaplace}\left(phi,-point\left(r\right)\right)+theta=0\right)\wedge completion=\mathrm{smul}\left(\mathrm{ofReal}\left(\frac{\mathrm{toReal}\left(lambda\right)}{2\cdot \mathrm{pi}\left(\right)}\right),\mathrm{volume}\left(\mathrm{Real}\left(\right)\right)\right)+\mathrm{sum}\left(r,I,\mathrm{smul}\left(weight\left(r\right),\mathrm{dirac}\left(point\left(r\right)\right)+\mathrm{dirac}\left(-point\left(r\right)\right)\right)\right)+\mathrm{smul}\left(weightZero,\mathrm{dirac}\left(0\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Complementary contact support places the residual measure on the real zeros of the canonical entire contact function. Positive pressure and Schwartz decay confine those zeros to a compact interval.

Analytic isolation makes the real contact set finite. Evenness then splits every singleton mass equally between its positive and negative Dirac representatives, including the possible zero atom.

References

• Truth anchor: D5/S3/Weil/TestFunctions/FiniteAtomicBudgetedCompletion.finite_atomic_budgeted_completion
• Dependency: D5/S3/Weil/TestFunctions/ActiveFiniteContactCompletion
• Dependency: D5/S3/Weil/TestFunctions/ComplementaryContactSupport