compRatio_pos
plain-language theorem explainer
For any closed observable framework, the comparison ratio of two states is strictly positive. Anyone deriving the domain of the recognition cost J from ledger data cites this: positivity is read off the framework observable rather than postulated. The proof is a one-line application of division-positivity to the two r_pos facts.
Claim. Let $F$ be a closed observable framework with state space $S$ and strictly positive observable $r:S\to\mathbb{R}$. For all states $s_1,s_2\in S$, the comparison ratio $r(s_1)/r(s_2)$ satisfies $0 < r(s_1)/r(s_2)$.
background
A ClosedObservableFramework packages a state space $S$, a dynamics $T$, and a real observable $r:S\to\mathbb{R}$ obeying $r(s)>0$ for every state (axiom C1/non-trivial observability also requires two states with distinct $r$). The comparison object between states is the ratio $\mathrm{compRatio}(F,s_1,s_2):=r(s_1)/r(s_2)$.
This module (Phase 3 of the ledger-to-composition path) closes the gap left after LedgerCompositionToJCost: the object to which the recognition cost $J$ is applied must be shown to be a positive ratio with reciprocal symmetry under state swap, not assumed a priori. The positive ray is exactly the classical domain of $J$ (the unique solution of the Recognition Composition Law, T5).
Upstream, $r_\mathrm{pos}$ on the framework is the sole positivity input; reciprocal structure on recognition events and the cost algebra supply the swap/inverse story used by sibling lemmas.
proof idea
Term-mode one-liner. Unfold the comparison ratio as $r(s_1)/r(s_2)$ and apply the standard real lemma that a quotient of two positive reals is positive, feeding $F.r_\mathrm{pos},s_1$ and $F.r_\mathrm{pos},s_2$. No further algebraic rewriting.
why it matters
This is the first of the three comparison facts that make the ledger realize the structural hypotheses on $J$. Downstream, comparison_cost_swap_invariant uses it to justify applying reciprocal symmetry of a cost to the inverted ratio after state swap: equal cost on a comparison and its swap is then automatic. The Phase 3 certificate ledgerComparisonCertificate records it as the field comparison_is_positive_ratio.
In the forcing chain this discharges the domain side of T5/$J$-uniqueness: $J$ lives on $\mathbb{R}_{>0}$ because ledger observables force positive ratios, not because the analytic setup assumed it. Together with swap-inversion and self-unitality, it feeds the path from cost-determined combination through HasMultiplicativeConsistency to forcing the comparison cost to be $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.