PRCCharacterOrbitProductNoMixedOrientation_iff_no_mixed_nonunit
plain-language theorem explainer
For a character on rational orbits, forbidding mixed identity/reciprocal orientations on product factors is equivalent to forbidding mixed orientations across any pair of nonunit orbits. Native-cost uniqueness arguments cite this to collapse two formulations of the same coherence obstruction. The proof is a pure Iff constructor from the two one-direction lemmas already proved in-module.
Claim. Let $\chi$ be a map on rational orbits. Then the following are equivalent: (i) whenever nonunit nonzero factors $a,b$ multiply to a nonunit nonzero $p$, $\chi$ cannot orient one factor by identity and the other by reciprocal; (ii) $\chi$ cannot assign identity orientation to one nonunit orbit direction and reciprocal orientation to another nonunit orbit direction.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction denominator). Orientation of an orbit direction is either identity or reciprocal; native cost uniqueness needs global coherence of those choices so that the character-derived cost matches the unique $J$-cost forced by the Recognition Composition Law.
Two Prop-level hypotheses package the remaining mixing obstruction. Product no-mixed orientation says that if nonunit nonzero $a,b$ multiply to nonunit nonzero $p$, then $\chi$ cannot mark one factor identity and the other reciprocal. Cross-nonunit no-mixed orientation says identity orientation at one nonunit direction cannot coexist with reciprocal orientation at any other nonunit direction (branch-coupling, separate from local existence of an orientation).
Both are the residual obstruction after same-orientation product algebra is discharged; this theorem identifies them.
proof idea
Term-mode Iff pair. The forward arrow is PRCCharacterNoMixedNonunitOrbitOrientation_of_product_no_mixed: from product no-mixed, instantiate the product hypothesis at $a=p$, $b=r$, $p\cdot r$ to rule out identity-at-$p$ with reciprocal-at-$r$. The reverse arrow is PRCCharacterOrbitProductNoMixedOrientation_of_no_mixed_nonunit: from cross-nonunit no-mixed, any mixed identity/reciprocal pair of product factors immediately yields the forbidden cross-nonunit pair. No further algebra.
why it matters
Feeds prc_native_cost_uniqueness_blocker_certificate, which packages the proved factorization targets and refutations that close the native-cost uniqueness blocker. Equating the product-factor formulation with the global cross-nonunit formulation lets downstream certificates cite whichever shape is convenient without a coherence gap.
In the forcing chain this sits under T5 $J$-uniqueness: native cost must be the unique $J(x)=(x+x^{-1})/2-1$ compatible with the Recognition Composition Law. Mixed identity/reciprocal orientations on nonunit orbits would spawn a second admissible character cost; collapsing the two no-mixing Props removes that residual degree of freedom before the uniqueness certificate is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.