compRatio
plain-language theorem explainer
Defines the comparison object between two states of a closed observable framework as the ratio of their positive observables. Anyone deriving that recognition cost acts on a positive ray (rather than assuming the domain) cites this. The body is a one-line quotient of the framework's observable map.
Claim. Given a closed observable framework $F$ with state space $S$ and strictly positive observable $r:S\to\mathbb{R}$, the comparison ratio of states $s_1,s_2\in S$ is $\mathrm{comp}(s_1,s_2):=r(s_1)/r(s_2)\in\mathbb{R}$.
background
Phase 3 of the ledger-to-composition program asks that the object fed to the recognition cost $J$ be derived from the ledger, not postulated. A ClosedObservableFramework packages a state type $S$, a dynamics $T$, and a strictly positive observable $r:S\to\mathbb{R}$ with $r(s)>0$ for every $s$, plus a nontriviality condition that $r$ is non-constant.
The module goal is to read the comparison between two observable states off $r$ itself: the ratio $r(s_1)/r(s_2)$. Upstream, the closed-framework structure already forces positivity of $r$; various cost constructions (observer forcing, multiplicative recognizers, rung coarsening) apply $J$ or a derived cost to positive ratios. This definition is the ledger-native name for that ratio.
proof idea
Definitional one-liner: unfold to $F.r,s_1/F.r,s_2$. No lemmas are applied; positivity, reciprocal swap, and unital self-comparison are proved in the sibling theorems that cite this def.
why it matters
This is the comparison object that closes the first Phase 3 checklist item: positive-ratio comparison derived from the ledger. Downstream, compRatio_pos shows the ratio lies on the positive ray (so the domain of $J$ is derived, not assumed); compRatio_swap shows state swap inverts the ratio (geometric origin of reciprocal symmetry); compRatio_self shows self-comparison is the unit. Those feed comparison_cost_swap_invariant and comparison_cost_self_zero, realizing IsReciprocalCost and IsNormalized on the ledger. The Phase 3 certificate LedgerComparisonCertificate packages the positivity and swap facts. Together with the factorization side of the module and LedgerCompositionToJCost, a cost-determined comparison through a ledger-posting combiner is forced to be the unique $J$ of the forcing chain (T5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.