Skip to content

Evidence reports

Install the plotting extra, then replay a witness or pair certificate into a shareable Markdown report with a PNG plot:

pip install 'twindex[report]'
twindex report examples/study/ode/sir_pair.json --output evidence

Open evidence/report.md. The directory also contains observations.png, the exact certificate.json snapshot, and replay.json. The report records a hash of the copied certificate, Twindex version, assumptions, prior, scalar target, noise bound, exact observations, replay reasons and a certified lower bound L only when a fresh pair replay is VALID. It always states no U claimed. A small L, an incompatible witness or an unsuccessful search proves no uniqueness.

Supported inputs are witness/pair certificates for the 1-D BVP, 2-D elliptic, heat and polynomial ODE backends. Pavings and box claims are outside this first report interface. The CLI uses the checker's exit codes: 0 for VALID, 1 for INVALID or an input error, and 2 for INCONCLUSIVE.

Python can supply a dict, a path, or a callable returning a certificate:

from twindex.report import write_report

replay = write_report("examples/study/ode/pk_pair.json", "pk-evidence")
# Or: write_report(lambda: my_certificate, "evidence")

Optional forward(theta) supplies a numerical measurement vector at each witness. Optional numerical_audit supplies an existing audit_model report. Audit data, prior and noise metadata must match the exact problem after float conversion. Both remain clearly labelled numerical evidence and cannot change the exact replay verdict. Generation and search are explicit preceding steps; the report never runs them implicitly.

ODE plots use physical time, dense piecewise-polynomial trajectories and one subplot per observed quantity. Shaded error tubes appear only for individually VALID witnesses, with exact bounds evaluated from their replay; they may be too thin to see at plot resolution. Titles state compatibility only after VALID replay. A parameter-plane panel shows the twins and target gap when two or more parameters exist; supplied audit points are labelled numerical.

Heat plots use time and group observations by spatial position. The 1-D BVP uses physical x; the 2-D backend retains the observation-index fallback. All plots show data with ±epsilon bars. Candidate samples, numerical forward overlays and audit points remain distinct. Plotting converts exact rationals to floats for display; exact claims live in the replay JSON and copied certificate. The independent checker still requires only Python's standard library.