PRCNoAdmissibleFactorForTwoAdicAxisTwistGeneratedCost
plain-language theorem explainer
If a ratio-orbit cost map is generated by the two-adic axis twist character, no admissible ratio character can reproduce it. Admissibility here means ratio-character laws, prime calibration, and prime-pair product cost consistency (valuation twists excluded). Cite when ruling out twist-generated countermodels to native J-cost uniqueness. The proof chains cross-equality through the 2–3 composite direction and closes on a J-cost mismatch between mixed and composite images.
Claim. Let $F$ be a map on ratio orbits such that for every orbit $q$, $F(q)$ is cross-equivalent to the cost induced by the two-adic axis twist character at $q$. Then there is no admissible ratio character $\psi$ (ratio-character laws, prime calibration, and prime-pair product cost consistency) for which $F(q)$ is cross-equivalent to the cost induced by $\psi$ at every $q$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed numerator orbit over a nonzero distinction-nat denominator. Equality is internal cross-multiplication balance (crossEq), not classical $\mathbb{Q}$ equality. The native cost on a ratio orbit is the orbit-level $J$-object $J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit.
Characters assign ratio orbits to ratio orbits. After a two-adic countermodel, admissibility was repaired: a character must obey the ratio-character laws, be prime-direction calibrated, and keep prime-pair product costs consistent with native $J$. That package preserves the two global orientations and deliberately excludes valuation twists.
costFromCharacter turns a character into a cost map. The two-adic axis twist is a concrete non-admissible character; this theorem says any cost it generates cannot be re-factored through an admissible character.
proof idea
Assume for contradiction an admissible $\psi$ whose induced cost matches $F$ under crossEq. Admissibility supplies prime-pair product cost consistency on the $2$ and $3$ prime orbits, so the cost of $\psi$ on the $2$–$3$ composite direction is cross-equivalent to native $J$ on that composite.
A dedicated image lemma for the two-adic axis twist sends the $2$–$3$ composite direction to the mixed $2$–$3$ direction. Unfolding costFromCharacter and applying orbit congruence, the twist-induced cost on the composite equals native $J$ on the mixed direction.
Transitivity and symmetry of crossEq, with the hypothesis that $F$ is the twist cost and equals the $\psi$ cost, force native $J$ on the mixed image to match native $J$ on the composite. That contradicts two_prime_composite_mixed_image_jcost_mismatch for the prime orbit $3$.
why it matters
Native cost uniqueness in PRC must block factorization loopholes: maps that look like costs but come from twisted characters. This theorem kills the two-adic axis twist as a source of admissible factorization.
It is consumed immediately by PRCNativeCostFactorizationAdmissibilityUpgradeTarget_not_of_two_adic_axis_twist_generated_cost, which lifts the pointwise obstruction to the named upgrade-target interface: if native hypotheses hold for a twist-generated cost, the factorization-admissibility upgrade target fails.
In the broader forcing chain this protects T5-style $J$-uniqueness at the discrete PRC layer. The Recognition Composition Law and the closed form $J(x)=(x+x^{-1})/2-1$ only pin physics if competing character-induced costs cannot sneak in under a weaker admissibility notion. The repaired admissible interface (no valuation twists) is exactly what makes the obstruction bite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.