identity_character_prime_orientation_coherent
plain-language theorem explainer
The identity map on rational orbits is prime-orientation coherent: on every native prime direction it keeps the identity orientation rather than flipping to the reciprocal. Anyone assembling native cost uniqueness or character factorization cites this as the canonical coherent witness. The proof is a one-line left disjunct via reflexivity of cross-equality on prime directions.
Claim. The identity character $\chi(q)=q$ on ratio orbits is prime-orientation coherent: for every native prime orbit direction $d_p$, one has $\mathrm{crossEq}(\chi(d_p), d_p)$. Equivalently, $\chi$ lies in the left branch of the coherence dichotomy (all primes identity-oriented, not all reciprocal-oriented).
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-denominator display of a positive rational class. Characters act as maps $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$. Prime directions are the distinguished ratio-orbit axes attached to native primes (DistinctionNat primes).
Prime-orientation coherence asks that a character not mix orientations across those axes: either $\chi(d_p)$ matches $d_p$ for every prime direction $d_p$, or it matches the reciprocal $\mathrm{recip}(d_p)$ for every such $d_p$. Cross-equality is the orbit-level identification used to state that match; it is reflexive.
This sits inside native cost uniqueness work: cost characters must be orientation-coherent before one can force the J-cost (or its doubled-trace avatar) as the unique native cost functional. Reciprocal and identity events from ledger/observer forcing supply the two global orientations being compared.
proof idea
Term proof selecting the left disjunct of coherence. After Or.inl, introduce an arbitrary prime $p$ with primality witness and apply RatioOrbit.crossEq_refl to primeDirection p hp. Because the character is the identity map, $\chi(d_p)=d_p$, so reflexivity closes the goal. No multiplicative or reciprocal automorphism lemmas are needed here.
why it matters
Feeds prc_native_cost_uniqueness_blocker_certificate, which packages zero-calibrated native-cost character factorization targets for the uniqueness program. Without an explicit coherent identity witness, the dichotomy between identity and reciprocal orientations would be empty on the identity side.
In the broader Recognition chain this is bookkeeping under T5 J-uniqueness: characters that preserve the multiplicative structure of positive ratios must still pick a global orientation; the identity map is the default choice before reciprocal is exhibited as a second coherent character. It does not yet force $J(x)=(x+x^{-1})/2-1$, but it clears a coherence gate those uniqueness certificates depend on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.