PRCNativeCostAdmissibleCharacterRigidityTarget_of_global_propagation
plain-language theorem explainer
Under the hypothesis that coherent prime orientation propagates to every ratio direction, every admissible ratio character induces a cost matching the canonical native J-cost on all ratio orbits. Strengthened native-cost uniqueness cites this bridge. The proof is a two-step term composition: global propagation yields admissible global orientation, which yields cost rigidity.
Claim. Assume that whenever a multiplicative ratio character has coherent prime orientation, that orientation extends to global cost orientation on every ratio orbit. Then for every admissible ratio character $\chi$ and every ratio orbit $q$, the cost induced by $\chi$ at $q$ is cross-equal to the canonical native cost on $q$.
background
In the Primitive Recognition Calculus, ratio orbits carry a native cost built from the J-functional $J(x)=(x+x^{-1})/2-1$ (the unique cost forced by the Recognition Composition Law). Multiplicative maps $\chi$ on ratio orbits act as characters; an admissible character is one compatible with the native factorization and calibration interface.
The target here is cost rigidity rather than pointwise character orientation: for admissible $\chi$, costFromCharacter must agree with the canonical orbit cost under the cross-equality relation on ratio orbits. An earlier absolute-value countermodel forced a repair: coherent prime orientation alone is not enough for pointwise identity-or-reciprocal orientation; one works with an admissible global-orientation interface and then collapses costs.
The hypothesis packages the sharper orientation blocker B: once prime orientation is coherent, the multiplicative character law and native rational factorization propagate that orientation to every ratio direction. Upstream, that hypothesis already implies the admissible global-orientation target.
proof idea
Pure term composition, no tactics. First apply the upstream lemma that turns the coherent-prime-to-global propagation hypothesis into the admissible-character global-orientation target (itself built from proved prime-coherence plus the same propagation hypothesis). Feed that orientation witness into the existing reduction theorem: admissible global orientation implies native-cost admissible character rigidity, by case-splitting each orbit into identity-oriented versus reciprocal-oriented and using orbit congruence of the canonical cost in either case.
why it matters
This is a wiring lemma in the native-cost uniqueness stack. It converts the global-propagation orientation blocker into the admissible character-rigidity target that the strengthened uniqueness theorem consumes alongside character factorization and two-point calibration.
Downstream, PRCStrengthenedNativeCostUniquenessTarget_of_character_factorization_two_calibration_and_coherent_global_propagation applies exactly this bridge, then routes through the factorization-plus-two-calibration-plus-admissible-rigidity assembly. In framework terms it supports T5-style J-uniqueness at the PRC layer: admissible characters cannot produce a competing cost; they collapse to canonical J on every ratio orbit once orientation propagates globally.
It does not itself prove propagation or factorization; it closes the orientation-to-rigidity edge so the uniqueness target can be stated under the coherent-global-propagation hypothesis package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.