threeAdicTwistRat
plain-language theorem explainer
The three-adic branch twist on nonzero rationals multiplies x by 3 to the power of minus twice its 3-adic valuation, fixing every prime axis other than 3 and inverting the 3-exponent. Native-cost uniqueness arguments cite it to exhibit a multiplicative character that agrees with the classical J-cost calibration at 2 yet moves the 3-axis. The body is a one-line closed formula in padicValRat.
Claim. For $x \in \mathbb{Q}$, define the three-adic twist $T_3(x) := x \cdot 3^{-2\,v_3(x)}$, where $v_3$ is the $3$-adic valuation on rationals (with the usual convention at $0$). Equivalently, if $x = \pm 3^k \cdot m/n$ in lowest terms with $3 \nmid mn$, then $T_3(x) = \pm 3^{-k} \cdot m/n$.
background
In the Primitive Recognition Calculus, rational displays carry a prime-axis decomposition via p-adic valuations. The native cost is a candidate cost functional on ratio orbits; uniqueness questions ask whether agreement with the classical J-cost $J(x)=(x+x^{-1})/2-1$ on one prime axis forces agreement on all axes.
The two-adic twist is the base-2 analogue already used to probe calibration at the prime 2. The three-adic twist is the parallel map at base 3: it leaves every prime factor other than 3 untouched and sends the 3-exponent $k$ to $-k$ (implemented as the factor $3^{-2v_3(x)}$, which doubles the sign flip in the exponent relative to a pure inversion of the 3-power). The surrounding module builds ratio-orbit characters and doubled-trace d'Alembert identities that compare native cost against J after such twists.
No external theorem is required for the definition itself; downstream lemmas establish that $T_3$ is multiplicative, sends inverses to inverses, and never hits zero on nonzero input.
proof idea
Pure definitional abbreviation: unfold to the closed formula $x \cdot 3^{-2,\mathrm{padicValRat},3,x}$. Noncomputable only because p-adic valuation on $\mathbb{Q}$ is noncomputable in the Mathlib sense. No tactics or lemmas are invoked at the definition site; algebraic properties (multiplicativity, inversion, nonvanishing) are proved separately by unfolding and case splits on zero.
why it matters
This map is the concrete witness that single-prime calibration of native cost does not propagate. Downstream, threeAdicAxisTwistCharacter lifts it to ratio orbits, and the algebraic lemmas threeAdicTwistRat_mul, _inv, _ne_zero, _one, and _primeDirection_of_ne_three equip it as a group-like character on $\mathbb{Q}^\times$. Those feed the native-cost uniqueness development: after forcing agreement with J along the 2-axis, the 3-twist produces a distinct character whose cost would still have to match if uniqueness held, yielding the separation between primes. In the broader Recognition forcing chain this sits under T5 J-uniqueness and the Recognition Composition Law: it shows that J's functional equation alone, once pinned at one prime display, does not automatically fix the cost on every other prime axis without further global hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.