Projective Primal Convergence

Abstract

Finite circle-moment primal optima converge to the full determining-family value by weak-star compactness and closedness.

Theorem 1.1 (Mass-bounded circle measures have a weak-star convergent subsequence).

$$\forall C\in \mathrm{NNReal}\left(\right),mu\in \mathrm{Nat}\left(\right)\to \mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right),\left(\forall n\in \mathrm{Nat}\left(\right),\mathrm{mass}\left(\mathrm{apply}\left(mu,n\right)\right)\le C\right)\Rightarrow \left(\exists muStar\in \mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right),phi\in \mathrm{Nat}\left(\right)\to \mathrm{Nat}\left(\right),\mathrm{mass}\left(muStar\right)\le C\wedge \left(\mathrm{StrictMono}\left(phi\right)\wedge \mathrm{Tendsto}\left((k\mapsto \mathrm{apply}\left(mu,\mathrm{apply}\left(phi,k\right)\right)),atTop,\mathrm{nhds}\left(muStar\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The proof extracts total masses in a compact interval and normalized probability measures in their compact metrizable weak topology, then reconstructs the finite-measure limit by continuous scalar multiplication.

Theorem 1.2 (The common primal budget box is weak-star compact).

$$\forall C\in \mathrm{NNReal}\left(\right),\mathrm{IsCompact}\left(\mathrm{commonFeasible}\left(C\right)\right)$$

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

Source. Repository-derived.

Commentary.

Both the Haar coefficient interval and the mass-bounded residual-measure set are compact, so their product is compact.

Theorem 1.3 (Finite-level primal feasible sets are weak-star closed).

$$\forall C\in \mathrm{NNReal}\left(\right),Gamma\in \mathrm{Nat}\left(\right)\to \mathrm{ContinuousMap}\left(\mathrm{Circle}\left(\right),\mathrm{Real}\left(\right)\right),w\in \mathrm{Nat}\left(\right)\to \mathrm{Real}\left(\right),N\in \mathrm{Nat}\left(\right),\mathrm{IsClosed}\left(\mathrm{levelFeasible}\left(C,Gamma,w,N\right)\right)$$

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

Source. Repository-derived.

Commentary.

The reconstruction mass cap and every finite moment equality are closed because mass and integration against continuous circle functions are continuous in the weak topology.

Theorem 1.4 (Every finite level has a primal optimizer).

$$\forall C\in \mathrm{NNReal}\left(\right),Gamma\in \mathrm{Nat}\left(\right)\to \mathrm{ContinuousMap}\left(\mathrm{Circle}\left(\right),\mathrm{Real}\left(\right)\right),w\in \mathrm{Nat}\left(\right)\to \mathrm{Real}\left(\right),N\in \mathrm{Nat}\left(\right),\mathrm{Nonempty}\left(\mathrm{fullFeasible}\left(C,Gamma,w\right)\right)\Rightarrow \left(\exists pStar\in \mathrm{Prod}\left(\mathrm{NNReal}\left(\right),\mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right)\right),\mathrm{Mem}\left(pStar,\mathrm{levelFeasible}\left(C,Gamma,w,N\right)\right)\wedge \left(\forall p\in \mathrm{Prod}\left(\mathrm{NNReal}\left(\right),\mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right)\right),\mathrm{Mem}\left(p,\mathrm{levelFeasible}\left(C,Gamma,w,N\right)\right)\Rightarrow \mathrm{objective}\left(p\right)\le \mathrm{objective}\left(pStar\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Full feasibility makes every finite level nonempty; the continuous Haar-floor coordinate therefore attains its maximum on the compact level set.

Theorem 1.5 (Circle primal frontiers decrease to the full frontier).

$$\forall C\in \mathrm{NNReal}\left(\right),Gamma\in \mathrm{Nat}\left(\right)\to \mathrm{ContinuousMap}\left(\mathrm{Circle}\left(\right),\mathrm{Real}\left(\right)\right),w\in \mathrm{Nat}\left(\right)\to \mathrm{Real}\left(\right),\mathrm{Nonempty}\left(\mathrm{fullFeasible}\left(C,Gamma,w\right)\right)\Rightarrow \left(\mathrm{Antitone}\left(\mathrm{levelFrontier}\left(C,Gamma,w\right)\right)\wedge \left(\mathrm{Tendsto}\left(\mathrm{levelFrontier}\left(C,Gamma,w\right),atTop,\mathrm{nhds}\left(\mathrm{fullFrontier}\left(C,Gamma,w\right)\right)\right)\wedge \left(\exists optimizer\in \mathrm{Nat}\left(\right)\to \mathrm{Prod}\left(\mathrm{NNReal}\left(\right),\mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right)\right),cluster\in \mathrm{Prod}\left(\mathrm{NNReal}\left(\right),\mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right)\right),phi\in \mathrm{Nat}\left(\right)\to \mathrm{Nat}\left(\right),\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{Mem}\left(\mathrm{apply}\left(optimizer,N\right),\mathrm{levelFeasible}\left(C,Gamma,w,N\right)\right)\right)\wedge \left(\mathrm{StrictMono}\left(phi\right)\wedge \left(\mathrm{Tendsto}\left((k\mapsto \mathrm{apply}\left(optimizer,\mathrm{apply}\left(phi,k\right)\right)),atTop,\mathrm{nhds}\left(cluster\right)\right)\wedge \left(\mathrm{Mem}\left(cluster,\mathrm{fullFeasible}\left(C,Gamma,w\right)\right)\wedge \mathrm{objective}\left(cluster\right)=\mathrm{fullFrontier}\left(C,Gamma,w\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Finite-level optimizers lie in one weak-star compact budget box. A convergent subsequence is extracted rather than supplied as a premise.

Closedness transfers the reconstruction budget and each fixed determining moment to the cluster, proving full feasibility. Continuity of the Haar-floor coordinate then identifies the antitone value limit with the full optimum.

References

• Truth anchor: D5/S3/Weil/Budget/ProjectivePrimalConvergence.commonFeasible_isCompact
• Truth anchor: D5/S3/Weil/Budget/ProjectivePrimalConvergence.levelFeasible_isClosed
• Truth anchor: D5/S3/Weil/Budget/ProjectivePrimalConvergence.level_optimizer_exists
• Truth anchor: D5/S3/Weil/Budget/ProjectivePrimalConvergence.mass_bounded_weakStar_subsequence
• Truth anchor: D5/S3/Weil/Budget/ProjectivePrimalConvergence.projective_primal_convergence
• Dependency: D5/S3/Weil/Budget/FullCirclePrimalAttainment