Twindex design contract (v2)¶

This file is the interface agreement between contributors. Change it only in a reviewed commit, and update every affected module in the same change.

1. The problem Twindex certifies¶

Boundary value problem, for a parameter vector θ = (θ0, …, θd):

−u''(x) + q(x; θ) f(u(x)) = g(x)   on (0, 1),     u(0) = α,  u(1) = β,
q(x; θ) = Σ_{j=0..d} θ_j B_j(x),   B_j(x) = C(d, j) x^j (1 − x)^(d − j),
f(u) = Σ_m a_m u^m   (every m odd, every a_m ≥ 0),   g a polynomial.

A model (twindex.model.Model) fixes d (0..20), the source g (degree ≤ 50), the nonlinearity terms (m, a_m) (odd m in 1..15, a_m ≥ 0) and the boundary values (α, β) (default (0, 0)). The default model, V1_MODEL, is the original problem: d = 3, f(u) = u³, g = 1. Odd powers with nonnegative coefficients make f nondecreasing, which is exactly what the barrier theorem needs.

A problem instance fixes:

field	meaning
`sensors`	points `x_i` in the open interval (0, 1)
`data`	measured values `y_i`, one per sensor
`epsilon`	noise bound `ε > 0` (sup norm over sensors)
`box`	prior box `Θ = Π [lo_j, hi_j]` (`d + 1` intervals), `0 ≤ lo_j ≤ hi_j`
`target`	index `k` of the scalar target `Q(θ) = θ_k` (default `0`)
`model`	the `Model` (default `V1_MODEL`)

Data-compatible set: C_y = { θ ∈ Θ : max_i |u_θ(x_i) − y_i| ≤ ε }. Target diameter: D_Q(y) = sup_{θ, θ' ∈ C_y} |θ_k − θ'_k|.

Every number in a problem or certificate is an exact rational. Floating point never enters the checker.

2. The mathematics the checker relies on¶

See docs/THEORY.md for full proofs. Summary:

Existence and uniqueness. If q ≥ 0 on [0, 1] the problem has exactly one classical solution u_θ.
Barrier bound. Let p be a polynomial with p(0) = α, p(1) = β and residual r = −p'' + q f(p) − g. If |r(x)| ≤ ρ on [0, 1] then |u_θ(x) − p(x)| ≤ ρ x(1 − x)/2 for every x in [0, 1].
Box extension. For a fixed p, r(x; θ) is affine in θ. For a box B = θc ± h (with B ⊆ Θ and lo ≥ 0), sup_{x, θ ∈ B} |r| ≤ sup_x |r(x; θc)| + Σ_j h_j sup_x |B_j(x) f(p(x))|.
Sup bounds. A polynomial's sup norm on [0, 1] is bounded above by the largest absolute Bernstein coefficient, refined by exact de Casteljau subdivision at dyadic points.

3. Modules and trust boundary¶

The current module map, the trusted computing base, and the certificate-kind → theorem → trusted-code table are maintained in architecture.md. The machine-readable list of trusted modules is twindex/_trusted.py.

Trust boundary. Only trusted modules can make a verdict VALID. They use the standard library only (no numpy, no floats), and the import-boundary test enforces this. Everything else is untrusted: it may use floats freely, and its only job is to produce certificates that the core then checks. A bug in untrusted code can cause INCONCLUSIVE results, never a wrong VALID.

4. Public API of the trusted core¶

# rational.py
def parse_rational(s: str | int) -> Fraction        # "3/7", "-2", "0.125" (finite decimal) ; rejects floats, nan, inf
def format_rational(q: Fraction) -> str              # canonical "a/b" or "a"

# poly.py
class Poly:                                          # immutable, monomial basis, Fraction coefficients
    coeffs: tuple[Fraction, ...]                     # coeffs[k] multiplies x**k; trailing zeros stripped
    def __init__(self, coeffs: Iterable[Fraction | int | str])
    def degree(self) -> int                          # -1 for the zero polynomial
    def __call__(self, x: Fraction) -> Fraction
    def __add__, __sub__, __mul__, __neg__, __pow__(n: int), __eq__
    def scale(self, c) -> Poly
    def deriv(self, k: int = 1) -> Poly
    @staticmethod
    def x() -> Poly ; def const(c) -> Poly
def bernstein_coeffs(p: Poly, n: int | None = None) -> list[Fraction]   # degree-n Bernstein coefficients on [0,1], n >= deg p
def sup_abs_bound(p: Poly, depth: int = 6) -> Fraction                   # certified upper bound of max_{[0,1]} |p|

# model.py
def bernstein_basis(d: int) -> tuple[Poly, ...]
@dataclass(frozen=True)
class Model:
    degree: int = 3
    source: Poly = Poly([1])
    nonlinearity: tuple[tuple[int, Fraction], ...] = ((3, Fraction(1)),)
    boundary: tuple[Fraction, Fraction] = (0, 0)             # u(0), u(1); optional in JSON
    num_params: int                                          # property: degree + 1
    basis: tuple[Poly, ...]                                  # Bernstein basis of `degree`
    def q(self, theta) -> Poly ; def f_of(self, p: Poly) -> Poly
    def residual(self, p: Poly, theta) -> Poly               # −p'' + q f(p) − g
V1_MODEL: Model                                              # d = 3, f = u³, g = 1
NUM_PARAMS, BERNSTEIN_Q, q_poly, residual                    # v1-model compatibility aliases
def barrier(x: Fraction) -> Fraction                         # x(1−x)/2
@dataclass(frozen=True)
class Problem:
    sensors: tuple[Fraction, ...]
    data: tuple[Fraction, ...]
    epsilon: Fraction
    box: tuple[tuple[Fraction, Fraction], ...]               # length model.num_params
    target: int = 0
    model: Model = V1_MODEL

# checker.py
class Verdict(Enum): VALID, INVALID, INCONCLUSIVE
@dataclass(frozen=True)
class Report:
    verdict: Verdict
    reasons: tuple[str, ...]          # human-readable, one per failed or decisive check
    details: dict                     # rho, sensor slacks, gap ... as canonical strings
def check_witness(problem, theta, p, depth=6) -> Report       # VALID: θ ∈ C_y proved
def check_pair(problem, w1, w2, claimed_gap, depth=6) -> Report
def check_box(problem, center, half_width, p, depth=6) -> Report   # VALID: B ⊆ C_y ; INVALID: B ∩ C_y = ∅ proved
def check_certificate(cert: dict, depth=6) -> Report          # dispatch on cert["kind"]

Reason codes. Every Report also carries code: str, a stable machine-readable reason serialized by to_dict(), for example VALID_PROVED, INVALID_MALFORMED, INVALID_FALSE_CLAIM or INCONCLUSIVE_INSUFFICIENT_BOUND (the full list is in results.md). Codes are reporting metadata only: they are derived from the verdict and never participate in a proof decision. The verdict semantics of §5 are unchanged.

5. Verdict semantics (binding)¶

VALID — every inequality of the claim was proved in exact arithmetic.
INVALID — the certificate is malformed, violates a hypothesis (e.g. p(0) ≠ 0, θ ∉ Θ, lo < 0), states a false exact fact (e.g. a claimed gap larger than the exact |θ_k − θ'_k|), or the checker proved the claim false (e.g. some sensor has |p(x_i) − y_i| − s_i > ε, which proves θ ∉ C_y).
INCONCLUSIVE — the certificate is well formed and not disproved, but the sufficient inequalities did not close (e.g. ρ too large). A larger depth or a better candidate may close it.

A failed sufficient condition is INCONCLUSIVE, never INVALID.

6. Certificate format v2 (JSON)¶

All numbers are JSON strings holding exact rationals ("1/1000", "500"). The library writes version 2. It also reads version 1, which is identical except that problem has no model key and the model is V1_MODEL. In version 2, problem.model is required.

{
  "format": "twindex-certificate",
  "version": 2,
  "kind": "pair",
  "problem": {
    "sensors": ["1/6", "1/3", "1/2", "2/3", "5/6"],
    "data":    ["...", "...", "...", "...", "..."],
    "epsilon": "1/1000",
    "box": [["0","1000"], ["0","1000"], ["0","1000"], ["0","1000"]],
    "target": 0,
    "model": {
      "coefficient_degree": 3,
      "source": ["1"],
      "nonlinearity": [{"power": 3, "coefficient": "1"}],
      "boundary": ["0", "0"]
    }
  },
  "witnesses": [
    {"theta": ["500","500","500","500"], "p": ["0", "c1", "c2", "..."]},
    {"theta": ["...", "...", "...", "..."], "p": ["0", "..."]}
  ],
  "claim": {"gap": "..."},
  "provenance": {"generator": "twindex.search 0.1.0", "notes": "free text, ignored by the checker"}
}

kind ∈ {"witness", "pair", "box", "paving"}. Top-level keys allowed per kind: witness {witnesses}, pair {witnesses, claim}, box {box, claim}, paving {candidates, paving, claim}; plus format, version, kind, problem, and optional provenance for all kinds.
p lists monomial coefficients, constant term first.
kind: "witness" has exactly one witness and no claim.
kind: "pair": claim.gap is a lower bound the checker verifies: |θ_k − θ'_k| ≥ gap.
kind: "box": {"center": [...], "half_width": [...], "p": [...], "sensitivities"?: [[...], ...]} and claim.status ∈ {"inside", "outside"}. The optional sensitivities (one polynomial per parameter, each vanishing at 0 and 1) turn the candidate into the affine family p + Σ_j Δ_j s_j of THEORY Theorem 3′. Instead of p, a box may give "corners": [p_lo, p_hi], candidates at the lower and upper corners. The box is then decided by THEORY Corollary 7 (monotone two-corner bound). This requires α, β ≥ 0 and a source certified g ≥ 0: INVALID if disproved, INCONCLUSIVE if undecided. A box has exactly one of p and corners.
kind: "paving" (SIVIA output): a bisection tree over the prior box Θ. Coverage holds by construction, because every split partitions its parent box.

"candidates": [["0", "c1", "..."], ["0", "..."]],
"paving": {"split": 0, "at": "500",
           "children": [ {"status": "outside", "p": 0},
                         {"split": 2, "at": "750", "children": [
                             {"status": "inside", "p": 1},
                             {"status": "unresolved"} ]} ]},
"claim": {"lower": "120", "upper": "180"}

A node is either a split {"split": j, "at": m, "children": [left, right]} with lo_j < m < hi_j for the node's box (the left child gets θ_j ∈ [lo_j, m], the right child [m, hi_j]), or a leaf {"status": s, "p": index, "s"?: [indices]} with s ∈ {"inside", "outside", "unresolved"}. p indexes candidates; it is required for inside/outside and forbidden for unresolved. The optional s lists one candidate index per parameter: the leaf's affine-family sensitivities (Theorem 3′), centred at the leaf's centre. Alternatively a classified leaf may give "corners": [i_lo, i_hi] (and no p/s): the monotone two-corner bound (Corollary 7) at the leaf's lower and upper corners.
The checker re-verifies every inside and outside leaf with check_box. Let In be the inside leaves and Out⁺ the inside plus unresolved leaves. Certified bounds on the target coordinate k are L = max_{B∈In} hi_k(B) − min_{B∈In} lo_k(B) (any two points of inside leaves are compatible) and U = max_{B∈Out⁺} hi_k(B) − min_{B∈Out⁺} lo_k(B) (every compatible θ lies in some leaf of Out⁺). U = 0 when Out⁺ is empty, and then C_y = ∅ is proved.
claim.lower (optional; requires a nonempty In) and claim.upper (required) state the bounds this paving proves. The verdict is VALID iff every leaf verifies and claim.lower ≤ L and claim.upper ≥ U. A leaf proved wrong, or a claim outside [L, U], gives INVALID. A leaf the checker cannot decide gives INCONCLUSIVE.
Limits (to bound checking cost): at most 200 000 nodes, tree depth at most 200.
Oriented pavings (THEORY Theorem 8): an optional top-level "transform": {"origin": [...], "matrix": [[...], ...], "root": [[lo, hi], ...]} with θ = origin + matrix · φ. The tree is then over the φ root box. The checker verifies, exactly, that the root covers the interval hull of matrix⁻¹(Θ − origin) (the matrix must be invertible). In this mode: outside leaves may omit the candidate when their parallelotope's interval hull misses Θ; candidate leaves use affine families in φ; inside leaves must have a hull inside Θ; corners leaves are not allowed. A candidate-free outside leaf in an ordinary paving is INVALID.
Unknown top-level keys → INVALID (catch typos). provenance is free-form.

6.1 Two-dimensional certificates (`witness2`, `pair2`)¶

The problem −Δu + q f(u) = g on (0,1)² with u = 0 on the boundary (THEORY §7.1) uses its own kinds, parsed by twindex.elliptic2d. twindex.checker.check_certificate and twindex check dispatch on the kind:

{"format": "twindex-certificate", "version": 2, "kind": "pair2",
 "problem": {"sensors": [["1/4","1/4"], ...], "data": [...], "epsilon": "1/100",
             "box": [["0","1000"], ...], "target": 0,
             "model": {"degree_x": 1, "degree_y": 1,
                       "source": [["0","0",...], ...],
                       "nonlinearity": [{"power": 3, "coefficient": "1"}]}},
 "witnesses": [{"theta": [...], "p": [[...], ...]}, {...}],
 "claim": {"gap": "60"}}

Polynomials are coefficient grids: grid[i][j] multiplies xⁱ yʲ, with degree at most 120 per variable. The coefficient q uses the tensor Bernstein basis, with θ in row-major order over (j, k). Each candidate must vanish exactly on the boundary. The verdict rules are those of §5.

6.2 Heat certificates (`witness_heat`, `pair_heat`)¶

The semilinear heat problem of THEORY §7.2 is parsed by twindex.parabolic. check_certificate and twindex check dispatch on these kinds. The envelope is format: "twindex-certificate", integer version: 2, kind, problem, witnesses, optional object provenance, and (only for pairs) claim: {"gap": "..."}. Unknown keys are rejected at each schema object. problem contains sensors (arrays of exactly [x, t]), data, epsilon, box (exactly [lo, hi] per parameter), optional integer target (default 0), and required model:

{"coefficient_degree": 3,
 "source": [["0"]],
 "initial": ["0", "1", "0", "-5/3", "0", "1", "-1/3"],
 "nonlinearity": [{"power": 3, "coefficient": "1"}]}

coefficient_degree is an integer in 0..20. source[i][j] and witness p[i][j] multiply x^i t^j (degree at most 120 per variable). initial lists constant-first coefficients in x, degree at most 120, and must vanish at both ends. Every rational is a string; floats and booleans are rejected. Nonlinearity powers are odd integers in 1..15 with distinct powers and nonnegative coefficients. Sensors satisfy 0 < x < 1, 0 < t <= 1. Other problem constraints match §1. A witness is {"theta": [...], "p": [[...], ...]}, with exactly degree + 1 parameters. witness_heat has exactly one witness and no claim; pair_heat has exactly two witnesses and a nonnegative rational gap. The candidate must match both lateral boundary values and the initial polynomial exactly. Verdicts follow §5; pairs prove only lower bounds. No heat boxes or pavings are supported.

6.3 ODE certificates (`witness_ode`, `pair_ode`)¶

These certificates use the same envelope as above (format, integer version 2, kind, problem, witnesses, plus claim for pairs and an optional provenance object). They are checked by Theorem 11 (THEORY §7.3).

"problem": {
  "model": {
    "states": ["S", "I"], "params": ["beta", "gamma"],
    "rhs": ["-beta*S*I", "beta*S*I - gamma*I"],
    "initial": ["99/100", "1/100"],
    "observables": {"I": "I"}
  },
  "measurements": [["1/2", "I", "<y>"], ...],
  "epsilon": "1/1000",
  "box": [["0", "2"], ["0", "1"]],
  "target": 0
},
"witnesses": [{
  "theta": ["1/2", "1/5"],
  "breaks": ["0", "1", "2", "3", "4"],
  "pieces": [[["<tau^0>", "<tau^1>", ...], [...]], ...],
  "delta": "1/100000",
  "scales": ["1", "1"]
}]

Model strings. These use the closed grammar of twindex/mpoly.py: numbers, names, + - *, division by a nonzero constant, and integer powers 0..64. Decimal literals are exact, and the name t is reserved for time.
rhs[i] may use t, the states and the parameters.
initial[i] may use only the parameters. An unknown initial value is modelled as a parameter; there is no separate initial-value noise.
Observables must be affine in the states.
Elementary models. rhs strings may also use / by any expression, negative integer powers, exp, sin and cos (THEORY §7.4). The checker lifts them deterministically to a polynomial system. Witness pieces then list one polynomial per lifted state: the user's states first, then the auxiliary states in the checker's creation order (__inv1, __exp2, ...). model.states lists the user's states only, and user names may not start with __ or be exp, sin or cos.
Derived targets. A pair_ode claim may carry "target_expr", a rational expression in the parameters such as "beta/gamma", using + − *, / and integer powers. The checker evaluates it exactly at both witnesses and requires |Q(θ₁) − Q(θ₂)| ≥ gap. A division by zero, an unknown name or an unsupported syntax makes the certificate INVALID. Without it, the target is the coordinate problem.target.
Noise. An optional problem.noise array gives one positive bound per measurement, in measurement order, for heteroscedastic data such as counts. Measurement i is then compared with noise[i] instead of epsilon; the epsilon field is still required and is used only where no per-measurement bound applies.
Measurements are [t, observable, y] with t ≥ 0. The horizon is the largest t, and breaks must start at 0, increase strictly and reach at least the horizon.
Pieces. pieces[k][i] holds the monomial coefficients of state i on segment k in the local variable τ = (t − b_k)/h_k ∈ [0, 1]. A measurement at a break uses the left segment.
Tube radius and scales. delta > 0 is the tube radius in the weighted max norm max_i |e_i|/scales_i. scales is optional, defaults to all ones, and every entry must be positive.
Limits: at most 50 states, 200 parameters, 2000 segments, piece degree 120, 10⁵ measurements, and expression length 20000. A polynomial may have at most 20000 terms, and total degree is capped at 64.

Verdicts follow §5:

INVALID for any schema violation, theta outside the box, a wrong arity, a candidate that is too short, or a measurement proved incompatible.
INCONCLUSIVE when μ⁺h ≥ 1 on some segment, when the error bound fails to stay strictly inside the tube, or when a measurement cannot be decided.
VALID otherwise.

7. Engineering rules¶

Python ≥ 3.10. Trusted core: standard library only. numpy only in untrusted modules (pip install twindex[search]).
ruff check and pytest must pass before any merge to main.
Every bug fix gets a regression test.
No float literal ever reaches a Fraction constructor in the core (parse_rational rejects Python floats).

6.4 ODE exclusion and upper bounds (`box_ode`, `paving_ode`)¶

These version-2 certificates reuse the exact problem object of §6.3. They support polynomial models and the elementary lifts of §6.3 and THEORY §7.4. Candidates are independent of parameters and contain the §6.3 witness fields except theta. The theorem of §6.3 is applied uniformly over a closed parameter box: initial error, residual and state Jacobian bounds cover every parameter in the box. Parameter deviations are expanded about the box midpoint, with absolute coefficient bounds and exact Bernstein bounds in time. Parameters are constant, so the Jacobian differentiates only states. The same strict tube and jump checks apply.

Lifted models. For a lifted model, the auxiliary states take part in the candidate and the tube exactly as for witnesses. The changes are:

Every initial value, of user states and of auxiliary states, is enclosed by an exact interval that covers the whole leaf box. The farthest endpoint deviation is charged to E₀.
A parameter-only reciprocal 1/D(θ) is enclosed over the box and treated as an independent constant pseudo-parameter. This is an over-approximation: it is never a state, never differentiated, and never a paving axis.
A box whose denominator interval contains zero, or whose initial argument is outside the supported range, stays INCONCLUSIVE. It is never excluded.

Exclusion is then proved by the per-θ lifting theorem (THEORY Theorem 12) together with the uniform tube theorem. The JSON schema is unchanged.

A box_ode has problem, box (one exact [lo,hi] per parameter, contained in the prior), candidate, and claim: {"status": "outside"}. VALID proves that this entire box contains no compatible parameter: some measurement has |obs(p)-y| - error > noise[i] uniformly. Equality does not exclude. Failed sufficient bounds are INCONCLUSIVE. Malformed certificates are INVALID.

A paving_ode has problem, candidates (an array of candidate objects), paving, and claim: {"upper": "..."}. Its tree partitions the entire prior. A split is exactly {"split": j, "at": "...", "children": [left,right]}; j is a non-boolean integer and the split is strictly interior. Leaves are exactly {"status": "outside", "candidate": i} or {"status": "unresolved"}. Indices are non-boolean integers into candidates. Each outside leaf must replay VALID as an exclusion. Unresolved leaves are retained without claiming compatibility. Limits: 200000 nodes, depth 200, and 10000 candidates, each subject to §6.3 limits. Uniform expansion is limited to 20000 pre-collection terms per polynomial; exceeding it is INCONCLUSIVE, never an exclusion.

The checker reports the target-coordinate hull of all unresolved leaves and its width U; claim.upper must be nonnegative and at least U. An all-outside tree proves emptiness, reported separately with null hull and U=0. A nonempty outer hull does not prove a nonempty compatible set. Lower bounds require a separate certified pair on the identical problem. No structural-identifiability claim follows. Unknown fields, altered coverage, and false exact upper claims are INVALID. Optional object provenance is ignored as in §6.3.