threeAdicAxisTwistCharacter
plain-language theorem explainer
Defines the ratio-orbit lift of the classical three-adic branch twist $x \mapsto x \cdot 3^{-2 v_3(x)}$. It fixes every prime axis other than 3 and inverts the orbit-3 direction. Cited when proving that native-cost calibration at a single prime (agreement with J at 2) does not force the remaining axes. The body is a one-line section–display–resection through rationals.
Claim. For a ratio orbit $q$, the three-adic axis twist character returns the ratio orbit of the rational display $q_{\mathbb{Q}} \cdot 3^{-2\,v_3(q_{\mathbb{Q}})}$, where $v_3$ is the $3$-adic valuation on $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). The map toRat is a verifier display of that orbit as an ordinary rational; the reverse section ratioOrbitOfRat rebuilds an orbit from a classical rational so that character interfaces can be stress-tested against classical countermodels.
The classical three-adic twist on rationals multiplies by $3^{-2 v_3(x)}$. It is the base-3 analogue of the two-adic twist: it leaves every non-3 prime axis fixed and inverts the orbit-3 exponent. The present definition simply transports that rational map through the ratio-orbit display, yielding a candidate PRC ratio character on orbits rather than on $\mathbb{Q}$.
The surrounding module studies uniqueness (and non-uniqueness) of native cost functionals built from ratio characters, against the canonical J-cost from the forcing chain.
proof idea
Pure definitional composition: display the input orbit as a rational via toRat, apply the classical three-adic twist threeAdicTwistRat, then re-section with ratioOrbitOfRat. No tactics; the nontrivial content lives in the lemmas that relate this character back to rationals and to the prime directions.
why it matters
This is the concrete witness used by the headline blocker prc_single_prime_calibration_insufficient: there exists a PRC ratio character that agrees with the canonical cost orientation at the prime 2 yet inverts the orbit-3 axis. Paired with the complementary two-adic orientation underdetermination, it shows orientation freedom is genuinely per-prime, so calibrating native cost at one prime does not propagate to the others.
Downstream lemmas establish that the map is a PRC ratio character, that it acts as the identity on the two-prime direction, that it sends the three-prime direction to its reciprocal, and that its rational display equals the classical twist. In the Recognition framework this blocks a naive uniqueness claim for native cost before the full J-uniqueness (T5) and RCL structure are imposed; single-axis agreement with J is not enough.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.