PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_coherent
plain-language theorem explainer
If prime calibration forces a single coherent orientation on every nonunit orbit direction, then it also forbids mixed identity/reciprocal orientations among those directions. Native-cost uniqueness arguments cite this as the bridge from the strong coherence target to the branch-coupling no-mix target. The proof is a one-line pointwise application of the character-level coherence-implies-no-mix lemma.
Claim. Assume that every ratio-orbit character that is prime-direction calibrated has a single coherent orientation on all nonunit orbit directions. Then every such character also satisfies the no-mixed condition: no identity-oriented nonunit direction coexists with a reciprocal-oriented nonunit direction.
background
In the primitive recognition calculus, ratio characters act on ratio orbits and carry orientation data on nonunit directions: each such direction is either identity-oriented or reciprocal-oriented. Global nonunit orientation coherence means all nonunit directions share one orientation; the no-mixed property is the weaker statement that the two orientations never appear together.
The coherent target asserts that prime-direction calibration forces full coherence for every ratio character. The no-mixed target asserts only that calibration forbids mixed identity/reciprocal pairs. The module treats the coherent target as the stronger replacement for product no-mixing: once coherence holds, mixed product factors are ruled out by nonunit non-self-reciprocity.
Upstream, the character-level lemma already shows that coherence of a single character implies its no-mixed property, by case-splitting on the global identity-versus-reciprocal alternative.
proof idea
One-line wrapper. Introduce a ratio character $\chi$ that is a ratio character and prime-direction calibrated. Apply the coherent target hypothesis to obtain nonunit orbit orientation coherence for $\chi$. Feed that coherence into the character-level lemma, which returns the no-mixed orientation property for $\chi$. Discharge the target quantifiers.
why it matters
This is the target-level packaging of coherence-implies-no-mix under prime calibration. Downstream it feeds the local no-mixed target-of-coherent theorem (pairing local orientation with no-mix to recover global coherence structure) and sits in the native-cost uniqueness blocker certificate stack, which certifies factorization and signed-admissible blockers for the uniqueness program.
In the Recognition Science foundation layer this is bookkeeping on the way to uniqueness of the native cost (the $J$-cost forced by the Recognition Composition Law and T5). It does not itself force $J$ or $\phi$; it only tightens orientation constraints that calibration must impose on nonunit orbits so mixed branches cannot spoil uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.