PRCCharacterNonunitIdentityWitnessExcludesReciprocal_iff_no_mixed
plain-language theorem explainer
Equivalence of two formulations of branch coupling for a ratio-orbit character: one-sided exclusion (any nonunit identity witness forbids every nonunit reciprocal witness) matches universal no-mixing (no pair of nonunit orbits may carry opposite orientations). Cited when packaging global nonunit coherence of PRC characters. Proof is the bidirectional packaging of the two already-proved implications.
Claim. For a map $\chi$ from ratio orbits to ratio orbits, the following are equivalent: (i) if some nonunit distinction carries identity orbit orientation under $\chi$, then no nonunit distinction carries reciprocal orbit orientation; (ii) identity orientation at one nonunit distinction and reciprocal orientation at another never coexist under $\chi$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction denominator (K4.7). Characters act as maps $\chi$ on these orbits. Orbit direction predicates record whether $\chi$ orients a given nonunit distinction as the identity branch or the reciprocal branch.
Two Prop-level formulations of branch coupling appear here. The no-mixed form asserts universally that identity orientation at one nonunit orbit and reciprocal orientation at another are incompatible. The one-sided exclusion form asserts that the mere existence of any nonunit identity witness already rules out every nonunit reciprocal witness. Local orientation existence is deliberately not bundled into either statement; both isolate the cross-nonunit coupling half of global nonunit coherence.
The two directions of the equivalence are already available as separate theorems in this module: exclusion implies no-mixed, and no-mixed implies exclusion.
proof idea
Term-mode packaging of an iff. The left-to-right arrow is the existing lemma that turns one-sided exclusion into universal no-mixing (introduce the two nonunit witnesses and feed the existential package into exclusion). The right-to-left arrow is the dual lemma that turns no-mixing into exclusion (unpack the existential identity witness and apply no-mixing pointwise). No new arithmetic or case analysis appears.
why it matters
Native cost uniqueness for PRC characters needs a clean statement of branch coupling: identity and reciprocal nonunit orientations must not mix, or the doubled-trace / d'Alembert route to the unique J-cost can fork. This declaration identifies the existential one-sided exclusion form with the universal no-mixed form, so either may be used as the coupling hypothesis without loss.
It sits in the Foundation forcing path toward T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) via the Recognition Composition Law, where character orientation coherence is part of locking the cost functional. No downstream consumers are recorded yet; the lemma is infrastructure for later global nonunit coherence and native-cost uniqueness theorems in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.