DimensionSystem
plain-language theorem explainer
A dimension system equips a physics framework with a type of dimensions, a map sending each observable to its dimension, and a distinguished dimensionless class. Anyone proving exclusivity or zero-parameter forcing cites it as the interface that makes “dimensionless observables” a precise predicate. The declaration is a pure structure definition with a default equality test for the dimensionless class.
Claim. For a physics framework $F$, a dimension system consists of a type $\mathrm{Dim}$ of dimensions, an assignment $\mathrm{dim}: F.\mathrm{Obs} \to \mathrm{Dim}$, a distinguished element $\mathbf{1} \in \mathrm{Dim}$ (the dimensionless class), and the predicate that an observable $o$ is dimensionless precisely when $\mathrm{dim}(o) = \mathbf{1}$.
background
In the exclusivity verification layer, a PhysicsFramework packages the observables of a candidate theory. Physical dimensions (length, time, mass exponents in the constants module, or the forced spatial dimension $D=3$ from the forcing chain) are not yet attached to those observables. This structure supplies that missing bookkeeping without committing to a particular dimension algebra.
Upstream, Observable is the recognition-forcing notion of a real-valued readout on a state space, and dimensional signatures elsewhere track $[L,T,M]$ exponents. Here the dimension type is abstract: any type with a distinguished dimensionless point works. The default field is_dimensionless is equality with that point, so later lemmas can quantify over “all observables are dimensionless” without inventing a new predicate each time.
The module sits between parameter-surface bookkeeping and the bridge theorems that convert strong zero-parameter posture into a positive dimensionless ratio interface.
proof idea
No proof body: this is a structure definition. Four fields are declared. Dimension is an arbitrary type; dim_of assigns a dimension to each framework observable; dimensionless names the unit class; is_dimensionless defaults to equality with that class. Downstream definitions and theorems instantiate or quantify over inhabitants of this structure rather than proving properties of the structure itself.
why it matters
Exclusivity arguments need a clean way to say that a framework has no dimensionful free knobs. This structure is the carrier for that language. It is consumed by HasDimensionlessObservables (all observables land in the dimensionless class), by zero_params_forces_dimensionless (strong zero parameters plus “dimensionful implies free real knob” forces every observable dimensionless), and by bridge B3 (bridge_B3_single_channel_forces_ratio), which upgrades zero parameters plus single-channel conservation to a positive dimensionless ratio interface $r:S\to\mathbb{R}_+$.
In the Recognition Science chain this is bookkeeping for the dimensionless sector that the forcing program (T5–T8, RCL, $\varphi$-ladder constants) already treats as the only admissible observable surface once free real knobs are excluded. It does not itself force $D=3$ or the eight-tick octave; it only names the dimension assignment those later bridges assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.