PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_local_no_mixed
plain-language theorem explainer
Prime calibration that already forces local nonunit orbit orientation and the cross-nonunit no-mixing law also forces a single coherent orientation on every nonunit orbit. Anyone reducing the native-cost uniqueness blocker to product-layer branch coupling cites this implication. The proof is a one-line lift: project the sharpened target and apply the character-level local-plus-no-mix lemma.
Claim. If prime calibration forces both (i) a local orientation branch on every nonunit ratio-orbit direction and (ii) the cross-nonunit no-mixing law, then prime calibration forces global nonunit orbit orientation coherence: every ratio character $\chi$ that is prime-direction calibrated is nonunit-orbit-orientation-coherent.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio characters $\chi$ act on ratio orbits. Prime-direction calibration is the standing hypothesis that pins how $\chi$ treats prime generators. Nonunit orbits are those not the unit class; each such direction can be oriented either as the identity branch or as the reciprocal branch.
Global nonunit orientation coherence asserts that a single choice of branch is used across all nonunit directions. The sharpened source target splits that obligation into two product-layer pieces: every nonunit direction has some local branch, and no identity-oriented nonunit direction coexists with a reciprocal-oriented one (the no-mixing law). The coherent target is the stronger global statement that mixed product factors become impossible once coherence holds, by nonunit non-self-reciprocity.
Upstream, the character-level lemma already shows that local orientation plus no-mixing imply coherence for a fixed $\chi$. The present declaration packages that fact at the calibration-target layer used by the uniqueness certificate.
proof idea
Term-mode one-line wrapper. Introduce a ratio character $\chi$ together with the ratio-character and prime-calibration hypotheses. From the sharpened target hypothesis extract the local-orientation half and the no-mixing half, each specialized at $\chi$. Feed those two facts into PRCCharacterNonunitOrbitOrientationCoherent_of_local_and_no_mixed, which returns nonunit orbit orientation coherence for $\chi$. That is exactly the coherent target.
why it matters
This is one direction of the equivalence between the coherent target and the local-plus-no-mixed sharpening; the sibling iff theorem quotes it as the reverse arrow. Downstream it feeds the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization and the refutation of signed admissible factorization as the remaining uniqueness gate.
In the Recognition framework this sits inside the foundation forcing chain that isolates the unique native cost (the $J$-cost of T5, $J(x)=(x+x^{-1})/2-1$) before $\phi$ and the eight-tick structure are forced. Coherent nonunit orientation is the branch-coupling step that rules out mixed reciprocal factors, so the cost functional cannot split across incompatible orbit orientations. Closing this target is part of discharging the uniqueness blocker rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.