PRCCharacterNoMixedNonunitOrbitOrientation_of_coherent
plain-language theorem explainer
Global coherence of nonunit orbit orientations (every nonunit direction is identity, or every one is reciprocal) implies the no-mixing property: identity at one nonunit cannot coexist with reciprocal at another. Cited by the prime-calibration forcing target and the native-cost uniqueness blocker certificate. Proof is a two-case term argument: each global branch forces a nonunit direction to equal its reciprocal under cross-equivalence, which is impossible.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If nonunit orbit orientation under $\chi$ is coherent (either every nonunit distinction $p$ has identity orientation, or every such $p$ has reciprocal orientation), then $\chi$ has no mixed nonunit orbit orientation: there cannot exist nonunits $p$ and $r$ with identity orientation at $p$ and reciprocal orientation at $r$.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction denominator. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality). The reciprocal map on ratio orbits sends zero to zero and otherwise inverts.
For a nonzero distinction $p$, orbitDirection is the ratio orbit with numerator the signed orbit of $p$ and denominator one. A character $\chi$ orients that direction either as identity or as reciprocal. Coherence means the choice is global on all nonunits: all identity, or all reciprocal. No-mixing is the pairwise consequence: identity at one nonunit and reciprocal at another is forbidden.
The module develops native-cost uniqueness for PRC characters. This lemma separates branch-coupling (no mixed orientations) from local orientation existence, so later calibration hypotheses can force the global branch without re-proving pairwise incompatibility.
proof idea
Assume coherence and, for contradiction, identity orientation at nonunit $p$ and reciprocal orientation at nonunit $r$. Case-split on coherence.
If every nonunit is identity-oriented, apply that to $r$ to get identity at $r$. Symmetry and transitivity of crossEq then yield that the orbit direction of $r$ is cross-equivalent to its own reciprocal. The lemma orbitDirection_nonunit_not_crossEq_recip rules that out for nonunits.
If every nonunit is reciprocal-oriented, the same construction at $p$ (identity hypothesis plus global reciprocal) again produces a nonunit direction cross-equivalent to its reciprocal, and the same impossibility lemma closes the case.
why it matters
Native cost uniqueness in PRC needs characters whose nonunit orientations do not mix identity and reciprocal branches; mixed factors would spoil the doubled-trace / d'Alembert route to the unique $J$-cost. This theorem converts the strong global coherence hypothesis into the pairwise no-mixing predicate used downstream.
It is applied directly by PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_coherent, which lifts prime-calibration forcing of coherence to forcing of no-mixing. That target feeds the native-cost uniqueness blocker certificate packaging zero-calibrated factorization results. In the broader Recognition chain, ruling out mixed orientations protects the path to T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$) under the Recognition Composition Law, by keeping character factors on a single reciprocal branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.