PRCCharacterTwoAdicAxisTwist_two_three_mixed_image
plain-language theorem explainer
Any ratio-character with the two-adic axis twist sends the composite 2·3 direction to the mixed orientation recip(2)·3, up to cross-equivalence. Used when ruling out two-adic twist characters as admissible PRC cost factors. Proof multiplies the twist on 2 by the identity on 3 and transports via character multiplicativity and crossEq transitivity.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). Suppose $\chi$ is a two-adic axis twist: $\chi$ sends the prime-$2$ direction to its reciprocal, and fixes every other native prime direction. Then $\chi$ sends the composite $2\cdot 3$ direction to the mixed direction $\mathrm{recip}(2)\cdot 3$, up to cross-equivalence of ratio orbits.
background
In the Primitive Recognition Calculus, costs are analyzed through d'Alembert-style factorizations at the level of ratio orbits rather than bare rationals. A RatioOrbit is an integer numerator over a nonzero distinction-nat denominator; two orbits are related by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality).
A PRCRatioCharacter is a map $\chi$ on ratio orbits that preserves the unit, multiplies, and sends reciprocals to reciprocals, all up to crossEq. The two-adic axis twist is the concrete countermodel one would build from a native $2$-adic valuation: $\chi$ flips the orientation of the prime-$2$ axis and leaves every other prime axis identity-oriented.
The composite direction $2\cdot 3$ and the mixed direction $\mathrm{recip}(2)\cdot 3$ are the natural test pair for whether that twist is compatible with multiplicative structure on products of distinct primes.
proof idea
Short tactic proof in three steps. First, instantiate the twist's second conjunct on the prime-$3$ orbit (distinct from $2$) to get $\chi(3)\sim 3$. Second, apply character multiplicativity to $2$ and $3$, so $\chi(2\cdot 3)\sim\chi(2)\cdot\chi(3)$. Third, use the twist's first conjunct $\chi(2)\sim\mathrm{recip}(2)$ together with the identity on $3$, and close under ratioOrbit_mul_congr, obtaining $\chi(2)\cdot\chi(3)\sim\mathrm{recip}(2)\cdot 3$. Finish by crossEq_trans.
why it matters
This is a local image lemma inside the native-cost uniqueness campaign: it pins what a two-adic twist character does on the first mixed prime product. Downstream it feeds PRCCharacterTwoAdicAxisTwist_two_three_local_orientation_absurd, which shows the twist cannot satisfy the two-three composite local-orientation constraint, and then the broader refutations twoAdicAxisTwistCharacter_not_prime_pair_product_cost_consistent, PRCNoAdmissibleFactorForTwoAdicAxisTwistGeneratedCost, twoAdicGeneratedNativeCost_not_prime_pair_product_calibrated, and PRCNativeCostUniquenessTarget_refuted.
In framework terms it helps eliminate the obvious $2$-adic valuation countermodel against unique native cost factorization, supporting the conditional universal-foundation certificate. It sits upstream of J-cost uniqueness (T5) rather than replacing it: the point is that only the symmetric J-character survives prime-pair product calibration, not a one-sided two-adic twist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.