absValueCharacter_not_signed_unit_calibrated
plain-language theorem explainer
The absolute-value character on verifier ratio orbits fails signed-unit calibration: it sends the orbit of −1 to the positive unit rather than fixing it. Anyone excluding absolute value from the admissible PRC character class cites this lemma. The proof rewrites calibration to the rational equality |−1| = −1 and closes by numeric contradiction.
Claim. The absolute-value character $\chi_{|\cdot|}$ on ratio orbits is not signed-unit calibrated: $\chi_{|\cdot|}(-1)$ is not cross-equal to the orbit of $-1$ (equivalently, its rational display is not $-1$).
background
In the Primitive Recognition Calculus, rational displays are RatioOrbit values: a signed integer numerator over a nonzero distinction-nat denominator. Characters act on these orbits. Signed-unit calibration asks that a character fix the orbit of $-1$ under cross-equality of displays; prime-direction data alone cannot force that condition.
The absolute-value character sends each orbit $q$ to the orbit of $|q.\mathrm{toRat}|$. It is a quotient-respecting ratio character, but by construction it erases the sign of $-1$. Cross-equality of orbits is equivalent to equality of their rational displays (crossEq_iff_toRat_eq).
This module develops uniqueness of the native PRC cost by classifying admissible characters and matching them to doubled-trace / J-cost data. The present lemma is a negative calibration fact about one concrete candidate character.
proof idea
Assume signed-unit calibration of the absolute-value character. Unfold the calibration predicate, replace cross-equality by rational equality via crossEq_iff_toRat_eq, then apply the simplifiers absValueCharacter_toRat and negativeOneRatio_toRat. The hypothesis becomes $|-1| = -1$ in $\mathbb{Q}$, which norm_num refutes.
why it matters
Native cost uniqueness needs to know which ratio characters can be admissible and cost-matching. Absolute value is the natural sign-erasing candidate; this lemma shows it fails the signed-unit calibration gate. Downstream, PRCAdmissibleCharacterSignedUnitCalibratedTarget_refuted applies it directly: any claim that every admissible character is signed-unit calibrated is false because absolute value is admissible yet not calibrated. That refutation prunes the character landscape before matching doubled-trace data to the J-cost forced by the Recognition Composition Law and T5 uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.