PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_of_local_and_nomixed
plain-language theorem explainer
Local prime-axis orientation plus a global no-mixing ban already force a single coherent orientation (all identity or all reciprocal) on every native prime axis for calibrated ratio characters. Anyone assembling the PRC native-cost uniqueness blockers cites this glue step. The proof is a short case split on whether any prime is identity-oriented, then contradiction against mixing.
Claim. If prime cost calibration forces each prime axis to be oriented as either the identity or the reciprocal, and moreover forbids independent mixed identity/reciprocal choices across distinct prime axes, then it forces one coherent orientation on all native prime axes: for every ratio character $\chi$ that is prime-direction calibrated, either $\chi$ acts as the identity on every prime direction, or $\chi$ acts as the reciprocal on every prime direction.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit displays (signed numerator over a nonzero distinction-orbit denominator). Equality of two such displays is the internal cross-multiplication relation crossEq: the scaled numerators balance as signed orbits. Native primes are DistinctionNat positions that are nonzero, non-unit, and free of nontrivial factorization (primeOrbit).
A ratio character $\chi$ is a map on ratio orbits. Prime-direction calibration asks that $\chi$ respect the distinguished prime axes. The local orientation target only requires that each such axis is sent either to itself (identity branch) or to its reciprocal. The no-mixed target forbids pairing an identity choice on one prime with a reciprocal choice on another. The coherent target is the sharper global statement: one branch for all primes at once.
This lemma sits in the native-cost uniqueness module, where these orientation blockers feed the uniqueness argument for the PRC cost functional built from characters and doubled traces.
proof idea
Term-mode proof by introducing a calibrated ratio character $\chi$ and applying the two hypothesis targets to obtain local orientation and no-mixing for $\chi$. Case-split on the existence of some prime orbit $p_0$ whose image under $\chi$ is cross-equal to the identity prime direction.
If such a $p_0$ exists, take the identity disjunct of the coherent goal. For an arbitrary prime $p$, local orientation gives identity or reciprocal; the reciprocal case is eliminated by feeding the identity witness at $p_0$ and the reciprocal at $p$ into the no-mixing hypothesis.
If no identity prime exists, take the reciprocal disjunct. Local orientation again yields identity or reciprocal; identity would supply the forbidden existential witness, so every prime is reciprocal.
why it matters
Coherent prime orientation is the sharper orientation blocker A in the native-cost uniqueness stack: mixed independent prime inversions must be ruled out before cost uniqueness can close. This theorem is the pure logical glue that upgrades the local and no-mixed targets into that coherent target.
Downstream it is applied by PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_of_no_mixed_prime_witnesses (discharging coherence from a witness-form no-mixing hypothesis plus the already-proved local target) and by PRCPrimeCalibrationPropagationTarget_of_sharpened_orientation, which routes coherent orientation into global orientation and then into prime-calibration propagation. The same chain appears inside the native-cost uniqueness blocker certificate assembly.
In the broader Recognition forcing picture this is foundation-side hygiene on the character side of the cost, not yet the T5 J-uniqueness or RCL step, but it clears an orientation obstruction that would otherwise leave multiple native cost realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.