axisTwistRat_ne_zero
plain-language theorem explainer
For any prime base b and nonzero rational x, the b-axis twist of x is nonzero. The twist multiplies x by an integer power of b that inverts twice the b-adic valuation. Anyone assembling ratio characters from axis twists on rational displays needs this nonvanishing. The proof unfolds the definition and multiplies two nonzero factors: x and a nonzero power of the prime b.
Claim. Let $b$ be a prime natural number and let $x\in\mathbb{Q}$ with $x\neq 0$. Then the $b$-axis twist satisfies $x\cdot b^{-2\,v_b(x)}\neq 0$, where $v_b(x)$ is the $b$-adic valuation of $x$.
background
In the Primitive Recognition Calculus, native cost uniqueness compares cost functionals built from ratio characters on rational displays. An axis twist is a base-parameterized map on $\mathbb{Q}$ that inverts the exponent along a single prime axis $b$ and fixes every other prime axis. Explicitly it sends $x$ to $x\cdot b^{-2,v_b(x)}$. For $b=2$ this is the two-adic twist; for $b=3$ the three-adic twist.
The surrounding module packages uniqueness of the native cost under doubled-trace and d'Alembert hypotheses. Nonvanishing of the twist is required before the twisted map can serve as a ratio character (values in the multiplicative group of nonzero rationals).
Upstream, the rational cast of a prime base is already known nonzero (axisTwistRat_base_ne_zero). The product of nonzero factors remains nonzero, which is the arithmetic content used after unfolding.
proof idea
Short term proof after unfolding. Expand the axis twist to the product $x\cdot b^{-2,v_b(x)}$. The first factor is nonzero by hypothesis. The second is an integer power of the rational cast of the prime $b$; that base is nonzero by axisTwistRat_base_ne_zero, and a nonzero base stays nonzero under integer powers (zpow_ne_zero). Finish with the field product rule mul_ne_zero.
why it matters
Supports the construction of ratio characters from axis twists: axisTwistCharacter_ratio_character needs twisted values to land in the nonzero rationals so the PRC ratio-character unit condition holds. That step sits inside native cost uniqueness, where characters built from prime-orbit axis twists are matched to doubled-trace costs. Without nonvanishing the twist could send displays to zero and break the character interface. The lemma is local arithmetic hygiene on rational displays, not a forcing-chain landmark (T5 J-uniqueness through T8), but it keeps the rational side of native cost uniqueness well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.