PRCCharacterDistinctPrimeMixedPairWitnesses_absurd_of_branch_uniform
plain-language theorem explainer
Branch uniformity of a ratio-orbit character forbids mixed identity/reciprocal orientations on two distinct native prime axes. Anyone closing the prime-calibration uniqueness path cites this obstruction lemma. The proof is a short term argument: transport identity orientation from one prime to the other, then contradict that a prime direction is never cross-equivalent to its reciprocal.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever one native prime axis is identity-oriented under $\chi$, every native prime axis is identity-oriented. Then there cannot exist two distinct native primes $p$ and $r$ such that $\chi$ fixes the prime direction of $p$ and sends the prime direction of $r$ to its reciprocal (up to cross-multiplication equivalence of ratio orbits).
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by cross-multiplication equivalence (crossEq): the internal PRC stand-in for rational equality, defined by balancing scaled signed orbits. Reciprocals are total on this type, sending the zero class to itself.
A character $\chi$ orients each prime axis either toward the identity direction or toward the reciprocal. Branch uniformity says identity orientation is all-or-nothing across native primes: if any prime direction is fixed by $\chi$ under crossEq, every prime direction is. A distinct-prime mixed-pair witness is the opposite obstruction: one prime fixed, a different prime sent to its reciprocal.
The local module develops native-cost uniqueness for PRC characters. This lemma is the pure orientation half of that story: it separates branch uniformity from trace construction and shows the mixed-pair witness cannot coexist with uniformity.
proof idea
Assume a mixed-pair witness and unpack it: primes $p\neq r$, with $\chi$ identity on the $p$-direction and reciprocal on the $r$-direction. Branch uniformity applied to the $p$-identity hypothesis forces the $r$-direction also to be identity-oriented. Symmetry then reverse-transitivity of crossEq glue the identity and reciprocal orientations of $r$ into a single relation: the prime direction of $r$ is crossEq to its own reciprocal. The dedicated lemma that no prime direction is cross-equivalent to its reciprocal yields the contradiction. The argument is pure equational transport on orientations; no cost or trace hypotheses enter.
why it matters
This is the left-to-right half of the local equivalence between prime-identity branch uniformity and absence of distinct-prime mixed-pair witnesses (under a local orientation hypothesis). Downstream, prime-calibration targets reuse it: if calibration forces branch uniformity, then no calibrated character can carry a distinct-prime mixed-pair witness. That feeds the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, ordered-field, and trace-logic passes for the PRC stack.
In the broader Recognition Science forcing chain, native-cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (T5) to a single admissible cost on ratio orbits. Clearing mixed prime orientations is a discrete obstruction step on that path: without it, reciprocal and identity branches could coexist on different primes and spoil uniqueness of the native cost character. The lemma itself is fully proved; remaining scaffolding sits in the larger calibration and certificate assembly, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.