Evaluation reads only the cone. Re-evaluating a tape from an environment of leaf values gives, at every node, a value that depends only on the leaves in that node's backward cone in the tape graph: two environments agreeing on the cone's named leaves give the same value at the node. The tape-side counterpart of the pedigree reading.

The accepted match is a weak bisimulation. When acceptance holds for R between a well-formed g and T, the bisimulation is a weak bisimulation, in both directions: every hop of g from a node is matched, from each of the node's components, by a tape step with the same label up to silent steps, and every tape step from a vertex is matched from every node the vertex is related to. The direction the seal consumes follows as a corollary: every path of the tape graph from a component of a node s to a component of a node b projects along R to a path of the value-flow digraph from s to b (reachable_of_tape_path_comps); and every tape edge between two observable vertices realizes one hop of one occurrence of g, with the kinds that occurrence names for its operand and its result (occurrence_of_edge) — so the kinds transported along R change across a tape edge only where an occurrence of g states the change. The tape-side analogue of the lemma that makes the influence probe's false a theorem — so an accepted match is evidence rather than a report.

Contraction makes the bisimulation strong. Under acceptance and well-formedness, R restricted to the observable vertices — node to component — is a strong bisimulation between g and the contracted tape graph: every hop of g is matched by one hyperedge of the contraction and conversely, with no silent step, and once the two node-identity mismatches are quotiented away it is an isomorphism of ordered hypergraphs — compaction, by matching against a hypergraph quotiented by derivation equality; nominal selection, by matching per branch. The contraction itself — a component to every component of its node, a root to every interior vertex of its realization — is a weak bisimulation between the contracted and the actual tape graph (isSWBisimulation_contraction), and the weak bisimulation between g and the tape graph is their composite: the weak bisimulation factors as this strong one composed with the contraction, which is the standard relation between weak and strong bisimulation up to silent-step abstraction. What the strong form deliberately loses is the interior, and the interior is where the numerical side conditions live: the license clause and the adequacy layer keep working on the uncontracted tape graph.

The seal of the computation. Let f be a module written once against the branchless carrier class with fixed-extent iteration, g its provenance hypergraph with c its declared boundary, and T the well-formed tape f records. Suppose (H1) g is well-formed, so that the seal of the module holds of it and, under agreement, of c; (H2) acceptance holds for a match R between g and the computational tape graph of T; and (H3) at a carrier, the value of f at an output o evaluates to the re-evaluation of T at the vertex realizing o. Then for every node o — in particular every produced port — and every vertex r realizing it: two environments that agree on the leaves realizing the influencers of o — the sources g names for it — give the same value at r, hence the same value of f at that carrier (semantic_seal_of_denotes); every leaf in the cone of r, a named input or a baked constant, realizes an influencer of o — every constant the computation uses is one the assumption ledger lists; and every tape edge between observable vertices realizes one hop of one occurrence of g, with the kinds that occurrence names — every kind change in the computation sits under an occurrence the source states. The hypergraph's absence claims become semantic: an input the harvest says cannot reach o provably does not, in the computation, at every carrier the bridge reaches.

Non-vacuity of the seal of the computation. (i) An instance in which acceptance is decided by the kernel and the recorded tape is the accepted graph: the module y = a · b + e at the complex carrier over the recording carrier, whose hypergraph has a product and a same-kind sum and whose tape expands the product to (ac − bd) + (ad + bc)j — four interior vertices the bisimulation is silent on. Acceptance is closed by decide; the strong bisimulation, the contraction, the weak bisimulation, the cone lemma and the seal of the computation are instantiated on it; and the tape the recorder writes, compacted, projects vertex for vertex onto that graph — a runtime check, since the tape's stored tensors are opaque to the kernel — with the recorded values checked against the seal's value clause. (ii) A mutant: a tape that bakes one constant the hypergraph does not list — acceptance refuses it, at the leaf clause the constant clause rests on. (iii) The axiom profiles of the seal of the computation, the cone lemma and the bisimulation theorems, pinned. The worked model's branchless dielectric chain — whose hypergraph is pinned, whose tape is recorded and whose (H3) is a chain of Evaluates lemmas — is the instrument the ledger still prices: the match between its two objects is what the recorder decision fixes.