Skip to content

Known limitations

This page lists what Twindex does not do or claim. It is updated with every release. When a limitation is lifted, it moves to the changelog.

What the certificates mean

statement what Twindex can certify
a parameter value fits all measurements yes: witness, a compatible witness
two parameters both fit, so ambiguity is at least L yes: pair, a lower bound
every compatible parameter lies in a set of width at most U yes, for 1-D BVPs and ODE models, via full-prior paving / paving_ode (an upper bound)
a region of parameters is incompatible yes: box / box_ode, an exclusion
the compatible set is nonempty only through a witness. An upper bound alone does not show nonemptiness
structural identifiability (uniqueness from ideal, noise-free data) no; this is a different question, see structural tools such as StructuralIdentifiability.jl
a statistical confidence or credible interval no; noise is a bounded set chosen by the user, not a probability model
that the model or the noise bound describes reality no; that requires external validation

A pair proves that ambiguity is at least L. It does not say the true range is L, and failing to find a pair proves nothing.

Scope of the certified backends

  • ODE models:
  • Right-hand sides use polynomials, division, integer powers, exp, sin and cos. Logarithms, square roots, non-integer powers, events, switching, delays and stochastic terms are not supported.
  • Observables must be affine in the states.
  • Proofs hold on a finite horizon.
  • Stiff systems, long horizons and chaotic dynamics may give INCONCLUSIVE or need many segments; there is no stiff-system benchmark yet.
  • ODE upper bounds:
  • Pavings split axis-aligned boxes at the widest coordinate and use midpoint candidates, so their cost grows quickly with the number of parameters.
  • The demonstrated examples have one to three parameters.
  • Parameter-only reciprocals in lifted models are enclosed as independent constants, which is sound but can be loose.
  • PDEs:
  • The 1-D steady problem, the 2-D elliptic problem on the unit square and the 1-D heat equation, with q ≥ 0 and nondecreasing odd-power nonlinearities.
  • Boxes and pavings exist only for the 1-D problem.
  • No general geometries, Neumann or Robin conditions, or variable diffusion.
  • Numerical audits of arbitrary Python models (audit_model, twindex audit-model) are numerical evidence only. They never produce VALID unless a separate exact problem is certified with certify_audit.

Examples and their assumptions

  • 1978 influenza (real data). The counting-error allowance 3√c + 5 boys is an assumed noise envelope, not a measured instrument uncertainty. Treating bed counts as the infected compartment is a modelling choice. Results that reach R₀ = 20 are limited by the prior.
  • Michaelis–Menten localization (synthetic data). Km = 1 and S₀ = 10 are fixed and known, and the data are rounded numerical integrations. The result shows that the method can certify localization. It says nothing about the precision of any real enzyme assay.
  • SIR, pharmacokinetic, FitzHugh–Nagumo, Hill and predator–prey templates. These use synthetic data generated from nominal parameters.

Engineering limits

  • Size limits. Inputs are size-limited:
  • expression length 20,000 characters and 5,000 syntax nodes;
  • polynomial total degree 64 and 20,000 terms;
  • at most 50 lifted states and 2,000 segments;
  • rational strings of 4,000 characters;
  • certificate files of 64 MB, JSON nesting depth 512 and integer literals of 4,000 digits. Duplicate JSON keys are rejected, because a certificate with two values for one key is ambiguous.

Inputs beyond these limits are rejected or give INCONCLUSIVE. - Arithmetic cost. Exact arithmetic is slow for high-degree candidates and many segments. Search time and certificate size are not yet benchmarked systematically. - Arbitrary code. twindex audit-model module:function imports and runs your Python code. Use it only on code you trust. - Expert review. The trusted core has had adversarial review by a second AI agent, an adversarial certificate corpus, mutation testing and, for 1-D certificates, an independent reference checker. It has not yet had an independent expert proof audit. The reference checker covers only the 1-D kinds, and it shares the barrier theorem with the main checker.