Changelog

All notable changes to this project are documented here. The format follows Keep a Changelog, and the project uses Semantic Versioning.

[Unreleased]

[0.9.0] - 2026-11-09

Added

• Certified derived targets for ODE pairs: target_expr (for example "beta/gamma") certifies a gap in any rational function of the parameters. It comes with an exact closed evaluator and the example examples/study/ode/sir_r0_pair.json, which certifies an R0 gap of 3245/4178.
• Hardening: SECURITY policy and severity guide, an architecture and trust-boundary document, known limitations, a trusted-module manifest with an import-boundary test, a numpy-free wheel replay in CI, JSON budgets (64 MB, depth 512, no duplicate keys), an adversarial certificate corpus with a proof-mutation campaign (Codex), search telemetry, frozen benchmarks and branching policies (Codex), reason codes, typed results and twindex inspect (Codex).
• Independent reference checker twindex_ref (Codex): a separate 1-D witness, pair and paving implementation with differential CI on the shipped certificates, the adversarial corpus and 4,000 generated cases. Derived targets are also supported in the shared verifier.

Fixed

• check_certificate accepted a decoded version of 2.0 as 2; it now requires an int. Found by the reference checker.
• Derived-target evaluation is bounded: literals obey the certificate limits, and intermediate values are capped at 16,384 bits before powers and products.

Added (continued)

• Shared problem IR and the validated-forward interface (twindex.ir, twindex.forward): one witness/pair verifier for every pointwise backend.

[0.8.0] - 2026-11-08

Added

• Certified identifiability for polynomial ODEs (Codex): box_ode and paving_ode certificates prove whole parameter boxes incompatible, uniformly in theta. Full-prior pavings give an exact upper bound U, and with a pair, L <= diam <= U. Includes an untrusted SIVIA search, the twindex ode-sivia command, reports and docs/ode-upper.md. Upper bounds extend to elementary (lifted) models through uniform interval enclosures.
• Flagship positive result: Michaelis-Menten Vmax certified to 1/50 <= diam <= 3/128 over the prior [0, 2] (studies/mm_localization.py), shown in the live demo.
• Top-level facade: tw.ODEModel, tw.identify_ode, tw.check and more, loaded lazily so import twindex stays dependency-free.
• Four non-polynomial templates: Michaelis-Menten, Hill repression, Rosenzweig-MacArthur predator-prey and seasonal SIR.
• Elementary ODE models (THEORY Theorem 12). Right-hand sides may use division, negative powers, exp, sin and cos, so Michaelis–Menten, Hill, Monod, Holling, Arrhenius and forced models certify. The checker lifts them deterministically to polynomial systems with proved-faithful auxiliary states. Irrational initial values are exact rational intervals charged to the initial error, and parameter-only reciprocals are exact derived constants. Lifted models get automatic state scales in the solver.

[0.7.0] - 2026-11-08

Added

• Live browser demo (docs/demo/, published at /demo/). It covers the 1978 boarding-school influenza outbreak, a certified twin for every prefix of the data, and the discovery loop. A "check this proof" button runs the exact checker in Pyodide inside a Web Worker. There is a gallery of certificates and drag-and-drop verification. CI replays every shipped certificate in WebAssembly against an expected-verdict manifest (Codex).
• Real-data study (studies/flu_1978.py, studies/flu_1978_next.py): SIR with R0 as a parameter on the BMJ 1978 counts. It uses prospective prefix searches and a compatibility witness for all 14 days. From five counts it certifies the separation of R0 = 2.52 and R0 = 20, and the recorded 27 January count proves both incompatible.
• Per-measurement noise bounds for ODE problems (ODEProblem(noise=...), JSON problem.noise, a CSV noise column). These suit heteroscedastic data such as counts.
• ODE templates (SIR, two-compartment PK, enzyme-complex mass action) with manifests, the twindex.design.design_ode experiment-design wrapper, notebooks/ode_discovery.ipynb, and a field-applicability page (Codex).
• A two-minute tour for newcomers (docs/tour.md).

Changed

• The ODE checker rounds every per-segment upper bound up to a multiple of 2^-96. This is sound, and it keeps certificates with many segments short and fast to check.

[0.6.0] - 2026-11-08

Added (ODE systems and evidence reports)

• Certified polynomial ODE systems (THEORY Theorem 11). Tube validation with exact residual and logarithmic-norm bounds, optional state scales for mixed units, witness_ode/pair_ode JSON certificates, and an exact, closed model-string grammar (twindex.mpoly). This covers mass-action kinetics, SIR/SEIR, pharmacokinetics, Lotka–Volterra, FitzHugh–Nagumo and others.
• Certified example: early-epidemic SIR data at ε = 10⁻³ cannot determine R₀ (twins with R₀ = 2.5 and about 1.72). A pharmacokinetic pair with an elimination-rate gap of 1/10, plus an honest incompatible witness.
• Adaptive untrusted ODE solver with checker-guided refinement, automatic scales and audit-driven pair search (Codex).
• One-call ODE workflow (Codex): twindex.identify_ode(...) and twindex ode model.json data.csv --eps ... --box p=lo,hi --target p --output dir/. The CLI reads exact CSV decimals and writes a certificate and a report. A quickstart lives in examples/ode_quickstart/.
• twindex.measurement.rank_measurement_times (Codex): a heuristic ranking of times that discriminate a certified twin pair, plus an exact test that a future datum would exclude at least one twin.
• twindex report certificate.json --output dir/ (Codex): a Markdown + PNG evidence report for every backend, with an exact replay, a certificate hash, a certified lower bound, and an explicit "no U claimed".

[0.5.0] - 2026-11-08

Added

• Oriented sweep (studies/oriented_sweep.py, Codex). It tightens seven upper bounds: the equispaced sensor layout to D ≤ 204.47 (was 718.75), which proves the ordering equispaced < boundary-clustered < centre-clustered at ε = 10⁻⁵; d = 2 to 26.30 ≤ D ≤ 29.46; and three off-centre generators to U < 175 (was 1000).

• Oriented upper bounds for 14 phase-diagram cells (Codex). The phase figure now shows certified two-sided bounds for every degree, for example 10.16 ≤ D ≤ 34.97 for d = 3 and 2.63 ≤ D ≤ 3.01 for d = 2 at ε = 10⁻⁶ with 17 sensors.

• Final oriented phase round (Codex): 11 more tightened upper bounds (for example d = 2, M = 3, ε = 10⁻⁶: 2.908 ≤ D ≤ 3.349), plus honest non-improvements at ε = 10⁻⁴ for d = 3. Certified finding: for a constant coefficient at large noise the linearised analysis underestimates the ambiguity (646.36 ≤ D ≤ 646.38 vs D_lin = 614.15).

Added (two dimensions)

• 2-D certified checks on the unit square (THEORY Theorem 9): twindex.elliptic2d (Model2, Problem2, check_witness2, check_pair2, 2-D JSON certificates witness2/pair2), exact bivariate polynomials with certified sup bounds (twindex.poly2), and an untrusted 2-D Chebyshev solver with exact candidates (twindex.solver2). Certified 2-D twin pairs work end to end. Sources that are nonzero at a corner put a floor on the residual bound ρ (documented).

Added (any forward model, Codex)

• Numerical audit of arbitrary simulators: twindex.general.audit_model and twindex audit-model module:function. Reports carry a scaled Jacobian, the SVD rank (FD tolerance max(1e-7, diff_step)) and numerically evaluated twins, and are always labeled numerical_only.
• certify_audit: replays audit endpoints against an explicit exact 1-D Problem and keeps a separate certified section. Only a fresh VALID replay counts, and the numerical report is never upgraded.

Added (time-dependent)

• Certified heat-equation checks (THEORY Theorem 10): u_t − u_xx + q(x;θ) f(u) = g with exact boundary and initial data and the barrier ρ·min(t, x(1−x)/2). Adds twindex.parabolic, JSON certificates witness_heat/pair_heat, an untrusted space-time solver (twindex.solver_heat), docs/time-dependent.md, and a replayable certified pair examples/study/heat/twins_heat_pair.json (gap 5, ε = 10⁻³).

Fixed

• 2-D certificate schema: exact sensor and box arity, data must be an array, and the version must be the integer 2.

0.4.0 - 2026-11-08

Added

• Oriented pavings (THEORY Theorem 8): parallelotope leaves θ = o + Aφ with an exact rational matrix A. The checker inverts A exactly, verifies coverage from the interval hull, and decides leaves with affine families in φ. New trusted module twindex/linalg.py.
• Oriented SIVIA (studies/oriented_sivia.py, Codex). It certifies 101.69308 ≤ D(θ₀) ≤ 125.01258 on the full prior for the cubic model (17 sensors, ε = 10⁻⁵), down from the axis-aligned 718.75.
• Monotone contractor pavings (studies/contractor_sivia.py): an honest negative result for the upper bound (see studies/results/contractor/).

0.3.0 - 2026-11-07

Added

• Monotone two-corner boxes (THEORY Lemma 2, Theorem 6, Corollary 7). When g ≥ 0 and the boundary values are nonnegative, the solution is nonincreasing in every parameter, so a whole box is decided by two corner solutions. Around θ̄ = 500 this is about 15× faster than affine families at the same box size. Available as box corners and paving-leaf corners.
• poly.nonneg_status: exact tri-state test of p ≥ 0 on [0, 1].
• Monotone SIVIA (mode="auto"|"monotone"|"affine"|"plain", boundary priority, exact corner caching). It gives the first informative full-prior enclosure: 85.588919 ≤ D(θ₀) ≤ 718.75 (17 sensors, ε = 10⁻⁵, prior [0,1000]⁴).
• Certified identifiability phase diagram over coefficient degree, sensors and noise (80 cells). A constant coefficient is certified identifiable with nearly matching two-sided bounds.
• Paper draft (paper/), compiled with tectonic.

Added after 0.3.0 (unreleased)

• Linearised (Jacobian) baseline across all 80 phase cells: the prediction lies inside the certified [L, U] in every cell.
• LP-seeded twin search: every certified lower bound reaches at least 0.8999 times the linearised width. The headline becomes 101.69308 ≤ D(θ₀) ≤ 718.75.

0.2.1 - 2026-11-07

Added

• "Does your PINN have a twin?" An executed, Colab-ready notebook (notebooks/pinn_twin.ipynb). It trains a small PINN, then exactly certifies twins on the same data. It runs in about 10 seconds on a CPU.
• README: Open in Colab badge, comparison table, results heatmap, proof sketch.

Fixed

• Nonzero boundary values now flow through the numerical side as well: the solver, exact candidates, synthetic data, twin search, audit and affine SIVIA. The checker always handled them.
• The source distribution now includes everything its tests need: the notebook and its evidence, study inputs and figures.
• The notebook test checks the certified claim, independent of floating-point details that vary across platforms.
• Explicit UTF-8 text I/O everywhere, so Windows works.
• More precise wording: both twins fit the same data within ε, and estimators on their own provide no independently checkable proof.
• GitHub Actions updated to current major versions.

0.2.0 - 2026-11-07

Added

• General models. Model(degree, source, nonlinearity): Bernstein coefficients of any degree up to 20, a polynomial source term, and nonlinearities Σ a_m u^m with odd m and a_m ≥ 0. The original problem is V1_MODEL. The theory is generalised accordingly (THEORY §1, §3–§5).
• Certificate format v2 with an explicit problem.model block. Version 1 certificates are still read and checked unchanged.
• Affine candidate families (THEORY Theorem 3′): a box certificate can carry sensitivity polynomials, so that one certificate covers a whole parameter box with residual bound Σ_α h^α ‖R_α‖. Around θ̄ = 500 this certifies boxes with 5× the half-width (625× the volume) of the plain bound.
• twindex audit: certify how well a parameter can be recovered from your own measurements (CSV), noise level, prior and model.
• Model-aware solver, twin search and SIVIA.
• Affine SIVIA: pavings use sensitivity families by default. On the full [0,1000]⁴ prior they now prove most leaves incompatible, but the compatible set is too thin for axis-aligned boxes, so certified upper bounds remain the prior width (see the study). A local example proves L = U = 50 with one affine leaf.
• twindex.fit: certify any callable (a PINN, a solver) as an exact candidate.
• Inhomogeneous boundary values u(0) = α, u(1) = β.
• A redesigned landing page with a hero figure, typeset equations and a results gallery.
• Sensor/noise studies for targets θ₀, θ₁ and θ₂ with certified results, and an executable tutorial.
• mypy --strict on the trusted core, a 90% coverage gate, and CI on Linux (Python 3.10–3.13), macOS and Windows.

0.1.0 - 2026-11-07

First public release.

Added

• Exact trusted core (standard library only, no floating point): rational parsing, exact polynomials, certified Bernstein sup-norm bounds, the model problem, a strict certificate format (v1), and the checker with VALID / INVALID / INCONCLUSIVE verdicts.
• Certificate kinds: witness, pair, box and paving (SIVIA-style two-sided bounds on the target diameter).
• Untrusted search side: a Chebyshev–Newton solver, exact candidate conversion, a local twin search and an adaptive SIVIA driver.
• twindex command line: check, example, search, sivia.
• Ten example certificates covering every kind and every verdict, replayed in CI on Python 3.10–3.13.
• Full proofs in docs/THEORY.md; interface contract in docs/DESIGN.md.