absValueGeneratedNativeCost_not_signReversing
plain-language theorem explainer
The absolute-value native cost on ratio orbits fails sign reversal: if two orbits display opposite rationals, the cost does not satisfy F(-q) = -F(q) - 2. Anyone screening candidate native costs in the PRC ledger cites this to drop the absolute-value generator without comparing it to the canonical J-cost. The proof is a direct counterexample at the unit and its negative, both of which evaluate to zero under absolute value.
Claim. The absolute-value-generated native cost $F$ on ratio orbits is not sign-reversing: it is not the case that whenever $r$ and $q$ satisfy $r^{\mathrm{to}\mathbb{Q}} = -q^{\mathrm{to}\mathbb{Q}}$, one has $F(r)^{\mathrm{to}\mathbb{Q}} = -F(q)^{\mathrm{to}\mathbb{Q}} - 2$.
background
In the Primitive Recognition Calculus native-cost ledger, candidate costs are maps $F$ from ratio orbits to ratio orbits. A ratio orbit packages a signed rational display via toRat. Sign reversal is the structural demand that flipping the orientation of a distinction flips the doubled trace: with $T = 2(F+1)$, one wants $T(-q) = -T(q)$, equivalently $F(-q) = -F(q) - 2$ on displays.
The absolute-value-generated native cost collapses every orbit to a non-negative display of its magnitude. In particular it sends both the unit orbit and the negative-unit orbit to zero cost. The module is building a minimality certificate that isolates the canonical native cost by successively excluding competitors; this declaration is the round-3 witness that the signed unit is load-bearing.
Upstream, cross-equality of orbits is identified with equality of rational displays (crossEq_iff_toRat_eq), and the negative-one orbit is known to evaluate to zero under absolute value.
proof idea
Assume for contradiction that absolute-value native cost is sign-reversing. Instantiate the universal quantifier at the unit orbit $q = 1$ and the negative-one orbit $r = -1$, after checking $r^{\mathrm{to}\mathbb{Q}} = -q^{\mathrm{to}\mathbb{Q}}$ by unfolding the two displays.
Unfold absolute value at the unit to get cost display $0$. Transport the already-proved fact that absolute value at negative one is the zero orbit across crossEq_iff_toRat_eq to get cost display $0$ there as well. Substitute both zeros into the sign-reversal identity to obtain $0 = -0 - 2$, then close by norm_num.
why it matters
Recognition Science forces the unique native cost $J(x) = (x + x^{-1})/2 - 1$ (T5 in the forcing chain) from structural axioms rather than by fitting data. Sign reversal is one of those axioms: orientation flip must negate the doubled trace. Absolute value is the natural first competitor that forgets sign; excluding it by a pure counterexample, with no numerical comparison to canonical $J$, shows the signed-unit field is indispensable rather than decorative.
The doc-comment frames this as the round-3 witness in the PRC native-cost structural ledger. Downstream use is not yet wired in this graph (used_by empty), but the lemma sits in the exclusion ladder that feeds the minimality certificate imported from PRCNativeCostMinimalityCertificate. It is pure foundation bookkeeping: no mass ladder, no $\alpha$ band, no eight-tick content, only the cost-selection filter that later physics inherits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.