PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_of_two_adic_axis_twist
plain-language theorem explainer
A prime-calibrated two-adic axis-twist character forces failure of the prime-pair product cost-consistency target. Anyone tracking character rigidity in the native-cost uniqueness branch cites this exclusion. The proof is a one-line contrapositive application of the matching absurdity lemma.
Claim. If there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and exhibits a two-adic axis twist, then it is not the case that every prime-direction-calibrated ratio character satisfies cost cross-equality on the product of any two native prime directions.
background
In the Primitive Recognition Calculus native-cost uniqueness module, characters on ratio orbits are candidate cost generators. A ratio character $\chi$ is prime-direction calibrated when its values on native prime directions match the intended cost calibration. The product-calibration target asks that this calibration propagate to every product of two prime directions: the cost extracted from $\chi$ on that composite must satisfy the cross-equality relation that identifies consistent cost values.
A two-adic axis twist is a concrete deformation of such a character along the $2$-adic direction. The existence proposition for a prime-calibrated two-adic axis-twist character is the native valuation route to refuting the current character-rigidity branch. The product target is the natural composite surface whose mixed-orientation $2\cdot p$ instance is the present branch-rigidity blocker.
Upstream, the absurdity lemma already shows that the product-consistency target implies there is no such twisted character. The present statement is the logical flip used at call sites that assume a twist model and need to discharge the target.
proof idea
Term-mode one-liner. Assume the product-consistency target hpair. Apply PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_prime_pair_product_cost_consistency to hpair, obtaining $\neg$ (existence of a prime-calibrated two-adic axis-twist character). Feed the hypothesis htwist into that negation to obtain False. Hence the target cannot hold under htwist.
why it matters
This exclusion is a local rigidity gate in the PRC native-cost uniqueness chain. It feeds the sibling exclusion for the broader two-adic axis-twist ratio-character package, which simply reduces to the present theorem. It also appears in the conditional universal-foundation certificate assembly in UniversalFoundation, where kernel, ordered-field, and trace-logic certificates are bundled only after character-side blockers are classified.
In the Recognition forcing picture this sits under cost uniqueness for the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) before $\phi$ and the eight-tick structure are forced. Closing or bypassing the two-adic twist branch is required before prime calibration can be promoted to full product consistency and thence to unique native cost. The declaration records that the twist model and the product target are incompatible, so any path that retains the twist must drop the target (or conversely).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.