PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_nonunit_coherent
plain-language theorem explainer
Prime-direction calibration that forces a single coherent orientation on every nonunit ratio orbit automatically rules out mixed identity/reciprocal factors under native multiplication. Anyone tracking the PRC native-cost uniqueness blockers or the product-no-mixing target cites this implication. The proof is a one-line wrapper: apply the character-level coherence-to-no-mixing lemma pointwise to the calibrated character.
Claim. If every prime-direction-calibrated ratio character has a single coherent orientation on all nonunit orbits (all identity-oriented or all reciprocal-oriented), then every such character also has no mixed identity/reciprocal factor orientations under native multiplication of orbits.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ map ratio orbits to ratio orbits and encode how a native cost factors along multiplicative structure. Prime-direction calibration restricts $\chi$ on prime orbit directions. Two related targets appear in the native-cost uniqueness program.
The product no-mixing target asks that prime calibration prevent any product of nonunit orbits from carrying mixed identity and reciprocal orientations. The stronger nonunit-orientation-coherence target asks that prime calibration force a single global choice: every nonunit orbit direction is identity-oriented, or every one is reciprocal-oriented.
Upstream, the character-level lemma already shows that nonunit orientation coherence alone implies product no-mixing, by case-splitting on the global identity-versus-reciprocal alternative and using that nonunit orbits are not self-reciprocal. The present declaration lifts that implication from individual characters to the quantified prime-calibration targets.
proof idea
Term-mode one-line wrapper. Introduce a ratio character $\chi$ together with the hypotheses that it is a PRC ratio character and is prime-direction calibrated. Apply the assumed coherence target to those data to obtain nonunit orbit orientation coherence for $\chi$. Feed that coherence into the upstream lemma PRCCharacterOrbitProductNoMixedOrientation_of_nonunit_coherent, which returns product no-mixing for $\chi$. Discharge.
why it matters
This is one direction of the equivalence between the product-no-mixing target and the stronger nonunit-coherence target under prime calibration. Downstream, that equivalence is packaged as an iff, and both targets feed the native-cost uniqueness blocker certificate that records which factorization and orientation constraints have been proved or refuted.
In the Recognition Science forcing chain, native cost uniqueness is the PRC-side route toward T5 J-uniqueness: the cost $J(x)=(x+x^{-1})/2-1$ is the unique symmetric defect compatible with the Recognition Composition Law. Ruling out mixed orientations under calibrated multiplication is a necessary structural step before a character can be forced to match the doubled-trace/J form. The declaration itself is closed (proved); it does not discharge the coherence target, only shows that coherence is enough for product no-mixing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.