PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_product_no_mixed
plain-language theorem explainer
Under prime calibration of a ratio character, ruling out mixed identity/reciprocal factors in products upgrades to a single coherent orientation on every nonunit orbit. Native-cost uniqueness and universal-foundation certificates cite this bridge. The proof wires local prime orientation, product-factor propagation from display compatibility, and the no-mixed nonunit lemma into the local-plus-no-mixed coherence criterion.
Claim. Assume that whenever $\chi$ is a ratio character that is prime-direction calibrated, products of nonunit orbits never mix identity-oriented and reciprocal-oriented factors. Then every such $\chi$ has a single coherent orientation across all nonunit orbit directions.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ maps ratio orbits to ratio orbits and is the algebraic carrier from which the native cost is recovered (via doubled-trace / d'Alembert structure). Prime-direction calibration fixes the orientation of $\chi$ on prime axes: each prime orbit is sent either to itself (identity branch) or to its reciprocal.
Product no-mixing says that if two nonunit factors are oriented, their product cannot pair an identity factor with a reciprocal factor. The stronger coherence target demands one global choice: either every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented. The module treats coherence as the preferred replacement for bare product no-mixing, because nonunit non-self-reciprocity then forbids mixed products automatically.
Upstream, local orientation on primes is already proved from calibration; product-local propagation follows from display compatibility plus no-mixing; and coherence is exactly local nonunit orientation plus the no-mixed nonunit condition.
proof idea
Term-mode assembly, not a new calculation. Fix $\chi$, character hypotheses, and prime calibration. From the assumed product no-mixing target and the already-proved display-compatibility target, obtain product-local orientation propagation. Combine that with the proved local-prime-orientation target to get local orientation on all nonunit orbits. Separately, product no-mixing specializes to the no-mixed nonunit orientation predicate. Feed those two facts into the lemma that local orientation plus no-mixed nonunit orientation yields global nonunit orientation coherence.
why it matters
This is the one-direction half of the equivalence between the product no-mixing target and the nonunit coherence target, so either formulation can be used as the calibration obligation. Downstream it discharges the hypothesis of the identity-branch transport target (via the coherent route), and it is the sink for alternative closures that first obtain product no-mixing from an identity-witness globalization or a successor-step pair. It appears in the native-cost uniqueness blocker certificate chain and in the conditional universal-foundation certificate. In framework terms it is part of locking the character that feeds J-uniqueness (T5) and the native cost, ensuring orientation does not flip across the multiplicative orbit lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.