absValueCharacter
plain-language theorem explainer
Defines the absolute-value character on verifier ratio orbits: map each orbit to the orbit of the absolute value of its rational display. It is a quotient-respecting ratio character that forgets the sign of −1. Downstream uniqueness and calibration lemmas cite it as the classical countermodel that is prime-calibrated and admissible yet fails signed-unit calibration. The body is a one-line section–display composite.
Claim. For a ratio orbit $q$, the absolute-value character returns the ratio orbit representing $|\mathrm{toRat}(q)|$, i.e. the absolute value of the rational display of $q$, re-embedded as a ratio orbit.
background
In the Primitive Recognition Calculus, a ratio orbit is a verifier display of a rational: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). The map toRat sends such a display to $\mathbb{Q}$ by integer division; the inverse section ratioOrbitOfRat rebuilds a ratio orbit from a classical rational, used to test whether the character interface already admits classical countermodels.
A ratio character is a self-map of ratio orbits used to build native costs via costFromCharacter. The absolute-value character is the simplest classical candidate: it respects the quotient structure of ratios but collapses $q$ and $-q$ whenever they differ only by sign.
The surrounding module studies uniqueness of the native cost on these displays, comparing characters that are prime-calibrated, signed-unit calibrated, and admissible under the PRC ratio-character axioms.
proof idea
One-line definition: compose the rational display of $q$ with ordinary absolute value on $\mathbb{Q}$, then re-embed via the verifier section ratioOrbitOfRat. No further proof obligations; noncomputable only because the section uses classical rational data.
why it matters
This character is the standard classical foil in the native-cost uniqueness development. Downstream results show it is admissible as a PRC ratio character and prime-direction calibrated (hence prime-pair product cost holds), yet it fails signed-unit calibration and does not match the canonical cost on the negative-one ratio; it also admits no global orientation at $-1$.
Those negative results pin what uniqueness must demand beyond prime calibration: orientation or signed-unit data that absolute value erases. In the broader Recognition forcing chain this sits under the foundation layer that isolates the unique $J$-cost (T5) before $\phi$ and the eight-tick structure are forced; the absolute-value map is exactly the sort of classical collapse the native character must rule out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.