PRCCharacterRespectsCrossEq
plain-language theorem explainer
Quotient-respect for a ratio character: cross-equivalent ratio-orbit displays must map to cross-equivalent character values. Anyone assembling a quotient-native PRC character from a raw map on ratio orbits cites this as the setoid-respect condition. It is a pure Prop definition, not a proved statement.
Claim. A map $\chi$ from ratio orbits to ratio orbits respects cross-equivalence when, for all ratio orbits $q,r$, if $q$ and $r$ are equivalent under cross-multiplication (balanced scaled numerators and denominators as signed orbits), then $\chi(q)$ and $\chi(r)$ are likewise cross-equivalent.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence is the internal PRC rational relation: two ratio orbits $a,b$ satisfy it when the scaled products $a.num\cdot b.den$ and $b.num\cdot a.den$ balance as signed orbits. That relation is the setoid whose quotient is the native rational type.
A ratio character is a map $\chi$ on ratio orbits meant to act as a multiplicative character before cost is recovered (via the doubled-trace / J-cost display). For $\chi$ to descend to the quotient and serve as a quotient-native PRC character, it must send cross-equivalent inputs to cross-equivalent outputs. This definition packages exactly that missing map-respects-setoid condition.
The surrounding module develops native-cost uniqueness: characters calibrated on primes and pairs, structural ledgers forcing the canonical cost, and transport from pair/two-point data to full prime-axis calibration.
proof idea
No proof: this is a Prop-valued definition. The body is the universal quantification that cross-equivalence of inputs implies cross-equivalence of $\chi$-images. Downstream lemmas treat the predicate as a hypothesis and apply it pointwise (for example, product-display compatibility is obtained by feeding the relevant orbit-direction pair into this respect condition).
why it matters
Native-cost uniqueness in PRC needs characters that are well-defined on the rational quotient, not merely on raw ratio-orbit displays. This predicate is the gate: without it, cost-from-character constructions and calibration statements would mix setoid classes.
It feeds directly into orbit-product display compatibility (one-line from respect), positive-orbit identity and reciprocal transport from all-prime data, structural calibration on positive integers, and the round-5 structural uniqueness target that forces the canonical cost. Downstream, prime-pair products plus two-point calibration then force prime-direction calibration once a genuine ratio character is in hand.
In the broader forcing chain this sits under cost uniqueness (T5 J-uniqueness and the Recognition Composition Law): only quotient-respecting characters can recover the unique J-cost on native displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.