trans
plain-language theorem explainer
Framework equivalence is transitive: if F is equivalent to G and G to H, then F is equivalent to H. Anyone chaining uniqueness or no-alternatives arguments across intermediate frameworks would cite this. The proof unpacks the two isomorphism witnesses, composes their state and observable equivalences, and discharges the evolution and measurement diagrams by simplification.
Claim. Let $F$, $G$, and $H$ be physics frameworks. If there is a structural isomorphism $F \simeq G$ and a structural isomorphism $G \simeq H$, then there is a structural isomorphism $F \simeq H$.
background
This module supplies the shared abstract interface used by both the NoAlternatives development and the necessity proofs, isolating core framework definitions so those branches do not import each other circularly.
A physics framework is a minimal carrier for "doing physics": a state space, an evolution map on states, an observable type, and a measurement map from states to observables (plus existence of initial conditions). Two frameworks are declared equivalent when the type of structural isomorphisms between them is inhabited. Such an isomorphism pairs equivalences of state spaces and of observable types that intertwine evolution and measurement.
The local namespace packages equivalence as a proposition (nonemptiness of an isomorphism) and then proves the expected equivalence-relation laws on that proposition. Transitivity is the composition law for those isomorphisms.
proof idea
Classical choice unpacks each equivalence hypothesis into a concrete isomorphism witness. The composite isomorphism is assembled by Equiv.trans on the state-space equivalences and on the observable equivalences. The two intertwining obligations (evolution commutes with the state map; measurement commutes with both maps) are discharged by simp using Equiv.trans_apply together with the corresponding commute fields of the two input isomorphisms. No external lemmas beyond the structure of framework isomorphisms are required.
why it matters
Exclusivity and necessity arguments in Recognition Science compare candidate physics frameworks up to structural isomorphism. Transitivity lets those comparisons be factored through intermediate presentations (e.g., an abstract interface, a ledger realization, and a continuum limit) without rebuilding a direct isomorphism each time.
The declaration sits in the shared verification layer that both NoAlternatives and the necessity proofs import. It closes the equivalence-relation package for framework equivalence alongside reflexivity and symmetry (siblings in the same namespace). No downstream consumers are recorded yet in the dependency graph; the lemma is infrastructure for later uniqueness chains rather than a leaf prediction. It does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or the phi-ladder mass formula; it only equips the meta-language in which those uniqueness claims are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.