threeAdicAxisTwistCharacter_toRat
plain-language theorem explainer
Transport lemma: the three-adic axis twist on ratio orbits, after display as a rational, equals the classical three-adic branch twist of that rational. Cost-uniqueness and character arguments cite it to move between orbit-level and verifier-rational statements. Proof is a one-line unfold plus the round-trip identity for ratioOrbitOfRat.
Claim. For every rational orbit $q$, the rational display of the three-adic axis-twist character applied to $q$ equals the classical three-adic branch twist of the rational display of $q$: $\mathrm{display}(\chi_3(q)) = \tau_3(\mathrm{display}(q))$, where $\tau_3(x)=x\cdot 3^{-2v_3(x)}$.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio orbits are the internal display of rationals: a signed-orbit numerator over a nonzero distinction-nat denominator. The map toRat is the verifier transport of that display to $\mathbb{Q}$ (spec tag A5: internal equality is cross-multiplication).
The classical three-adic branch twist on rationals is $\tau_3(x)=x\cdot 3^{-2v_3(x)}$. It fixes every prime axis other than $3$ and inverts the $3$-adic exponent. Its purpose is comparative: agreement of native cost with $J$ at the prime $2$ need not force the same calibration on the $3$-axis.
The orbit-level character is defined by pushing $q$ through toRat, applying $\tau_3$, and lifting back via ratioOrbitOfRat. The round-trip theorem (ratioOrbitOfRat x).toRat = x is the algebraic hinge that makes orbit and rational statements interchangeable.
proof idea
One-line term proof. Unfold the definition of the three-adic axis-twist character (which is ratioOrbitOfRat (threeAdicTwistRat q.toRat)), then apply ratioOrbitOfRat_toRat to the rational threeAdicTwistRat q.toRat. No further arithmetic is needed.
why it matters
This transport is the bridge used by three immediate parents: the proof that the three-adic axis twist is a PRCRatioCharacter (unit axiom via display equality), the identity on the two-prime direction (cross-equality after display), and the reciprocal relation on the three-prime direction. Together those facts show that a character can match native cost calibration at $2$ while twisting the $3$-axis, so uniqueness of the native cost cannot be read off from a single prime axis alone.
In the broader Recognition forcing picture this sits under native-cost uniqueness relative to the $J$-cost (T5: $J(x)=(x+x^{-1})/2-1$). It is a negative-control lemma: multi-prime characters exist that preserve ratio-character axioms yet disagree with pure $J$-calibration off the calibrated prime. Downstream uniqueness arguments must therefore pin the cost on all axes, not just the two-adic one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.