Stationarity and complementary slackness extraction

Proved

VectorSpaceOpt.kkt_complementary_slackness

by wenxinzhang · Aug 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complementary-slacknessdual-positivekktstationarity

Let a cone-positive continuous functional z₀ accompany a feasible constraint value xConstraint. Suppose the separating inequality

0 ≤ f'h + z₀(xConstraint+G'h)

holds for every direction h in the decision space. Then the part linear in h must vanish, and the remaining constant is forced to vanish by feasibility and positivity. Consequently, f' + z₀ ∘ G' = 0 and z₀(xConstraint) = 0. This theorem isolates the sign-sensitive algebra at the end of p. 250. It is a small but valuable reusable interface: geometric separation need only produce the universal affine inequality, after which stationarity and complementary slackness follow without any further topology or differentiability.

Preamble

import Definitions.Def_VectorSpaceOpt_cone_optimization

Formal statement

namespace VectorSpaceOpt

/-- The stationarity and complementary-slackness extraction on p. 250. -/
theorem kkt_complementary_slackness
    {X Z : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z]
    (P : ConvexCone ℝ Z) (xConstraint : Z)
    (f' : X →L[ℝ] ℝ) (G' : X →L[ℝ] Z) (z₀ : Z →L[ℝ] ℝ)
    (hz : dualPositive P z₀) (hfeas : coneLE P xConstraint 0)
    (hsep : ∀ h : X, 0 ≤ f' h + z₀ (xConstraint + G' h)) :
    f' + z₀.comp G' = 0 ∧ z₀ xConstraint = 0 := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.4, final extraction in the proof of Theorem 1, printed p. 250 (physical PDF p. 268). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5

Let $X,Z$ be real normed spaces, $P$ a convex cone in $Z$ , $c∈Z$ , $f':X→ℝ$ and $G':X→Z$ continuous real-linear maps, and $z₀:Z→ℝ$ a continuous real-linear functional. Assume $z₀$ is nonnegative on $P$ , assume $c≤_{P}0$ —that is, $-c∈P$ —and assume that for every $h∈X$ , $0≤f'h+z₀(c+G'h)$ . Then $f'+z₀∘G'$ is the zero functional on $X$ and $z₀(c)=0$ . The separator inequality includes $h=0$ and both arbitrary $h$ and its negative; there are no differentiability, completeness, interior, or regularity hypotheses in this theorem.

Human review

Endorsed by Shuze Chen · Aug 26, 2026
Endorsed by wenxinzhang · Aug 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph