absValueCharacter_negative_one_cost_not_canonical
plain-language theorem explainer
The absolute-value character, which forgets the sign of −1, induces a cost at the ratio orbit −1 that is not cross-equivalent to the native PRC J-cost J(q)=(q+q⁻¹)/2−1. Anyone arguing character rigidity of the native cost cites this as the concrete counterexample. The proof reduces both sides to rational displays and closes by numerical contradiction.
Claim. Let $J(q)=\frac{q+q^{-1}}{2}-1$ be the native PRC cost on ratio orbits, and let $c_{|\cdot|}$ be the cost induced by the absolute-value character $q\mapsto |q|$. Then the ratio-orbit values $c_{|\cdot|}(-1)$ and $J(-1)$ are not cross-equivalent: their cross-multiplied numerator/denominator orbits do not balance.
background
In the Primitive Recognition Calculus, rational displays are RatioOrbit objects: a signed-orbit numerator over a nonzero distinction-nat denominator. Equivalence of two such displays is internal cross-multiplication (crossEq): the scaled numerators balance as signed orbits. By K4.10 this agrees with ordinary rational equality of the verifier displays (toRat).
The native PRC cost on a ratio orbit is the orbit-level J-object
$J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit. Separately, a ratio character can be turned into a cost via costFromCharacter. The absolute-value character sends each orbit to the orbit of $|q.toRat|$; it is a quotient-respecting ratio character, but it erases the sign of $-1$.
This lemma sits in the native-cost uniqueness module, which tests whether every calibrated ratio character must reproduce the native J-cost on all ratio orbits.
proof idea
Assume cross-equivalence of the two costs at negativeOneRatio. Rewrite the assumption by crossEq_iff_toRat_eq, then push both sides to rationals with costFromCharacter_toRat, absValueCharacter_toRat, onRatioOrbit_toRat, and negativeOneRatio_toRat. The resulting rational equality is false by norm_num (absolute value sends $-1$ to $1$, so the induced cost is $J(1)=0$, while $J(-1)=-2$).
why it matters
This is the explicit witness that kills naive character rigidity. Downstream, PRCNativeCostCharacterRigidityTarget_refuted applies it: if every ratio character that is two-calibrated agreed with the native cost on all orbits, then the absolute-value character would match at $-1$, contradicting this theorem.
In the broader Recognition forcing chain, T5 forces the unique continuous cost $J(x)=\cosh(\log x)-1$ (equivalently $(x+x^{-1})/2-1$). The PRC layer must still show that discrete ratio characters cannot quietly substitute a different cost. Absolute value is the natural spoiler: it preserves the multiplicative character laws yet collapses the sign that $J$ sees at $-1$. The lemma therefore pins a necessary side-condition (sign sensitivity / oddness under inversion) before any rigidity theorem can hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.