absValueCharacter_ratio_character
plain-language theorem explainer
The absolute-value map on ratio orbits is a PRC ratio character: it fixes the unit, multiplies, reciprocates, is normalization-invariant, and preserves nonzeroness, all up to cross-equivalence. Anyone building admissible characters for native-cost uniqueness, or refuting over-strong rigidity/orientation targets, cites this. The proof discharges each structure field by reducing cross-equivalence to rational equality and using ordinary absolute-value algebra.
Claim. Let $\chi_{\mathrm{abs}}$ be the absolute-value character on ratio orbits. Then $\chi_{\mathrm{abs}}$ is a PRC ratio character: $\chi_{\mathrm{abs}}(1)\sim 1$, $\chi_{\mathrm{abs}}(xy)\sim\chi_{\mathrm{abs}}(x)\chi_{\mathrm{abs}}(y)$, $\chi_{\mathrm{abs}}(x^{-1})\sim\chi_{\mathrm{abs}}(x)^{-1}$, $\chi_{\mathrm{abs}}$ is invariant under ratio normalization, and $\chi_{\mathrm{abs}}(q)\neq 0$ whenever $q\neq 0$, where $\sim$ denotes cross-equivalence of ratio orbits.
background
In the Primitive Recognition Calculus, costs are built on ratio orbits (quotient-native fractions of signed distinction data). A PRC ratio character is a map $\chi$ on ratio orbits that is a candidate factor in a d'Alembert-style factorization of a native cost. It is stated with cross-equivalence rather than definitional equality, so it stays well-defined on the orbit quotient.
Cross-equivalence of two orbits is equivalent to equality of their rational verifier displays (crossEq_iff_toRat_eq). Multiplication and reciprocal on orbits push forward to ordinary rational multiplication and inversion (mul_toRat, and the reciprocal display). Absolute value on the underlying signed orbits multiplies: $(zw)^{\mathrm{abs}}=z^{\mathrm{abs}}w^{\mathrm{abs}}$.
The local module develops native-cost uniqueness: which characters generate admissible PRC costs, and which rigidity claims about those characters fail. The absolute-value character is the canonical positive example against which signed and orientation-sensitive targets are tested.
proof idea
Tactic proof, one block per structure field. Each algebraic field rewrites the goal with crossEq_iff_toRat_eq, unfolds the absolute-value character on the rational display, and finishes by simp with the corresponding orbit-to-rational lemma plus ordinary abs algebra (abs_mul, abs_inv, norm_num for the unit).
Normalization invariance again reduces to rational equality and uses that normalizing a ratio does not change its rational display. Nonzero preservation is immediate: the rational display of the character is an absolute value, hence nonzero exactly when the input display is nonzero.
why it matters
This is the first gate for treating absolute value as a legitimate PRC character. Downstream, absValueCharacter_admissible packages it with prime calibration into a full admissible ratio character, and absValueGeneratedNativeCost_native_hypotheses uses the same character family to witness native-cost hypotheses for the abs-generated cost.
It is also the counterexample engine for two refuted targets in the uniqueness program. PRCNativeCostCharacterRigidityTarget_refuted shows that character rigidity fails: absolute value is a ratio character calibrated at two, yet its cost on the negative unit is not the canonical native cost. PRCCoherentPrimeOrientationPropagatesToGlobalTarget_refuted shows coherent prime orientation does not force global orientation, because absolute value fixes every positive prime axis but sends $-1$ to $+1$.
In the broader Recognition chain this sits under native J-cost uniqueness (the T5 J-uniqueness / RCL layer): it separates the positive multiplicative skeleton of a cost character from signed-unit calibration, which must be imposed separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.