Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Single shooting amplifies an initial-slope error on a decaying-mode BVP

Example

For λ>0, consider u′′=λ2(u+1) on [0,1] with u(0)=−1 and u(1)=0. In first-order form the state is x=(u,v) with u′=v, v′=λ2(u+1), and the square boundary map is B(x0,x1)=(u0+1,u1). The scalar solution component u stays in [−1,0], but changing the unknown initial slope by δ changes the terminal value by δsinh⁡(λ)/λ. The factor exceeds one for every λ>0 and is unbounded as λ increases, so a small initial-slope error can be strongly amplified by single shooting.

Verification

Given: λ>0, first-order state x=(u,v), boundary map B(x0,x1)=(u0+1,u1), and an exact IVP evaluator so that the shooting residual is the exact terminal boundary residual.

[F1] Square nonlinear two-point boundary-value problems and endpoint residuals: the BVP is a first-order system with a square endpoint residual.

[F2] Certified differentiable IVP approximation interface for shooting: an exact flow can be used as an endpoint evaluator with error bound zero.

[F3] Finite-budget single shooting for a nonlinear two-point BVP: single shooting applies finite-budget Newton to the endpoint residual when this evaluator is used.

1.1givenF1algebra

The substitution w=u+1 gives w′′=λ2w with w(0)=0 and w(1)=1. Solving this constant-coefficient equation gives w(t)=sinh⁡(λt)/sinh⁡λ, so u(t)=w(t)−1∈[−1,0] because sinh⁡(λt) increases from 0 to sinh⁡λ. Its initial slope is s∗=w′(0)=λ/sinh⁡λ.

2.1step 1.1algebra

If the initial slope is s∗+δ while u(0)=−1 remains fixed, linearity of the equation for w gives wδ(t)=(s∗+δ)sinh⁡(λt)/λ. Subtracting the exact shot yields wδ(1)−w(1)=δsinh⁡λ/λ.

3.1F2F3step 2.1algebra∎

Since sinh⁡λ−λ has value zero at 0 and derivative cosh⁡λ−1>0 for λ>0, we have sinh⁡λ/λ>1. Also the derivative of q(λ)=sinh⁡λ/λ has numerator g(λ)=λcosh⁡λ−sinh⁡λ, where g(0)=0 and g′(λ)=λsinh⁡λ>0; hence q is increasing. For λ≥2, sinh⁡λ≥eλ−1/2, so q(λ)≥eλ−1/(2λ)→∞. The perturbed terminal boundary residual vector changes by (0,δsinh⁡λ/λ), while [F2]–[F3] identify this as the endpoint residual evaluated by exact single shooting.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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