ExampleConstruction: AI-adaptedVerification: 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.

Backward Euler differentiates a stiff scalar decay fit on its exact branch

Example

For $u^{'} = - k u$ with fixed $u_{0} > 0$ and step size $h > 0$ , take $k \in (0, (2 h)^{- 1})$ and the one-stage backward Euler equation $Y = u_{0} - h k Y$ . Its fixed-point map sends the invariant interval $[u_{0} / 2, u_{0}]$ into itself and has contraction factor $h k < 1 / 2$ , so the branch selected by Small-step implicit Runge–Kutta stages have a unique branch and controlled residual error is well defined. The observation is zero and the terminal loss is $J (k) = \frac{1}{2} Y (k)^{2}$ .

Facts & Assumptions

Given: The scalar backward Euler stage equation, the stated parameter interval, and the terminal quadratic objective.

[F1]

The one-stage implicit Runge--Kutta residual has the selected stage root and residual bound under its invariant-ball contraction hypotheses (Small-step implicit Runge–Kutta stages have a unique branch and controlled residual error).

[F2]

On a nonsingular selected stage branch, implicit differentiation gives $D_{θ} Y = - G_{Y}^{- 1} G_{θ}$ and differentiates the Runge--Kutta update (An implicit Runge-Kutta stage has the stated parameter sensitivity on its selected branch).

[F3]

Backward Euler is the one-stage implicit Runge--Kutta method with $A = (1)$ and $b = (1)$ (Backward Euler step equation and algebraic residual).

Verification

1.1F1F2F3givenalgebra

To apply [F1] with the prescribed center $u_{0}$ , use the larger closed ball $B = [0, 2 u_{0}]$ of radius $R = u_{0}$ . For $F (Y) = - k Y$ , take $M = 2 k u_{0}$ and $L = k$ ; then $h M = 2 h k u_{0} < R$ and $q = h k < 1 / 2$ . The field is $C^{1}$ on $R$ with derivative bounded by $L$ , so the nonsingularity hypotheses inherited by [F2] hold on this ball. Solving the scalar residual gives $(1 + h k) Y = u_{0}$ , hence $Y = u_{0} / (1 + h k)$ . Since $1 + h k > 0$ , this is the unique root in the stated interval and agrees with the branch in [F1].

2.1F2step 1.1algebra∎

Differentiate the residual $(1 + h k) Y - u_{0} = 0$ : $(1 + h k) Y_{k} + h Y = 0$ , so [F2] gives $Y_{k} = - h u_{0} / (1 + h k)^{2}$ . Therefore $J_{k} = Y Y_{k} = - h u_{0}^{2} / (1 + h k)^{3}$ .

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

John C. Butcher, Implicit Runge-Kutta Methods, tutorial, §§1–2 (standard reference, not scraped)
William W. Hager, Runge-Kutta methods in optimal control and the transformed adjoint system, §§2–3 (standard reference, not scraped)