absValueCharacter_negative_one_no_global_orientation
plain-language theorem explainer
The absolute-value ratio character sends the signed unit −1 to +1, so under PRC cross-multiplication it matches neither −1 nor its reciprocal. Orientation-coherence arguments for native cost uniqueness cite this as the exact obstruction at the signed unit. The proof case-splits the disjunction, rewrites to rational displays, and finishes by arithmetic.
Claim. Let $c_{|\cdot|}$ be the absolute-value ratio character and let $r_{-1}$ be the ratio orbit of $-1$. Then it is false that $c_{|\cdot|}(r_{-1})$ is cross-equivalent to $r_{-1}$ or to the reciprocal orbit $r_{-1}^{-1}$. Equivalently, neither $c_{|\cdot|}(r_{-1})\sim r_{-1}$ nor $c_{|\cdot|}(r_{-1})\sim r_{-1}^{-1}$ holds under the internal PRC cross-multiplication relation on ratio orbits.
background
In the Primitive Recognition Calculus, a ratio orbit packages signed numerator and denominator $\delta$-orbits. Cross-equivalence is the internal rational relation: two orbits match when cross-multiplication balances as signed orbits. Upstream, that relation is proved equivalent to equality of the rational verifier displays, so orientation questions reduce to comparing toRat values.
The absolute-value character is a ratio character that collapses sign. On positive prime axes it is coherent, but on the signed unit it sends $-1$ to $+1$. The reciprocal of a ratio orbit inverts the rational display; for $-1$ the reciprocal is again $-1$.
The local setting is native cost uniqueness inside the foundation layer. One asks whether prime-axis orientation coherence of a character automatically yields a global orientation target on every ratio, including signed units. This lemma isolates the failure mode at $-1$.
proof idea
Assume either cross-equivalence holds and case-split. In the same-orbit branch, rewrite by the bridge that cross-equivalence iff rational displays agree, together with the display lemmas for the absolute-value character and for the $-1$ orbit; the resulting equality is $1=-1$, discharged by norm_num. In the reciprocal branch, the same bridge plus the reciprocal display lemma again yields $1=-1$ after reducing both sides. No analytic or measure machinery is used; the argument is pure rational arithmetic on displays.
why it matters
This is the exact obstruction fed to the refutation that coherent prime orientation does not propagate to a global target. The parent result states that the coherent-prime-to-global target is false without signed-unit calibration: the absolute-value character fixes every positive prime axis, yet sends $-1$ to $+1$, so the global orientation conclusion fails exactly at the signed unit.
In the Recognition foundation this sits inside native cost uniqueness for the J-cost lineage (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$). It shows that character-level sign data cannot be recovered from absolute values alone; a separate signed-unit calibration is required before orientation can be promoted from primes to the full ratio group. The lemma therefore closes a natural false path rather than proving uniqueness itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.