PhysicsFramework
plain-language theorem explainer
Minimal abstract interface for a physics theory: a nonempty state space, a dynamics map, an observable type, and a measurement map from states to observables. Exclusivity and dimensionless-forcing arguments quantify over this type, so any candidate theory must instantiate it. The declaration is a pure structure definition with no proof obligations.
Claim. A physics framework consists of a type $S$ of states, an evolution map $E : S \to S$, a type $O$ of observables, a measurement map $m : S \to O$, and a witness that $S$ is nonempty (initial conditions exist).
background
The Verification.Exclusivity.Framework module supplies shared scaffolding for the NoAlternatives and necessity arguments, isolating core framework definitions so those developments do not import each other circularly.
A physics framework is the thinnest interface that still lets one "do physics": states, dynamics, and extractable observables. The carrier StateSpace is an arbitrary type; evolve is a single-step (or discrete-time) dynamics endomorphism; Observable is the type of measurable quantities; measure pulls observables from states. Nonemptiness of the state space records that initial data exist.
Upstream, RecognitionForcing already uses a leaner Observable as a real-valued functional on states. Here the observable type is left abstract so dimension systems and conservation laws can be layered on later without fixing the codomain to $\mathbb{R}$.
proof idea
No proof: this is a structure declaration. The five fields are the data of the interface; hasInitialState is the sole propositional field and is just Nonempty StateSpace. Downstream lemmas quantify over an arbitrary PhysicsFramework and add typeclass or structure hypotheses (zero parameters, dimension systems, single-channel conservation).
why it matters
Every exclusivity bridge that forces dimensionless ratios or zero free knobs is parameterized by this interface. Downstream, DimensionSystem, HasDimensionlessObservables, SingleChannelConservation, and ratio_from_conservation all take a PhysicsFramework argument; Bridge B3 (bridge_B3_single_channel_forces_ratio) uses strong zero-parameter posture plus single-channel conservation on such an $F$ to force a positive dimensionless ratio interface.
In the Recognition Science program this is the formal stand-in for "any competing physics," against which the forcing chain (T5 J-uniqueness through T8 dimension count) and the Recognition Composition Law are compared. Sibling notions (HasZeroParameters, DerivesObservables, FrameworkIso) refine or relate instances of this structure. It does not itself encode the J-cost or the phi-ladder; those enter only when a concrete RS instance is built.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.