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.

MFCQ identifies the linearized and Bouligand tangent cones

Statement

For the $C^{2}$ program of Inequality constrained programs, tangent cones, constraint qualifications, and KKT, if MFCQ holds at a feasible point $x$ , then $T_{C} (x) = L_{C} (x) .$

Facts & Assumptions

Given: The feasible point, $C^{2}$ constraint maps, tangent and linearized-cone definitions, and MFCQ at $x$ .

[F1]

Every vector in $T_{C} (x)$ satisfies $D h (x) d = 0$ and $D g_{i} (x) d \leq 0$ for active $i$ , by the definitions and first-order differentiability (Inequality constrained programs, tangent cones, constraint qualifications, and KKT).

[F2]

If $D h (x)$ has full row rank, this rank persists on a neighborhood, and after restriction to that neighborhood the level $h = h (x)$ has a local $C^{2}$ graph over $\ker D h (x)$ whose graph correction $ψ$ satisfies $ψ (0) = 0$ and $D ψ (0) = 0$ (Differential rank is lower semicontinuous, A regular level set is locally a $C^{k}$ graph of dimension $m - n$ ).

[F3]

A $C^{2}$ map with zero value and zero derivative has a second-order remainder of size $O (∥ u ∥^{2})$ near the base point (Second-order Taylor expansion $f (a + h) = f (a) + \nabla f (a) \cdot h + \frac{1}{2} h^{T} H_{f} (a) h + o (∥ h ∥^{2})$ ).

Proof

1.1givenF1algebra

Take $d \in T_{C} (x)$ and use its defining feasible sequence $x + t_{k} d_{k}$ , where $t_{k} ↓ 0$ and $d_{k} \to d$ . For $h (x) = 0$ , Taylor expansion gives $0 = h (x + t_{k} d_{k}) = t_{k} D h (x) d + o (t_{k})$ , hence $D h (x) d = 0$ . For active $i$ , feasibility gives $0 \geq g_{i} (x + t_{k} d_{k}) = t_{k} D g_{i} (x) d + o (t_{k})$ , hence $D g_{i} (x) d \leq 0$ . Therefore $d \in L_{C} (x)$ .

1.2givenF2F3construct

Now take $d \in L_{C} (x)$ . Let $w$ be the MFCQ direction; if no inequality is active set $w = 0$ . Both $d$ and $w$ lie in $\ker D h (x)$ . When there are equality constraints, [F2] supplies a local graph $x + u + ψ (u)$ over this kernel; with no equalities use $ψ = 0$ . For $t > 0$ small, define $u (t) = t d + t^{3 / 2} w$ and $x (t) = x + u (t) + ψ (u (t))$ . Then $h (x (t)) = 0$ and [F3] yields $x (t) - x = t d + t^{3 / 2} w + O (t^{2})$ , so $(x (t) - x) / t \to d$ .

2.1step 1.2givenalgebra

If $i$ is active, Taylor expansion gives $g_{i} (x (t)) = t D g_{i} (x) d + t^{3 / 2} D g_{i} (x) w + O (t^{2}) + o (t^{2})$ . When $D g_{i} (x) d < 0$ , its order- $t$ term makes this negative for all sufficiently small $t > 0$ . When $D g_{i} (x) d = 0$ , MFCQ gives $D g_{i} (x) w < 0$ , and its order- $t^{3 / 2}$ term dominates the remainder of order $t^{2}$ . Inactive inequalities remain strict by continuity. Since there are finitely many inequalities, one positive $τ$ works for all of them and every $0 < t < τ$ . Thus $x (t)$ is feasible for such $t$ .

3.1step 1.1step 1.2step 2.1construct∎

Taking $t_{k} = τ / 2^{k + 1}$ gives feasible points with $t_{k} ↓ 0$ and $(x (t_{k}) - x) / t_{k} \to d$ , so $d \in T_{C} (x)$ . This proves $L_{C} (x) \subseteq T_{C} (x)$ ; step 1.1 gives the reverse inclusion.

Depends on

Used by

MFCQ gives KKT multipliers at a smooth local minimizer Theorem

Dependency tree · two levels

21 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)
Boyd and Vandenberghe, Convex Optimization (standard reference, not scraped)