zero_params_forces_dimensionless
plain-language theorem explainer
Under a strong zero-parameter posture, every framework observable must be dimensionless. Anyone building the exclusivity/bridge layer cites this to rule out dimensionful free knobs. The argument is a short contradiction: a dimensionful observable would induce a free real knob, which zero parameters already exclude.
Claim. Let $F$ be a physics framework with a parameter record and a dimension system $D$. Assume $F$ has strongly zero free parameters, and that every dimensionful observable of $F$ would induce a free real-valued knob. Then every observable of $F$ is dimensionless with respect to $D$.
background
In the exclusivity verification layer, a PhysicsFramework carries an observable type and a parameter surface. A dimension system assigns to each observable a dimension and marks the dimensionless class; the framework has dimensionless observables when every observable lands in that class.
Strong zero parameters means the framework admits no free real knobs in the non-vacuous parameter-record sense. The companion fact used here is that strong zero parameters already exclude any free real knob. The local module packages these notions so that dimensionless structure can be forced before single-channel ratio bridges are stated.
The hypothesis that dimensionful observables force knobs is the bridge between dimensional analysis and the parameter surface: a genuine dimensionful reading would leave a continuous scale freedom, which zero-parameter posture forbids.
proof idea
Fix an arbitrary observable $o$. Argue by contradiction that $o$ fails to be dimensionless. The dimensionful-forces-knob hypothesis then yields a free real knob on $F$. That contradicts the upstream exclusion theorem that strong zero parameters rule out free real knobs. Discharge the contradiction; universality over $o$ gives the dimensionless-observables predicate.
why it matters
This is the first forcing step inside DimensionlessForcing: zero free parameters imply a purely dimensionless observable interface. Downstream, bridge_B3_single_channel_forces_ratio consumes exactly this conclusion together with single-channel ledger conservation to force a positive ratio interface $r : S \to \mathbb{R}_+$.
In the Recognition exclusivity program, dimensionless observables are required before claiming that the theory has no continuous dials left to fit. The result sits under the zero-parameter exclusivity chain rather than under T5–T8 directly, but it is the verification hinge that turns the strong zero-parameter posture into a concrete restriction on what can be measured.
Without it, Bridge B3 could not promote single-channel conservation into a forced ratio; dimensionful leftovers would still look like free scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.