Skip to content

Certified ODE upper bounds

Twindex can now replay a global diameter upper bound for a polynomial or elementary-lifted ODE's bounded-noise inverse problem. A paving_ode certificate partitions the entire prior, excludes boxes with uniform error proofs, and retains every unresolved box. Its target-coordinate outer hull encloses every data-compatible parameter. This is practical localization under the specified prior, model and noise. It does not establish structural identifiability or nonemptiness.

Replay two examples

twindex check examples/study/ode/linear_localization_pair.json \
  examples/study/ode/linear_localization_upper.json
twindex check examples/study/ode/decay_localization_pair.json \
  examples/study/ode/decay_localization_upper.json

The linear acceptance case is x'=a, x(0)=0, a in [0,4], with the measurement x(1)=2 and noise 1/4. Its true compatible interval is exactly [7/4,9/4], with diameter 1/2. The pair proves L=1/2; the 64-leaf paving proves U=67/128, with outer hull [223/128,145/64]. Boundary strips remain unresolved because equality at the noise boundary cannot prove exclusion.

The decay example is x'=-a*x, x(0)=1, a in [0,4], with x(1)=1/2 and noise 1/10. Its 32-leaf paving proves U=7/16, with outer hull [1/2,15/16]. The independently certified pair proves L=1/5. These are synthetic acceptance examples, not experimental datasets.

Both pairs have exactly the same problem objects as their corresponding pavings. Nonemptiness follows from the pair; the outer hull by itself supplies no such claim. All-outside pavings instead prove an empty compatible set, with a null hull and a separately reported empty: true. The reported width is then zero.

Positive result: Michaelis–Menten enzyme kinetics

For substrate depletion S' = -Vmax*S/(1+S), fix Km=1 and S(0)=10. The unknown Vmax has the full prior [0,2]. Four synthetic substrate measurements at t=1/4,1/2,3/4,1 use noise 1/100. They are rounded reference samples at Vmax=1, rather than experimental observations.

python studies/mm_localization.py
twindex check examples/study/ode/mm_localization_pair.json \
  examples/study/ode/mm_localization_upper.json

The pair at Vmax=0.99 and 1.01 proves L=1/50=0.02. The full-prior paving proves U=3/128=0.0234375, with outer hull [253/256,259/256] = [0.98828125,1.01171875]. Thus the compatible diameter lies in [0.02,0.0234375]. The prior width was 2. Both certificates share an identical problem and replay without numpy or scipy. The browser gallery includes both proofs for fresh replay.

This is a real-world model with synthetic data and known initial substrate and Michaelis constant. It establishes practical localization of Vmax conditional on those assumptions. It does not establish simultaneous recovery of unknown Vmax and Km, structural identifiability, or experimental accuracy.

Generate and report

twindex ode-sivia examples/study/ode/linear_localization_pair.json \
  --max-leaves 64 --min-width 1/1000 --output upper.json
twindex check upper.json --json
twindex report upper.json --output upper-report

Generation requires twindex[general]; replay uses only the Python standard library. Numerical candidates propose exclusions; exact replay decides each one. The generated numbers may differ from the saved example because its candidates are exact analytic polynomials. Reports give exact hull endpoints, width and emptiness, with no lower bound inferred from the paving.

Python callers can use twindex.search_ode_bounds.sivia_ode(problem, ...), which returns a certificate and its fresh exact report. An optional candidate_factory(problem, box) returns a parameter-independent ODECandidate. The default integrates at the box midpoint and tries several tube radii. Set max_leaves, min_width, and fit_options (for candidate_ode) to limit work. Integration or proof failure retains the box or triggers subdivision.

Why the uniform check is sound

Fix a leaf parameter box and one candidate polynomial per time segment. Write each parameter as its midpoint plus its half-width times a variable in [-1,1]. Expand the residual and state Jacobian into powers of these variables and the normalized state-tube variables. Each coefficient is an exact polynomial in local time. Summing its Bernstein absolute bounds bounds the whole expansion. For the diagonal Jacobian's constant term, use a signed upper bound; this preserves contraction where available. The weighted row sums bound the state log norm uniformly for every parameter in the box. Parameters are constant and are not differentiated as states.

Bound every polynomial initial value over the same parameter box and charge its entire deviation from the candidate to the entry error. Charge jumps at piece boundaries too. The existing weighted tube continuation proof then applies separately to every parameter, using the same uniform bounds. The error must remain strictly inside the tube over every segment. Rounding is outward, and all replay arithmetic is rational.

At a measurement, the candidate's affine observable value is independent of parameters. Its weighted error bound encloses every actual observable value in the box. A box is excluded only when that entire enclosure is strictly separated from at least one measurement's allowed interval, using that row's noise bound. Failure of a sufficient test is INCONCLUSIVE.

Every split is checked to partition its parent at a strict interior point, starting with the exact prior. Thus the union of unresolved leaves contains the entire compatible set once every outside leaf verifies. Their target hull width is U. The schema is in DESIGN §6.4.

Elementary lifting over a box

The same uniform proof applies to the deterministic polynomial lift. Initial user-state polynomials are enclosed over the parameter box; auxiliary initial values are then enclosed in atom creation order with exact interval arithmetic. The initial error charges the farthest endpoint for every lifted state. A parameter-only reciprocal 1/D(theta) receives a uniform interval and is included as an independent constant pseudo-parameter. Discarding its correlation with theta enlarges the domain, so it cannot strengthen an exclusion incorrectly. Pseudo-parameters are never differentiated as states or used as paving axes.

For every fixed theta, these enclosures contain the initial lifted system and its derived constants. The weighted tube proof therefore applies to that theta, with uniform bounds for all theta in the box. The lifting invariants then give the original solution. A box whose denominator enclosure includes zero, including an exactly zero singleton, is retained as INCONCLUSIVE. Unsupported elementary initial ranges also remain INCONCLUSIVE. No singular box is discarded by a failure to initialize. Candidate-free unresolved pavings require no initialization.

Current limits

Polynomial and supported elementary ODE models, axis-aligned trees, parameter-independent candidates, and outside/unresolved leaves are supported. Parameter-affine candidates, oriented boxes and tensor Bernstein refinements require further work. Paving cost can grow exponentially with parameter dimension. A coarse or failed search can leave U equal to the full prior width; that does not imply ambiguity or uniqueness. Lower bounds continue to require a separate certified pair.

Search diagnostics are separate from proof: sivia_ode(..., telemetry=path_or_dict) records exact box counts, volumes, retained target hull/U checkpoints, rejection reasons, generation/verification/final-replay times, certificate bytes and stopping conditions. twindex ode-sivia writes search_telemetry.json beside its output. identify_ode accepts the same telemetry destination and writes it in its output directory. Identification records checked L (or null), never U; it does not run a box partition, so box counts/volumes are null. Intermediate hulls are search observations; only the final replayed certificate proves U. RSS is the process lifetime high-water mark in bytes, or null where resource is unavailable.

branching_policy selects widest (the default), normalized-width (width relative to the prior), target-weighted (twice the target's normalized score), or sensitivity-guided (largest noise-normalized observable change between axis endpoints through the midpoint). The last uses numerical simulations, adds probe cost and falls back to normalized widths on failed/nonfinite probes. All policies retain unresolved boxes and emit the same exact midpoint partition schema. They promise neither convergence nor an improvement in U. The same policies are available in search.sivia for the 1-D PDE. CLI: ode-sivia --branching-policy. Equal-budget results, including failures, are in benchmarks/.