PRCPrimeCalibrationForcesCharacterCrossEqRespectTarget_of_normalizeRatio_canonical
plain-language theorem explainer
Canonical GCD normalization uniqueness on cross-equivalent ratio orbits already forces every ratio character to respect cross-equivalence, so the prime-calibration-to-cross-eq target holds under that hypothesis alone. Native-cost uniqueness certificate work and the reduced sign-canonical discharge path both cite it. Proof is a short wrapper: apply the character-level cross-eq lemma and drop the unused prime-calibration assumption.
Claim. Assume that whenever two ratio orbits are cross-equivalent, native GCD normalization returns the same raw representative. Then every ratio character that is prime-direction calibrated respects ratio cross-equivalence: if $\chi$ is a ratio character and prime-direction calibrated, and $q\sim r$ by cross-equivalence, then $\chi(q)$ and $\chi(r)$ are cross-equivalent.
background
In the Primitive Recognition Calculus, ratio orbits are raw multiplicative distinction displays. Cross-equivalence identifies displays that represent the same quotient class. A ratio character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ is intended to act on that quotient; without respect for cross-equivalence it is not yet quotient-native.
The canonical-normalization target states that DistinctionNat.normalizeRatio is constant on cross-equivalence classes: cross-equivalent $q,r$ yield the same normalized raw representative. Upstream documentation calls this "the exact quotient-normalization uniqueness statement needed to turn normalized_invariant into general quotient respect."
The prime-calibration-forces-cross-eq target packages a sharper source of product-display compatibility: every prime-direction-calibrated ratio character should automatically respect cross-equivalence. The present result shows that target follows from canonical normalization alone.
proof idea
Short tactic wrapper. Introduce an arbitrary map $\chi$ with the ratio-character and prime-direction-calibration hypotheses, discard the prime hypothesis, and apply PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical, which already yields cross-equivalence respect from the character axioms plus the canonical-normalization target. Prime calibration is unused on this path.
why it matters
One of two discharge routes for the prime-calibration-forces-cross-eq target. The sibling theorem routes through reduced sign-canonical uniqueness, first deriving the canonical-normalization target and then invoking this result. Downstream, the native-cost uniqueness blocker certificate records factorization and signed-admissibility status in the PRC native-cost program; quotient-native characters are required before the native cost can be identified with the J-cost forced by T5, $J(x)=(x+x^{-1})/2-1$, and the Recognition Composition Law. Closing cross-equivalence respect is a concrete step toward uniqueness of the admissible native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.