TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generated

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.

Exact-Hessian SQP converges locally to a regular transcription KKT point

Statement

Fix a mesh and a finite transcription generated from the pointwise smooth data in Finite-horizon ODE optimal-control transcription data. Suppose its NLP functions have continuous derivatives through order three on an open neighborhood of a KKT point $(z_{*}, μ_{*})$ , LICQ holds there, every active inequality multiplier is strictly positive, and the second-order sufficient condition holds on the critical cone. Then, after the correct active set is identified, the exact-Hessian full-step branch using Full-step exact-Hessian SQP after active-set identification is well-defined from a sufficiently close primal-dual start and converges quadratically to $(z_{*}, μ_{*})$ . The finite-budget dispatch of Finite-budget barrier or SQP solve for a transcription NLP may terminate before this local convergence is realized.

This also has the following conditional mesh-family conclusion. For each mesh index $N$ , let $K_{N} : Z_{N} \to Y_{N}$ be the square active-set KKT residual map of a finite transcription, with finite-dimensional normed spaces $Z_{N}, Y_{N}$ , and let $z_{N}^{0} \in Z_{N}$ be a reference primal-dual pair. Let $Z$ be a common Banach space containing the continuous primal and multiplier fields, with bounded linear reconstruction maps $E_{N} : Z_{N} \to Z$ that use the same fixed norms and satisfy $\sup_{N} ∥ E_{N} ∥ \leq C_{E}$ . Suppose a continuous KKT pair $z^{†} \in Z$ and mesh-consistent constraints satisfy $∥ E_{N} z_{N}^{0} - z^{†} ∥_{Z} \to 0$ and $∥ K_{N} (z_{N}^{0}) ∥_{Y_{N}} \leq ε_{N} \to 0$ . Suppose the discrete sensitivity maps $D K_{N} (z_{N}^{0}) : Z_{N} \to Y_{N}$ are invertible with $∥ D K_{N} (z_{N}^{0})^{- 1} ∥ \leq β$ uniformly, and $D K_{N}$ is $L$ -Lipschitz on a common radius $r$ about each $z_{N}^{0}$ , with constants independent of $N$ . For all sufficiently large $N$ , require $2 β ε_{N} \leq r$ and $2 β^{2} L ε_{N} \leq \frac{1}{2}$ . Then there is a unique active-set KKT root $z_{N}^{*}$ in the radius- $2 β ε_{N}$ ball, and $∥ E_{N} z_{N}^{*} - z^{†} ∥_{Z} \leq ∥ E_{N} z_{N}^{0} - z^{†} ∥_{Z} + 2 C_{E} β ε_{N} \to 0$ . If these roots satisfy LICQ, strict complementarity, SOSC, and a common local full-step basin for exact-Hessian SQP, then the exact-Hessian iterates from starts in that basin converge quadratically to $z_{N}^{*}$ for each such mesh. The varying systems are compared through the reconstruction maps and their fixed norms; this conclusion makes no global optimizer, path-feasibility, or finite-budget convergence claim.

Facts & Assumptions

Given: A fixed smooth finite transcription, a KKT pair, LICQ, strict complementarity, the second-order sufficient condition, a correct identified active set, and an initial primal-dual point sufficiently close to the KKT pair.

[F1]

The transcription is a finite NLP with the objective and constraints returned by Finite-horizon shooting and Runge–Kutta collocation transcription. The C3 regularity of these actual reduced functions on the stated neighborhood is an explicit hypothesis; smooth data alone do not certify a differentiable implicit-stage solve branch (Finite-horizon ODE optimal-control transcription data).

[F2]

The KKT convention is $g_{i} \leq 0$ with nonnegative active multipliers (Inequality constrained programs, tangent cones, constraint qualifications, and KKT).

[F3]

The exact-Hessian local SQP theorem gives quadratic convergence for a $C^{2}$ NLP with LICQ, strict complementarity, SOSC, and locally Lipschitz active-KKT Jacobian (Exact-Hessian SQP converges quadratically on the identified active KKT system).

[F4]

The strict second-order sufficient condition used here is positivity of the Lagrangian Hessian on every nonzero critical-cone direction (Strict second-order positivity on the critical cone gives a strict local minimum).

[F5]

The actual NLP functions are $C^{3}$ by [F1]. On a closed ball compactly contained in their open $C^{3}$ neighborhood, their third derivatives are bounded, so their Hessians and the active KKT Jacobian are locally Lipschitz.

[F6]

The active-set KKT Jacobian and full-step exact-Hessian SQP branch have the local properties stated in the fixed-system theorem (Exact-Hessian SQP converges quadratically on the identified active KKT system).

[F7]

Each finite-dimensional normed space $Z_{N}$ is complete (Every finite-dimensional normed space is Banach). A closed ball in $Z_{N}$ is complete: every Cauchy sequence in the ball converges in $Z_{N}$ , and continuity of the norm keeps its limit in the ball. A contraction of a nonempty closed ball into itself therefore has a unique fixed point by A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point.

[A1]

For the mesh-family conclusion, the reconstruction, residual-consistency, uniform inverse, uniform Jacobian-Lipschitz, active-set, and common-basin assumptions in the Statement hold.

Proof

1.1F1given

A fixed transcription has finitely many decision variables. By the regularity hypothesis in the Statement and [F1], its actual objective and constraint functions have continuous derivatives through order three on a neighborhood of the KKT point. For an implicit-stage transcription this hypothesis includes the selected local stage-solve branch; no differentiability of that branch is inferred from the smooth-data definition alone.

1.2A1F7algebra

For the mesh-family branch, set $A_{N} = D K_{N} (z_{N}^{0})$ and $T_{N} (z) = z - A_{N}^{- 1} K_{N} (z)$ . If $ε_{N} = 0$ , $z_{N}^{0}$ is already a root. Otherwise take the closed ball of radius $R_{N} = 2 β ε_{N}$ . The residual bound gives $∥ T_{N} (z_{N}^{0}) - z_{N}^{0} ∥ \leq β ε_{N} = R_{N} / 2$ . For $z$ in that ball, the uniform Lipschitz bound gives $∥ D T_{N} (z) ∥ = ∥ I - A_{N}^{- 1} D K_{N} (z) ∥ \leq β L R_{N} \leq 1 / 2$ . Thus $T_{N}$ maps the ball into itself and is a contraction. Completeness [F7] gives its unique fixed point $z_{N}^{*}$ , which is exactly the unique root of $K_{N}$ there and satisfies $∥ z_{N}^{*} - z_{N}^{0} ∥ \leq R_{N}$ .

2.1F2F3F4F5givenstep 1.1

The KKT map for the identified active set is built from the first derivatives of those objective and constraint functions. Its Jacobian is locally Lipschitz by continuity and local boundedness of their third derivatives in [F5]. The assumed LICQ, strict complementarity, and SOSC from [F4] are exactly the remaining hypotheses of [F3].

3.1F3givenstep 2.1algebra

Apply [F3] to the active KKT system. It provides a neighborhood in which exact-Hessian full Newton steps are defined and converge quadratically from a sufficiently close start, which is the asserted fixed-mesh branch. The dispatcher has a finite outer cap, so it can stop before the local sequence converges.

4.1A1F6step 1.2algebra∎

By boundedness of $E_{N}$ , $∥ E_{N} z_{N}^{*} - z^{†} ∥_{Z} \leq C_{E} ∥ z_{N}^{*} - z_{N}^{0} ∥ + ∥ E_{N} z_{N}^{0} - z^{†} ∥_{Z} \leq 2 C_{E} β ε_{N} + ∥ E_{N} z_{N}^{0} - z^{†} ∥_{Z}$ , which tends to zero. The assumed LICQ, strict complementarity, SOSC, local Lipschitz conditions, and common basin let [F6] apply at each $z_{N}^{*}$ ; hence each exact-Hessian full-step sequence from that basin converges quadratically.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

63 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

Jorge Nocedal and Stephen J. Wright, Numerical Optimization, 2nd ed. (standard reference, not scraped)
S. Gros and M. Diehl, Numerical Optimal Control, draft course manuscript, Chapter 13 §13.4 (standard reference, not scraped)