PRCCharacterNonunitIdentityWitnessExcludesReciprocal_of_no_mixed
plain-language theorem explainer
If a ratio-orbit character never mixes identity orientation on one nonunit with reciprocal orientation on another, then the existence of any nonunit identity witness already rules out every nonunit reciprocal witness. Cost-uniqueness and prime-calibration arguments cite this as the one-sided packing of branch coupling. The proof is a three-line unpack of the existential witness followed by direct application of the universal no-mix hypothesis.
Claim. Let $\chi$ be a map on rational orbits. Suppose that for all nonzero nonunit distinction naturals $p$ and $r$, identity orientation of $\chi$ at $p$ cannot coexist with reciprocal orientation of $\chi$ at $r$. Then: if there exists at least one nonzero nonunit $p$ at which $\chi$ has identity orientation, no nonzero nonunit $r$ can have reciprocal orientation under $\chi$.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction-natural denominator). Orientation of a character at a nonzero distinction natural records whether the character treats that orbit direction as the identity branch or the reciprocal branch.
PRCCharacterNoMixedNonunitOrbitOrientation is the universal branch-coupling statement: identity orientation at one nonunit cannot coexist with reciprocal orientation at any other nonunit. The doc-comment separates this from local orientation existence: it is only the cross-nonunit coherence half of global nonunit coherence.
PRCCharacterNonunitIdentityWitnessExcludesReciprocal is the one-sided existential packing of the same coupling: once any nonunit identity witness is present, every nonunit reciprocal witness is forbidden. Local orientation existence is deliberately not bundled into that predicate.
proof idea
Term-mode unpacking, not a deep argument. Introduce the existential nonunit identity witness $(p, hp, h_{\mathrm{unit}}, h_{\mathrm{id}})$ and an arbitrary candidate reciprocal witness $(r, hr, h_{\mathrm{unit}}', h_{\mathrm{rec}})$. Feed those eight data into the universal no-mix hypothesis hnomix. The resulting False is exactly the consequent of the one-sided exclusion predicate. No auxiliary lemmas are required beyond the two predicate definitions.
why it matters
This is one direction of the equivalence PRCCharacterNonunitIdentityWitnessExcludesReciprocal_iff_no_mixed, which identifies the universal no-mix form with the existential-witness exclusion form of branch coupling. Downstream, PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_of_no_mixed lifts the same implication to the prime-calibration target layer: once calibration forces no-mixed orientation, it forces the one-sided exclusion target as well.
In the Recognition Science foundation stack this sits inside native cost uniqueness for PRC characters. Branch coupling is what keeps the doubled-trace / d'Alembert side of the native cost from admitting mixed reciprocal and identity nonunit readings, which would break uniqueness of the cost functional descending from the Recognition Composition Law and the T5 J-cost $J(x)=(x+x^{-1})/2-1$. The lemma itself is pure logical packaging; the physics content lives in the calibration hypotheses that discharge the no-mix premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.