FrameworkIso
plain-language theorem explainer
A structural isomorphism between two physics frameworks is a pair of type equivalences on states and observables that intertwine evolution and measurement. Anyone comparing candidate frameworks in the exclusivity/no-alternatives line cites this carrier. It is a bare structure definition: four fields, no proof obligations beyond the commuting diagrams.
Claim. A structural isomorphism between physics frameworks $F$ and $G$ consists of type equivalences $\mathrm{State}_F \simeq \mathrm{State}_G$ and $\mathrm{Obs}_F \simeq \mathrm{Obs}_G$ such that evolution and measurement commute: $\Phi(\mathrm{evolve}_F(s)) = \mathrm{evolve}_G(\Phi(s))$ and $\Psi(\mathrm{measure}_F(s)) = \mathrm{measure}_G(\Phi(s))$ for every state $s$.
background
The module supplies shared core definitions for the NoAlternatives and necessity arguments, isolating the abstract interface so those developments do not import each other circularly.
A physics framework is the minimal package needed to "do physics": a state space, an evolution map on states, an observable type, and a measurement map from states to observables (plus an existence-of-initial-conditions field not used here). The present structure compares two such packages.
Upstream, the recognition-forcing Observable is a real-valued extraction on a carrier; here Observable is kept abstract as a type so that framework comparison stays purely structural. Constants such as $G$ appear only as ambient imports and play no role in the isomorphism data.
proof idea
Definitional structure, not a proved theorem. The four fields are: a Lean equivalence of state spaces, an equivalence of observable types, a naturality square for evolution, and a naturality square for measurement. No tactics or lemmas are invoked; inhabiting the structure is exactly exhibiting those four pieces of data.
why it matters
This is the witness type behind framework equivalence: FrameworkEquiv F G is defined as nonempty existence of a FrameworkIso F G, and iso recovers a classical choice of witness. Downstream exclusivity arguments (NoAlternatives / necessity) use equivalence to say two frameworks are the same up to relabeling of states and observables, so distinct predictive content cannot hide behind a change of presentation.
In the Recognition Science verification stack this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8). It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only standardizes when two abstract frameworks count as identical for the exclusivity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.