PRCNativeCostAdmissibleCharacterRigidityTarget_of_admissible_prime_coherence_and_global_propagation
plain-language theorem explainer
Under prime-orientation coherence for admissible characters and propagation of that coherence to every ratio direction, the induced cost equals canonical J-cost on all ratio orbits. Native-cost uniqueness proofs cite this to discharge the admissible rigidity target from the two orientation blockers. The argument is a two-step term composition: prime coherence plus propagation yields global orientation, which already implies cost rigidity.
Claim. Assume every admissible ratio character has coherent prime-axis orientation, and that coherent prime orientation propagates (via the multiplicative character law and rational factorization) to a global identity-or-reciprocal cost orientation. Then for every admissible ratio character $\chi$ and every ratio orbit $q$, the cost built from $\chi$ at $q$ is cross-equal to the canonical $J$-cost on $q$.
background
In the Primitive Recognition Calculus, ratio orbits carry a native cost that should collapse to the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law (forcing step T5). Characters $\chi$ on ratio orbits induce a cost via costFromCharacter; admissibility packages the structural hypotheses under which that cost is a legitimate competitor.
The rigidity target asks not that $\chi$ itself be the identity or reciprocal map, but that the induced cost match canonical $J$ pointwise up to the orbit cross-equality. After an absolute-value countermodel, orientation is repaired: first force all prime axes to one branch (prime-orientation coherence), then propagate that choice to every ratio direction (global cost orientation).
Upstream, prime coherence plus the propagation blocker already yield the admissible global-orientation target. Separately, global orientation implies cost rigidity by case-splitting identity versus reciprocal orientation and applying orbit congruence of the canonical cost.
proof idea
Pure term-mode composition of two prior theorems. First apply the lemma that turns the pair of hypotheses (admissible prime-orientation coherence, and coherent-prime-to-global propagation) into the admissible global-orientation target. Feed that orientation witness into the existing reduction from admissible global orientation to admissible character cost-rigidity. No new case analysis appears here; both steps are already proved.
why it matters
This declaration sits on the native-cost uniqueness spine of the foundation layer. It packages the two orientation blockers into the admissible rigidity target that the strengthened uniqueness theorem consumes: the downstream result PRCStrengthenedNativeCostUniquenessTarget_of_character_factorization_two_calibration_admissible_prime_coherence_and_global_propagation takes character factorization, two-point calibration, and exactly these two hypotheses, and concludes strengthened native-cost uniqueness.
In framework terms it advances the T5 $J$-uniqueness story inside PRC: once orientation is coherent on primes and propagates globally, every admissible character-induced cost is forced to canonical $J$ on ratio orbits. It does not itself close uniqueness; it is the rigidity leg that uniqueness assembles with factorization and calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.