PRCCharacterPrimeIdentityBranchUniform_of_local_no_distinct_prime_pair
plain-language theorem explainer
Under local prime orientation, forbidding mixed identity/reciprocal choices on distinct native primes forces global identity-branch uniformity: if any prime axis is fixed, every prime axis is fixed. Native-cost uniqueness and prime-calibration arguments cite this bridge. The proof is a short case split on whether the two primes coincide, discharging the unequal case by the mixed-pair exclusion.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose every native prime direction is sent by $\chi$ either to itself or to its reciprocal (local prime orientation), and suppose there is no pair of distinct native primes on which $\chi$ chooses identity on one and reciprocal on the other. Then identity orientation is uniform across primes: whenever $\chi$ fixes one prime direction, it fixes every prime direction.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. Native primes determine distinguished ratio directions via primeDirection. A ratio character $\chi$ acts on these orbits; the cost uniqueness programme asks when the cost generated by $\chi$ must match the canonical $J$-cost on prime axes.
Local prime orientation is the single-axis content of $J$-cost equality: for each prime $p$, $\chi$ sends the prime direction either to itself or to its reciprocal. A distinct-prime mixed-pair witness is the obstruction that $\chi$ picks identity on one prime and reciprocal on a different prime. Prime identity branch uniformity says the identity choice cannot be partial: if any prime is identity-oriented, every prime is.
The module develops native-cost uniqueness from character and trace hypotheses. This lemma is the purely combinatorial half of the local-orientation $\leftrightarrow$ no-mixed-pair equivalence for the identity branch.
proof idea
Term-mode proof by direct introduction of primes $p,r$ and an identity hypothesis on $p$. Case on $p=r$: if equal, substitute and the identity hypothesis on $p$ is the claim (after unfolding the prime-direction notation). If unequal, apply local orientation to $r$: the identity disjunct is exactly the goal; the reciprocal disjunct packages with the identity on $p$ and $p\neq r$ into a mixed-pair witness, contradicting the no-distinct hypothesis via False.elim.
why it matters
This is one direction of the local iff that equates identity-branch uniformity with absence of distinct-prime mixed pairs under local orientation. Downstream, the calibration theorem PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_no_distinct_prime_pair_witness_character applies it after promoting prime calibration to local orientation, so calibrated characters cannot mix identity and reciprocal on distinct primes without breaking uniformity.
That target feeds the broader native-cost uniqueness chain: ruling out independent prime-axis inversions is the remaining obstruction once local $J$-agreement is known, before global character-to-cost matching. The universal-foundation conditional certificate lists related PRC kernel and trace infrastructure among its components, so this combinatorial step sits on the path from local prime $J$-equality toward the forced unique native cost (the $J$-uniqueness landmark T5 in the forcing chain).
No scaffolding remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.