absValueGeneratedNativeCost_negative_one_not_canonical
plain-language theorem explainer
The absolute-value generated native cost fails to match the canonical J-cost at the signed unit ratio −1. Anyone arguing that the sign field can be dropped from native-cost uniqueness cites this counterexample. The proof reduces cross-equality to rational equality, substitutes the known zero value of the abs-cost at −1, and finishes by norm_num against J(−1).
Claim. The absolute-value generated native cost at the ratio orbit $-1$ is not cross-equivalent (via balanced cross-multiplication of numerator and denominator orbits) to the canonical PRC $J$-cost $J(q)=((q+q^{-1})/2)-1$ evaluated at $-1$.
background
In the Primitive Recognition Calculus, rationals are carried as RatioOrbit displays: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by crossEq, the internal cross-multiplication relation; by K4.10 this agrees with equality of the verifier rationals (crossEq_iff_toRat_eq).
The canonical cost on ratio orbits is onRatioOrbit, the discrete $J$-object $J(q)=((q+q^{-1})/2)-1$. Separately, the module builds an absolute-value generated native cost that collapses sign. A sibling lemma already records that this abs-cost at the negative-one ratio is the zero orbit.
The local setting is native-cost uniqueness for PRC: which axioms force the cost to be exactly $J$, and which candidate costs survive weaker axiom packages.
proof idea
Assume for contradiction that the abs-cost at negative-one is crossEq to onRatioOrbit at negative-one. Rewrite via crossEq_iff_toRat_eq to equality of toRat displays. From absValueGeneratedNativeCost_negative_one_zero and the same iff, the abs-cost side is the zero orbit, so its toRat is $0$. Substitute that and the known toRat of $J(-1)$, then norm_num yields the contradiction $0=-2$.
why it matters
This is the concrete obstruction that kills uniqueness packages missing signed-unit calibration. Downstream it is applied verbatim to refute the strengthened, zero-calibrated, and slim-sans-sign uniqueness targets, and to show the abs-cost is not signed-unit calibrated. The minimality certificate quotes it for signed-unit necessity: base + pairs + zero admit the abs-cost, which fails at the signed unit, so the sign field cannot be dropped.
In the Recognition forcing chain this sits under T5 ($J$-uniqueness): $J(x)=(x+x^{-1})/2-1$ is the cost fixed by the composition law, and sign-blind competitors are ruled out on the discrete ratio-orbit carrier before the real-analytic bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.