axisTwistRat
plain-language theorem explainer
Defines the base-b axis twist on nonzero rationals: multiply x by b to the power of minus twice its b-adic valuation. This inverts the exponent of the prime b in the factorization of x and leaves every other prime fixed. Downstream uniqueness arguments for native PRC cost cite it as the rational model of a single-axis twist; the body is a one-line closed formula.
Claim. For a natural number $b$ and a rational $x$, the base-$b$ axis twist is $x \cdot b^{-2\,v_b(x)}$, where $v_b$ is the $b$-adic valuation on $\mathbb{Q}$. Equivalently, if $x = \pm b^k m/n$ in lowest terms with $b\nmid m,n$, the map sends $x$ to $\pm b^{-k} m/n$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, rational displays carry a prime factorization, and each prime axis can be twisted independently. The $b$-adic valuation $v_b(x)$ extracts the exponent of the prime $b$ in $x$ (extended by the usual conventions at $0$).
The axis twist is the unique monomial map that sends the exponent of $b$ to its negative while fixing the sign and all other prime powers. Special cases $b=2$ and $b=3$ recover the two-adic and three-adic twists used earlier in the module. The construction lives in the PRC native-cost uniqueness layer, which compares cost functionals built from ratio-orbit characters against doubled-trace and d'Alembert constraints.
No external lemma is required for the definition itself; later theorems impose Nat.Prime b when multiplicativity and inversion laws are proved.
proof idea
Pure definitional equation: return $x$ times the integer power $b^{-2 v_b(x)}$ (cast to $\mathbb{Q}$). Noncomputable only because p-adic valuation on rationals is noncomputable in the library. No tactics or upstream lemmas.
why it matters
This is the rational skeleton of single-axis twisting used throughout PRC native-cost uniqueness. It feeds axisTwistCharacter, which lifts the map to ratio orbits via ratioOrbitOfRat, and the companion lemmas axisTwistRat_mul, axisTwistRat_inv, axisTwistRat_ne_zero, axisTwistRat_one, and axisTwistRat_self that establish it is a group automorphism of $\mathbb{Q}^\times$ fixing off-axis primes.
Those facts power axisTwistCharacter_off_axis_identity (twist leaves a distinct prime direction fixed up to cross-equality) and the character-to-rational round-trip. In the broader Recognition chain, axis twists probe whether a cost functional can depend on a preferred prime direction; uniqueness of the native J-cost (T5-style) requires that such twists either preserve cost or are ruled out by the composition law and doubled-trace hypotheses. The definition therefore sits under the native-cost uniqueness argument rather than under the forcing chain T0–T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.