twoAdicGeneratedNativeCost_not_prime_pair_product_calibrated
plain-language theorem explainer
The two-adic generated native cost fails prime-pair product calibration: on the product of the 2- and 3-prime directions it disagrees with the canonical rational J-cost. Anyone proving native-cost uniqueness or pair-field necessity cites this no-go. The proof chains cross-equivalence through the two-adic axis-twist character and closes with the mixed-versus-composite J-cost mismatch on ratio orbits.
Claim. Let $F$ be the two-adic generated native cost on ratio orbits. Then $F$ is not prime-pair product calibrated: it is false that for every pair of prime orbits $p,r$, $F(p\cdot r)$ is cross-equivalent to the rational $J$-cost $J(q)=((q+q^{-1})/2)-1$ evaluated at $q=p\cdot r$.
background
Primitive Recognition Calculus works on ratio orbits: integer numerator over a nonzero distinction-nat denominator. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality).
The canonical rational $J$-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$, realized as the ratio-orbit map onRatioOrbit. Prime-pair product calibration demands that a candidate native cost $F$ already agree with this $J$ on every product of two native prime directions: $F(p\cdot r)\sim J(p\cdot r)$ under cross-equivalence. The doc-comment flags this as the exact surface where the two-adic generated cost slips past the older native-cost hypotheses.
The two-adic generated cost is built from a character along the two-adic axis; on composite directions it can twist away from pure $J$. The mixed $(2,3)$ image versus the plain composite $(2\cdot 3)$ direction is the concrete witness used below.
proof idea
Assume calibration and instantiate at the prime orbits $2$ and $3$. Calibration yields $F(2\cdot 3)\sim J(2\cdot 3)$. Separately, the generated-cost identity gives $F(2\cdot 3)\sim$ cost-from-character of the two-adic axis-twist character at that composite. The twist character sends the composite to the mixed $(2,3)$ direction, so cost-from-character equals $J$ on the mixed direction (via congruence of onRatioOrbit). Transitivity and symmetry of cross-equivalence then force $J(\mathrm{mixed})\sim J(\mathrm{composite})$. That contradicts the dedicated mismatch lemma for the two-prime composite versus mixed image under $J$.
why it matters
This is the concrete no-go that forces the pair-product field into the native-cost interface. Downstream, PRCSlimSansPairUniquenessTarget_refuted applies it directly: base + sign + zero alone admit the two-adic twist, which fails prime-pair products at the mixed $(2,3)$ orbit, so the pair field cannot be dropped. The sibling twoAdicGeneratedNativeCost_not_strengthened_hypotheses packages the same fact as failure of the strengthened native-cost hypotheses.
In the Recognition forcing chain this protects T5-style $J$-uniqueness at the discrete PRC layer: without pair calibration, a non-canonical two-adic twist would survive as a competing native cost. The result closes the gap named in the calibration doc-comment between older PRCNativeCostHypotheses and the repaired interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.