PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_of_no_mixed
plain-language theorem explainer
Prime calibration that forbids mixed nonunit orbit orientations also forces the one-sided witness rule: any identity-oriented nonunit witness excludes every reciprocal-oriented nonunit witness. Orientation-coherence and native-cost uniqueness arguments cite this reduction. The proof is a one-line specialization of the character-level no-mixed implication under the prime-calibration hypotheses.
Claim. Assume that every ratio-orbit character $\chi$ that is prime-direction calibrated has no mixed nonunit orbit orientation (no identity-oriented nonunit direction coexists with a reciprocal-oriented one). Then every such $\chi$ also satisfies the one-sided witness-exclusion property: the existence of an identity-oriented nonunit witness is incompatible with every reciprocal-oriented nonunit witness.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit another orbit and is constrained by multiplicative and calibration axioms. Nonunit directions on the orbit space can be oriented either as identity-type or reciprocal-type; mixed orientation means both kinds appear among nonunit directions for the same $\chi$.
The no-mixed target asserts that prime-direction calibration already rules out that coexistence, which (with local orientation) is global nonunit orientation coherence. The witness-exclusion target is the one-sided globalization form: a single identity-oriented nonunit witness must exclude every reciprocal-oriented nonunit witness, stripping local orientation bookkeeping from witness arguments.
Upstream, the character-level lemma states that no-mixed orientation on a fixed $\chi$ already yields witness exclusion for that $\chi$. The present declaration lifts that implication to the quantified prime-calibration targets used in the native-cost uniqueness blocker stack.
proof idea
One-line wrapper. Introduce a character $\chi$ together with the ratio-character and prime-direction-calibration hypotheses. Apply the no-mixed target hypothesis at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain no mixed nonunit orbit orientation for $\chi$. Feed that fact into the character-level lemma PRCCharacterNonunitIdentityWitnessExcludesReciprocal_of_no_mixed, which converts no-mixed orientation into identity-witness exclusion of every reciprocal nonunit witness. No further algebraic work.
why it matters
Closes one arrow of the equivalence between the branch-coupling (no-mixed) target and the one-sided witness-exclusion target under prime calibration; the sibling converse plus this arrow give the iff used to swap formulations in uniqueness arguments.
Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, which packages zero-calibrated factorization and signed-admissible refutation into the native-cost uniqueness blocker, and appears in the conditional universal-foundation certificate that assembles kernel, real complete ordered field, and trace-logic passes. In the Recognition stack this is bookkeeping on the path toward J-cost uniqueness (T5) and the Recognition Composition Law: orientation coherence must not leave a reciprocal branch that could support a second native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.