PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalNoMixedTarget_of_coherent
plain-language theorem explainer
Prime calibration that forces one coherent orientation on every nonunit ratio-orbit direction also forces the sharpened package of local orientation plus cross-nonunit no-mixing. Anyone tracking the two equivalent formulations of the nonunit-coherence target cites this direction. The proof is a two-component pair: local orientation from coherence, and the no-mixing target from the same coherent hypothesis.
Claim. Assume that whenever $\chi$ is a ratio character that is prime-direction calibrated, $\chi$ has a single coherent orientation on all nonunit orbit directions. Then the same prime-calibration hypothesis forces both (i) a local orientation branch on every nonunit orbit direction and (ii) the cross-nonunit no-mixing law (no identity-oriented nonunit direction coexists with a reciprocal-oriented one).
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and carry an orientation on each nonunit direction: either the identity branch or the reciprocal branch. Global nonunit orientation coherence means every nonunit direction shares one common branch. Local orientation is the weaker pointwise statement that each nonunit direction has some definite branch.
The coherent target asserts that prime-direction calibration forces full coherence for every such character. The local-no-mixed target splits that obligation into two pieces: local orientation on every nonunit direction, and a product-layer no-mixing law forbidding identity-oriented and reciprocal-oriented nonunit directions from coexisting. The module doc for the coherent target notes that once coherence is available, mixed product factors are impossible by nonunit non-self-reciprocity.
Upstream, PRCCharacterNonunitOrbitLocalOrientation_of_coherent extracts local orientation from a coherent character by case-splitting the global branch. The companion lemma PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_coherent already turns the coherent target into the no-mixing target.
proof idea
Term-mode pair constructor for the conjunction that defines the local-no-mixed target.
Left conjunct: introduce a character $\chi$ with the ratio-character and prime-calibration hypotheses, apply the coherent target hypothesis to obtain nonunit orientation coherence of $\chi$, then invoke PRCCharacterNonunitOrbitLocalOrientation_of_coherent to downgrade coherence to local orientation.
Right conjunct: one-line application of PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_coherent to the same coherent-target hypothesis.
why it matters
This is one arm of the equivalence PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_local_no_mixed, which identifies the strong coherent target with the sharpened local-plus-no-mixing package. That equivalence lets the uniqueness pipeline switch formulations without changing content.
Downstream it also feeds prc_native_cost_uniqueness_blocker_certificate, the certificate that packages the proved factorization targets and refutations closing the native-cost uniqueness blockers. In the broader Recognition chain this sits inside the PRC attack on native cost uniqueness, the calculus-level counterpart of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Establishing that prime calibration forces a single orientation branch is a step toward ruling out mixed character factorizations that would spoil uniqueness of the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.