threeToFiveRebaseRat
plain-language theorem explainer
Defines the rational map that multiplies a nonzero rational by (5/3) raised to its 3-adic valuation, thereby swapping the prime-3 factor for a matching power of 5 while leaving the 2-adic content untouched. Cost-uniqueness and character-calibration arguments cite it as the explicit two-axis countermodel: calibrating only 2 and 3 does not force the 5-axis. The body is a one-line arithmetic formula.
Claim. For $x\in\mathbb{Q}$, set $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$). The map replaces every factor of $3$ in the prime factorization of $x$ by a factor of $5$, and fixes the $2$-adic content.
background
In the Primitive Recognition Calculus, native cost uniqueness is studied through multiplicative characters on ratio orbits: rational points modulo the recognition scaling that feeds the J-cost $J(x)=(x+x^{-1})/2-1$. A character is determined by how it acts on prime axes; the native story privileges the primes $2$ and $3$ that appear in the eight-tick and ternary structure of the forcing chain.
The present map is the elementary rational witness that two-axis calibration is insufficient. Writing $v_3(x)$ for the $3$-adic valuation, one multiplies $x$ by $(5/3)^{v_3(x)}$. Every power of $3$ is rewritten as the same power of $5$, while powers of $2$ (and all other primes) are left alone. The construction lives in the PRC native-cost uniqueness module, which builds cost functionals from characters and doubled-trace D'Alembert identities.
Downstream lemmas immediately record that the map is a group homomorphism on $\mathbb{Q}^\times$, sends $1$ to $1$, never hits zero on nonzero input, and intertwines with inversion.
proof idea
Pure definition: the body is the single arithmetic expression $x\cdot((5:\mathbb{Q})/3)^{\mathrm{padicValRat},3,x}$. No tactics or lemmas are invoked at the definition site. Subsequent theorems unfold the definition and apply standard facts about $p$-adic valuations (multiplicativity, behaviour under inversion, vanishing on units coprime to $3$).
why it matters
The map is the narrow countermodel advertised in the module: calibrating the native cost character only on the primes $2$ and $3$ does not force the calibration on $5$. It is lifted to ratio orbits as the character threeToFiveRebaseCharacter, and the companion lemmas (_mul, _inv, _ne_zero, _one, _two, _three, _toRat) equip that character with the algebraic properties needed for cost-from-character constructions.
In the broader Recognition framework this sits inside the foundation layer that isolates which data uniquely determine the J-cost before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick) is applied. It shows that uniqueness proofs must either calibrate every prime axis or invoke an additional structural hypothesis (e.g. a global D'Alembert or cross-equation constraint) rather than two-point matching alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.