threeToFiveRebaseRat_three
plain-language theorem explainer
The rational rebase that replaces the 3-adic axis by a factor of 5 sends the integer 3 to 5. Anyone auditing the two-calibration countermodel in native cost uniqueness cites this evaluation. The proof unfolds the definition, applies the self-valuation identity for the 3-adic valuation on 3, and closes by arithmetic.
Claim. The rational map $x \mapsto x \cdot (5/3)^{v_3(x)}$ evaluates at $x=3$ to $5$, where $v_3$ is the $3$-adic valuation on $\mathbb{Q}$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, rational characters on $\mathbb{Q}$ serve as verifiers for how cost data sit on prime axes. The three-to-five rebase is the map $x \mapsto x \cdot (5/3)^{v_3(x)}$. It multiplies by a pure power of $5/3$ according to the $3$-adic valuation, so it moves mass off the prime-$3$ axis onto prime $5$ while leaving the $2$-axis fixed.
Its stated role is a narrow countermodel: two prime calibrations need not force every prime calibration. The present lemma is the elementary evaluation of that map at the generator $3$ itself. Upstream, the definition of the rebase and the standard identity $v_p(p)=1$ (for prime $p$) are the only inputs.
proof idea
Term-mode proof by unfolding the rebase definition. The key step is the library identity that the $3$-adic valuation of $3$ equals $1$ (via padicValRat.self with the trivial bound $1<3$). After rewriting, the expression collapses to $3\cdot(5/3)^1$, which norm_num reduces to $5$.
why it matters
This evaluation is the arithmetic kernel of threeToFiveRebaseCharacter_three_to_five, which lifts the same fact to the character attached to the three-prime direction and concludes that character sends that direction to $5$. Together they witness that a two-axis calibration (here $2$ fixed, $3$ rebased to $5$) need not determine all prime axes, so native cost uniqueness cannot be forced from two calibrations alone. The result sits in the Foundation layer of the Recognition calculus, upstream of any claim that the native $J$-cost is the unique cost compatible with the full prime lattice. It does not itself invoke the forcing chain T5–T8 or the RCL identity; it is pure rational arithmetic supporting the countermodel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.