axisTwistRat_self
plain-language theorem explainer
For any prime b, the b-axis twist sends the rational b to its reciprocal 1/b. Anyone tracking axis-twist characters or native-cost uniqueness on prime orbits cites this identity. The proof unfolds the twist definition, inserts the self p-adic valuation padicVal_b(b)=1, and reduces the resulting integer power of b to b^{-1}.
Claim. Let $b$ be a prime natural number. The base-$b$ axis twist on rationals, defined by $x \mapsto x\, b^{-2\,v_b(x)}$ where $v_b$ is the $b$-adic valuation on $\mathbb{Q}$, satisfies $\mathrm{twist}_b(b)=b^{-1}$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, rational displays are acted on by axis twists parameterized by a prime base $b$. The twist multiplies $x$ by $b$ raised to $-2$ times the $b$-adic valuation of $x$: it inverts the exponent along the $b$-axis and fixes every other prime axis. Special cases include the two-adic and three-adic twists.
The $b$-adic valuation on $\mathbb{Q}$ is the unique additive valuation with $v_b(b)=1$ and $v_b(p)=0$ for primes $p\neq b$. The lemma that the cast of a prime $b$ is nonzero in $\mathbb{Q}$ is recorded separately so that integer powers of $b$ are well-defined.
Locally the module builds characters and doubled-trace cost functionals that must match the Recognition Composition Law cost $J$. Axis twists supply the reciprocal action on prime directions needed for that matching.
proof idea
Unfold the definition of the axis twist to $b\cdot b^{-2,v_b(b)}$. From primality of $b$ one has $1<b$, so Mathlib's padicValRat.self gives $v_b(b)=1$, and the exponent simplifies to $-2$. Rewrite the leading factor as $b^1$, combine exponents via $zpow_add$ (using that $b\neq 0$ in $\mathbb{Q}$), obtain $b^{-1}$, and finish with $zpow_neg_one$. Pure term-level algebra after one valuation fact.
why it matters
The identity is the on-axis evaluation of the rational twist: twisting the prime itself yields its reciprocal. Downstream, axisTwistCharacter_on_axis_reciprocal lifts this to the character level, proving that the axis-twist character on a prime orbit direction is cross-equal to the reciprocal ratio orbit. That step is part of showing character-trace data match the native cost, which feeds uniqueness of the PRC cost functional against the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Without the self-reciprocal evaluation, the on-axis case of the character comparison would not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.