PRCAdmissibleCharacterGlobalOrientationTarget_of_prime_coherence_and_global_propagation
plain-language theorem explainer
If every admissible ratio character has coherent prime-axis orientation, and coherent prime orientation propagates to every ratio direction, then every admissible character is globally identity- or reciprocal-oriented. Cited by the native-cost admissible-character rigidity chain and by the one-hypothesis global-propagation corollary. Proof is a three-line composition: admissibility supplies the ratio-character law, prime coherence is applied, then the propagation hypothesis closes global orientation.
Claim. Assume (i) every admissible ratio character has coherent prime-axis orientation, and (ii) whenever a multiplicative ratio character has coherent prime orientation, that orientation propagates to global cost orientation on every ratio orbit. Then every admissible ratio character is globally identity-oriented or reciprocal-oriented pointwise.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio characters are maps $\chi$ on ratio orbits obeying a multiplicative character law. Admissibility strengthens this with the native cost interface (trace-matching and related hypotheses). Global cost orientation means that, pointwise, $\chi$ acts as the identity branch or the reciprocal branch on every ratio direction.
Two intermediate targets split the orientation problem after an absolute-value countermodel forced a repair. The prime-orientation subtarget asks that the repaired prime-pair field force all prime axes onto one coherent branch. The sharper propagation target (blocker B) then asks that the multiplicative law plus native rational factorization push that coherent prime choice out to every ratio direction.
The conclusion target is exactly admissible-character rigidity reduced to orientation: under the repaired interface, every admissible character should be globally identity- or reciprocal-oriented pointwise.
proof idea
Term-mode composition, three lines. Fix an admissible character $\chi$. From admissibility extract the underlying ratio-character law (hadm.ratio_character). Apply the prime-coherence hypothesis at $\chi$ to obtain coherent prime orientation. Feed $\chi$, the ratio-character fact, and that coherence witness into the propagation hypothesis; its conclusion is global cost orientation of $\chi$. No further algebraic work.
why it matters
Closes the two-hypothesis bridge from prime coherence plus propagation to the admissible global-orientation target that the native-cost rigidity story needs. Downstream, PRCAdmissibleCharacterGlobalOrientationTarget_of_global_propagation specializes it by plugging in the already-proved prime-coherence theorem, leaving only propagation as a remaining hypothesis. The same composition feeds PRCNativeCostAdmissibleCharacterRigidityTarget_of_admissible_prime_coherence_and_global_propagation, which routes through global orientation into full admissible-character rigidity for the native cost.
In the Recognition forcing chain this sits under T5 J-uniqueness: native cost is the J-cost $J(x)=(x+x^{-1})/2-1$, and character rigidity is the algebraic spine that forces admissible cost functionals onto that unique shape (via the Recognition Composition Law). The declaration itself is pure interface glue; the analytic content lives in the two named targets it composes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.