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.

A valid shooting BVP can fail Newton at a singular initial guess

Example

For $y^{'} = 0$ on $[0, 1]$ with $B (y (0), y (1)) = y (0)^{2} - 1$ , the exact shooting residual is $R (s) = s^{2} - 1$ . It has simple roots $s = \pm 1$ , but exact-Jacobian Newton at $s = 0$ immediately returns singular-jacobian because $R^{'} (0) = 0$ . Local convergence near a simple root does not imply convergence from every initial guess.

Verification

Given: The scalar BVP, an exact flow evaluator, and a zero residual tolerance with at least one Newton correction allowed.

[F1] Square nonlinear two-point boundary-value problems and endpoint residuals: the exact shooting residual is $B (s, ϕ (1; s))$ .

[F2] Certified differentiable IVP approximation interface for shooting: the exact flow is an allowed evaluator with zero trajectory error.

[F3] Derivative of the nonlinear shooting residual: the derivative of the shooting residual is the derivative of $B (s, Φ (s))$ by the chain rule.

[F4] Finite-budget single shooting for a nonlinear two-point BVP: Newton first checks the residual tolerance and then attempts the Jacobian correction; singular Jacobian is a returned status.

[F5] Local Newton convergence for a simple nonlinear shooting root: the local theorem requires an invertible derivative at the root and makes no arbitrary-start claim.

1.1givenF1F2algebra

The exact ODE flow for $y^{'} = 0$ is $ϕ (t; s) = s$ , so [F1] gives $R (s) = B (s, s) = s^{2} - 1$ , and [F2] certifies that the exact evaluator used by the algorithm has zero IVP error. Thus $R (1) = R (- 1) = 0$ and $R^{'} (s) = 2 s$ , making both roots simple.

2.1F3F4step 1.1algebra

At the initial guess $s_{0} = 0$ , the residual is $- 1$ , so a zero tolerance is not met; the Jacobian is the zero $1 \times 1$ map because $R^{'} (0) = 0$ . The linear correction therefore has no solution in the sense required by Newton and [F4] returns singular-jacobian before any update.

3.1F5step 1.1step 2.1algebra∎

The roots at $\pm 1$ have nonzero derivative, so the simple-root condition can hold on a sufficiently small ball around either root, where the polynomial derivative is Lipschitz. Fact [F5] then gives a local Newton basin there, while step 2.1 exhibits a valid start outside both guaranteed basins for which the method stops.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

R. Verfürth, Numerical Methods and Stochastics, Part I: Numerical Methods, Lecture Notes (standard reference, not scraped)
E. Hairer and G. Wanner, Solving Ordinary Differential Equations II, Chapter VI: Iterative Methods—Nonlinear Equations (standard reference, not scraped)