bridge_B3_single_channel_forces_ratio
plain-language theorem explainer
Strong zero-parameter posture plus single-channel ledger conservation force a dimensionless positive ratio interface on observables. Anyone citing Bridge B3 in the exclusivity/verification layer uses this packaging. The proof is a two-line term assembly: dimensionless observables from the zero-params lemma, and the ratio map extracted from the conserved quantity with positivity and measure-determination hypotheses.
Claim. Let $F$ be a physics framework with a parameter record, strong zero free parameters, and a dimension system $D$. Suppose every dimensionful observable would induce a free real knob, the ledger conserves a single positive quantity $C$, and equal conservation ratios imply equal measures. Then every observable is dimensionless under $D$, and there exists $r:S\to\mathbb{R}_{>0}$ such that $r(s_1)=r(s_2)$ implies $F.measure(s_1)=F.measure(s_2)$.
background
This module sits in the exclusivity verification layer: it asks when a physics framework is forced to present only dimensionless observables and a one-dimensional positive ratio interface. A DimensionSystem assigns a dimension to each observable and marks a distinguished dimensionless class. HasDimensionlessObservables means every observable lands in that class.
SingleChannelConservation packages a ledger with exactly one independent conserved real quantity, a positive reference state, and invariance under evolution. From that structure one extracts a ratio map (conserved quantity relative to the reference) and a positivity lemma for all states when the conserved quantity is everywhere positive.
The strong zero-parameter hypothesis rules out free real knobs. Upstream, the sibling lemma that zero parameters force dimensionless observables uses the non-vacuous parameter-record formalization: a dimensionful observable would induce a genuine real-valued knob, contradicting exclusion of free knobs.
proof idea
Term-mode packaging, not a deep argument. The first conjunct is discharged by applying the sibling zero_params_forces_dimensionless to the strong zero-parameter hypothesis, the dimension system, and the knob-forcing hypothesis on dimensionful observables.
The second conjunct is an existential package: take the ratio extracted from single-channel conservation as the witness $r$, feed positivity of the conserved quantity into ratio_pos_of_conservation to get $\forall s,,0<r(s)$, and reuse the given hypothesis that equal ratios determine equal measures. No further rewriting or case analysis.
why it matters
Bridge B3 is the exclusivity hinge that turns two structural assumptions (no free real knobs; one conserved ledger channel) into a concrete observable interface: dimensionless data factored through a positive ratio $r:S\to\mathbb{R}_+$. That is the shape Recognition Science needs before dimensionless constants and ladder ratios can be forced rather than fitted.
In the broader forcing chain, dimensionless observables and single-channel ratios sit downstream of the J-cost uniqueness and self-similar fixed point (T5–T6) and the eight-tick / $D=3$ cadence (T7–T8): once the ledger is one-dimensional and parameters are closed, measured ratios become the only free interface. No used_by edges are recorded yet, so this theorem is presently a leaf packaging step inside DimensionlessForcing rather than a cited parent of a larger exclusivity theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.