symm
plain-language theorem explainer
Framework equivalence is symmetric: if F is equivalent to G then G is equivalent to F. Anyone treating physics frameworks up to structural isomorphism in the exclusivity or necessity arguments will cite this. The proof inverts the underlying state and observable equivalences and conjugates the evolution and measurement commutation identities through those inverses.
Claim. If $F$ and $G$ are physics frameworks (each carrying a state space, an evolution map, an observable type, and a measurement map) and $F$ is framework-equivalent to $G$ (i.e., there exists a structural isomorphism between them), then $G$ is framework-equivalent to $F$.
background
This module supplies the shared abstract interface used by both the NoAlternatives and necessity developments, so those branches do not import each other. A physics framework is the minimal package needed to "do physics": a carrier type of states, an evolution operator on that carrier, a type of observables, 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. A structural isomorphism pairs equivalences of state spaces and of observable types that intertwine evolution and measurement: evolving then transporting equals transporting then evolving, and likewise for measurement. Equivalence is the propositional shadow of that isomorphism type (Nonempty of the iso).
The local goal is the elementary groupoid laws for that relation (reflexivity, symmetry, transitivity), so later uniqueness and exclusivity theorems can rewrite frameworks up to iso without choosing orientations.
proof idea
Term-mode construction under classical choice. Unpack the hypothesis to a concrete isomorphism iso : FrameworkIso F G. Build the reverse record whose state and observable maps are iso.stateEquiv.symm and iso.observableEquiv.symm.
For evolution commutation: apply the original evolve_comm at the preimage state iso.stateEquiv.symm s, then push both sides of the resulting equality through iso.stateEquiv.symm via congrArg, and flip the equality. Measurement commutation is identical with measure_comm and observableEquiv.symm. The two goals are discharged by simpa.
why it matters
Symmetry is the middle leg of the equivalence-relation package on physics frameworks inside the Verification/Exclusivity layer. Without it, framework equivalence cannot be used as a genuine equivalence relation when comparing candidate theories in the NoAlternatives and necessity proofs that this shared module was split out to support.
No downstream consumers are recorded yet on the dependency graph (used_by is empty), so the immediate value is infrastructural: it closes the symmetry law next to the reflexivity and transitivity siblings in the same namespace. In the broader Recognition Science program this sits under verification rather than the forcing chain (T0–T8); it does not itself force φ, the eight-tick octave, or D = 3, but it lets exclusivity arguments treat two presentations of the same dynamics as interchangeable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.