threeToFiveRebaseRat_two
plain-language theorem explainer
The rational 3-to-5 rebase map fixes the integer 2: evaluating it at 2 returns 2. Anyone building the narrow countermodel that rebases the prime-3 axis onto 5 while leaving the 2-axis alone cites this identity. The proof unfolds the definition, inserts the fact that the 3-adic valuation of 2 is zero, and finishes by arithmetic.
Claim. Let $r:\mathbb{Q}\to\mathbb{Q}$ be the map $r(x)=x\cdot(5/3)^{v_3(x)}$, where $v_3$ is the $3$-adic valuation on rationals. Then $r(2)=2$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, rational characters act on ratio orbits and must be checked against the doubled-trace / d'Alembert cost structure. The map threeToFiveRebaseRat is the explicit verifier character that multiplies a rational by $(5/3)$ raised to its $3$-adic valuation. Its stated role is to rebase the native prime-$3$ axis onto $5$ while fixing the prime-$2$ axis, supplying a narrow countermodel to the claim that two-point calibration forces every prime calibration.
The only arithmetic input needed here is that $v_3(2)=0$: the integer $2$ is not divisible by $3$, so the $3$-adic valuation vanishes. That fact is recorded as the sibling lemma padicValRat_three_two_eq_zero. With the exponent zero, the rebase factor collapses to $1$ and the map acts as the identity at $2$.
proof idea
Term-mode proof in three steps. Unfold the definition of the rebase map to expose $2\cdot(5/3)^{v_3(2)}$. Rewrite the exponent via padicValRat_three_two_eq_zero, which gives $v_3(2)=0$. Then norm_num evaluates $(5/3)^0=1$ and concludes $2\cdot 1=2$.
why it matters
This identity is the rational core of the character-level statement that the 3-to-5 rebase character is the identity on the generator two. The immediate parent is threeToFiveRebaseCharacter_two_identity, which reduces the ratio-orbit cross-equation for that character at two to the present rational equality via crossEq_iff_toRat_eq and the toRat lemmas.
In the broader PRC native-cost uniqueness argument, the rebase character is the narrow countermodel showing that fixing the $2$-axis (two-calibration) does not force every prime calibration: the $3$-axis can still be moved to $5$. Establishing that $2$ itself is fixed is the first consistency check that the countermodel really preserves the $2$-axis. It sits inside the Foundation layer that feeds J-cost uniqueness and the forcing chain, rather than a numbered T-step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.