PRCCharacterNoMixedNonunitOrbitOrientation_of_product_no_mixed
plain-language theorem explainer
Product-level no-mixed orientation of a ratio-orbit character implies cross-nonunit no-mixing: identity orientation on one nonunit distinction cannot coexist with reciprocal orientation on another. Used to collapse product orientation constraints into global nonunit coherence. Proof instantiates the product hypothesis at factors p, r and product p*r, then projects the mixed-orientation obstruction.
Claim. Let $\chi$ be a map on ratio orbits. If product factors under $\chi$ cannot carry mixed identity/reciprocal orientations, then $\chi$ cannot assign identity orientation to one nonunit orbit direction and reciprocal orientation to another nonunit direction.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction, and RatioOrbit is a rational display (signed numerator over a nonzero orbit denominator). Characters $\chi$ act on these ratio orbits and induce orientation data: identity versus reciprocal direction on each nonzero orbit position.
Two related coherence predicates appear here. Product no-mixed orientation says that if nonunit nonzero factors $a,b$ multiply to a nonunit nonzero product $p$, then $\chi$ cannot orient one factor as identity and the other as reciprocal. Cross-nonunit no-mixing is the global branch-coupling statement: identity orientation at one nonunit direction cannot coexist with reciprocal orientation at another, independent of a displayed product factorization.
The local arithmetic facts used are that products of nonzero orbit positions stay nonzero, and that a left nonunit factor forces the product to be nonunit.
proof idea
Term-mode specialization. Fix nonunit nonzero $p,r$ with identity orientation at $p$ and reciprocal at $r$. Apply the product no-mixed hypothesis to the triple $(p,r,p\cdot r)$, feeding nonzero-ness of the product via mul_ne_zero and nonunit-ness of the product via orbit_mul_not_unit_of_left_not_unit. The product equality is reflexivity. The resulting obstruction's first disjunct is exactly the forbidden mixed pair $\langle$identity at $p$, reciprocal at $r\rangle$, which yields False.
why it matters
This is one direction of the equivalence between product no-mixed orientation and cross-nonunit no-mixing, so the two formulations of the residual orientation obstruction may be swapped freely. Downstream, prime-calibration targets that force product no-mixed orientation immediately force the no-mixed nonunit target and the full nonunit orientation-coherence target. It also sits in the native-cost uniqueness blocker certificate chain, which packages the residual obstacles to uniqueness of the native cost character after same-orientation product algebra is discharged. In the Recognition forcing picture this is bookkeeping on character orientation coherence ahead of J-uniqueness (T5) and the Recognition Composition Law, not a new physical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.