ratio_pos_of_conservation
plain-language theorem explainer
Under single-channel conservation, if the conserved quantity is strictly positive on every state, the extracted state-to-reference ratio is strictly positive. Exclusivity and dimensionless-forcing arguments cite this to land in R₊ rather than bare R. The proof unfolds the ratio definition and applies the standard positivity of quotients.
Claim. Let $F$ be a physics framework and $C$ a single-channel conservation structure on $F$ (one conserved real quantity $Q$, a reference state $s_\ast$ with $Q(s_\ast)>0$, and $Q$ invariant under evolution). If $Q(s)>0$ for every state $s$, then for every $s$ the extracted ratio $r(s)=Q(s)/Q(s_\ast)$ satisfies $r(s)>0$.
background
In the exclusivity verification layer, a PhysicsFramework packages a state space and an evolution map. Single-channel conservation asserts that the ledger carries exactly one independent conserved real quantity $Q:S\to\mathbb{R}$, together with a fixed reference state whose $Q$-value is positive, and the conservation law $Q(\mathrm{evolve},s)=Q(s)$.
Ratio extraction normalizes any state against that reference: $r(s)=Q(s)/Q(s_\ast)$. The module's Bridge B3 programme then asks when observables factor through a map $r:S\to\mathbb{R}+$, i.e. a dimensionless positive ratio interface. That requires both zero free real parameters (dimensionless observables) and a one-dimensional conserved channel; positivity of $r$ is the elementary arithmetic step that puts the codomain in $\mathbb{R}+$ rather than $\mathbb{R}$.
The local setting is dimensionless forcing: strong zero-parameter hypotheses plus conservation collapse the observable interface to a single positive scale-free ratio.
proof idea
Term-mode, two steps. Unfold the definition of the extracted ratio (state value over reference value). Apply Mathlib div_pos to the two hypotheses $Q(s)>0$ (from the pointwise positivity assumption at $s$) and $Q(s_\ast)>0$ (the structure field reference_pos). No conservation identity is needed for positivity itself.
why it matters
Feeds directly into bridge_B3_single_channel_forces_ratio, the Bridge B3 theorem: strong zero parameters plus single-channel conservation force a dimensionless positive ratio interface $r:S\to\mathbb{R}_+$. Without this lemma the bridge only reaches a real-valued ratio; positivity is what matches the RS display convention that observables live on positive orbits.
In the broader Recognition exclusivity story, Bridge B3 is the step that turns "no free knobs and one conserved channel" into a forced dimensionless ratio, aligning with the phi-ladder and J-cost normalization where physical comparisons are scale-free. It is a small arithmetic gate, but it is the gate that lets later forcing cite $\mathbb{R}_+$ rather than an unsigned real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.