PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_identity_witness_excludes
plain-language theorem explainer
Prime calibration that makes any identity-oriented nonunit witness incompatible with every reciprocal-oriented nonunit witness already forces global non-mixing of identity and reciprocal nonunit orbit orientations. Branch-coupling and native-cost uniqueness arguments in the primitive recognition calculus cite this target-level implication. The proof specializes the assumed exclusion target to a character and applies the character-level witness-exclusion lemma.
Claim. Assume that whenever $\chi$ is a ratio character that is prime-direction calibrated, any identity-oriented nonunit witness for $\chi$ excludes every reciprocal-oriented nonunit witness. Then, for every such $\chi$, no identity-oriented nonunit orbit direction coexists with any reciprocal-oriented nonunit orbit direction.
background
In the primitive recognition calculus, a ratio character $\chi$ maps ratio orbits to ratio orbits and carries orientation data on nonunit directions: identity-oriented versus reciprocal-oriented. Prime-direction calibration is a normalization condition on how $\chi$ treats prime generators.
Two packaged targets record what prime calibration is expected to force. The one-sided witness-exclusion target says an identity-oriented nonunit witness cannot coexist with any reciprocal-oriented nonunit witness ("strips local orientation out of witness globalization"). The branch-coupling target says no identity-oriented nonunit direction coexists with any reciprocal-oriented nonunit direction; together with local nonunit orientation this is global nonunit orientation coherence.
At fixed $\chi$, an upstream lemma already turns witness-exclusion into no-mixed orientation. The present result lifts that implication to the universally quantified target propositions used by uniqueness certificates.
proof idea
Short term proof. Introduce a ratio character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the assumed one-sided exclusion target at $\chi$ to obtain character-level nonunit identity-witness exclusion. Feed that hypothesis into the upstream lemma that converts identity-witness exclusion into no-mixed nonunit orbit orientation for a single character (that lemma unpacks a mixed pair into an identity witness and a reciprocal witness and invokes exclusion). No further algebra is done at the target layer.
why it matters
This is one direction of the equivalence between the one-sided witness-exclusion target and the no-mixed orientation target, so the two branch-coupling blockers may be swapped freely in certificate code. Downstream it feeds the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate: mixed identity/reciprocal nonunit branches would block coherent character factorization and native-cost uniqueness. Inside Recognition Science this is bookkeeping in the primitive recognition calculus that supports J-cost uniqueness (forcing step T5 and the Recognition Composition Law), not a new constant or dimension claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.