absValueGeneratedNativeCost_prime_pair_product_cost
plain-language theorem explainer
The absolute-value-generated native cost is already canonical on products of two prime directions: its value there is cross-equal to the standard ratio-orbit cost. Anyone packaging the strengthened native-cost interface for uniqueness cites this. The proof is a short crossEq-transitivity chain through the character-level prime-pair identity and the generated-cost bridge.
Claim. Let $F$ be the native cost generated from the absolute-value character on ratio orbits. For every pair of prime orbits $p,r$, writing $q$ for the product of their prime directions, one has $\mathrm{crossEq}\bigl(F(q),\,C(q)\bigr)$, where $C$ is the canonical ratio-orbit cost. In other words $F$ is prime-pair-product calibrated.
background
In the Primitive Recognition Calculus, costs act on RatioOrbit (integer numerator over a nonzero orbit denominator). Equality of costs is the choice-free relation crossEq, which compares two orbits by an integer cross-multiplication identity rather than by rational display.
A native cost is generated from a character by sending the unit orbit to zero and otherwise applying costFromCharacter. The absolute-value character yields absValueGeneratedNativeCost. After the two-adic no-go, the older native-cost hypotheses are insufficient: a cost can still slip on products of prime directions. The repair is the predicate PRCNativeCostPrimePairProductCalibrated, which demands that $F$ already match the canonical cost on every product of two prime directions.
Upstream, the character itself is already prime-pair-product consistent (absValueCharacter_prime_pair_product_cost), and the generated cost is always crossEq to the character cost (absValueGeneratedNativeCost_crossEq_generated). Transitivity of crossEq is the integer-bridge lemma crossEq_trans.
proof idea
Term-mode after intro p hp r hr. Form the product orbit $q = \mathrm{mul}(\mathrm{primeDirection},p,,\mathrm{primeDirection},r)$. Apply crossEq_trans to the two legs:
absValueGeneratedNativeCost_crossEq_generated q, which equates the generated cost at $q$ withcostFromCharacter absValueCharacter q;absValueCharacter_prime_pair_product_cost p hp r hr, which equates that character cost at the prime-pair product with the canonicalonRatioOrbitvalue.
The composite is exactly the calibration goal. No case splits or classical choice beyond what those lemmas already encapsulate.
why it matters
This is the cost-level repair that closes the surface where two-adic generated costs escaped the older PRCNativeCostHypotheses. Downstream it is the prime_pair_product_cost field of absValueGeneratedNativeCost_strengthened_hypotheses, which packages the absolute-value-generated cost into PRCStrengthenedNativeCostHypotheses.
In the Recognition forcing chain this sits under native J-cost uniqueness (T5): the cost must be forced to the canonical $J(x)=(x+x^{-1})/2-1$ shape, and prime-pair products are the minimal multiplicative generators where a non-canonical character could still deviate. Calibrating the absolute-value generator here is a concrete step toward uniqueness of the PRC native cost, and thus toward the Recognition Composition Law identity that pins $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.