compRatio_swap
plain-language theorem explainer
Swapping two states inverts their comparison ratio: the ratio of positive observables becomes its reciprocal. Anyone deriving reciprocal symmetry of recognition cost from the ledger cites this. The proof is a two-step algebraic identity: unfold the ratio definition and apply the field law that the inverse of a quotient is the swapped quotient.
Claim. Let $F$ be a closed observable framework with strictly positive observable $r:S\to\mathbb{R}$. For any states $s_1,s_2\in S$, the comparison ratios satisfy $$\frac{r(s_2)}{r(s_1)}=\Bigl(\frac{r(s_1)}{r(s_2)}\Bigr)^{-1}.$$
background
Phase 3 of the ledger-to-composition program asks that the object fed to the recognition cost $J$ be a positive ratio read off the ledger, not postulated. A ClosedObservableFramework supplies a state space $S$ and a strictly positive observable $r:S\to\mathbb{R}$ (axiom $r_pos$), together with non-trivial observability and closure.
The comparison ratio between two states is defined as $r(s_1)/r(s_2)$. Because $r$ is strictly positive, this ratio lands in the positive ray, which is exactly the domain of $J$. The present lemma records the elementary reciprocal law under state swap: that geometric fact is what later turns an abstract reciprocal-cost axiom into a ledger identity.
Upstream, the framework structure only guarantees positivity and non-triviality of $r$; no cost functional is assumed here.
proof idea
Term-mode, two steps. Unfold the comparison-ratio definition on both sides, so the goal becomes $r(s_2)/r(s_1)=(r(s_1)/r(s_2))^{-1}$. Rewrite by the standard field identity inv_div (inverse of a quotient is the swapped quotient). No framework axioms beyond the definition are used; positivity is not needed for the equality itself.
why it matters
This is the geometric origin of reciprocal symmetry on the ledger. Downstream, comparison_cost_swap_invariant applies it once: if $J$ is a reciprocal cost, then $J$ of a comparison equals $J$ of the swapped comparison, because the swap inverts the positive ratio and reciprocity identifies $J(x)$ with $J(x^{-1})$. That realizes IsReciprocalCost as a ledger fact rather than an external analytic assumption.
It is also one of the five fields of ledgerComparisonCertificate, the Phase 3 certificate that positive-ratio comparison (positivity, swap-inversion, self-unit) and factorization-as-cost-determinedness both hold. Together with LedgerCompositionToJCost, a comparison cost whose combination is cost-determined 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.