PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical
plain-language theorem explainer
A ratio character that is invariant under native GCD normalization respects cross-equivalence of ratio orbits once normalization is canonical on equivalent displays. Anyone building quotient-native PRC characters or transporting cost calibration cites this. The proof chains normalized invariance through equality of normalized representatives and the crossEq equivalence laws.
Claim. Let $\chi$ map ratio orbits to ratio orbits and satisfy the ratio-character axioms (unit, multiplicativity, and reciprocity up to cross-equivalence). Assume that whenever two ratio orbits are cross-equivalent, their native GCD normalizations are definitionally equal. Then $\chi$ respects cross-equivalence: if $q\sim r$ then $\chi(q)\sim\chi(r)$.
background
In the Primitive Recognition Calculus, costs and characters are carried on RatioOrbit displays: signed-orbit numerators over nonzero distinction-nat denominators. Equality of displays is the coarser relation cross-equivalence (balanced integer cross-multiplication), not definitional equality, so maps must be proved to respect that setoid before they can act as quotient-native characters.
A ratio character is a map $\chi$ with unit, multiplicative, and reciprocal laws stated via cross-equivalence. Separately, each character is assumed normalized-invariant: $\chi(q)$ is cross-equivalent to $\chi$ of the GCD-normalized representative of $q$. Canonical normalization says that cross-equivalent inputs share one and the same normalized raw representative.
The target property is exactly map-respects-setoid for $\chi$: cross-equivalent inputs yield cross-equivalent character values. That is the missing bridge from raw orbit functions to quotient-level PRC characters used in native-cost uniqueness.
proof idea
Term proof by introducing $q$, $r$, and $q\sim r$, then chaining three cross-equivalences with crossEq_trans.
First apply normalized invariance at $q$: $\chi(q)\sim\chi(\mathrm{normalize}(q))$. Second, rewrite by the canonical-normalization hypothesis so $\mathrm{normalize}(q)=\mathrm{normalize}(r)$, then close with reflexivity of cross-equivalence at $\chi(\mathrm{normalize}(r))$. Third, reverse normalized invariance at $r$ via crossEq_symm. The composite is $\chi(q)\sim\chi(r)$.
why it matters
Quotient respect is the gate for treating a raw ratio character as a genuine PRC character on the orbit setoid. Downstream, structural-ledger display transport (character_display) applies this theorem with the proved canonical-normalization target to move character values along equal rational displays. The same respect hypothesis feeds prime-orientation coherence implying character zero, the prime-calibration forcing targets, and the native-cost uniqueness blocker certificate.
In the broader Recognition chain this sits inside native-cost uniqueness for the d'Alembert factorization of the PRC cost: once characters respect cross-equivalence, calibration on two-points and prime-pair products can force the canonical $J$-shaped cost rather than a raw display artifact. It is a proved infrastructure lemma, not a physics endpoint, but it closes the setoid gap that otherwise blocks structural uniqueness of the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.