absValueGeneratedNativeCost
plain-language theorem explainer
Absolute-value generated native cost sends each rational orbit to a cost orbit via the absolute-value character, with the unit orbit forced to zero. It is the standard counterexample witness that primitive recognition cost uniqueness needs a signed-unit axiom: it satisfies the slim sans-sign package but fails sign reversal at −1. Defined by a classical case split on the unit orbit, then cost-from-character.
Claim. For each rational orbit $q$, the absolute-value generated native cost is the zero orbit when $q$ is the unit orbit, and otherwise the cost generated from the absolute-value character of $q$ (the character that replaces $q$ by the orbit of $|q|$ as a rational).
background
In the primitive recognition calculus, rational displays are RatioOrbit values: a signed numerator orbit over a nonzero distinction-natural denominator. Characters are maps on these orbits that respect the ratio structure. The absolute-value character is the quotient-respecting map that erases the sign of $-1$, sending $q$ to the orbit of $|q|$ as a rational.
Cost-from-character turns any such character $\chi$ into a cost map by applying the native on-orbit cost construction to $\chi(q)$. The canonical PRC cost is the identity-character case. The present definition is the absolute-value special case, with an explicit unit-orbit calibration to zero so that doubled-trace and zero-calibration lemmas apply cleanly.
Local setting is native-cost uniqueness in the PRC foundation: which axiom fields force the cost to be the canonical $J$-type cost on rational orbits, versus which fields admit exotic witnesses.
proof idea
Definition by classical case split. If the input orbit equals the unit orbit, return the zero orbit. Otherwise return cost-from-character applied to the absolute-value character at that orbit. No further lemmas are invoked in the body; downstream theorems re-establish cross-equality with the pure character cost and package the native or sans-sign hypothesis bundles.
why it matters
This is the load-bearing exotic witness for signed-unit necessity in native-cost uniqueness. Downstream, it inhabits the slim sans-sign hypothesis class, is shown not sign-reversing, and is fed into the refutation that uniqueness fails if the signed-unit field is dropped: the uniqueness target without that field is false because this cost meets base, pairs, and zero calibration yet is non-canonical at $-1$.
In the Recognition framework this sits under T5 $J$-uniqueness. The canonical cost is the identity-character case tied to $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law. Showing that absolute-value collapse produces a distinct cost that still satisfies most structural axioms isolates the signed unit as indispensable, rather than decorative, in the forcing chain toward a unique native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.