PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_no_mixed_nonunit
plain-language theorem explainer
If prime calibration already forces global nonunit orientation coherence (no identity-oriented nonunit direction coexists with a reciprocal-oriented one), then it also forces product no-mixing: mixed identity/reciprocal factor orientations under native multiplication are impossible. Anyone closing the branch-coupling side of native-cost uniqueness cites this implication. The proof is a one-line pointwise reduction through the character-level product lemma.
Claim. Assume that every prime-direction-calibrated ratio character $\chi$ has no mixed nonunit orbit orientations: an identity-oriented nonunit direction cannot coexist with a reciprocal-oriented nonunit direction. Then every such $\chi$ also has no mixed orientations among product factors under native multiplication.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode orientation data for the native cost. Prime-direction calibration is the local constraint that pins each prime direction's orientation. Two branch-coupling targets sit above that constraint.
The stronger target is global nonunit orientation coherence: under prime calibration, no identity-oriented nonunit direction may coexist with any reciprocal-oriented nonunit direction. The product target is weaker in form: under native multiplication, the two factors of a product must not carry opposite (identity vs reciprocal) orientations.
The module develops uniqueness of the native cost functional. These targets are the orientation-side blockers that keep the cost from admitting mixed-branch characters once primes are calibrated.
proof idea
Term-style reduction after introducing the character. Fix a ratio character $\chi$ that is prime-direction-calibrated. Apply the hypothesis to obtain no mixed nonunit orbit orientation for $\chi$. Feed that fact into the character-level lemma that turns global nonunit orientation coherence into product no-mixing (via nonunit non-self-reciprocity). Discharge.
why it matters
Closes the logical gap between the two branch-coupling targets in the native-cost uniqueness stack: once prime calibration forces coherent nonunit orientation, mixed product factors are automatic. Downstream uniqueness arguments can therefore assume the stronger orientation target and inherit product no-mixing for free.
In the broader Recognition forcing chain this is orientation bookkeeping beneath T5 (J-uniqueness). The native cost is the discrete avatar of $J$; ruling out mixed identity/reciprocal branches keeps the cost on a single coherent sheet, which is required before the d'Alembert/RCL identities can pin $J(x)=(x+x^{-1})/2-1$. No open scaffold remains on this arrow: the implication is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.