identity_character_global_orientation
plain-language theorem explainer
The identity map on rational ratio-orbits has global cost orientation: every orbit is sent to itself (hence also to a reciprocal-symmetric partner). Anyone proving native cost uniqueness or character factorization cites this as the trivial coherent orientation. The proof is a one-line left-disjunct via reflexivity of cross-equality.
Claim. The identity character $\chi(q)=q$ on ratio-orbits satisfies global cost orientation: for every ratio-orbit $q$, either $\chi(q)$ is cross-equal to $q$, or $\chi(q)$ is cross-equal to the reciprocal of $q$.
background
In the primitive recognition calculus, a ratio-orbit is a rational display: a signed integer numerator over a nonzero distinction-natural denominator. Characters act on these orbits. Global cost orientation for a character $\chi$ means that every rational direction $q$ is sent either to itself or to its reciprocal (up to the cross-equality relation on orbits).
J-cost is reciprocal-symmetric, so this binary choice is exactly the orientation data needed to propagate costs from primes to composites without independent prime inversions breaking composite values. The identity character is the baseline coherent choice: no orbit is inverted.
Upstream, cross-equality is reflexive on ratio-orbits (crossEq_refl), which is the only algebraic fact required here.
proof idea
Unfold the orientation predicate and introduce an arbitrary ratio-orbit $q$. The identity sends $q$ to $q$, so the left disjunct of the orientation alternative applies. Discharge it by reflexivity of cross-equality on ratio-orbits. No reciprocal case is needed.
why it matters
Native cost uniqueness in the PRC stack requires that prime calibration force a coherent global orientation; without it, independent prime inversions can preserve prime costs while breaking composite costs. The identity character is the canonical coherent orientation and is recorded here as a proved instance.
Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, which packages zero-calibrated factorization targets and refutations used to close the native-cost uniqueness blocker. In the broader Recognition forcing chain this sits under T5 J-uniqueness and the Recognition Composition Law: orientation coherence is the discrete bookkeeping that lets the unique J-cost propagate consistently on the rational skeleton before continuum extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.