PRCAdmissibleCharacterPrimeOrientationCoherentTarget_proved
plain-language theorem explainer
Every admissible ratio-orbit character has coherent prime orientation: on each prime axis the repaired prime-pair field picks a single branch. Native-cost uniqueness and global-orientation arguments cite this as the discharged prime-coherence subtarget. The proof is a one-line intro that applies the already-proved admissibility-implies-prime-coherence lemma.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is an admissible ratio character, then $\chi$ is prime-orientation coherent (the repaired prime-pair field forces every prime axis onto one coherent branch).
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode how multiplicative structure is read. Admissibility packages the structural hypotheses under which such a character is a legitimate candidate for the native cost (calibration, factorization, and related constraints from the PRC kernel and J-cost layer).
Prime orientation concerns the choice of branch on each prime axis once the prime-pair field has been repaired. Coherence means those local choices agree: every prime axis selects one branch rather than mixing signs or orientations. The target proposition simply asserts that admissibility already forces this coherence for every such $\chi$.
The module sits in the native-cost uniqueness development: uniqueness of the cost functional (tied to the J-cost $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law) requires that admissible characters cannot flip orientation independently on different primes.
proof idea
One-line wrapper. Introduce an arbitrary ratio-orbit map $\chi$ and an admissibility hypothesis, then apply PRCCharacterPrimeOrientationCoherent_of_admissible, which already proves that every admissible ratio character is prime-orientation coherent (via the local prime-calibration forcing lemma). No extra algebraic work occurs at this site; the target Prop is discharged by specializing that lemma.
why it matters
Discharges the prime-orientation subtarget under admissibility, a named blocker piece in the native-cost uniqueness certificate path. Downstream, global-orientation theorems apply it directly: PRCAdmissibleCharacterGlobalOrientationTarget_of_global_propagation feeds this proved target plus a propagation hypothesis to obtain global cost orientation for admissible characters; the signed variant and PRCSignedAdmissibleRatioCharacter_global_orientation sit on the same spine.
It also appears in the native-cost uniqueness blocker certificate and, one module up, in the conditional universal-foundation certificate. In the forcing chain this is bookkeeping for T5-style J-uniqueness: without coherent prime orientation, admissible characters could still disagree on branch choice and spoil uniqueness of the native cost. The open remainder is propagation from prime coherence to full global orientation, not the prime step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.