twoAdicAxisTwistCharacter_not_prime_pair_product_cost_consistent
plain-language theorem explainer
The two-adic axis-twist ratio character fails prime-pair product cost consistency: its induced cost on a product of distinct prime directions is not cross-equivalent to the native J-cost on that product. Anyone ruling out non-native PRC characters cites this. The proof assumes consistency on the 2–3 composite, pushes the character image to the mixed 2–3 direction, and obtains a contradiction from the known J-cost mismatch between composite and mixed orbits.
Claim. The two-adic axis-twist character $\chi$ on ratio orbits is not prime-pair product cost consistent: it is not the case that for every pair of prime orbits $p,r$, the cost induced by $\chi$ on the product of the corresponding prime directions is cross-equivalent (in the PRC rational sense) to the native $J$-cost $J(q)=((q+q^{-1})/2)-1$ evaluated on that same product direction.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit objects (signed numerator over a nonzero distinction-nat denominator). Equality of displays is the choice-free cross-multiplication relation crossEq: two orbits match when scaled numerators balance. The native cost on a ratio orbit is the rational $J$-object $J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit.
A ratio character $\chi$ induces a cost by composing $\chi$ with that native $J$. Prime-pair product cost consistency (character-local form) demands that for every pair of prime orbits, the induced cost on the product of their prime directions agrees, under crossEq, with native $J$ on that product. This is one field of admissibility for a character, separate from the global calibration target that forces the same condition from prime calibration alone.
The two-adic axis-twist character is a candidate non-native map on ratio orbits. The surrounding module develops native-cost uniqueness by showing that only characters matching the doubled-trace/$J$ picture survive the full admissibility package.
proof idea
Proof by contradiction. Assume the twist character is prime-pair product cost consistent. Instantiate that hypothesis on the prime orbits of 2 and 3: the induced cost on the 2–3 composite prime-product direction is crossEq to native $J$ on that composite.
A dedicated image lemma for the two-adic axis twist then shows that $\chi$ sends the composite direction to the mixed 2–3 direction. Congruence of onRatioOrbit under crossEq therefore moves the induced cost to native $J$ on the mixed direction.
Symmetry and transitivity of crossEq glue the two cost identities, yielding native $J$ on the mixed direction equivalent to native $J$ on the composite. That contradicts the pre-established mismatch lemma two_prime_composite_mixed_image_jcost_mismatch for the 3-orbit. Hence consistency fails.
why it matters
This is a concrete exclusion step inside PRC native-cost uniqueness: the two-adic axis twist is a natural algebraic deformation along the 2-axis, and it must be killed before claiming that only the native $J$-cost character is admissible.
Its sole recorded consumer is twoAdicAxisTwistCharacter_not_admissible, which simply unpacks admissibility and applies this theorem to the prime-pair product cost field. That non-admissibility feeds the broader forcing that admissible ratio characters reproduce the Recognition Composition Law cost $J(x)=(x+x^{-1})/2-1$ (T5 J-uniqueness in the unified forcing chain).
In framework terms, product-cost consistency is the discrete PRC shadow of RCL multiplicativity on prime generators; failing it means the twist cannot serve as a recognition cost, so it cannot compete with the $\phi$-forced native ladder cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.