FrameworkEquiv
plain-language theorem explainer
Two physics frameworks count as equivalent precisely when a structural isomorphism between them exists. The relation is the working notion of sameness used by exclusivity and no-alternatives arguments. It is a one-line definition: nonempty of the isomorphism structure (state and observable bijections that intertwine evolution and measurement).
Claim. Two physics frameworks $F$ and $G$ are equivalent when there exists a structural isomorphism between them: bijections $F.StateSpace \simeq G.StateSpace$ and $F.Observable \simeq G.Observable$ that intertwine evolution and measurement, i.e. the diagrams for dynamics and observables commute.
background
This module supplies shared core definitions for NoAlternatives and necessity proofs, isolating the abstract interface so those developments do not circularly depend on each other.
A physics framework is the minimal package needed to "do physics": a state space, an evolution map, an observable type, a measurement map from states to observables, and existence of initial conditions. A structural isomorphism between two such frameworks is a pair of type equivalences on states and on observables together with two commuting identities: evolution pushed across the state equivalence equals evolution in the target, and measurement pushed across equals measurement in the target.
Equivalence of frameworks is then the mere existence of such an isomorphism (as a proposition), not a chosen witness. Downstream code recovers a witness classically when needed.
proof idea
Pure definitional abbreviation: the proposition is Nonempty applied to the structural-isomorphism structure. No tactics, no lemmas. The companion iso definition later extracts a concrete witness via classical choice; reflexivity, symmetry, and transitivity build explicit isomorphisms and wrap them in Nonempty.
why it matters
Equivalence is the sameness relation on which the exclusivity stack sits. It is consumed immediately by the local equivalence-relation kit: iso (witness extraction), refl, symm, and trans. Those facts let later uniqueness or no-alternatives theorems treat frameworks up to structural isomorphism rather than up to syntactic identity of carriers.
In the broader Recognition program this is bookkeeping infrastructure, not a forcing step (T0–T8). It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only says when two abstract physics packages may be identified so that exclusivity claims are well-posed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.