absValueCharacter_prime_pair_product_cost
plain-language theorem explainer
The absolute-value ratio character meets prime-pair product cost consistency: for any two primes, the character-induced cost of the product of their prime directions is cross-equivalent to the on-ratio-orbit display of that product. Anyone assembling admissibility of the absolute-value character cites this field. The proof reduces cross-equality to rational displays and uses nonnegativity of the prime naturals.
Claim. Let $\chi_{|\cdot|}$ be the absolute-value map on ratio orbits. For every pair of prime distinction-naturals $p,r$, writing $d_p$ and $d_r$ for their prime directions, the cost induced by $\chi_{|\cdot|}$ on the product orbit $d_p\cdot d_r$ is cross-equivalent (as ratio orbits) to the on-ratio-orbit display of $d_p\cdot d_r$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-natural denominator (K4.7). Two ratio orbits are related by cross-multiplication equivalence when the scaled signed numerators balance; this internal relation agrees with equality of the rational verifier displays (K4.10: crossEq iff toRat equality).
A ratio character is a map on ratio orbits used to build a cost. Character-local prime-pair product cost consistency asks that, for every pair of primes, the cost induced by the character on the product of the two prime directions matches the on-ratio-orbit display of that product under cross-equivalence. Unlike a global calibration target, this is a single-character admissibility field.
The absolute-value character sends each ratio orbit to the orbit whose rational display is the absolute value of the original. Multiplication of ratio orbits multiplies rational displays, and prime directions display as the corresponding nonnegative naturals.
proof idea
Fix primes $p,r$. First prove that the absolute-value character applied to the product of the two prime directions is cross-equivalent to that product itself. Rewrite cross-equivalence as equality of rational displays, expand the character and the product via the toRat lemmas for the character, multiplication, and prime directions, and conclude by $|p\cdot r|=p\cdot r$ from nonnegativity of the two naturals (abs_of_nonneg and mul_nonneg, casting Nat.zero_le).
Then apply the congruence of the on-ratio-orbit display under cross-equivalence to obtain the required match between character-induced cost and on-ratio-orbit display of the product.
why it matters
This discharges the prime-pair product cost field in the admissibility package for the absolute-value character. Downstream, absValueCharacter_admissible assembles ratio-character, prime-calibration, and this product-cost field into full admissibility of $\chi_{|\cdot|}$.
That admissibility feeds the uniqueness pipeline for native cost: the sibling theorem on absolute-value-generated native cost uses the same prime-pair product calibration pattern (via cross-equivalence transitivity through the generated cost) to show the generated native cost is prime-pair product calibrated.
In the broader Recognition foundation, native cost uniqueness is the PRC route to forcing the J-cost shape (T5 landmark: $J(x)=(x+x^{-1})/2-1$) from recognition axioms rather than by postulate. Closing character admissibility is a concrete step on that forcing path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.