PRCAdmissibleCharacterPrimeOrientationCoherentTarget
plain-language theorem explainer
Under the repaired admissibility package, every ratio character on rational orbits must pick one global prime-axis orientation: either identity on all native primes or reciprocal on all of them. Native-cost uniqueness and rigidity arguments cite this Prop as the prime-coherence subtarget. The body is a pure universal implication packaging admissibility into orientation coherence.
Claim. For every map $\chi$ from rational orbits to rational orbits, if $\chi$ is an admissible ratio character (ratio-character laws, prime-direction calibration, and prime-pair product-cost consistency), then $\chi$ is prime-orientation 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 orbit denominator. Characters act as maps $\chi$ on these orbits and are meant to encode multiplicative orientation data that later feeds the native cost (the J-cost side of the uniqueness program).
Admissibility is the repaired interface after the two-adic countermodel: a character must obey the ratio-character laws, be prime-direction calibrated, and keep prime-pair product costs consistent. That package still allows two global orientations but rules out valuation twists.
Prime-orientation coherence is the discrete choice that every native prime axis is treated the same way: either $\chi$ acts as the identity on every prime direction, or as the reciprocal on every prime direction. This definition packages the claim that admissibility forces that coherent choice.
proof idea
Definitional packaging only: the Prop is the universal statement that every admissible ratio character is prime-orientation coherent. No tactics or lemmas are invoked in the body; discharge happens downstream via the proved instance that applies the admissibility-to-coherence lemma to any admissible $\chi$.
why it matters
This is the prime-coherence subtarget in the native-cost uniqueness ladder. Downstream, the proved instance feeds global-orientation propagation: admissibility plus this target plus propagation yields the global-orientation target, which in turn yields admissible-character rigidity. The strengthened uniqueness assembly takes the same hypothesis alongside character factorization and two-calibration. It also appears in the uniqueness blocker certificate and the universal-foundation open-target ledger, marking a repaired positive interface rather than a refuted route. In framework terms it tightens the discrete orientation data that must sit under any unique native cost before the J-uniqueness (T5) and RCL surface is forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.