absValueGeneratedNativeCost_negative_one_zero
plain-language theorem explainer
At the ratio orbit for −1, the absolute-value-generated native cost is cross-equivalent to the zero orbit. Uniqueness and structural-ledger arguments cite this to kill the absolute-value competitor without comparing full cost tables. The proof unfolds the generator, reduces cross-equivalence to rational equality, and finishes by norm_num on |−1|.
Claim. Let $C_{|\cdot|}$ be the native cost generated from the absolute-value character on ratio orbits. Then $C_{|\cdot|}(-1)$ is cross-equivalent to the zero ratio orbit: the internal cross-multiplication relation identifies $C_{|\cdot|}(-1)$ with $0$.
background
Primitive Recognition Calculus (PRC) works with ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator, the internal stand-in for nonzero rationals. Two orbits are related by crossEq when scaled numerators balance under the signed-orbit product, which is exactly rational equality of the verifier displays (crossEq_iff_toRat_eq).
The absolute-value character sends a ratio orbit $q$ to an orbit displaying $|q.\mathrm{toRat}|$. The generated native cost absValueGeneratedNativeCost returns zero on the unit orbit and otherwise applies costFromCharacter to that absolute-value character. The special orbit negativeOneRatio is the internal display of $-1$.
This module builds uniqueness and exclusion lemmas for candidate native costs. Absolute value is the natural non-canonical competitor once a character-to-cost bridge is available; evaluating it at $-1$ is the first concrete obstruction.
proof idea
Term-mode rewrite proof. Unfold absValueGeneratedNativeCost and discharge the unit branch by negativeOneRatio_ne_one, so the value is costFromCharacter absValueCharacter negativeOneRatio. Rewrite crossEq to rational equality via crossEq_iff_toRat_eq, then chain costFromCharacter_toRat, absValueCharacter_toRat, negativeOneRatio_toRat, and zero_toRat. The resulting numerical identity is closed by norm_num (absolute value of $-1$ feeds a cost that displays as $0$).
why it matters
Feeds two exclusion results. Downstream, absValueGeneratedNativeCost_negative_one_not_canonical uses the zero evaluation to separate absolute-value cost from the canonical on-ratio cost at $-1$. The structural ledger theorem absValueGeneratedNativeCost_not_signReversing cites the same point as the round-3 witness that the signed-unit field is load-bearing: absolute value is ruled out by sign reversal with no reference to the canonical cost table.
In the broader Recognition forcing chain this is local scaffolding under T5 J-uniqueness: candidate costs built from non-canonical characters must fail either the d'Alembert/RCL identities or a structural axiom such as sign reversal. Pinning $C_{|\cdot|}(-1)=0$ is the elementary arithmetic step that makes those failures checkable inside PRC rather than only on real displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.