threeToFiveRebaseRat_mul
plain-language theorem explainer
Multiplicativity of the rational rebase that sends the 3-adic axis to 5 while fixing the 2-axis: f(xy)=f(x)f(y) on Q. Cited when building ratio characters or the narrow countermodel that two prime calibrations need not force all others. Proof is zero-case analysis plus the p-adic product formula and additivity of integer powers.
Claim. Let $f:\mathbb{Q}\to\mathbb{Q}$ be $f(x)=x\cdot(5/3)^{v_3(x)}$, where $v_3$ is the $3$-adic valuation on rationals (with the usual convention at $0$). Then for all $x,y\in\mathbb{Q}$, $f(xy)=f(x)f(y)$.
background
In the primitive recognition calculus, native cost uniqueness asks how much prime-axis calibration is forced once a cost functional is fixed on ratio orbits. The three-to-five rebase is a rational verifier character: it multiplies $x$ by $(5/3)$ raised to the $3$-adic valuation of $x$, so the $3$-axis is rewritten as a $5$-axis while the $2$-axis is left alone. Its doc-comment calls it "the narrow countermodel to two-calibration forcing all prime calibrations."
The $3$-adic valuation $v_3$ on $\mathbb{Q}$ is multiplicative on nonzero products, and the integer power map $a\mapsto a^k$ (for fixed nonzero base $a$) turns addition of exponents into multiplication. Multiplicativity of the full rebase is the algebraic fact needed before one can promote it to a ratio character in the PRC sense.
proof idea
Unfold the definition $f(x)=x\cdot(5/3)^{v_3(x)}$. Split on $x=0$ and $y=0$; both sides vanish by simplification. On the nonzero branch, rewrite $v_3(xy)=v_3(x)+v_3(y)$ via the standard product formula for rational $p$-adic valuations, then apply additivity of integer powers at the nonzero base $5/3$, and finish by ring normalization.
why it matters
This lemma is the multiplicative step that lets the three-to-five rebase become a PRC ratio character. Downstream, threeToFiveRebaseCharacter_ratio_character installs the ratio-character structure, using the unit case together with this product law. In the native-cost uniqueness thread, that character is the explicit countermodel showing that calibrating two prime axes need not force every prime calibration: the 3-axis can be rebased onto 5 while the 2-axis stays fixed. It sits in the foundation layer that polices how rigidly recognition costs determine arithmetic structure, short of the full T5 J-uniqueness and RCL forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.