PRCCharacterNoMixedNonunitOrbitOrientation
plain-language theorem explainer
Cross-nonunit no-mixing for a ratio-orbit character: identity orientation on one nonunit direction cannot coexist with reciprocal orientation on another. Anyone proving global nonunit coherence or branch transport cites this Prop. It is a pure predicate definition, not a proved theorem.
Claim. A map $\chi$ on ratio orbits has no mixed nonunit orbit orientation when, for all nonzero nonunit distinction-orbit indices $p$ and $r$, if $\chi$ is identity-oriented at the orbit direction of $p$ then it cannot be reciprocal-oriented at the orbit direction of $r$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction, and the native unit predicate holds only for the one-step orbit. A RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-orbit denominator.
A character $\chi$ assigns to each ratio orbit another ratio orbit. Identity orientation at a nonzero direction $p$ means $\chi$ fixes the orbit direction of $p$ up to the native cross-equality; reciprocal orientation means $\chi$ sends that direction to its reciprocal. The identity event of observer forcing sits at the J-cost minimum $x=1$, which anchors the identity branch of the character.
This module isolates native cost uniqueness for such characters. The present definition separates the branch-coupling (no-mixing) half of global nonunit coherence from the local existence of an orientation at each nonunit direction.
proof idea
Definitional: the body is the universal Prop that any pair of nonzero nonunit directions cannot simultaneously carry identity orientation and reciprocal orientation under $\chi$. It composes the already-defined identity-orientation and reciprocal-orientation predicates on arbitrary nonzero orbit directions; there is no proof obligation beyond the Prop encoding.
why it matters
This is the branch-coupling fragment of global nonunit coherence for PRC characters, the half that forbids mixed identity/reciprocal orientations across nonunit directions. Downstream, coherence, identity branch transport, identity-witness exclusion of the reciprocal, and product no-mixing each imply this Prop; conversely it pairs with local orientation to recover identity branch transport, and it is equivalent to the identity-witness-excludes-reciprocal form.
In the Recognition forcing picture this keeps the character on a single branch away from the identity event, so the native cost built from the character can match the unique J-cost (T5) without orientation flips on composite orbit positions. It does not itself force J-uniqueness or the phi fixed point; it is infrastructure those uniqueness arguments rely on when characters act on the orbit lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.