Re-check a stored structural witness against both stored models with the independent checker (pkg/morphism), which does no search. Given a structural edge's id, checks every witness of that edge; an edge with none answers unwitnessed (unproven, not disproved). Verdicts: valid, invalid (the map is not a morphism of the stored models), or uncheckable (a model was deleted, a net is malformed, or the predicate is now checked under a newer definition). Public: no sign-in. A witness or edge id is free (no compute tokens). With derivation (from sim_query): re-checks every step's witness, the chain, the composed map's digest and the composed map against both end models, and answers {verdict, reason, hops} (the body POST /api/derivation/check returns); a derivation naming a definition other than the predicate's current one is uncheckable; costs 1 compute token. With reach (a sim_reach answer): replays a trace through metamodel.Enabled/Fire and the guards, or re-checks an invariant witness against the stored model, answering {verdict, reason}; from and to are held to the scenario caps (1,000,000 per place, 4,000,000 in total), and a replay is priced before its first firing and is uncheckable over 200,000,000 work units; an exhaustive no is uncheckable (re-run sim_reach); an unknown answer is refused; costs 1 compute token (POST /api/reach/check). With reach on a system's answer, via is re-checked whole with it: the system is stored and holds the net, every other model has exactly one embedding, each embedding's witness or derivation re-checks valid now, and any translation of component places follows them. With reachResult (the result id sim_reach returns): re-checks a stored answer end to end — the record (its bytes hash to its id, its stored question asks what the answer answers under the budgets it records, and over names what it rests on), via as above, and the witness — answering {verdict, reason, parts, answer, currency}; an unknown answer stays unknown (its witness part is uncheckable, never a no); currency says whether this server would compute the same result (definition, budgets, registry, view, every model still stored) and lists superseded models without flipping current; costs 1 compute token (POST /api/reach/check with {"result": …}, or GET /api/lineage/). With refutation (a refuted sim_prove answer's refutation, ROADMAP.md Phase 12i): re-checks its counterexample against both stored models with pkg/morphism — a refines trace replayed through the shared firing rule on both nets, or for preservesInvariant each embedding re-checked as an induced embedding, its invariant re-checked as a P-invariant of the object (y·C = 0 for every transition) and its pullback shown to break at the subject transition named (that the list holds every embedding is the search's claim and is not re-checked) — answering {verdict, reason}; costs 1 compute token (POST /api/refutation/check). A preservesInvariant or refines witness id re-checks its cover or simulation relation the same way (free, bounded: at most 4,096 cover terms, or 4,096 pairs and 20,000,000 firing-rule units). Give exactly one of id, derivation, reach, reachResult or refutation. Writes nothing.