Active Finite-Contact Completion

Abstract

Positive active pressure produces an exact finite-contact completion.

Theorem 1.1 (Active pressure gives a finite atomic completion).

$$\forall d\in \mathrm{Nat}\left(\right),a\in \mathrm{Real}\left(\right),theta\in \mathrm{Real}\left(\right),alpha\in \mathrm{NNReal}\left(\right),phi\in \mathrm{WeilTestFunction}\left(\right),observer\in \mathrm{Fin}\left(d\right)\to \mathrm{WeilTestFunction}\left(\right),sigma\in \mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right),\left(0<a\wedge \left(0<theta\wedge \left(\left(\forall i\in \mathrm{Fin}\left(d\right),x\in \mathrm{Real}\left(\right),\mathrm{conj}\left(observer\left(i\right)\left(x\right)\right)=observer\left(i\right)\left(x\right)\right)\wedge \mathrm{support}\left(sigma\right)\subseteq \left\{\mathrm{cayleyMomentFunction}\left(a,phi,z\right)+theta=0\mid z\in \mathrm{Circle}\left(\right)\right\}\right)\right)\right)\Rightarrow \left(\exists I\in Type,finiteI\in \mathrm{Fintype}\left(I\right),point\in I\to \mathrm{Circle}\left(\right),weight\in I\to \mathrm{Real}\left(\right),muStar\in \mathrm{Measure}\left(\mathrm{Circle}\left(\right)\right),\mathrm{card}\left(I\right)\le d+1\wedge \left(\left(\forall r\in I,0<weight\left(r\right)\right)\wedge \left(\left(\forall r\in I,\mathrm{cayleyMomentFunction}\left(a,phi,point\left(r\right)\right)+theta=0\right)\wedge \left(\left(\forall r\in I,\mathrm{cayleyMomentFunction}\left(a,phi,\mathrm{inv}\left(point\left(r\right)\right)\right)+theta=0\right)\wedge \left(\mathrm{sum}\left(r,I,weight\left(r\right)\right)=\mathrm{measureReal}\left(sigma,\mathrm{univ}\left(\mathrm{Circle}\left(\right)\right)\right)\wedge \left(muStar=\mathrm{smul}\left(alpha,\mathrm{normalizedCircleHaar}\left(\right)\right)+\mathrm{sum}\left(r,I,\mathrm{smul}\left(\mathrm{ofReal}\left(weight\left(r\right)\right),\mathrm{dirac}\left(point\left(r\right)\right)\right)\right)\wedge \left(\forall i\in \mathrm{Fin}\left(d\right),\mathrm{integral}\left(z,\mathrm{Circle}\left(\right),\mathrm{cayleyMomentFunction}\left(a,observer\left(i\right),z\right),\mathrm{sum}\left(r,I,\mathrm{smul}\left(\mathrm{ofReal}\left(weight\left(r\right)\right),\mathrm{dirac}\left(point\left(r\right)\right)\right)\right)\right)=\mathrm{integral}\left(z,\mathrm{Circle}\left(\right),\mathrm{cayleyMomentFunction}\left(a,observer\left(i\right),z\right),sigma\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

A finite residual supported on the active KKT contact set can be replaced by positive contact atoms while retaining its mass and every moment in the supplied real observer family.

The completion keeps the same nonnegative Haar coefficient, uses at most d plus one atoms, and every chosen contact has an inverse contact, so the support is indexed by at most d plus one conjugate contact orbits.

References

• Truth anchor: D5/S3/Weil/TestFunctions/ActiveFiniteContactCompletion.active_finite_contact_completion
• Dependency: D5/S3/Weil/TestFunctions/CayleyMomentTransport