PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_product_no_mixed
plain-language theorem explainer
If prime calibration forces product-level no-mixing of identity and reciprocal orientations under native orbit multiplication, then it also forces the stronger branch-coupling property: no identity-oriented nonunit direction can coexist with a reciprocal-oriented one. Native-cost uniqueness and orientation-coherence arguments cite this implication. The proof is a one-line pointwise application of the character-level product-to-branch-coupling lemma.
Claim. Assume that every ratio-orbit character that is prime-direction calibrated has no mixed identity/reciprocal factor orientations under native multiplication. Then every such character also has no mixed nonunit orbit orientation: it cannot send one nonunit direction to the identity branch and another to the reciprocal branch.
background
In the Primitive Recognition Calculus, a ratio-orbit character $\chi$ assigns to each ratio orbit either the identity or reciprocal orientation. Prime-direction calibration constrains how $\chi$ behaves on prime generators. Two related global targets package what calibration is expected to force.
The product no-mixing target asserts that, for every calibrated character, native multiplication never multiplies an identity-oriented factor by a reciprocal-oriented factor. The branch-coupling (no-mixed nonunit) target is stronger in packaging: it forbids any identity-oriented nonunit direction from coexisting with any reciprocal-oriented nonunit direction. Together with local nonunit orientation, that is exactly global nonunit orientation coherence.
Upstream, the character-level lemma already shows that product no-mixing of a fixed $\chi$ implies no mixed nonunit orientation for that same $\chi$, by specializing the product condition to a pair of nonunit orbits and their product.
proof idea
Term-mode one-liner. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the product-no-mixing target hypothesis at $(\chi, h\chi, h\mathrm{prime})$ to obtain product no-mixing for $\chi$. Feed that into the character-level lemma PRCCharacterNoMixedNonunitOrbitOrientation_of_product_no_mixed, which converts product no-mixing into no mixed nonunit orientation. Discharge.
why it matters
This is one direction of the equivalence between the product no-mixing target and the branch-coupling target; the iff theorem cites it as the forward map. It is also the second component in the local-product-to-local-no-mixed packaging theorem, which upgrades a sharp local product hypothesis into the full local no-mixed target pair.
Downstream it feeds the native-cost uniqueness blocker certificate and, through the Universal Foundation layer, the conditional universal-foundation certificate. In the Recognition forcing picture this is orientation bookkeeping on the ratio lattice that supports uniqueness of the native cost (the $J$-cost side of T5), not a new physical constant. It closes a packaging gap: once product no-mixing is known, branch coupling is free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.