Vector trajectories, adaptive estimates, and validated ODE tubes
Compare fixed and adaptive demonstrations with checked Picard/Taylor enclosures and honest or certified event candidates.
Use a public Calculus graph for the equation y'=y, y(0)=1. The problem record is inert mathematical structure; choosing a solver is a later action.
Euler and RK4 are demonstrations, not certificates
Both methods retain exact rational step arithmetic here. Exact arithmetic does not make the discretization exact: neither result includes a proved truncation bound.
Euler returns 625/256; one classical RK4 step returns 65/24. They can be compared with known values or a certified real, but the ODE result itself stays :approximate.
Validate existence, uniqueness, and a tube
The Picard method searches for a complete interval tube on each segment. It checks both the right-hand-side range and the symbolically derived state derivative over that tube.
validated.At(1/2) returns the complete certified tube covering one half. It does not pretend to be a point value:
Solve a vector system
The same APIs preserve coordinate order for the harmonic oscillator. RK4 is still approximate; ValidatedPicard checks the entire two-by-two Jacobian and a box contraction.
Adapt steps without overclaiming
Step doubling gives a useful local estimate but not a global proof.
Keep event claims honest
An approximate sign change is an observed candidate. A validated range that misses zero is a proof that no event occurs on that segment.
Tighten the tube and certify one event
The second-order solver first proves the Picard existence tube, then encloses the total derivative and recenters a Taylor remainder on every segment. For y'=1, the remainder is exactly zero, so the half-height event contracts to an exact time.
The event proof is not inferred merely from a tube containing zero. It retains the endpoint range checks, the checked identity g_t + grad(g) dot f, and every interval-Newton contraction.
Bounded failure preserves useful work
A deliberately inadequate radius budget cannot validate y'=100y over one large step. The unresolved attempted segment remains in the result.
Increase maxTubeIterations, increase steps, or both. More work may find a self-map, but work exhaustion is never reported as nonexistence.
Fixed Taylor stepping likewise stops at its first unresolved tube. It keeps that failed segment so its diagnostics remain inspectable.
Adapt a certified trajectory
A single step for y'=y on [0,1] fails the strict contraction test because h L = 1. The adaptive method halves that step, validates smaller segments, and carries their certified endpoint intervals forward.
For a vector equation with known solution (t^2/2,t^2), a local remainder budget forces smaller steps even when a Picard tube is already available.
That tolerance bounds the local remainder, while finalState carries the accumulated enclosure. Exhausting attempts retains only the accepted prefix as the trajectory and stores failed candidates in work.attempts.
Higher-order certified flow
Each segment uses start-point derivative bounds and a highest-derivative bound over a Picard existence tube. Try order=3 or raise maxOrder explicitly. AdaptiveValidatedTaylor adds the existing attempt/minimum-step controller; remainderTolerance bounds only the local highest-order remainder. Stored interval uncertainty and wrapping remain. rangeOptions configures range work and semantic precision, while derivativeOptions configures derivative checking. Unsupported symbolic/domain cases report errors rather than fabricated enclosures.
Integrating backward in time
Knowing the state at a later time can also define an IVP. The equation is unchanged; we take negative time steps. Here y'=1 and y(1)=1 give y(0)=0.
The interval 1:0 retains its orientation; 0:1 with initial time 1 is rejected. The same convention works for Euler, RK4, Picard and adaptive methods. Certified methods use the magnitude of the step for contraction and remainder tests, but retain its sign in the integration formula. Event :rising means rising with increasing physical time, even when the solver is moving backward. Backward integration may amplify uncertainty; it is not guaranteed to undo numerical error.
Exercises
1. Compare Euler and RK4 for y'=t+y at several fixed step counts. 2. Give the validated solver an interval initial state such as (99/100):(101/100) and inspect how it propagates measurement uncertainty. 3. Reduce the Picard step count and watch wrapping widen the endpoint. 4. Compare the vector RK4 oscillator against its validated component boxes. 5. Change an event direction and observe which endpoint sign changes qualify. 6. Explain why a validated event range containing zero still needs an existence or interval-Newton argument. 7. Compare ValidatedPicard and ValidatedTaylor2 endpoint widths on y'=y as the number of segments changes.