PRCCharacterOrbitProductNoMixedOrientation_of_no_mixed_nonunit
plain-language theorem explainer
If a ratio-orbit character never mixes identity orientation on one nonunit direction with reciprocal orientation on another, then it also never mixes those orientations on the two nonunit factors of a product. Anyone tracking native-cost uniqueness or prime-calibration coherence cites this implication. The proof is a short case split that instantiates the global no-mix hypothesis on the two factors.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that for any two nonzero nonunit distinction naturals $p$ and $r$, $\chi$ cannot place the identity orientation on the $p$-direction while placing the reciprocal orientation on the $r$-direction. Then whenever $a\cdot b=p$ with $a,b,p$ all nonzero and nonunit, $\chi$ cannot orient one of $a,b$ by identity and the other by reciprocal.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed orbit numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits and induce orientations on nonzero directions: identity versus reciprocal.
Two coherence predicates appear here. Cross-nonunit no-mixing says identity orientation at one nonunit orbit direction cannot coexist with reciprocal orientation at another; the doc calls this "the branch-coupling part of global nonunit coherence, separated from local orientation existence." Product no-mixed orientation says the two nonunit factors of a product cannot carry opposite orientations; it is "the exact obstruction left after the pure same-orientation product algebra is discharged."
The local setting is native-cost uniqueness for PRC characters: one must rule out mixed identity/reciprocal branch assignments that would spoil uniqueness of the cost reconstructed from the character.
proof idea
Term-mode proof by introduction and a two-sided constructor. Fix nonunit factors $a,b$ of a nonunit product $p$. The goal is to forbid both mixed pairs (identity on $a$ and reciprocal on $b$; reciprocal on $a$ and identity on $b$).
Each mixed pair is discharged by applying the hypothesis PRCCharacterNoMixedNonunitOrbitOrientation directly to the two factors (swapping order in the second case). Product data and unit-negation hypotheses are unused beyond the intro binders; the global cross-nonunit statement already specializes to any pair of nonunits.
why it matters
This is one half of the equivalence between product-factor no-mixing and global cross-nonunit no-mixing (PRCCharacterOrbitProductNoMixedOrientation_iff_no_mixed_nonunit). Downstream, identity-branch transport yields product no-mixing by composing with this lemma, and prime-calibration targets lift the same way (PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_no_mixed_nonunit).
It feeds the native-cost uniqueness blocker certificate path: mixed orientations on product factors are the residual obstruction after same-orientation product algebra is cleared. In the broader RS forcing picture this is bookkeeping inside character/cost uniqueness (toward the unique $J$-cost of T5 and the Recognition Composition Law), not a new physical constant, but it closes a concrete branch-coherence gap in the PRC native-cost stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.