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 program of Inequality constrained programs, tangent cones, constraint qualifications, and KKT, let be a local minimizer satisfying LICQ, and let be its KKT multipliers. Then
Facts & Assumptions
Given: The program, local minimizer , LICQ, and a critical direction .
LICQ gives existence of KKT multipliers at a local minimizer (LICQ implies MFCQ and makes KKT multipliers unique).
A critical direction lies in the linearized cone and satisfies for every active with (Critical directions are tangent to every positively weighted active inequality).
A regular level set realizes any second-order jet satisfying and (A regular level set realizes every compatible second-order jet).
For a scalar function, (Second-order Taylor expansion ).
Proof
If the result is immediate, so assume . Let and . Put . By LICQ the rows of , together with the rows for , are independent. Thus the combined finite-dimensional linear map is onto. Choose solving and The first two groups say .
By [F3] there is a curve with , , , and . For the corresponding active inequality is exactly fixed at zero. An active has ; by [F2], either , giving , or , giving . Inactive inequalities remain strict by continuity. Hence is feasible for all sufficiently small .
Taylor expansion [F4], criticality , and give Stationarity gives . The jet equations in step 1.1 therefore make the coefficient in parentheses equal to .
Local minimality gives for small . If the displayed Lagrangian quadratic form were negative, step 2.2 would make this difference negative for all sufficiently small positive , a contradiction. Thus the quadratic form is nonnegative, as claimed.
Depends on
- Inequality constrained programs, tangent cones, constraint qualifications, and KKT
- LICQ implies MFCQ and makes KKT multipliers unique
- Critical directions are tangent to every positively weighted active inequality
- A regular level set realizes every compatible second-order jet
- Second-order Taylor expansion $f(a+h)=f(a)+\nabla f(a)\cdot h+\tfrac12h^TH_f(a)h+o(\|h\|^2)$
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
- Nocedal and Wright, Numerical Optimization, second edition (standard reference, not scraped)
- J. M. Lee, Introduction to Smooth Manifolds (standard reference, not scraped)