PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_identity_branch_transport
plain-language theorem explainer
Equivalence of two branch-coupling blockers under prime calibration: forbidding mixed identity/reciprocal orientations in orbit products is the same as forcing identity-branch transport on every nonunit direction. Native-cost uniqueness certificates and the product-no-mixing refutation cite it. Proof is a pure Iff pair from the two already-proved one-way implications.
Claim. The assertion that prime calibration forces every ratio character to have no mixed identity/reciprocal factor orientations under native orbit multiplication is equivalent to the assertion that prime calibration forces identity-branch transport across all nonunit directions: if any nonunit direction stays identity-oriented, that identity branch extends to every nonunit direction.
background
In the Primitive Recognition Calculus, ratio characters assign to each ratio orbit another orbit, subject to multiplicative and calibration constraints. Prime-direction calibration pins the character on prime generators. Two blocker targets encode the same orientation rigidity in different languages.
The product no-mixing target says that, once a character is prime-calibrated, native multiplication never multiplies an identity-oriented factor by a reciprocal-oriented factor. The identity-branch transport target is the positive dual: if any nonunit direction remains identity-oriented under that calibration, the identity branch must transport to every nonunit direction.
Both sit in the native-cost uniqueness module, which isolates which cost functionals can arise from PRC characters. Upstream one-way theorems already connect product no-mixing to orientation coherence and thence to transport, and conversely recover no-mixing from transport via the character-level no-mixing lemma.
proof idea
Term-mode Iff constructor. The forward arrow is the existing theorem that product no-mixing implies nonunit identity-branch transport (via the intermediate coherent-orientation target). The reverse arrow is the existing theorem that identity-branch transport implies product no-mixing, by applying the character-level transport-to-no-mixing lemma at each calibrated character. No new algebra is done here.
why it matters
Closes the logical loop between the two blocker formulations so either can be attacked or discharged. Downstream, the product-no-mixing target is refuted by transporting the identity-branch-transport refutation across this equivalence (mp). The same link feeds the native-cost uniqueness blocker certificate and, indirectly, the conditional universal-foundation certificate in UniversalFoundation.
In the Recognition forcing chain this is local scaffolding around native J-cost uniqueness (T5 territory: the unique cost compatible with the Recognition Composition Law), not a direct T0–T8 step. It records that mixed orientation under multiplication is not an independent obstruction once branch transport is settled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.