The bridge that replay cannot finish

The tempting intuition is simple. If two systems return the same answer often enough, perhaps they are the same system written differently. That intuition is sound only when the tested answers determine every relation that matters. Usually they do not. A finite benchmark observes selected inputs, selected outputs and a chosen time horizon. It leaves internal branching, untested interventions, authority changes and information loss outside the frame.

Suppose a source system has states a, b and c, while a target has states x, y and z. A mapping F tells us which target state represents each source state. A proof then asks whether relevant source relations survive after applying F. Without that mapping, “the systems are similar” is not wrong so much as unevaluable. There is no specified object on which a proof obligation can land.

The word “equivalent” hides several grades of claim. A lexical resemblance might generate a question. Output agreement can support a regression test. A homomorphism preserves selected operations in one direction. An embedding additionally prevents relevant distinctions from being collapsed. Bisimulation matches possible moves in both directions. Isomorphism or category equivalence supplies a suitable form of reconstruction. These are not ceremonial labels. Each grade licenses a different decision.

flowchart LR
  A["The bridge that replay cannot<br/>finish"] --> B["Write down what must survive"]
  B --> C["Choose the right return ticket"]
  C --> D["Put the claim through a<br/>transport gate"]
  D -. "re-test" .-> A
  classDef first fill:#0a1424,stroke:#087A98,stroke-width:2px,color:#e6f3ff
  classDef step fill:#0a1424,stroke:#3f7da0,stroke-width:1px,color:#e6f3ff
  class A first
  class B,C,D step

Write down what must survive

A proof begins by freezing two signatures. For present purposes, describe a source structure as 𝒮 = (O_S, R_S, Ω_S, ≈_S, I_S). The target 𝒯 has corresponding components. The notation is only useful if each symbol names something concrete.

• O contains the typed objects or states, such as incidents, resources, assignments and credentials.
• R contains relations, such as “authorised for”, “precedes”, “depends on” or “can transition to”.
• Ω contains operations and their composition, such as assign, cancel, merge, add or compile.
• ≈ states what counts as equality or observational indistinguishability. Bitwise equality, equal traces and equal final balances are different contracts.
• I names the admissible interventions or contexts under which the claim must continue to hold.

A mapping F translates source objects into target objects and, where required, source actions into target actions. For an n-ary operation op, the central preservation question is whether the two paths below meet.

Individual relations are not enough when the system can compose actions. Category theory makes this obligation explicit through identity and composition laws. Translating an identity action should behave like the identity action on the translated object. Translating a composite should agree with composing the translated actions:

The dispatch case failed the second law. “Assign, then cancel” had the same final recommendation as “do nothing”, but it did not have the same authority history. Testing assign and cancel separately would still miss the defect if the target combined them through a stale queue. The proof obligation must range over the compositions that can occur in the real environment, including interruption, retry, rollback and concurrent update where those are permitted.

Preservation is only half of a strong structural claim. For a binary relation R, preservation has the form R_S(x,y) ⇒ R_T(F(x),F(y)). Reflection reverses the implication for relations among mapped objects. If the target says two mapped states are adjacent, authorised or equal, reflection asks whether the corresponding source relation really held. Reflection blocks a target from inventing distinctions or permissions that the source did not license.

Different disciplines encode this reverse demand differently. A faithful functor prevents distinct morphisms from collapsing. A full functor ensures that every target morphism between mapped objects comes from a source morphism. A graph embedding preserves and reflects adjacency on its image. A bisimulation matches possible transitions in both directions. The shared mechanism is not the terminology. It is a reverse challenge to a forward story.

When the inverse is coherent rather than literal

Strict isomorphism asks for maps F and G whose two composites are literally the respective identity maps. Category equivalence relaxes this. It asks for functors in both directions and natural isomorphisms connecting GF and FG to the identity functors. Informally, translate and reconstruct, then show that the reconstructed object is coherently isomorphic to the original across every allowed morphism. It need not be the same token or representation.

A standard characterisation says that a functor is an equivalence when it is full, faithful and essentially surjective, subject to the usual set-theoretic assumptions for the converse construction. Fullness covers target morphisms between represented objects. Faithfulness prevents morphism collapse. Essential surjectivity says every target object is isomorphic to one in the image. Riehl’s treatment makes the crucial point visible: equivalence concerns preserved organisation, not objectwise equality [1]. Fong and Spivak show how this compositional viewpoint becomes a practical language across systems [2].

Naturality is the coherence check that stops the return map from being a collection of bespoke repairs. Imagine that each source object can be reconstructed from its target image, but the reconstruction chosen after one allowed transformation differs from the reconstruction chosen before it. Object by object, every case appears recoverable. Across the network of transformations, the choices contradict one another. A natural isomorphism requires the reconstruction to commute with those transformations, so the witness works as one system rather than as many unrelated lookup tables.

Even this strong formal result does not settle every interpretive question. Two categories may be equivalent after important physical, semantic or modal structure has been omitted from their objects and morphisms. Philosophers of scientific theories therefore distinguish several strengths of formal equivalence and debate which structure should count as interpretation-preserving [10] [11]. The proof can be impeccable inside a category that was too weak for the decision.

Choose the right return ticket

“Show the inverse” is good discipline, but not every valid transport needs a strict inverse. Optimising compilers erase names and rearrange instructions. Causal abstractions intentionally compress microstates. Simulations may guarantee that every source move has an acceptable target move without promising the reverse. The proof must therefore name the return ticket it actually offers.

Causal structure requires intervention transport

Observational agreement is especially weak when the claim concerns cause. Imagine two binary models that always produce X = Y. In Model A, X causes Y. In Model B, Y causes X. Passive observations cannot distinguish them. Set X to zero while holding the mechanism for Y fixed. Model A propagates the change to Y; Model B need not.

Work on causal model abstraction formalises this demand. Exact transformations relate low-level and high-level state spaces while translating allowed interventions. Applying a low-level intervention and then abstracting its outcome should agree with applying the translated high-level intervention directly [3] [4]. Later treatments relax exactness by adding an explicit metric and error measure rather than quietly replacing equality with “close enough” [5]. Mechanistic-interpretability work has adapted these ideas to interchange interventions on representations [6].

Approximation introduces three obligations that exact diagrams can hide. The discrepancy metric must represent the decision. The domain or distribution must state where the bound applies. The map class must be restricted enough that success is informative. A zero training error from an arbitrarily expressive translator may say more about the translator than either system.

stateDiagram-v2
  [*] --> Claim
  state "Keep every tested answer,<br/>replace the mechanism" as Claim
  state "Keep both systems fixed,<br/>change what counts as equal" as Test
  state "When the inverse is coherent<br/>rather than literal" as Revision
  Claim --> Test: expose mechanism
  Test --> Decision: evidence survives
  Test --> Revision: rival survives
  Revision --> Claim: narrow or rebuild
  Decision --> [*]

Put the claim through a transport gate

The practical contribution of this paper is a Structural Transport Contract. It converts a broad equivalence claim into eight fields that can fail independently. The contract is deliberately stricter than a comparison narrative and weaker than demanding one universal notion of sameness.

1. Decision. Name the action the result will support: replace, compile, compare, abstract, reuse or infer.
2. Signatures. List source and target object types, relations, operations, observations and interventions.
3. Admissible map. Declare how mappings may be constructed and what complexity or regularity they must obey.
4. Preservation. Specify every forward law that must commute.
5. Reflection and coverage. State which target relations must come from the source and how much of the target must be represented.
6. Return witness. Supply a strict inverse, coherent quasi-inverse, bisimulation relation, simulation relation or reconstruction bound.
7. Validation. Include held-out compositions, interventions, rival mappings and explicit error thresholds.
8. Break and permission. Publish the first known counterexample, the scope boundary and the exact inference the proof permits.

Locate the failure instead of averaging it away

A failed gate should report where the bridge broke. Four locations recur across mathematical, computational and cross-domain comparisons. They should remain separate because each calls for a different repair.

Vocabulary failure occurs before a functional test can begin. A source type, relation or operation has no declared target counterpart. A phenomenological account may distinguish an experienced horizon from an attended object, while the proposed machine description contains only token positions and weights. Inventing a shared label does not supply the missing target object. The honest result is an untranslated commitment and, perhaps, a design question.

Functional failure occurs when named counterparts do not respond alike under the relevant intervention. Two systems may both contain something called “memory”, yet one is an immutable training parameter and the other is writable episodic state. Resetting, updating or withholding the candidate components reveals different roles. The repair is to narrow the relation, change the target, or abandon the correspondence.

Structural failure occurs when local correspondences exist but their relations or compositions do not commute. Each role may map to a capability, each state to a state and each action to an API call, while revoke-after-approve, fork-then-merge or concurrent update behaves differently. This is the characteristic failure of attractive box-to-box diagrams. The repair is a law-level intervention, not better labels.

Ontological residue remains when the formal structure transports successfully but the source makes a further claim about what the structure is. A mathematical model of report, reflexivity or temporal integration can be instantiated in several substrates. That does not by itself decide whether any instance is conscious, biological, intentional in the phenomenological sense, or metaphysically fundamental. The proof should preserve the residue as an explicit non-inference rather than smuggling it through a shared diagram.

These failures can coexist, but they should not be blended into one confidence score. A score of 0.72 cannot tell a reader whether the missing piece is a term, an operation, a composition law or an ontological bridge. The location of failure is part of the result because it determines the next experiment.

Executable lab: the finite-structure mapping gate

The browser tool below audits finite typed relational structures. Each structure declares object identifiers, object types and named binary relations. The map assigns every source object to a target object. The gate checks totality, target membership, type preservation, injectivity, surjectivity, relation-signature agreement, preservation and reflection.

from __future__ import annotations

from dataclasses import dataclass
from typing import Mapping, Sequence

Pair = tuple[str, str]


@dataclass(frozen=True)
class FiniteStructure:
    name: str
    objects: Mapping[str, str]
    relations: Mapping[str, frozenset[Pair]]


@dataclass(frozen=True)
class Audit:
    verdict: str
    checks: Mapping[str, bool]
    counterexamples: tuple[str, ...]


def audit_mapping(
    source: FiniteStructure,
    target: FiniteStructure,
    mapping: Mapping[str, str],
) -> Audit:
    errors: list[str] = []
    source_ids = set(source.objects)
    target_ids = set(target.objects)

    total = source_ids <= set(mapping)
    images_exist = all(mapping.get(s) in target_ids for s in source_ids)
    typed = total and images_exist and all(
        source.objects[s] == target.objects[mapping[s]] for s in source_ids
    )

    image_values = [mapping[s] for s in source_ids if s in mapping]
    injective = len(image_values) == len(set(image_values)) == len(source_ids)
    surjective = set(image_values) == target_ids
    same_signature = set(source.relations) == set(target.relations)

    preservation = total and images_exist
    for relation, pairs in source.relations.items():
        target_pairs = target.relations.get(relation, frozenset())
        for left, right in pairs:
            mapped = (mapping.get(left), mapping.get(right))
            if mapped not in target_pairs:
                preservation = False
                errors.append(f"{relation}: {left,right} maps to {mapped}, absent in target")

    reflection = injective and images_exist
    if reflection:
        inverse = {mapping[s]: s for s in source_ids}
        image = set(inverse)
        for relation, pairs in target.relations.items():
            source_pairs = source.relations.get(relation, frozenset())
            for left, right in pairs:
                if left in image and right in image:
                    preimage = (inverse[left], inverse[right])
                    if preimage not in source_pairs:
                        reflection = False
                        errors.append(f"{relation}: target {left,right} reflects to absent {preimage}")

    checks = {
        "total": total,
        "images_exist": images_exist,
        "type_preservation": typed,
        "injective": injective,
        "surjective": surjective,
        "same_relation_signature": same_signature,
        "relation_preservation": preservation,
        "relation_reflection": reflection,
    }

    if typed and preservation and reflection and injective and surjective and same_signature:
        verdict = "exact structural isomorphism"
    elif typed and preservation and reflection and injective:
        verdict = "structural embedding"
    elif typed and preservation:
        verdict = "relation-preserving homomorphism"
    else:
        verdict = "failed structural mapping"

    return Audit(verdict, checks, tuple(errors))

Where the gate should stop

The gate should not be applied as a universal metaphysics machine. A correct finite-structure proof can show that two typed relational presentations are isomorphic. It cannot establish that they are made of the same kind of thing, have the same causal powers outside the signature, realise the same experience, or arose from the same historical lineage. Those are separate claims with separate evidence.

Nor should every useful mapping be forced upward to equivalence. One-way simulation may be exactly right for an implementation. Approximate abstraction may be the honest result for a noisy biological system. A lexical analogy may be enough to generate an experiment. The discipline is to lower the noun when the proof is weaker, not to inflate the proof until it matches the noun.

sequenceDiagram
  participant Q as Question
  participant M as Mechanism
  participant E as Evidence
  participant D as Decision
  Q->>M: The bridge that replay cannot finish
  M->>E: Keep every tested answer, replace the mechanism
  E-->>M: compare rival explanations
  E->>D: Approve only the transport contract that survives a break
  D-->>Q: revise scope or act

Approve only the transport contract that survives a break

When a proposed bridge appears between a transformer and a cognitive theory, a biological measure and an artificial system, a legacy service and its rewrite, or two philosophical descriptions, stop asking whether the endpoints “are equivalent” in general. Ask which decision needs to cross.

If the decision is reversible format migration, demand a lossless reconstruction witness. If it is behavioural substitution, specify the observations and require matched transitions under adversarial contexts. If it is causal explanation, transport interventions. If it is a lossy abstraction, publish the metric, distribution, error and discarded distinctions. If it is only hypothesis generation, call it a correspondence and preserve the residue.

This changes the release decision from “the outputs look the same” to “the decision-relevant structure is preserved under the interventions we may actually perform”. It changes comparative research from “these vocabularies resemble one another” to “this named relation survives this map, while these commitments do not transfer”. Most proposed equivalences will become narrower. That is progress. A bounded result can be tested, reused and revised; an unbounded resemblance can only be repeated.