axisTwistRat_one
plain-language theorem explainer
For every prime base b, the rational axis twist fixes the unit 1. Ratio-character and native-cost uniqueness arguments cite this as the identity case of the twist. The proof unfolds the definition, uses that the b-adic valuation of 1 vanishes, and reduces by arithmetic.
Claim. Let $b$ be a prime natural number. The base-$b$ axis twist on rationals sends $1$ to itself: $1 \cdot b^{-2\,v_b(1)} = 1$, where $v_b$ is the $b$-adic valuation on $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, rational displays carry a multiplicative cost structure built from prime-axis data. The axis twist for a fixed prime base $b$ multiplies a rational $x$ by $b$ raised to $-2$ times the $b$-adic valuation of $x$. That operation inverts the exponent along the $b$-axis and leaves every other prime axis fixed. Special cases recover the two-adic and three-adic twists.
The module develops uniqueness of the native recognition cost from ratio-character and doubled-trace hypotheses. Axis twists appear as candidate automorphisms that must preserve the ratio-character axioms if the cost is to be unique. The unit $1$ is the multiplicative identity of the display group, so any such twist is forced to fix it before character axioms can be checked.
Upstream, axisTwistRat is the explicit map $x \mapsto x, b^{-2 v_b(x)}$. The only external fact needed here is the standard valuation identity $v_b(1)=0$.
proof idea
Unfold the definition of the axis twist. Rewrite with the lemma that the $b$-adic valuation of $1$ is zero. The remaining power is $b^{0}=1$, so the product collapses to $1$ by elementary arithmetic (norm_num).
why it matters
This identity is the base case for showing that the character induced by an axis twist remains a PRC ratio character. Downstream, axisTwistCharacter_ratio_character invokes it (under a prime-orbit hypothesis on the distinction) to verify the unit axiom of the twisted character. That step sits inside the native-cost uniqueness development: admissible twists must preserve the ratio-character interface before cost-from-character reconstruction can be unique. In the broader Recognition forcing chain the native cost is the J-cost fixed by T5 and the Recognition Composition Law; fixing the unit under axis twists keeps those algebraic constraints intact on rational displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.