PRCNativeCostAdmissibleCharacterRigidityTarget_of_admissible_global_orientation
plain-language theorem explainer
Global identity-or-reciprocal orientation of every admissible ratio character forces the character-derived cost to match the canonical PRC cost on every ratio orbit. Anyone assembling native-cost uniqueness from orientation hypotheses cites this reduction. The argument is a two-branch case split: identity orientation gives congruence directly; reciprocal orientation routes through reciprocal symmetry of the cost and crossEq transitivity.
Claim. If every admissible ratio character $\chi$ is globally cost-oriented (pointwise either identity-oriented or reciprocal-oriented), then for every such $\chi$ and every ratio orbit $q$, the character-derived cost at $q$ is cross-equivalent to the canonical PRC cost on $q$.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: an integer-signed numerator over a nonzero distinction-natural denominator. Equality of costs is expressed by crossEq, a choice-free balanced relation on these orbits (symmetric and transitive via the integer bridge).
The canonical cost on ratio orbits is the PRC rational cost (onRatioOrbit), which is reciprocal-symmetric: its value on $q$ matches its value on the reciprocal orbit. Characters $\chi$ map ratio orbits to ratio orbits; under admissibility one builds a cost from the character. The rigidity target asks that this character cost collapse, via crossEq, to the canonical cost everywhere.
The orientation target is the weaker global statement that each admissible $\chi$ is, at every orbit, either identity-oriented or reciprocal-oriented. This lemma is the bridge from that orientation package to full cost rigidity.
proof idea
Term-mode proof by introducing an admissible character $\chi$ and an orbit $q$, then casing on the orientation hypothesis at $(\chi,q)$.
Identity branch: $\chi(q)$ is cross-equivalent to $q$, so onRatioOrbit_congr pushes the relation through the canonical cost and yields the rigidity goal.
Reciprocal branch: $\chi(q)$ is cross-equivalent to $\mathrm{recip}(q)$. Apply onRatioOrbit_congr to get cost equivalence with the reciprocal orbit, then chain with crossEq_trans against the symmetric form of reciprocal_symmetric (canonical cost of $q$ equals canonical cost of $\mathrm{recip}(q)$). The composite is the required cross-equivalence.
why it matters
This is the standard discharge step from global orientation to admissible character-cost rigidity inside the native-cost uniqueness stack. Downstream wrappers apply it after building orientation from signed-unit calibration, from coherent prime orientation plus global propagation, or from global propagation alone; the strengthened uniqueness target also routes through it once factorization and two-calibration are in hand.
In the Recognition forcing chain this supports T5-style J-uniqueness: admissible multiplicative characters cannot produce a cost other than the canonical $J$ (equivalently $\cosh(\log x)-1$) once orientation is controlled. Reciprocal symmetry of $J$ is exactly what lets the reciprocal branch close, so the lemma encodes that the cost, not the character label, is the rigid object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.