refl
plain-language theorem explainer
Every abstract physics framework is equivalent to itself. Anyone treating framework equivalence as a relation (for exclusivity or uniqueness arguments) needs this reflexivity leg. The proof builds the identity structural isomorphism: identity maps on states and observables, with the two commutation squares discharged by simplification.
Claim. For every physics framework $F$ (state space, evolution map, observable type, and measurement map), $F$ is framework-equivalent to itself: there exists a structural isomorphism $F \simeq F$.
background
The module supplies shared core definitions for exclusivity and necessity arguments, so that NoAlternatives-style proofs and related necessity chains do not import each other circularly.
A physics framework is the minimal interface needed to "do physics": a state space, an evolution operator on states, an observable type, and a measurement map from states to observables (plus existence of initial conditions). Two frameworks are framework-equivalent when the type of structural isomorphisms between them is inhabited. That isomorphism pairs equivalences of state spaces and of observable types that intertwine evolution and measurement.
Reflexivity is the first algebraic property of that equivalence relation on frameworks.
proof idea
Construct an explicit structural isomorphism witness and wrap it in Nonempty. Take the identity equivalence on the state space and on the observable type. The two remaining fields are the commutation identities (evolution and measurement must commute with the state/observable maps). Both reduce by introducing a state and simplifying against the identity equivalences; no nontrivial dynamics or measurement lemmas are required.
why it matters
Exclusivity and "no alternatives" arguments compare candidate physics frameworks up to structural equivalence. Reflexivity is the baseline leg of that relation: without it, equivalence classes and uniqueness-up-to-iso statements are ill-formed.
The declaration sits in the shared Framework layer used by both NoAlternatives and the necessity proofs. Downstream consumers are not yet wired in this graph snapshot (used_by is empty), but sibling material (framework isomorphisms, zero-parameter and algorithmic-spec interfaces, observable-derivation predicates) is exactly the setting where a reflexive, symmetric, transitive equivalence is expected. It does not itself touch forcing-chain landmarks (T5–T8, RCL, phi, eight-tick, $D=3$); it only equips the verification layer that will host those uniqueness claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.