comparison_cost_self_zero
plain-language theorem explainer
A normalized recognition cost vanishes on self-comparison of any state in a closed observable framework, because that comparison is the unit ratio. Cite this when realizing the unit condition of J on the ledger rather than as an external analytic axiom. The proof rewrites the self-ratio to 1 and applies J(1)=0.
Claim. Let $F$ be a closed observable framework with positive observable $r:S\to\mathbb{R}$, and let $J:\mathbb{R}\to\mathbb{R}$ be normalized ($J(1)=0$). Then for every state $s\in S$, $J\bigl(r(s)/r(s)\bigr)=0$.
background
A closed observable framework supplies a state space $S$ and a strictly positive observable $r:S\to\mathbb{R}$ (with a nontriviality condition that $r$ is not constant). The ledger comparison of two states is the positive ratio $r(s_1)/r(s_2)$. That ratio is inverted by state swap and equals $1$ on self-comparison.
Normalization of a real cost $J$ means $J(1)=0$. In the functional-equation package this is the unit condition paired with reciprocity and calibration; here it is realized on the ledger by evaluating $J$ at the self-comparison ratio. The module's Phase 3 setting derives positive-ratio comparison from the framework (domain, swap symmetry, unit) rather than assuming it as analytic input to the recognition cost.
Upstream, ledger reconstruction already lists a unit field $J(1)=0$ among the hypotheses that build a zero-parameter comparison ledger from a closed framework.
proof idea
Term-mode, two steps. Rewrite the self-comparison ratio by the sibling lemma that $r(s)/r(s)=1$. The goal collapses to $J(1)=0$, which is exactly the normalization hypothesis on $J$. No further lemmas are needed.
why it matters
This is the ledger-native reading of normalization: self-comparison is the unit ratio, so every normalized cost vanishes there. Together with the swap-invariance sibling (reciprocity realized by state swap), it shows that the unit and reciprocal structure of the recognition cost is read off the closed observable framework, not imposed from outside.
It fills the unit half of the Phase 3 checklist item "derive positive-ratio comparison from ledger" in this module. That checklist feeds the larger chain in which a comparison cost whose symmetric combination is cost-determined (through a ledger-posting combiner) is forced to the unique $J$ of T5, $J(x)=(x+x^{-1})/2-1$. No recorded downstream uses yet; the natural consumers are the cost-determined-combination and ledger-comparison-forces-$J$ siblings in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.