PRCCharacterPrimeIdentityBranchUniform_of_local_no_mixed_prime_orientation
plain-language theorem explainer
Local prime-axis orientation plus a global ban on mixed identity/reciprocal choices forces branch uniformity: if any native prime axis is identity-oriented, every native prime axis is. Anyone closing the native-cost uniqueness blockers cites this bridge. The proof is a two-case split on the local disjunction, with the reciprocal case killed by the no-mix hypothesis.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose every prime axis is sent by $\chi$ either to itself or to its reciprocal, and $\chi$ never chooses identity on one prime axis while choosing reciprocal on another. Then identity orientation is uniform across primes: if $\chi$ fixes any prime direction, it fixes every prime direction.
background
In the primitive recognition calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction denominator). Characters $\chi$ act on these orbits. Prime directions are the native axes labelled by prime distinction naturals.
Local prime orientation is the algebraic content of matching $J$-costs on a single prime direction: for each prime $p$, $\chi$ sends the prime direction either to itself or to its reciprocal (cross-equality of orbits). No mixed prime orientation is the trace-coherence ban on independent prime-axis inversions: identity on one prime and reciprocal on another is forbidden.
Prime identity branch uniformity is the remaining obstruction after local orientation is known: if any native prime axis is identity-oriented, every native prime axis is. The module develops native-cost uniqueness by forcing characters that match the doubled-trace $J$-cost to be the identity branch on primes.
proof idea
Term-mode case split, no external lemmas. Fix primes $p,r$ and assume $\chi$ is identity on $p$'s prime direction. Apply local orientation at $r$: either $\chi$ is identity on $r$, or reciprocal on $r$. The identity case is the goal. The reciprocal case is absurd by no-mixed orientation applied to the identity witness at $p$ and the reciprocal witness at $r$ (False.elim).
why it matters
This is the pure logical bridge from local orientation plus no-mix to branch uniformity, without constructing traces. Downstream, PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_no_mixed_prime_orientation applies it once prime calibration has already forced local orientation, discharging the branch-uniformity target under a no-mix hypothesis. That target feeds the native-cost uniqueness blocker certificate, which packages the proved factorization and refuted signed-admissible paths for the uniqueness program.
In the Recognition framework this sits under native $J$-cost uniqueness (T5-adjacent): characters compatible with the cost must not flip prime axes independently. Branch uniformity is the combinatorial half of ruling out mixed reciprocal choices before full identity of the character is recovered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.