Try
An adaptive solver has accepted two Euler half steps. Its local comparison was small enough for its controller. What, exactly, can we guarantee about the distance from the true solution? We will build a separate error ledger whose entries are exact rational numbers. This ledger certifies discretization error for a declared equation; the controller’s comparison does not replace it.
Use the dimensionless family y′=−λ(y−t²)+2t, y(0)=1, on 0≤t≤1, with λ positive. Substitution verifies the exact solution y(t)=t²+exp(−λt): its derivative is 2t−λ exp(−λt), equal to the right side. The equation is globally affine in y, so the usual uniqueness result applies. The manufactured solution is a mathematical test case, not an observed physical process.
For λ=4, a proposed interval of length H=1/4 has coarse Euler result 0 and two-half-step result 37/128. Their difference is 37/128. Predict whether that comparison is the same number as a proved global error bound. Review local-to-global error and step control for the distinction between a controller and an error proof.
Predict
Write e=y(t)−Y for the current signed error, where Y is the numerical value, and suppose a nonnegative number B satisfies |e|≤B. For one Euler substep of length h, the difference of the right sides evaluated at y(t) and Y is exactly −λe. Predict the factor multiplying old error: it is 1−λh, not always a positive number and not automatically a contraction.
The error ledger uses the absolute factor |1−λh|. A factor above 1 can make the bound large, but does not invalidate the inequality. A small or zero old error does not remove the new local defect. Rejected trial calculations, meanwhile, do not advance the accepted state and therefore do not inject a new accepted-path defect.
Experiment
Perform the following exact arithmetic independently of an exponential calculator. At λ=4 the second-derivative bound will be M=18. Each half step has h=1/8, amplification |1−4/8|=1/2, and defect budget Mh²/2=9/64.
| Accepted node | Euler value Y | New budget calculation | Bound B |
|---|
| 0 | 1 | Exact initial value | 0 |
| 1/8 | 1/2 | (1/2)·0+9/64 | 9/64 |
| 1/4 | 37/128 | (1/2)(9/64)+9/64 | 27/128 |
The first slope is −4. At the midpoint the slope is −4(1/2−1/64)+1/4=−27/16, giving Y=1/2−27/128=37/128. If this trial is accepted, the exact node enclosure is
10/128 ≤ y(1/4) ≤ 64/128,
because Y−B=10/128 and Y+B=64/128. Independently, y(1/4)=1/16+exp(−1)≈.430379 and its error from 37/128 is approximately .141317. That approximate exponential calculation is a diagnostic, not an interval enclosure. The bound 27/128≈.210938 was obtained without computing the exponential.
This is a conditional accepted-path calculation, not a claim that every tolerance accepts the trial. Its controller comparison 37/128 exceeds, for example, tolerance 1/4. If rejected, the accepted state remains t=0,Y=1,B=0. The trial still consumed work. If the controller does accept, both half steps—not the coarse full step—belong to the error ledger.
Understand
Derive the single-substep recurrence
Let F(t,z)=−λ(z−t²)+2t. The exact solution has y″(t)=2+λ²exp(−λt), so |y″(t)|≤M=2+λ² throughout [0,1]. This bound concerns the exact solution; it does not rely on numerical observations lying near it.
Taylor’s integral identity gives
y(t+h)=y(t)+hF(t,y(t))+r,
where r=∫ from 0 to h of (h−s)y″(t+s) ds and |r|≤Mh²/2, whenever 0≤t≤t+h≤1. Euler gives Ynext=Y+hF(t,Y). Subtraction therefore gives the exact signed identity
enext=(1−λh)e+r.
The triangle inequality proves the certified update
Bnext=|1−λh|B+(2+λ²)h²/2.
Starting from B₀=0 is justified because Y₀=y(0)=1 exactly. If only |y(0)−Y₀|≤δ is known, start from B₀=δ instead. Induction over the accepted substeps proves |y(tⱼ)−Yⱼ|≤Bⱼ. The affine dependence makes the propagation identity global in Y; there is no hidden numerical-state neighborhood assumption for this family.
Unroll a genuinely nonuniform path
For accepted substeps h₀,…,hₙ₋₁ define aⱼ=|1−λhⱼ| and dⱼ=Mhⱼ²/2. Repeated substitution gives
Bₙ=(product over j=0,…,n−1 of aⱼ) B₀ + sum over i=0,…,n−1 of dᵢ (product over j=i+1,…,n−1 of aⱼ).
An empty product is 1 and an empty sum is 0. Prove this by induction: multiplying Bₙ by aₙ appends one factor to every old product, while adding dₙ supplies the new empty-product term. No division by an amplification factor occurs, so zero factors cause no difficulty. The formula shows why simply adding local budgets can fail when later factors exceed 1, and why an early defect can disappear from this upper bound when a later factor is zero.
For λ=4 and substeps 1/8,1/8,1/4, the factors are 1/2,1/2,0. The final budget is 9/16, entirely from the last defect budget; the old contribution is multiplied by zero. This is a stipulated nonuniform Euler path, not the assertion that the workbench’s paired-step controller produces that grid. It ends at t=1/2, not t=1. A certificate must carry its time as well as its radius.
Stability and failed trials have different roles
For the homogeneous error propagation, |1−λh|≤1 exactly when 0≤λh≤2. Outside this range the recurrence remains valid but may amplify error strongly. For example, λ=16 and two substeps h=1/4 give M=258, a=3 and d=129/16. From B₀=0, B₂=129/4. It would be false to replace the factor 3 by 1 merely because the exact exponential decays. This hypothetical accepted Euler path illustrates the bound; a controller can reject its proposed interval.
A rejected trial is not an additional mesh point. Charge its derivative evaluations to the work ledger, but preserve the accepted t,Y,B. If a run stops at t<1 because of a minimum step, trial cap or arithmetic cap, its existing certificate still concerns that last accepted time only. A small B there is not a solution at the requested endpoint.
Exact arithmetic and reference arithmetic
For integer λ and rational t,Y,h,B, every Euler and budget operation above is rational, including the absolute value and comparisons. An implementation can use integer numerators and positive denominators, reduce by gcd, and compare fractions by exact cross multiplication. An exact certificate must retain these fractions; a rounded decimal label alone is not an outward-rounded interval.
The bounded laboratory contract uses λ∈❴1,4,16,64❵, proposed H=2⁻ᵏ for k=0,…,12, tolerance 2⁻ᑫ for q=0,…,20, at most 512 trials and a 4096-bit rational arithmetic cap. Accepted substeps have length H/2, so the half step may be 2⁻¹³ even though proposed H never is. A cap is a resource limit, not an accuracy theorem. Exceeding it must stop or reject the computation with an explicit status, retaining only a previously certified accepted record; it must not silently switch to floating point. All intermediate arithmetic needed for a claim must respect the implementation’s declared cap policy.
If numerical updates instead incur perturbations ηⱼ, then the proof needs Bnext=aⱼB+dⱼ+|ηⱼ|. Without justified bounds on those perturbations, reusing the rational recurrence does not certify a floating-point trajectory. Likewise a floating evaluation of exp(−λt) gives a useful independent comparison but not a verified enclosure unless its own error is bounded. A claim between nodes needs a separate interpolation estimate.
Apply
Change the manufactured equation to y′=−λ(y−t³)+3t² with y(0)=1. Derive a new bound on [0,1], rather than copying M=2+λ². For λ=4, compute the exact two-half-step budget for a proposed H=1/4, and check the fine Euler value. Explain why the old budget constant has not been justified for this changed problem.
Review the changed forcing
The exact solution is y=t³+exp(−λt), verified by substitution. Its second derivative is 6t+λ²exp(−λt), bounded in absolute value by 6+λ² on [0,1]. The same affine propagation proof applies, with M=22 when λ=4. Each half-step defect budget is 11/64, so B₂=(1/2)(11/64)+11/64=33/128. Starting at Y=1, the first half step gives 1/2. The midpoint slope is −4(1/2−1/512)+3/64=−249/128, so the fine result is 1/2−249/1024=263/1024. The rational enclosure at 1/4 is therefore [−1/1024,527/1024]. The former derivative-bound proof used a second derivative with constant polynomial part 2; it does not prove the changed bound merely by reusing the old code.
Continue
Compare methods only after matching the equation, initial condition and endpoint. Report accepted substeps, rejected trials, derivative work, resource status, the exact bound and the approximate reference diagnostic separately. A smaller estimator, a smaller bound and lower work are different comparisons. Return to accepted steps and rejected work to audit the path, and verification and method selection to assemble a reproducible report. This proof certifies one declared manufactured family; it is not a universal adaptive-solver theorem.