Prove a structural relation between two stored models and record it with its witness. isomorphicTo: an exact canonical-labelling search (the one behind sim_canonical, seeded with exactly what the check compares) finds a place/transition bijection preserving arcs (direction, type, weight, kinetic), place sort, initial marking, capacity, rate or delay and refine.* tags. It does not compare guards, stages, schedules, constraints, non-refine tags (outcome, port.*), data-place types and initial values, objectives, players or asserted classes; those the pair carries are listed as notCompared, so proved is not 'behaves the same'. subnetOf: a bounded embedding search finds an injective, sort-preserving map (token places to token places, data places to data places, transitions to transitions) of the subject's places and transitions into the object's whose arcs among the image are exactly the subject's (initial markings, capacities, rates, delays and tags are not compared). preservesInvariant (invariant-pullback-v1): an induced embedding as subnetOf's along which every P-invariant of the object pulls back to a P-invariant of the subject (the incidence the shared firing rule implies: consuming and producing arcs on token places). Proved carries the map and a cover — per subject transition, rational coefficients of object transitions with the same incidence — which proves it for every invariant at once, plus invariantDimension (0 means vacuous: the object conserves nothing). Embeddings are tried one image at a time (embeddings onto one image differ by a symmetry of the subject, which keeps or breaks the pullback with them), at most 16 images. refines (id-simulation-v1): every firing sequence of the subject from its initial marking, transitions the object has no transition of (by id) dropped as silent, is one of the object from its own; untimed, guards and fixed delays refused (unknown: a delay is a timer whose in-flight markings an atomic step skips), rates not compared, at least one shared transition id required. Proved carries a simulation relation (pairs of markings closed under the subject's firings, at most 4,096; relationPairs counts them, GET /api/lineage/ lists them), which makes the claim unbounded. Neither is declared transitive, so sim_query never closes over them. The answer is proved (with the map, in the caller's direction, or the relation), refuted (exhaustive, with the reason; a refuted refines, or a refuted preservesInvariant where the subject embeds at all, carries refutation, a counterexample sim_check_witness(refutation=…) re-checks: a trace for refines, an invariant per embedding for preservesInvariant, whose list of embeddings is the search's claim; a preservesInvariant refuted because no embedding exists carries none, as a refuted subnetOf carries none) or unknown (a search budget ran out; nothing is recorded, retrying gives the same answer, and unknown is not a no). Needs sign-in (opens OAuth the first time), including with record=false. Costs 3 compute tokens from your account's bucket, or 2 with record=false. Budgets: 1,000,000 refinement steps for both nets' canonical labelling together (isomorphicTo), 2,000,000 embedding steps (subnetOf), 4,000,000 units for elimination, embedding and tests together (preservesInvariant), 20,000,000 firing-rule units and 4,096 pairs (refines); the whole call is also bounded by the 55 s request limit. Writes, only when proved and record is true (the default): one witness, then one relation; isomorphicTo is stored with the smaller id as subject, and storedAs says so when that turned the call round. Otherwise it writes nothing. sim_check_witness re-checks either at any time. With via, sim_prove promotes instead of searching: it takes a structural fact sim_query derived (two to eight stored witnesses composed), re-derives it here from the stored witnesses — every step's witness re-checked against both stored models now, the chain, the composed map's digest, and the composed map checked against the two end models by pkg/morphism — and records the composed map as one direct witness through the same write gate as a search's, so the edge has the same id (one per subject, predicate and object) and is trusted exactly as far. The witness records the derivation as promotedFrom; re-promoting the same derivation writes nothing new (existing: true). A derivation that re-checks invalid or uncheckable is refused and nothing is written; an unknown is never promoted. Costs 2 compute tokens (a derivation re-check plus a store) instead of 3; record=false is refused with via.