Projective Strong Duality

Abstract

Finite attained dual minima converge exactly to the full primal value.

Theorem 1.1 (The finite strong-duality tower has no projective gap).

$$\begin{array}{r}\forall Point:\mathrm{Type},Test:\mathbb{N}\to \mathrm{Type},\\ Gamma:\mathrm{DependentMap}(N:\mathbb{N},Test(N),Point\to \mathbb{R}),\\ e0:\mathrm{DependentMap}(N:\mathbb{N},Test(N),\mathbb{R}),W:\mathrm{DependentMap}(N:\mathbb{N},Test(N),\mathbb{R}),\\ a:\mathbb{R},C:\mathbb{R},Lambda:\mathbb{N}\to \mathbb{R},Lambd{a}_{\infty }:\mathbb{R},\\ \mathrm{let}(D:\mathbb{N}\to \mathrm{Set}(\mathbb{R}),\forall N:\mathbb{N},D_N=\{x\in \mathbb{R}\mid \exists phi:Test(N),\exists theta:\mathbb{R},0\le theta\wedge (\forall z:Point,0\le Gamma(N,phi,z)+theta)\wedge 2a\le 2ae0(N,phi)+theta\wedge x=W(N,phi)+thetaC\})\\ (\forall N:\mathbb{N},0\le Lambda(N))\wedge \mathrm{Antitone}(Lambda)\wedge \\ \mathrm{Tendsto}(Lambda,\mathrm{atTop}(\mathbb{N}),\mathrm{nhds}(Lambd{a}_{\infty }))\wedge (\forall N:\mathbb{N},\mathrm{IsLeast}(D_N,Lambda(N)))\\ \Rightarrow Lambd{a}_{\infty }={\inf }_{N\in \mathbb{N}}\mathrm{sInf}(D_N)\wedge \\ \forall N:\mathbb{N},\exists phi:Test(N),\exists theta:\mathbb{R},0\le theta\wedge (\forall z:Point,0\le Gamma(N,phi,z)+theta)\wedge 2a\le 2ae0(N,phi)+theta\wedge \mathrm{sInf}(D_N)=W(N,phi)+thetaC.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/ProjectiveStrongDuality.projective_strong_duality (✓ std3). ∎

Source. Repository-derived.

Commentary.

The point carrier and the dependent family of finite test spaces are public. The circle slack, evaluation at zero, pairing, budget, finite primal values, and full primal value are all supplied on those carriers.

Every finite dual-value set is constructed from a nonnegative pressure, the pointwise circle-slack inequality, the Haar-floor inequality, and the affine pairing-plus-budget objective. Finite strong duality states that the corresponding primal value is its least element.

Nonnegativity bounds the decreasing primal tower below. Pinned Mathlib monotone convergence identifies its infimum with the supplied full limit, while each finite least-element certificate rewrites that infimum as the attained finite dual minimum.

The public conclusion also returns a feasible minimizer at every finite stage. It makes no assertion that one test and pressure pair attains the full infinite-dimensional dual.

References

• Truth anchor: D5/S3/Observer/Budget/ProjectiveStrongDuality.projective_strong_duality