absValueCharacter_toRat
plain-language theorem explainer
On every rational orbit display, the absolute-value character transports back to the ordinary absolute value of the displayed rational. Cost-uniqueness arguments that must erase sign while keeping magnitude cite this identity. The proof is a one-line rewrite: unfold the character and apply the ratio-orbit round-trip on rationals.
Claim. For every rational orbit display $q$ (signed-orbit numerator over a nonzero distinction-nat denominator), if $\chi_{|\cdot|}(q)$ denotes the absolute-value character of $q$ and $(\cdot)^{\sim}$ is the verifier map to $\mathbb{Q}$, then $(\chi_{|\cdot|}(q))^{\sim} = |q^{\sim}|$.
background
In the primitive recognition calculus, a ratio orbit is a display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator. The verifier map sends such a display to $\mathbb{Q}$ by integer division of the two components (spec tag A5: a transport wrapper whose internal equality is cross-multiplication).
The absolute-value character rebuilds a ratio orbit from the ordinary absolute value of that rational display. It is quotient-respecting as a ratio character, but by construction it forgets the sign of $-1$. The companion round-trip lemma states that rebuilding a ratio orbit from any rational $x$ and reading it back recovers $x$ exactly.
This module develops native-cost uniqueness for PRC characters: which multiplicative characters on ratio orbits can generate the canonical cost, and which fail calibration or orientation tests.
proof idea
One-line wrapper. Rewrite by the definition of the absolute-value character (rebuild via the absolute value of the displayed rational), then apply the round-trip theorem that reading a ratio orbit rebuilt from a rational recovers that rational. The absolute-value on $\mathbb{Q}$ is left as-is.
why it matters
This simp identity is the computational bridge from the absolute-value character to concrete rational arithmetic. Downstream it discharges the unit and prime-identity clauses of the ratio-character structure, the prime-pair product-cost consistency check, and the generated-cost cross-equality and doubled-trace calibration lemmas.
It is also the lever that kills signed-unit calibration and global orientation at $-1$: after transport, the character sends the negative-one ratio to $+1$, so it cannot match the canonical cost or either orientation of $-1$. That negative result is part of the native-cost uniqueness story: only characters that retain the signed unit can sit under the Recognition Composition Law cost forced later in the T5 J-uniqueness chain.
No open scaffold remains here; the theorem is fully proved and marked simp for routine rewriting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.