absValueCharacter_admissible
plain-language theorem explainer
The absolute-value map on ratio orbits is an admissible ratio character in the repaired PRC interface: it obeys ratio-character laws, is prime-calibrated, and has consistent prime-pair product costs. Anyone separating unsigned admissibility from signed-unit calibration cites this. The proof is a structure constructor packing three prior lemmas.
Claim. The absolute-value character on ratio orbits (sending each orbit to the orbit of $|q|$ for a rational representative $q$) is an admissible ratio character: it satisfies the ratio-character axioms, is calibrated on primes, and is consistent for prime-pair product costs.
background
In the Primitive Recognition Calculus, ratio orbits are the quotient of nonzero rationals under the verifier display equivalence. A ratio character is a self-map of that quotient obeying the algebraic laws of a multiplicative character on displays (unit fixed, compatible with products and inverses in the orbit sense).
After a two-adic countermodel, the repaired admissible interface requires three fields: the ratio-character laws, prime-direction calibration, and prime-pair product-cost consistency. The doc-comment states this "preserves the two global orientations but excludes valuation twists." The absolute-value character is the map $q \mapsto |q|$ on representatives; it is a quotient-respecting ratio character that erases the sign of $-1$.
Upstream lemmas already establish each of the three fields for this map separately: ratio-character laws, prime calibration via the prime identity, and prime-pair product-cost consistency.
proof idea
Term-mode structure constructor for PRCAdmissibleRatioCharacter. It fills the three fields by naming the three prior theorems: ratio-character laws from absValueCharacter_ratio_character, prime calibration from absValueCharacter_prime_calibrated, and prime-pair product-cost consistency from absValueCharacter_prime_pair_product_cost. No new algebra is done here.
why it matters
This packages the absolute-value character as a concrete witness of the repaired unsigned admissible interface. Downstream, PRCAdmissibleCharacterSignedUnitCalibratedTarget_refuted applies it: if every admissible character preserved the signed unit, then the absolute-value character would, but it erases the sign of $-1$, so the stronger signed-unit-calibrated target is false.
In the PRC native-cost uniqueness arc this separates orientation-preserving admissibility from signed-unit calibration. It sits in the foundation layer that forces the native cost (linked to the J-cost uniqueness chain T5 and the Recognition Composition Law) by ruling out twisted characters while keeping the absolute-value example inside the admissible class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.