threeAdicAxisTwistCharacter_two_identity
plain-language theorem explainer
The three-adic axis twist character fixes the prime-2 ratio orbit under cross-equivalence: it acts as the identity orientation on the 2-axis. Downstream uniqueness blockers cite this to separate 2-calibration from 3-axis freedom. The proof rewrites cross-equivalence to rational equality and applies the general fact that the three-adic twist fixes every prime direction other than 3.
Claim. Let $\chi_3$ be the three-adic axis twist character on ratio orbits (the orbit realization of $x \mapsto x \cdot 3^{-2 v_3(x)}$). Then $\chi_3$ applied to the prime-$2$ direction is cross-equivalent to that same prime-$2$ direction: the signed cross-multiplication balance holds, equivalently the verifier rational displays agree.
background
In the Primitive Recognition Calculus (PRC), rationals are carried as ratio orbits: a signed numerator orbit over a nonzero distinction-nat denominator. Two ratio orbits are related by cross-equivalence when the scaled numerators balance as signed orbits; by K4.10 this is equivalent to equality of the verifier rational displays toRat.
The three-adic axis twist character is the ratio-orbit realization of the verifier map $x \mapsto x \cdot 3^{-2 v_3(x)}$. On rationals it multiplies by a pure power of 3 determined by the 3-adic valuation, so it is expected to fix every prime direction other than the 3-orbit. The companion lemma threeAdicTwistRat_primeDirection_of_ne_three states exactly that: for any prime orbit $p \neq 3$, the twist leaves the corresponding prime direction's rational display unchanged.
This module develops native-cost uniqueness and its blockers: characters that match the canonical cost $J$ on some axes while flipping others, showing orientation is not forced by single-prime calibration.
proof idea
Term-mode proof in three steps. First rewrite the goal via crossEq_iff_toRat_eq, converting orbit cross-equivalence into equality of rational displays. Second, unfold the character through threeAdicAxisTwistCharacter_toRat, so the goal becomes equality of threeAdicTwistRat on the 2-direction with the 2-direction itself. Third, discharge by threeAdicTwistRat_primeDirection_of_ne_three at the 2-orbit (using that 2 is prime and threeOrbit ≠ twoOrbit), with a short simpa on the definition of twoPrimeDirection.
why it matters
This is a local identity lemma feeding the headline blocker prc_single_prime_calibration_insufficient. That theorem exhibits a PRC ratio character (exactly this three-adic axis twist) that agrees with the canonical cost orientation at prime 2 yet inverts the orbit-3 axis. Paired with the complementary underdetermination result that fixes every odd prime and flips 2, it shows orientation freedom is genuinely per-prime: pinning a single prime does not force the native cost character.
In the broader Recognition framework this sits inside native-cost uniqueness for the PRC cost built from the J-functional (T5: $J(x)=(x+x^{-1})/2-1$). The point is negative but structural: without multi-prime calibration, the doubled-trace / d'Alembert route to a unique native cost remains underdetermined. Closing that gap is what later uniqueness theorems must supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.