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.

Second-order necessity on the critical cone under LICQ

Statement

For the C2 program of Inequality constrained programs, tangent cones, constraint qualifications, and KKT, let x∗ be a local minimizer satisfying LICQ, and let (ν,λ) be its KKT multipliers. Then

dT∇xx2L(x∗,ν,λ)d≥0for every d∈K(x∗,ν,λ).

Facts & Assumptions

Given: The C2 program, local minimizer x∗, LICQ, and a critical direction d.

[F1]

LICQ gives existence of KKT multipliers at a local minimizer (LICQ implies MFCQ and makes KKT multipliers unique).

[F2]

A critical direction lies in the linearized cone and satisfies Dgi(x∗)d=0 for every active i with λi>0 (Critical directions are tangent to every positively weighted active inequality).

[F3]

A regular level set realizes any second-order jet satisfying DH(x∗)d=0 and DH(x∗)z+D2H(x∗)[d,d]=0 (A regular level set realizes every compatible second-order jet).

[F4]

For a C2 scalar function, f(x∗+s)=f(x∗)+∇f(x∗)Ts+12sT∇2f(x∗)s+o(∥s∥2) (Second-order Taylor expansion f(a+h)=f(a)+∇f(a)⋅h+12hTHf(a)h+o(∥h∥2)).

Proof

1.1givenF1F2construct

If d=0 the result is immediate, so assume d≠0. Let P={i∈I(x∗):λi>0} and Z={i∈I(x∗):λi=0, Dgi(x∗)d=0}. Put H=(h,(gi)i∈P). By LICQ the rows of DH(x∗), together with the rows Dgi(x∗) for i∈Z, are independent. Thus the combined finite-dimensional linear map is onto. Choose z solving Dh(x∗)z+D2h(x∗)[d,d]=0,Dgi(x∗)z+D2gi(x∗)[d,d]=0 (i∈P), and Dgi(x∗)z+D2gi(x∗)[d,d]=−1 (i∈Z). The first two groups say DH(x∗)z+D2H(x∗)[d,d]=0.

2.1step 1.1F2F3F4algebra

By [F3] there is a C2 curve γ with H(γ(t))=H(x∗), γ(0)=x∗, γ′(0)=d, and γ′′(0)=z. For i∈P the corresponding active inequality is exactly fixed at zero. An active i∉P has λi=0; by [F2], either Dgi(x∗)d<0, giving gi(γ(t))=tDgi(x∗)d+O(t2)<0, or i∈Z, giving gi(γ(t))=−t2/2+o(t2)<0. Inactive inequalities remain strict by continuity. Hence γ(t) is feasible for all sufficiently small t>0.

2.2F1F2step 1.1F4algebra

Taylor expansion [F4], criticality ∇f(x∗)Td=0, and γ(t)=x∗+td+12t2z+o(t2) give f(γ(t))−f(x∗)=12t2(∇f(x∗)Tz+dT∇2f(x∗)d)+o(t2). Stationarity gives ∇f(x∗)Tz=−νTDh(x∗)z−∑i∈PλiDgi(x∗)z. The jet equations in step 1.1 therefore make the coefficient in parentheses equal to dT∇xx2L(x∗,ν,λ)d.

3.1step 2.1step 2.2givenassume-contradischarge-contradiction∎

Local minimality gives f(γ(t))−f(x∗)≥0 for small t>0. If the displayed Lagrangian quadratic form were negative, step 2.2 would make this difference negative for all sufficiently small positive t, a contradiction. Thus the quadratic form is nonnegative, as claimed.

Depends on

Used by

Dependency tree · two levels

14 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