compRatio_self
plain-language theorem explainer
Self-comparison of any observable state against itself yields the unit ratio one. Phase 3 ledger work cites this to realize cost normalization on the diagonal: a normalized cost vanishes at self-comparison. The proof is a one-line term applying division-by-self to the strictly positive observable.
Claim. Let $F$ be a closed observable framework with strictly positive observable $r:S\to\mathbb{R}$. For every state $s\in S$, the comparison ratio of $s$ with itself equals one: $r(s)/r(s)=1$.
background
A closed observable framework packages a state space $S$, dynamics $T$, and a strictly positive real-valued observable $r$ (for every $s$, $0<r(s)$), plus nontriviality and closure. The comparison between two states is the ratio $r(s_1)/r(s_2)$.
This module closes the Phase 3 checklist item that the object fed to the recognition cost $J$ is a positive ratio read off the ledger, not an external analytic input. That ratio is strictly positive, inverted by state swap, and unital under self-comparison. Unitality is exactly the present claim; it is what lets a normalized cost vanish on the diagonal.
Upstream structure supplies $r_pos$ as a field of the closed-observable package. No deeper cost algebra is needed here: only positivity of a single value $r(s)$.
proof idea
One-line term proof. Self-comparison is $r(s)/r(s)$. Framework positivity gives $r(s)>0$, hence $r(s)\neq 0$, and the standard division-by-self identity yields $1$. No intermediate lemmas beyond that positivity witness.
why it matters
Unitality leg of the Phase 3 positive-ratio comparison package. Downstream, the normalization-on-the-ledger theorem rewrites through this identity to conclude that any normalized cost $J$ satisfies $J(r(s)/r(s))=0$, realizing the normalization axiom on ledger comparisons. The same fact is recorded as the self-unit field of the Phase 3 ledger comparison certificate.
With positivity and swap-inversion of the ratio, this closes the first Phase 3 item: derive positive-ratio comparison from the ledger. That package, together with cost-determined combination, feeds the forcing that a ledger comparison cost is the unique $J$ (T5 $J$-uniqueness via the Recognition Composition Law), after the composition-to-$J$ step already discharged in the sibling module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.