Alphabeta Math
LemmaStatement: 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 single and multiple shooting have the same reduced feasible controls

Statement

Fix a mesh, controls u0,…,uN−1, and a successful deterministic Runge–Kutta interval map Φj from Finite-horizon shooting and Runge–Kutta collocation transcription. In the single-shooting NLP, define states recursively from X0,0=x0 and Xj+1,0=Φj(Xj,0,uj). In the multiple-shooting NLP, impose the same initial state and continuity equations. Then projection from the multiple-shooting feasible set onto its control coordinates is a bijection onto the single-shooting feasible controls. Any objective and node constraints that use the same recursively determined states have identical reduced values and feasibility. This is an algebraic equivalence of the discrete NLPs; it is not an equivalence to the continuous ODE problem.

Facts & Assumptions

Given: The fixed mesh, the deterministic interval maps, and controls for which every interval map succeeds.

[F1]

An interval map is available only after its explicit stages or implicit stage residual solve return a successful status; it assigns exactly one deterministic endpoint to that successful start/control pair, and single shooting applies it recursively (Finite-horizon shooting and Runge–Kutta collocation transcription).

[F2]

The multiple-shooting variables satisfy X0,0=x0 and Xj+1,0=Φj(Xj,0,uj) (Finite-horizon shooting and Runge–Kutta collocation transcription).

Proof

1.1F1givenconstruct

Given any control tuple feasible in single shooting, calculate X1,0=Φ0(x0,u0), then each later Xj+1,0=Φj(Xj,0,uj). Uniqueness of each deterministic map makes this recursively defined state tuple well-defined; by construction it satisfies every multiple-shooting continuity equation.

2.1F1F2step 1.1induction

Conversely, a multiple-shooting feasible tuple has fixed X0,0=x0 and satisfies each continuity equation. Induction on j forces its Xj,0 to equal the recursive single-shooting value for the same controls. Hence there is exactly one multiple-shooting state tuple for each feasible control tuple and the projection is bijective.

3.1step 1.1step 2.1givenalgebra∎

Under this bijection the states at all shared nodes agree. Therefore every node constraint has the same value and every objective formed from the same node/stage values is identical. Thus reduced feasibility and objective values coincide.

Depends on

Used by

Dependency tree · two levels

16 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