identity_ratio_character
plain-language theorem explainer
The identity map on ratio orbits is a ratio character for d'Alembert factorization of a PRC cost. Anyone checking that the character interface is inhabited by the canonical cost map cites this sanity check. Each field is discharged by reflexivity of cross-equivalence (plus one normalization lemma), so the proof is a short tactic package rather than an algebraic construction.
Claim. The identity map $\chi(q)=q$ on ratio orbits is a ratio character: $\chi(1)\sim 1$, $\chi(xy)\sim\chi(x)\chi(y)$, $\chi(x^{-1})\sim\chi(x)^{-1}$ (all up to cross-equivalence), $\chi$ is invariant under normalization of the underlying distinction, and $\chi$ preserves nonzeroness.
background
In the Primitive Recognition Calculus, costs are analyzed at the level of ratio orbits: pairs (signed numerator, nonzero distinction denominator) that display rational ratios without collapsing to definitional equality on representatives. Cross-equivalence is the quotient-native sameness relation on those orbits (reflexive via balanced reflexivity of signed orbits).
A ratio character is a map $\chi$ on ratio orbits that behaves like a group homomorphism for the d'Alembert factorization of a PRC cost: it fixes the unit, multiplies, and inverts, all up to cross-equivalence, and it respects normalization and nonzeroness. The structure is deliberately quotient-native so candidates need not be definitionally equal on raw data.
This module builds the uniqueness path for native PRC costs. The identity map is the canonical candidate that should sit under the cost itself; establishing it as a character anchors the interface before admissibility and uniqueness certificates are assembled.
proof idea
The proof packages the five fields of the ratio-character structure for $\chi=\mathrm{id}$.
Unit, multiplicativity, and reciprocity are each one-line applications of reflexivity of cross-equivalence at the relevant orbit (one, mul x y, recip x). Normalization invariance invokes the existing lemma that a ratio orbit is cross-equivalent to its normalized form. Nonzero preservation is pure identity on the hypothesis: if $q$ is nonzero, so is $\mathrm{id}(q)$.
No algebraic construction is needed; the identity already satisfies the homomorphism laws definitionally, and cross-equivalence only has to witness that fact.
why it matters
Doc-comment role: a sanity check that anchors the character interface to the canonical cost. Downstream, it is the ratio_character field of the admissible identity character, which adds prime calibration and prime-pair product-cost consistency. That admissible package feeds the native-cost uniqueness blocker certificate (zero-calibrated factorization target proved; signed admissible factorization refuted).
In the broader Recognition chain this sits under cost uniqueness: T5 forces the J-cost $J(x)=(x+x^{-1})/2-1$, and the PRC native-cost path must show that characters factoring costs cannot wander off the identity once calibration is imposed. The identity character is the baseline witness that the interface is inhabited before uniqueness and refutation steps close the blocker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.