PRCCharacterNoMixedNonunitOrbitOrientation_of_identity_witness_excludes
plain-language theorem explainer
The one-sided exclusion form of branch coupling implies full cross-nonunit no-mixing for a ratio-orbit character χ. Anyone tracking global nonunit coherence of PRC characters will cite this. The proof is a three-line unpacking: package the identity witness existentially and discharge the universal reciprocal prohibition.
Claim. Let $\chi$ be a map on rational orbits. If the existence of any nonunit identity-orientation witness for $\chi$ already forbids every nonunit reciprocal-orientation witness, then $\chi$ has no mixed nonunit orbit orientations: identity orientation at one nonunit distinction cannot coexist with reciprocal orientation at another.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed numerator over a nonzero distinction denominator. Characters $\chi$ act on these orbits and may orient each nonunit distinction either as identity or as reciprocal.
Two equivalent-looking branch-coupling statements appear. The no-mixed form says: for all nonunit $p,r$, identity orientation at $p$ and reciprocal orientation at $r$ cannot both hold. The one-sided exclusion form says: if there exists even one nonunit identity witness, then no nonunit reciprocal witness is allowed. Local orientation existence is deliberately not bundled into either statement; only cross-nonunit coupling is at issue.
This lemma sits in the native-cost uniqueness development, where character orientation coherence is needed before cost-from-character and doubled-trace matching can force the unique native $J$-cost.
proof idea
Pure logical unpacking, no arithmetic. Introduce the universal data of the no-mixed goal: nonunit $p$ with identity orientation and nonunit $r$ with reciprocal orientation. Feed $\langle p,\ldots\rangle$ into the existential hypothesis of the exclusion form, then apply that hypothesis at $r$ to obtain False. The converse direction is a separate sibling lemma; together they feed the iff.
why it matters
Branch coupling is the global half of nonunit coherence for PRC characters: once one nonunit orbit is identity-oriented, no other nonunit orbit may be reciprocal-oriented. This direction closes half of the equivalence PRCCharacterNonunitIdentityWitnessExcludesReciprocal_iff_no_mixed, so either packaging may be used downstream.
It is also the bridge used by PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_identity_witness_excludes, lifting the same implication to the prime-calibration target layer. That layer feeds native-cost uniqueness: characters compatible with prime calibration cannot mix identity and reciprocal branches, which is required before the doubled-trace d'Alembert path can pin the cost to the unique $J$ of the forcing chain (T5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.