PRCCharacterNonunitOrbitOrientationCoherent_of_local_and_no_mixed
plain-language theorem explainer
Local orientation plus cross-nonunit no-mixing forces global coherence of character orientation on nonunit orbits: every nonunit direction is identity, or every one is reciprocal. Anyone assembling the native-cost uniqueness chain cites this bridge from pointwise alternatives to a single branch. The proof is a pure case split on existence of an identity-oriented nonunit direction, with no-mixing killing the mixed case.
Claim. If a ratio-orbit character $\chi$ is locally oriented on every nonunit direction (each is either the identity branch or the reciprocal branch) and identity orientation at one nonunit never coexists with reciprocal orientation at another, then $\chi$ is globally coherent on nonunits: either every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented.
background
In the Primitive Recognition Calculus, a ratio orbit displays rational structure as a signed numerator over a nonzero distinction-orbit denominator. DistinctionNat is the base-neutral finite orbit of repeated distinction; its only multiplicative unit is the one-step orbit.
A character $\chi$ acts on ratio orbits. Local nonunit orientation asserts that for every nonzero nonunit distinction $p$, $\chi$ chooses either the identity direction or the reciprocal direction on that axis (the nonprime analogue of the already-proved local-prime alternative). Cross-nonunit no-mixing is the branch-coupling constraint: identity at one nonunit cannot coexist with reciprocal at another. Coherence is the global disjunction: all identity, or all reciprocal, which is strong enough to rule out mixed product factors.
The surrounding module develops native-cost uniqueness by forcing characters to match the doubled-trace / J-cost structure; orientation coherence is the intermediate target that keeps product factors on a single branch.
proof idea
Case-split on whether there exists a nonzero nonunit $p$ carrying identity orientation under $\chi$.
If such a $p_0$ exists, fix any other nonunit $q$. Local orientation supplies identity or reciprocal at $q$. Reciprocal at $q$ together with identity at $p_0$ is exactly the forbidden mixed pair, so $q$ must be identity. Quantifying over $q$ yields the all-identity disjunct of coherence.
If no identity-oriented nonunit exists, local orientation at an arbitrary nonunit $q$ cannot land on identity (that would witness the existential), so every nonunit is reciprocal, giving the all-reciprocal disjunct.
No external lemmas beyond the three named predicates are required; the argument is pure classical case analysis.
why it matters
This is the pure logical glue that turns local orientation plus no-mixing into the coherent target used throughout native-cost uniqueness. Downstream, several prime-calibration force theorems reduce their coherent-target goals to a local-and-no-mixed package by applying this lemma directly (the local-no-mixed, local-product-no-mixed, and product-no-mixed variants). The identity-branch-transport path also routes through it, and the native-cost uniqueness blocker certificate ultimately depends on the coherent orientation infrastructure.
In the Recognition Science forcing picture, keeping character branches aligned on nonunit orbits prevents mixed-factor pathologies that would otherwise block recovery of the unique J-cost (T5) from the Recognition Composition Law on the orbit lattice. Without this bridge, local alternatives alone do not rule out inconsistent product orientations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.