PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget
plain-language theorem explainer
Packages the repaired orientation target: any ratio-orbit character that is a genuine ratio character, fixes the signed unit −1, and orients all prime axes coherently (all identity or all reciprocal) must send every rational orbit to itself or its reciprocal. Cited by the native-cost uniqueness blocker ledger and the admissible global-orientation bridge. Pure Prop interface; the discharging proof lives in the sibling _proved theorem.
Claim. For every map $\chi$ on rational orbits, if $\chi$ is a ratio character, $\chi(-1)=-1$ up to cross-equality, and $\chi$ orients every native prime direction either all as identity or all as reciprocal, then for every rational orbit $q$ one has $\chi(q)\sim q$ or $\chi(q)\sim q^{-1}$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a signed integer numerator over a nonzero native orbit denominator (K4.7). Characters act on these orbits. Global cost orientation means every rational direction is sent either to itself or to its reciprocal; because the J-cost $J(x)=(x+x^{-1})/2-1$ is reciprocal-symmetric, that is exactly the orientation data needed to push cost values along the character.
Prime-axis coherence is weaker: the character picks one global choice on all native primes (all identity, or all reciprocal). After an absolute-value countermodel, prime coherence alone does not force the signed unit. Signed-unit calibration requires $\chi(-1)\sim -1$ separately; prime-direction data cannot supply it.
This module sits in the native-cost uniqueness development: the goal is to force any admissible character-derived cost to match the unique J-cost forced by the Recognition Composition Law (T5).
proof idea
Definitional Prop, not a proved theorem. The body is the single quantified implication
ratio-character + signed-unit calibration + prime-orientation coherence ⇒ global cost orientation.
No tactics or lemmas are applied here. The discharging argument is the sibling theorem PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved, which introduces a character, obtains cross-equality respect from normalize-ratio canonicity, and checks the identity-or-reciprocal alternative at each rational orbit.
why it matters
Exact repaired orientation target after the absolute-value countermodel (doc-comment). Coherent prime orientation must be supplemented by signed-unit calibration before one may demand global pointwise identity-or-reciprocal orientation.
Downstream, PRCAdmissibleCharacterGlobalOrientationTarget_of_signed_global_propagation turns this Prop plus a signed-unit admissibility target into the admissible global-orientation target. It appears in PRCNativeCostUniquenessBlockerCertificate (Pass-25 split of missing mathematics into exact Lean targets) and in the historical ledger PRCUniversalFoundationOpenTargets.
Framework role: orientation control is the bridge from character data to J-cost uniqueness (T5). Without global orientation, cost propagation along the character cannot be forced to the unique reciprocal-symmetric cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.