PRCCharacterNoMixedPrimeOrientation_of_branch_uniform
plain-language theorem explainer
Branch uniformity of prime-axis identity orientation forces a ratio-orbit character to forbid mixed prime orientations: it cannot be identity on one prime axis and reciprocal on another. Native-cost uniqueness and prime-calibration targets cite this reduction. The argument transports identity via uniformity, composes with the reciprocal hypothesis, and contradicts that a prime direction is never cross-equivalent to its reciprocal.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever $\chi$ is identity-oriented on one native prime axis, it is identity-oriented on every native prime axis. Then $\chi$ cannot be identity-oriented on one prime axis and reciprocal-oriented on another: if $\chi(p)\sim p$ and $\chi(r)\sim r^{-1}$ for prime directions $p,r$, one obtains a contradiction.
background
In the Primitive Recognition Calculus, ratio orbits are numerator/denominator displays built from signed $\delta$-orbits. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits; this is the internal PRC stand-in for rational equality. Reciprocal swaps num/den (with the zero convention of $\mathbb{Q}$).
A character $\chi$ acts on ratio orbits. Prime directions are the native prime axes in this display. Identity orientation means $\chi$ fixes a prime direction up to crossEq; reciprocal orientation means it sends that axis to its reciprocal.
Branch uniformity says identity orientation is all-or-nothing across primes: if any prime axis is identity-oriented, every prime axis is. No mixed prime orientation is the coherence ban on choosing identity on one prime and reciprocal on another. The module develops these as blockers toward uniqueness of the native cost character.
proof idea
Term-mode proof by contradiction on two primes $p,r$. Assume $\chi$ is identity on $p$ and reciprocal on $r$. Branch uniformity applied to that identity hypothesis yields that $\chi$ is also identity on $r$. Symmetry of crossEq plus transitivity then give crossEq between the prime direction of $r$ and its reciprocal. The lemma that a prime direction is never cross-equivalent to its own reciprocal closes the contradiction, discharging the mixed-orientation goal.
why it matters
This is the pure character-level bridge from branch uniformity to the no-mixed-prime-orientation coherence condition. Downstream, PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_branch_uniformity applies it under prime-calibration hypotheses, and the native-cost uniqueness blocker certificate package depends on that chain.
In Recognition Science terms, ruling out independent prime-axis inversions is part of forcing a single coherent orientation for the cost character before J-uniqueness and the native cost can be pinned down. The result does not itself force $\phi$ or the eight-tick structure; it clears a discrete orientation obstruction inside PRC native-cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.