axisTwistRat_base_ne_zero
plain-language theorem explainer
A prime natural number remains nonzero when cast to the rationals. Anyone building multiplicative characters or p-adic twists on Q cites this as the base nonvanishing fact. The proof is a one-line wrapper: primality gives positivity, hence the cast cannot be zero.
Claim. If $b\in\mathbb{N}$ is prime, then the image of $b$ in $\mathbb{Q}$ satisfies $b\neq 0$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, one constructs an axis twist on rationals relative to a fixed prime base $b$. The map multiplies a rational by a power of $b$ whose exponent is built from the $b$-adic valuation, so every algebraic identity for the twist needs $b\neq 0$ in $\mathbb{Q}$.
The ambient module studies uniqueness of native cost functionals via ratio characters, doubled traces, and d'Alembert-type functional equations. Nonvanishing of the prime base is the elementary gate that lets inverses, products, and self-evaluations of the twist stay inside the multiplicative group of nonzero rationals.
Upstream positivity results for monotone multiplicative maps (on naturals and on structural ledgers) already guarantee that such maps stay positive above the unit; the present lemma is the corresponding cast-level fact for the prime itself.
proof idea
One-line wrapper. Primality of $b$ supplies $0<b$ via the standard positivity of primes. Nat.cast_ne_zero then converts that strict inequality into the statement that the cast $(b:\mathbb{Q})$ is nonzero. No further case analysis or valuation arithmetic is required.
why it matters
The lemma is the nonvanishing seed for the whole axisTwistRat algebra inside native-cost uniqueness. Downstream it is invoked by the multiplicative law, the inversion law, the general nonvanishing statement for nonzero inputs, and the self-evaluation identity that sends the base to its reciprocal. Those four facts together make the twist a group homomorphism on $\mathbb{Q}^\times$, which is the algebraic input needed when matching ratio characters to native cost and closing the doubled-trace d'Alembert route. Within the broader Recognition forcing chain this sits in the foundation layer that isolates the unique cost shape before T5 J-uniqueness and the phi fixed point are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.