threeToFiveRebaseRat_ne_zero
plain-language theorem explainer
If a nonzero rational is rebased by replacing the 3-adic valuation factor with a 5/3 power, the result stays nonzero. Anyone building the three-to-five countermodel character (or proving it is a ratio character) cites this. The proof unfolds the rebase map and multiplies two nonzero rationals, using that integer powers of 5/3 never vanish.
Claim. For every rational $x \neq 0$, the three-to-five rebase $x \cdot (5/3)^{v_3(x)}$ is nonzero, where $v_3$ is the $3$-adic valuation on $\mathbb{Q}$.
background
In the primitive recognition calculus, ratio characters are maps on rational orbit data that preserve the multiplicative structure used to match native cost. The three-to-five rebase is the explicit rational map $x \mapsto x \cdot (5/3)^{v_3(x)}$. It leaves the $2$-axis fixed and swaps the native prime-$3$ calibration for a prime-$5$ factor. The module presents it as a narrow countermodel: two-axis calibration need not force every prime calibration.
Non-vanishing is a basic sanity condition for any such character. Upstream orbit arithmetic already records that products of nonzero orbit positions stay nonzero; here the same idea is applied on $\mathbb{Q}$ after unfolding the rebase formula. The $3$-adic valuation $v_3(x)$ is an integer, so the power $(5/3)^{v_3(x)}$ is a well-defined nonzero rational whenever the base $5/3$ is nonzero.
proof idea
Unfold the definition to $x \cdot (5/3)^{v_3(x)}$. Check $5/3 \neq 0$ by norm_num. Integer powers of a nonzero rational stay nonzero (zpow_ne_zero), so the second factor is nonzero. Conclude with rational mul_ne_zero from $x \neq 0$ and that power.
why it matters
The lemma is a local gate for the three-to-five countermodel inside native-cost uniqueness. Downstream, threeToFiveRebaseCharacter_ratio_character installs the rebased map as a PRCRatioCharacter; its unit clause and related ratio identities need the image of nonzero rationals to stay nonzero. Without this fact the character package cannot even state multiplicative nondegeneracy.
In the broader Recognition stack this sits in foundation work on which cost functionals are forced by calibration data, not in the T5–T8 forcing chain itself. It supports the negative claim that two-prime calibration does not pin every prime axis, sharpening what uniqueness theorems must assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.