PRCCharacterOrbitProductDisplayCompatible_of_crossEq_respect
plain-language theorem explainer
Any ratio-orbit character that respects cross-equivalence automatically respects native orbit-product displays: the character on the product direction matches the character on the product of the factor directions. Cited when discharging the product-display half of native cost uniqueness from the weaker setoid-respect hypothesis. The proof is a direct application of crossEq-respect to the orbitDirection multiplication lemma.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If $\chi$ preserves cross-equivalence (whenever two orbits are cross-equivalent, so are their images under $\chi$), then $\chi$ is orbit-product display compatible: for all nonzero distinction naturals $a,b,p$ with $a\cdot b=p$, the value $\chi$ on the direction of $p$ is cross-equivalent to $\chi$ on the ratio-orbit product of the directions of $a$ and $b$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed orbit numerator over a nonzero distinction-natural denominator. The map orbitDirection sends a nonzero distinction natural $p$ to the pure direction with numerator the signed orbit of $p$ and denominator one.
Cross-equivalence (RatioOrbit.crossEq) is the setoid identifying displays that represent the same underlying ratio class. A character $\chi : \mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ is said to respect cross-equivalence when it sends cross-equivalent inputs to cross-equivalent outputs; that is the missing map-respects-setoid condition for treating a raw function as a quotient-native PRC character.
Orbit-product display compatibility asks something stronger-looking on the nose: when $a\cdot b=p$, the character on the direction of $p$ must agree (up to cross-equivalence) with the character on the ratio product of the factor directions. Upstream, orbitDirection_mul_crossEq already shows that the bare directions themselves are cross-equivalent under multiplication, so the product-display condition is not independent of setoid respect.
proof idea
Term-mode, essentially one application. Introduce nonzero $a,b,p$ and the hypothesis $a\cdot b=p$. Apply the crossEq-respect hypothesis of $\chi$ to the pair consisting of orbitDirection p and the ratio-orbit product of orbitDirection a with orbitDirection b. The required cross-equivalence premise is exactly orbitDirection_mul_crossEq, which states that those two displays are cross-equivalent whenever the underlying distinction naturals multiply. No further algebra is needed.
why it matters
This closes the gap between the bare character interface and the product-display obligation used in native cost uniqueness. Downstream, PRCPrimeCalibrationForcesOrbitProductDisplayCompatibilityTarget_of_crossEq_respect lifts the same implication to the prime-calibration target: once prime calibration forces crossEq-respect, product-display compatibility follows for free. It is also consumed on the path to PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved, where signed coherent prime orientation is propagated globally after crossEq-respect is recovered from normalize-ratio canonicity.
In the uniqueness blocker certificate stack, this is part of discharging the pure same-orientation product algebra so that the remaining obstruction is the mixed identity/reciprocal orientation of product factors. That obstruction sits inside the PRC native-cost uniqueness program, which aims to force the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) as the unique native cost on ratio orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.