Architecture and trust boundary

Twindex separates untrusted search from a small trusted checker. Search code may use floating point, heuristics and third-party libraries. It only proposes certificates. A claim counts as proved only when the trusted checker replays it and returns VALID. This page lists exactly which code can produce VALID, which theorem each certificate kind relies on, and how the checker fails closed.

The trusted computing base

The trusted modules are listed in twindex/_trusted.py, which is the single source of truth. CI type-checks exactly that list with mypy --strict, and tests/test_trust_boundary.py proves two things:

• Every import in a trusted module, including imports inside functions, is either a listed standard-library module or another trusted module.
• Replaying the shipped certificates never loads numpy, scipy or matplotlib.

module	role
rational	exact rational parsing and formatting; floats are rejected
poly, poly2	exact polynomials; Bernstein enclosures with de Casteljau subdivision (THEORY §6)
mpoly	multivariate exact polynomials and the closed expression grammar
linalg	exact rational linear algebra for oriented pavings
model, affine, certificate	1-D problem definition, residuals, barrier bounds, affine families, certificate schema
checker	verdicts for 1-D certificates and dispatch for all other kinds
elliptic2d, parabolic	2-D elliptic and heat-equation witnesses and pairs
elementary	certified polynomialization of elementary ODE right-hand sides
ode, ode_bounds	ODE witnesses and pairs; ODE box exclusion and pavings
ir, forward	shared problem objects, and the backend-agnostic witness/pair verifier

Everything else is untrusted:

• Solvers and search: solver*, search*, candidate, fit, identify, design, measurement.
• Adapters and output: general (numerical audits), report, cli, audit.
• The browser demo.

A bug in untrusted code can waste time or produce INCONCLUSIVE, but it cannot produce a wrong VALID.

Certificate kinds, theorems and checking code

kind	proves	theorem (docs/THEORY.md)	trusted path
witness, pair	one or two compatible parameters for the 1-D BVP	existence and barrier bound, Theorems 1–2	checker → model, poly
box (affine or corners)	a parameter box inside or outside the compatible set	Theorems 3, 3′, 6, Cor. 7	checker → affine, model, poly
paving (axis or oriented)	two-sided bounds L ≤ diam ≤ U for the 1-D BVP	Theorems 4, 5, 8	checker → affine, linalg, poly
witness2, pair2	2-D elliptic compatibility	Theorem 9	checker → elliptic2d → poly2
witness_heat, pair_heat	heat-equation compatibility	Theorem 10	checker → parabolic → poly2
witness_ode, pair_ode	ODE compatibility, polynomial or lifted	Theorems 11, 12	checker → ode → mpoly, elementary, poly
box_ode, paving_ode	ODE parameter-box exclusion; full-prior upper bound U	Theorem 11 applied uniformly, DESIGN §6.4	checker → ode_bounds → ode, elementary

The validated-forward interface

twindex.forward writes the witness and pair semantics once. A pointwise backend proves, for one parameter value and its candidate solution, that each observation's prediction lies in an exact interval [c − r, c + r]. The backend owns its theorem and every precondition: boundary data, existence, and prior membership. The shared verifier then applies the same rules to every backend:

• compatible when |c − y| + r ≤ b;
• proved incompatible when |c − y| − r > b (strict);
• for a pair, an exact gap check on the target.

It rejects a backend that does not enclose exactly the declared observations.

Two backends implement it today: PDE1DBackend (Theorem 2) and ODEBackend (Theorems 11 and 12). tests/test_forward.py shows that the shared verifier gives the native verdict on all 73 shipped and adversarial 1-D and ODE witness and pair certificates, across all three verdicts. A new certified forward model only has to supply enclosures.

Backends are part of the trust boundary

The shared verifier proves only that the decision follows from the enclosures. It cannot check that a backend's enclosures are true. A backend therefore belongs to the trusted computing base exactly as its theorem does: it must be listed in twindex/_trusted.py, use only exact arithmetic, and pass proof review. A third-party object implementing PointwiseBackend is not trusted merely because it satisfies the protocol, and its verdicts must not be presented as Twindex certificates.

Proof obligations the checker discharges

For every kind, the checker itself recomputes, in exact arithmetic:

1. Input grammar. Strict schema validation, string rationals only (floats rejected), closed expression grammar, and size limits.
2. Data. Boundary and initial conditions are matched exactly, or enclosed by exact intervals for irrational initial values.
3. Residual bounds. Bernstein enclosures, together with log-norm bounds over the tube for ODEs.
4. Transfer. The barrier or tube theorem moves each residual bound to an error bound on the true solution, including existence and continuation for ODEs.
5. Measurement decisions. At each measurement, deviation + error ≤ ε proves compatibility, and deviation − error > ε (strict) proves incompatibility.
6. Claim. The pair gap, the paving's coverage of the whole prior, and the hull and U are recomputed from the leaves, never read from the certificate.

Failing closed

The checker never turns a failure into VALID:

• Malformed input: unknown fields, floats, wrong arity, unsupported syntax and oversized input give INVALID.
• Insufficient bounds: a tube that does not close, μh ≥ 1, an undecidable initial value, an expansion over budget, or a measurement too close to call give INCONCLUSIVE.
• False claims: a measurement proved incompatible, an overstated gap, or incomplete coverage give INVALID.

INCONCLUSIVE never means "probably true" or "probably false". It means nothing was proved.

What a VALID certificate does not say

A certificate is exactly as strong as its stated assumptions: the model equations, the prior, the noise bounds and the observation map. It does not show that the model describes nature, that the noise bound is right, or (for a pair) how wide the true range is. A failed search proves nothing. See Known limitations.

Independent reference checker

twindex_ref/ is a second, deliberately different implementation for 1-D witness, pair and axis-paving certificates:

• it has its own rational and schema parsing;
• it stores polynomials as sparse exponent maps;
• it bounds polynomials with exact interval Horner on a uniform grid;
• it keeps its own ledger of paving leaves.

It imports nothing from twindex, which a test enforces. tests/test_reference_checker.py and a CI workflow run both checkers on every shipped certificate, on the adversarial corpus and on 4,000 generated cases. The reference checker may be weaker, returning INCONCLUSIVE where the main checker returns VALID. The two must never disagree in the opposite VALID/INVALID direction, and none have. Both still rely on the same barrier theorem, so this cross-checks the implementation, not the theorem. The differential testing has already found one real schema bug: a decoded version 2.0 was accepted.

Review rules

Any change to a trusted module, to the manifest, or to a certificate schema is a trust-boundary change. Such a change needs:

• a proof-impact note in the commit message;
• adversarial tests, including near-miss cases at strict inequalities;
• an independent review before release.

Since v0.3 every trusted change in this repository has been reviewed adversarially by a second agent (Codex reviews Claude Code and vice versa), and review notes are kept in docs/*_REVIEW.md. This is not a substitute for review by an independent human expert, which is still pending.