PRCCharacterPrimeIdentityBranchUniform_iff_no_distinct_prime_pair_of_local
plain-language theorem explainer
Under local prime orientation of a ratio-orbit character, identity-branch uniformity is equivalent to the absence of a mixed pair of distinct primes (one identity-oriented, one reciprocal-oriented). Native-cost uniqueness and universal-foundation arguments cite this bridge. The proof is a two-constructor Iff packaging the two already-proved one-sided lemmas.
Claim. Let $\chi$ act on rational orbits. Assume every prime direction is sent either to itself or to its reciprocal (local prime orientation). Then the following are equivalent: (i) if any prime direction is identity-oriented under $\chi$, every prime direction is; (ii) there are no distinct primes $p\neq r$ with $\chi$ identity-oriented on $p$ and reciprocal-oriented on $r$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed numerator over a nonzero distinction-nat denominator. Characters act on these orbits. Prime directions are the native prime axes of the distinction lattice.
Local prime orientation means each prime axis is sent either to itself or to its reciprocal; that is the algebraic content of matching J-cost on a single prime direction. A distinct-prime mixed-pair witness is a pair of different primes where one axis is identity-oriented and the other is reciprocal-oriented. Branch uniformity says identity orientation, once present on any prime axis, forces identity on every prime axis.
The module develops native-cost uniqueness for PRC characters. The two one-sided lemmas already show that branch uniformity kills mixed pairs, and that local orientation plus no mixed pair recovers branch uniformity. This declaration packages the equivalence.
proof idea
Term-mode proof of an Iff by pairing the two existing one-sided results. The forward direction is PRCCharacterDistinctPrimeMixedPairWitnesses_absurd_of_branch_uniform: branch uniformity immediately rules out any mixed pair. The reverse direction is PRCCharacterPrimeIdentityBranchUniform_of_local_no_distinct_prime_pair, which needs the local-orientation hypothesis: given no mixed pair, an identity orientation on one prime forces identity on every other prime (the only remaining local option would be reciprocal, which would build a mixed pair). No further case analysis is done here.
why it matters
This is the clean logical bridge between the trace-free branch-uniformity blocker and the mixed-pair witness language used elsewhere in native-cost uniqueness. Downstream it is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles the conditional PRC universal-foundation certificate (kernel, real complete ordered field, trace logic).
In the broader Recognition Science chain this sits inside the uniqueness apparatus for the native cost, feeding the J-uniqueness story (forcing-chain T5: $J(x)=(x+x^{-1})/2-1$). Ruling out independent prime-axis inversions is exactly the coherence needed so that a character cannot flip some primes and not others while still matching costs. The declaration itself is fully proved; it closes the equivalence gap rather than leaving a scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.