Circle Primal Equivalence

Abstract

The budgeted circle primal is the attained maximal normalized-Haar floor, equivalently the attained maximal coefficient in a positive residual decomposition.

Theorem 1.1 (The circle primal and residual programs have the same attained maximum).

$$\begin{array}{r}a>0,\forall i,\int \mathrm{apply}(Gamma,i)\mathrm{d}{m}_T=2a\mathrm{apply}(c,i),\\ {\mathcal{M}}_C\ne \varnothing \Rightarrow \exists \mu ,\alpha ,\mu \in {\mathcal{M}}_C\wedge \alpha m_T\le \mu ,\\ Lambda=2a\underset{\mu \in {\mathcal{M}}_C}{\max }\mathrm{hfloor}(\mu )=2a\alpha ,\\ \frac{Lambda}{2a}=\alpha =\underset{\alpha \ge 0}{\max }\left\{\alpha :\exists \sigma \ge 0,\alpha +\mathrm{mass}(\sigma )\le C,\forall i,2a\alpha \mathrm{apply}(c,i)+\int \mathrm{apply}(Gamma,i)\mathrm{d}\sigma =\mathrm{apply}(W,i)\right\}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/CirclePrimalEquivalence.circle_primal_equivalence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The continuous moment family is normalized so that its Haar integral is twice a times the designated center evaluation. The positivity assumption on a is required when dividing the primal identity by twice a; without it Lean’s totalized division would collapse that quotient to zero.

The existing full-circle attainment theorem supplies a feasible measure and a globally greatest dominated Haar coefficient. Taking the measure difference constructs a positive residual and gives the displayed budget and moment equations.

Conversely, adding any positive residual to the Haar component constructs a feasible measure dominating that coefficient. Thus the measure floor maximum and the explicit residual maximum have exactly the same feasible coefficients and the same attained optimizer.

References

• Truth anchor: D5/S3/Weil/Budget/CirclePrimalEquivalence.circle_primal_equivalence
• Dependency: D5/S3/Weil/Budget/FullCirclePrimalAttainment