Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Convex KKT conditions certify a global minimum and an outward normal

Statement

Let m≥0 be an integer. Let U⊆Rn be open and convex, and suppose the objective f:U→R and inequalities gi:U→R (1≤i≤m) are differentiable and convex. Let the equalities be Ax=b and define the feasible set C={x∈U:Ax=b, gi(x)≤0 (1≤i≤m)}. If a feasible tuple (x∗,ν,λ) satisfies the KKT conditions with λ≥0, then x∗ is a global minimizer over the feasible set C. Moreover, −∇f(x∗)∈NC(x∗), where the normal cone has the convention of Scaled KKT residual and convex normal cone.

Facts & Assumptions

Given: The convex program, feasible KKT tuple, and normal-cone definition.

[F1]

For differentiable convex φ on an open convex set, φ(y)≥φ(x)+∇φ(x)T(y−x) (Differentiable convex functions are characterized by the gradient inequality).

[F2]

The normal cone is NC(x)={v:⟨v,y−x⟩≤0 for every y∈C} (Scaled KKT residual and convex normal cone).

Proof

1.1givenF1algebra

Fix any feasible y and put d=y−x∗. Then Ad=0. KKT stationarity gives ∇f(x∗)Td=−∑iλi∇gi(x∗)Td. If λi=0 its term is zero. If λi>0, complementarity gives gi(x∗)=0, and [F1] applied to gi gives ∇gi(x∗)Td≤gi(y)≤0. Hence ∇f(x∗)Td≥0.

2.1step 1.1F1F2algebra∎

Applying [F1] to f yields f(y)≥f(x∗)+∇f(x∗)Td≥f(x∗). Since y was arbitrary, x∗ is globally minimizing. Step 1.1 also gives ⟨−∇f(x∗),y−x∗⟩≤0 for every feasible y, which is exactly −∇f(x∗)∈NC(x∗) by [F2].

Depends on

Used by

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources