PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_no_mixed_nonunit
plain-language theorem explainer
Equivalence of two prime-calibration targets on ratio-orbit characters: product no-mixing (no mixed identity/reciprocal factor orientations under native multiplication) is the same as branch-coupling (no identity-oriented nonunit direction coexists with a reciprocal-oriented one). Native-cost uniqueness and blocker-certificate work cite this bridge. Proof is a pure Iff constructor from the two already-proved one-way implications.
Claim. The following two assertions are equivalent. (A) Every prime-direction-calibrated ratio character has no mixed identity/reciprocal orientations under native orbit products. (B) Every prime-direction-calibrated ratio character has coherent nonunit orientation: no identity-oriented nonunit direction coexists with any reciprocal-oriented nonunit direction.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit another orbit and is required to respect the multiplicative structure used to build the native cost. Prime-direction calibration fixes how $\chi$ acts on prime generators of the orbit lattice, pinning the local choice between the identity branch and the reciprocal branch.
Two blocker targets package what calibration is expected to force. The product no-mixing target says calibrated characters never mix identity and reciprocal orientations across factors of a native product. The branch-coupling (no-mixed-nonunit) target is stronger in wording: it forbids any identity-oriented nonunit direction from living alongside any reciprocal-oriented nonunit direction. With local nonunit orientation, that is global orientation coherence.
Both targets live in the native-cost uniqueness module, which isolates which calibration hypotheses would pin the cost functional uniquely (and which are already refuted).
proof idea
Term-mode Iff pair. The forward arrow is the existing lemma that product no-mixing implies no-mixed-nonunit orientation (apply the product hypothesis to $\chi$, then the character-level product-to-branch lemma). The reverse arrow is the dual lemma that no-mixed-nonunit implies product no-mixing (same pattern with the character-level branch-to-product lemma). No new calculus; just packaging the two directions as $\leftrightarrow$.
why it matters
This bridge lets the development treat product no-mixing and branch-coupling as interchangeable calibration demands. Downstream, the no-mixed-nonunit target is refuted by transporting the product-side refutation across this iff (.mpr). The same equivalence feeds the native-cost uniqueness blocker certificate and appears in the conditional universal-foundation certificate stack.
In the Recognition forcing picture, native-cost uniqueness is the gate before J-uniqueness (T5) and the self-similar fixed point $\phi$ (T6). Showing two candidate blockers are the same proposition cleans the certificate graph: one refutation kills both wordings. It does not itself force J or $\phi$; it only collapses redundant target language on the path toward those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.