ratio_from_conservation
plain-language theorem explainer
Given a physics framework with single-channel conservation, this extracts the dimensionless ratio of the conserved quantity at any state to its value at a fixed reference state. Anyone proving Bridge B3 (zero free parameters plus one conserved channel force a positive ratio interface) cites this. The body is a pure definitional quotient; no proof content.
Claim. Let $F$ be a physics framework and $C$ single-channel conservation data on $F$: a real-valued map $Q$ on the state space, a reference state $s_{\mathrm{ref}}$ with $Q(s_{\mathrm{ref}})>0$, and $Q$ invariant under evolution. The extracted ratio at state $s$ is $r_C(s) := Q(s)/Q(s_{\mathrm{ref}})$.
background
The module DimensionlessForcing sits in the exclusivity verification stack: it asks when a physics framework is forced to expose only dimensionless observables, with no free real knobs. A PhysicsFramework supplies a state space and an evolution map.
Single-channel conservation packages the ledger hypothesis that there is exactly one independent conserved real quantity $Q$ on states, together with a reference state of strictly positive $Q$, and the identity $Q(\mathrm{evolve}, s)=Q(s)$ for every $s$. The reference positivity field guarantees the denominator in the ratio is nonzero and positive.
Upstream conservation ideas (e.g. functionals preserved by round-trip coarsening) motivate treating $Q$ as an invariant of the dynamics; the CPT-side ratio coordinate $ι_S(s)/ι_O(o)$ is the analogous quotient used in reciprocal-cost factorization. Here the quotient is internal to one conserved channel.
proof idea
Definitional, not a proof. The value is the ordinary real division of the conserved quantity at $s$ by its value at the packaged reference state. Noncomputable only because the ambient real arithmetic is. Downstream positivity (ratio_pos_of_conservation) unfolds this definition and applies the hypothesis that $Q$ is positive on every state together with the packaged reference positivity.
why it matters
This is the concrete ratio map that Bridge B3 consumes. That bridge states: strong zero-parameter structure plus single-channel conservation force a dimensionless positive ratio interface $r:S\to\mathbb{R}_+$, so the observable interface factors through one positive real coordinate when (i) there are no free real knobs and (ii) the ledger conserves a single quantity.
In the Recognition exclusivity program, dimensionless forcing is how competing frameworks are pinned to the same ratio geometry that feeds J-cost and the reciprocal composition law, rather than carrying dimensionful free parameters. The sibling positivity lemma closes the $\mathbb{R}_+$ landing; together they turn the conservation structure into the ratio interface B3 needs.
No T0–T8 step is proved here; the declaration is scaffolding for the B3 exclusivity bridge, not a forcing-chain landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.