HasDimensionlessObservables
plain-language theorem explainer
A physics framework paired with a dimension system has only dimensionless observables when every observable is assigned the dimensionless class. Exclusivity and bridge arguments cite this predicate as the target of zero-parameter forcing. It is a one-line universal quantification over the framework's observable type.
Claim. Given a physics framework $F$ and a dimension system $D$ on $F$, $F$ has dimensionless observables (relative to $D$) if and only if every observable $o$ of $F$ satisfies $D$'s dimensionless predicate, i.e. $\mathrm{dim}(o)$ equals the distinguished dimensionless class.
background
In the exclusivity verification layer, a PhysicsFramework carries an observable type. A dimension system on $F$ is a structure that assigns to each observable a dimension value, marks one distinguished dimensionless class, and defines the predicate "is dimensionless" as equality with that class.
The local module develops dimensionless forcing: strong zero-parameter posture should rule out dimensionful knobs. Downstream, if a dimensionful observable existed it would induce a free real-valued parameter, contradicting the zero-parameter record formalization.
Upstream, observables appear as real-valued maps on state (recognition/cost structure). Spatial dimension $D=3$ is forced elsewhere in the chain (T8/T9), but this definition is purely about the dimension assignment on observables, not about spacetime dimension.
proof idea
No proof: this is a definitional abbreviation. The body is the proposition $\forall o : F.\mathrm{Observable},, D.\mathrm{is_dimensionless}, o$, using the default field of the dimension-system structure that equates $\mathrm{dim_of}(o)$ with the distinguished dimensionless class.
why it matters
This predicate is the conclusion type of zero_params_forces_dimensionless: strong zero parameters plus the bridge hypothesis that any dimensionful observable yields a free real knob force every observable to be dimensionless. It is also an input hypothesis shape for Bridge B3 (bridge_B3_single_channel_forces_ratio), which combines dimensionless observables with single-channel conservation to force a positive ratio interface $r : S \to \mathbb{R}_+$.
In Recognition Science exclusivity, dimensionless observables are the observable-side face of the zero-parameter posture: no free units knobs survive once the parameter record is empty. That feeds the uniqueness story linking the recognition composition law and forced constants to a unique dimensionless interface, rather than a family of dimensionful couplings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.