PRCPrimeCalibrationPropagationTarget_of_global_orientation
plain-language theorem explainer
If prime-direction calibration forces a single coherent global orientation on a ratio character, then character cost matches the native cost on every rational orbit. Cost-uniqueness and rigidity arguments cite this implication. The proof case-splits on identity versus reciprocal orientation and closes each arm with congruence and reciprocal symmetry of the native cost.
Claim. Assume that every ratio character $\chi$ that is calibrated on all prime directions is globally cost-oriented (identity on every orbit, or reciprocal on every orbit). Then for every such $\chi$ and every rational orbit $q$, the character cost of $q$ is cross-equal to the native PRC cost of $q$.
background
In the Primitive Recognition Calculus, rational directions are displayed as RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator. Two orbits are identified up to cost when they satisfy crossEq, a choice-free balanced equality of signed displays.
A ratio character $\chi$ assigns an orbit to each orbit. Prime-direction calibration means $\chi$ agrees with the native cost (or its reciprocal) on every prime axis. The native cost onRatioOrbit is reciprocally symmetric: the cost of $q$ is cross-equal to the cost of its reciprocal. Congruence onRatioOrbit_congr pushes crossEq through the native cost.
The hypothesis is the sharper blocker that prime calibration forces a coherent global orientation: once primes are calibrated, $\chi$ cannot mix identity and reciprocal choices across directions. The conclusion is target B of the rigidity problem: prime calibration propagates, so character cost equals native cost on every rational orbit (the unique-factorization side).
proof idea
Term-mode introduction of $\chi$, the character and prime-calibration hypotheses, and an arbitrary orbit $q$. Apply the global-orientation hypothesis to obtain a disjunction: either $\chi(q)$ is cross-equal to $q$, or $\chi(q)$ is cross-equal to the reciprocal of $q$.
Identity arm: onRatioOrbit_congr turns that equality into cross-equality of native costs, which is the required match of character cost to native cost.
Reciprocal arm: apply onRatioOrbit_congr to the inverse equality, then transitively compose (crossEq_trans) with the symmetric form of reciprocal_symmetric on $q$ (crossEq_symm), recovering native cost of $q$.
why it matters
This is a Pass-27 refinement link inside native cost uniqueness: it reduces the unique-factorization propagation target to the sharper global-orientation blocker. Downstream, PRCPrimeCalibrationForcesGlobalOrientationTarget_refuted uses the implication contrapositively (propagation is already refuted, so global orientation cannot hold). The sharpened-orientation route also factors through this lemma.
In the Recognition forcing picture this sits under J-uniqueness and the Recognition Composition Law: cost rigidity on the rational orbit lattice is the discrete skeleton that later pins $J(x)=(x+x^{-1})/2-1$ and the self-similar scale $\phi$. The blocker certificate for native cost uniqueness records related factorization targets; this arrow clarifies which orientation hypothesis would have been enough for prime-to-composite propagation, and why a mixed-inversion counterexample defeats it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.