iso
plain-language theorem explainer
From a mere existence proof that two physics frameworks are equivalent, extract a concrete structural isomorphism between them. Anyone proving uniqueness or exclusivity of frameworks (NoAlternatives, universal forcing certificates) uses this to turn a Prop-level equivalence into a usable iso witness. The body is classical choice on the nonempty type.
Claim. Given physics frameworks $F$ and $G$ and a hypothesis that they are equivalent (i.e. that a structural isomorphism exists), produce a concrete isomorphism $F \cong G$ with state-space and observable equivalences that commute with evolution and measurement.
background
This module supplies shared core definitions for NoAlternatives and necessity proofs, breaking circular imports. A PhysicsFramework is the minimal interface to "do physics": a state space, an evolution map, an observable type, and a measurement map from states to observables.
A structural isomorphism between frameworks $F$ and $G$ consists of equivalences of state spaces and of observables that intertwine evolution and measurement. Framework equivalence is the corresponding Prop: the type of such isomorphisms is nonempty.
The declaration lives in the FrameworkEquiv namespace and is the standard bridge from existence to a chosen witness under classical logic.
proof idea
One-line definition: apply Classical.choice to the equivalence hypothesis. Since equivalence is defined as Nonempty (FrameworkIso F G), choice yields an element of FrameworkIso F G. No further algebraic work.
why it matters
Exclusivity and forcing arguments need actual isomorphisms, not bare existence. Downstream, universal-forcing certificates (universalForcingIsoCert, strictUniversalForcingIsoCert) and uniqueness results (forcing_equiv_unique, universal_forcing_iff) consume iso witnesses of this shape when comparing forced arithmetics or framework realizations. Circle-winding and unknot-retract material also reference the same iso plumbing. In the Recognition exclusivity story, this is the classical extraction step that lets equivalence of frameworks be used as a concrete structure-preserving map rather than a Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.