PRCCharacterOrbitProductNoMixedOrientation_of_nonunit_coherent
plain-language theorem explainer
Global coherence of nonunit orbit orientations (all identity, or all reciprocal) implies that product factors cannot mix those orientations. Anyone closing the native-cost uniqueness chain for ratio characters will cite this. The proof is a two-branch case split: each mixed pair forces some nonunit direction to equal its reciprocal under cross-equivalence, which is impossible.
Claim. Let $\chi$ assign to each ratio orbit another ratio orbit. Suppose every nonunit nonzero distinction has the same orientation under $\chi$: either all are identity-oriented, or all are reciprocal-oriented. Then for any factorization $a\cdot b=p$ of nonunit nonzero distinctions, the pair $(a,b)$ cannot be mixed (one identity-oriented and one reciprocal-oriented) under $\chi$.
background
In the primitive recognition calculus, ratio data live on RatioOrbit: a signed numerator orbit over a nonzero distinction denominator. Equality of displays is the internal cross-multiplication relation crossEq (K4.10): two orbits match when scaled numerators balance. Reciprocals are total on this type, sending the zero display to zero.
Each nonzero distinction $p$ has a canonical direction orbitDirection p, the ratio with numerator the signed orbit of $p$ and denominator one. A character $\chi$ orients that direction either as identity or as reciprocal. Coherence of nonunit orientations means the choice is uniform across all nonunit nonzero distinctions: the whole family is identity-oriented, or the whole family is reciprocal-oriented.
The product no-mix predicate is the residual obstruction after same-orientation product algebra is already handled: for a factorization $a\cdot b=p$ of nonunits, the two factors must not carry opposite orientations. The module sits in native-cost uniqueness for PRC characters, where orientation bookkeeping feeds doubled-trace and d'Alembert constraints tied to the J-cost lineage.
proof idea
Term-mode proof by introducing the product data and case-splitting the coherence hypothesis into the all-identity branch and the all-reciprocal branch.
In the all-identity branch, a mixed pair is either (identity at $a$, reciprocal at $b$) or the reverse. Coherence supplies identity at the reciprocal-tagged factor; symmetry and transitivity of crossEq then identify that factor's orbitDirection with its own reciprocal. The lemma orbitDirection_nonunit_not_crossEq_recip rules that out for nonunits.
The all-reciprocal branch is symmetric: coherence forces reciprocal orientation on the identity-tagged factor, again producing a self-reciprocal cross-equivalence and the same contradiction. No multiplicative arithmetic beyond the given factorization hypotheses is used.
why it matters
This lemma converts a global orientation-coherence hypothesis into the exact product no-mix obstruction named in the module as what remains after pure same-orientation product algebra is discharged. Downstream, PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_nonunit_coherent is a one-line application: prime-calibration coherence targets yield the corresponding no-mix target for characters.
It also feeds the local-orientation propagation path under display-compatible no-mix, and ultimately the native-cost uniqueness blocker certificate that packages zero-calibrated factorization targets. In the broader Recognition forcing picture, native cost uniqueness is the character-level route toward the unique J-cost ($J(x)=(x+x^{-1})/2-1$, T5) and the Recognition Composition Law; keeping product orientations unmixed is a necessary bookkeeping step so that cost-from-character constructions cannot flip branches mid-factorization.
No open scaffold remains here: the claim is fully proved and only packages prior nonunit non-self-reciprocal facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.