PRCCharacterGlobalCostOrientation
plain-language theorem explainer
A ratio character has global cost orientation when every rational orbit is mapped either to itself or to its reciprocal (up to cross-multiplication equality). Cost theorists cite it as the exact orientation data needed for J-cost propagation, since J is reciprocal-symmetric. The body is a pure Prop definition: a pointwise disjunction over all ratio orbits.
Claim. A map $\chi$ on rational orbits has global cost orientation if for every rational orbit $q$, either $\chi(q)$ is cross-multiplication equivalent to $q$, or $\chi(q)$ is cross-multiplication equivalent to the reciprocal of $q$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two such orbits are related by cross-multiplication equality when the scaled numerators balance as signed orbits; that is the internal PRC stand-in for rational equality. The total reciprocal on ratio orbits sends zero to zero and otherwise inverts, matching the dual-recognition involution $\iota(x)=x^{-1}$ on the positive reals.
A ratio character is a map $\chi$ on these orbits. Because the native J-cost is reciprocal-symmetric ($J(x)=J(x^{-1})$), cost values cannot distinguish a direction from its reciprocal. The only residual freedom that matters for cost propagation is therefore a global choice, at each rational direction, of whether $\chi$ keeps the direction or flips it to its reciprocal.
This module packages native-cost uniqueness for PRC characters. Global cost orientation is the Prop that freezes that residual freedom pointwise.
proof idea
Definition only: no proof obligations. The body is the universal quantification over ratio orbits of the disjunction "crossEq to self or crossEq to reciprocal". Downstream theorems discharge instances by intro q and either Or.inl with reflexivity of crossEq (identity character) or by propagation lemmas from prime calibration and signed admissibility.
why it matters
This Prop is the common target of the native-cost uniqueness orientation program. Downstream, the identity character is shown to satisfy it immediately; signed admissible characters inherit it via coherent prime-orientation propagation. It appears as the conclusion of two sharper blocker targets: prime calibration must force global orientation (otherwise independent prime inversions can keep prime costs while breaking composite costs), and coherent prime orientation must propagate multiplicatively to every ratio direction.
Those targets feed the Pass-25 uniqueness blocker certificate, which splits the remaining gap in native cost uniqueness into exact Lean interfaces. In framework terms this is orientation control for the reciprocal-symmetric J-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), not a new forcing step: it ensures characters cannot scramble composite costs while preserving prime data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.