PRCCharacterPrimeOrientationCoherent_of_admissible
plain-language theorem explainer
Any admissible ratio character on rational orbits has globally coherent prime-axis orientation: it is either the identity on every native prime direction, or the reciprocal on every one. Native-cost uniqueness arguments cite this to rule out mixed prime orientations after the two-adic repair. The proof chains local orientation from prime calibration, the identity-iff-two normal form, and two-prime branch control into the coherence lemma.
Claim. Let $\chi$ map rational orbits to rational orbits. If $\chi$ is admissible (ratio-character laws, prime-direction calibration, and prime-pair product cost consistency), then prime-axis orientation is coherent: either $\chi$ fixes every native prime direction, or $\chi$ sends every native prime direction to its reciprocal.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed integer numerator over a nonzero distinction-nat denominator. Characters act on these orbits. After the two-adic countermodel, admissibility was repaired: a character must obey the ratio-character laws, be prime-direction calibrated, and keep prime-pair product costs consistent. That package preserves the two global orientations and excludes valuation twists.
Prime-axis orientation coherence means the character does not mix choices across native primes. Formally it is a disjunction: identity on every prime direction, or reciprocal on every prime direction. A companion normal form says identity on a prime axis is equivalent to identity on the distinguished orbit-$2$ prime axis, so the two-prime branch can control all primes once local orientation is known.
This module develops native-cost uniqueness from such character constraints, feeding the J-cost uniqueness line in the forcing chain (T5).
proof idea
Term-mode assembly of four facts. First, prime calibration on the admissible character yields local prime orientation (PRCPrimeCalibrationForcesLocalPrimeOrientationTarget_proved). Second, admissibility implies the identity-iff-two normal form (PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_admissible). Third, local orientation plus that iff gives two-prime branch control of all primes (PRCCharacterTwoPrimeBranchControlsPrimes_of_local_prime_identity_iff_two). Fourth, local orientation with branch control yields global coherence (PRCCharacterPrimeOrientationCoherent_of_local_two_prime_branch_controls). No new case analysis at this layer.
why it matters
This is the admissible-to-coherence bridge used immediately by PRCAdmissibleCharacterPrimeOrientationCoherentTarget_proved, which packages the target as a proved interface fact: every admissible character is prime-orientation coherent. That closes a gap in the native-cost uniqueness program: mixed prime orientations are incompatible with the repaired admissibility interface.
In the broader Recognition framework, coherent orientation keeps characters inside the two global branches that feed unique native cost and thus the J-cost uniqueness step (T5: $J(x)=(x+x^{-1})/2-1$). Without coherence, valuation-style twists could survive and spoil uniqueness of the recognition cost before the Recognition Composition Law and the phi fixed point are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.