absValueCharacter_prime_orientation_coherent
plain-language theorem explainer
The absolute-value character on ratio orbits is prime-orientation coherent: on every native prime direction it acts as the identity, not the reciprocal. Anyone tracking orientation hypotheses for PRC native-cost uniqueness cites this. The proof is a one-line left injection of the already-proved prime-identity lemma into the coherence disjunction.
Claim. The absolute-value character $\chi_{|\cdot|}$ on ratio orbits is prime-axis orientation coherent: for every native prime direction $p$, one has $\chi_{|\cdot|}(p)\simeq p$ (cross-equality), so the global choice is the identity branch rather than the reciprocal branch.
background
In the primitive recognition calculus, ratio orbits are the quotient displays of verifier rationals. A character $\chi$ is a map RatioOrbit $\to$ RatioOrbit used to build native costs. Prime directions are the orbits of native primes in DistinctionNat; each carries a preferred axis and a reciprocal.
Prime-axis orientation coherence means $\chi$ picks one consistent polarity on every such axis: either $\chi(p)\simeq p$ for all primes $p$, or $\chi(p)\simeq p^{-1}$ for all primes. The absolute-value character sends each orbit $q$ to the orbit of $|q.{\rm toRat}|$. It respects the ratio-character laws but collapses the sign of $-1$.
Upstream, the identity lemma already shows $\chi_{|\cdot|}(p)\simeq p$ on every prime direction by reducing cross-equality to equality of rational displays and using nonnegativity of absolute value.
proof idea
One-line wrapper. Coherence is a disjunction (all-identity or all-reciprocal). Apply Or.inl to the existing theorem that the absolute-value character fixes every prime direction under cross-equality, discharging the left disjunct. No further case analysis.
why it matters
This fact is the positive half of a sharpness counterexample in native-cost uniqueness. Downstream, PRCCoherentPrimeOrientationPropagatesToGlobalTarget_refuted feeds it (with the ratio-character and negative-one lemmas) to show that coherent prime orientation does not force a global orientation target: the absolute-value character fixes every positive prime axis yet sends $-1$ to $+1$, so signed-unit calibration is indispensable.
In the Recognition forcing picture this sits under cost uniqueness for the J-cost (T5: $J(x)=(x+x^{-1})/2-1$), separating prime-axis polarity from full signed orientation before the composition law and ladder constructions are locked in. It closes a local scaffolding gap: coherence of this concrete character is now a proved lemma, not a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.