threeToFiveRebaseRat_one
plain-language theorem explainer
The 3-to-5 rational rebase map fixes the unit: it sends 1 to 1. Anyone building the ratio-character countermodel that swaps the native 3-prime axis for 5 while keeping the 2-axis fixed cites this unit check. The proof is a short unfold plus the fact that the 3-adic valuation of 1 vanishes.
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(1)=1$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, one studies multiplicative characters on positive rationals that could serve as cost calibrations along prime axes. The map threeToFiveRebaseRat is the explicit rational verifier character that multiplies by $(5/3)$ raised to the $3$-adic valuation: it rebases the native $3$-prime axis onto $5$ while leaving the $2$-axis fixed.
Its doc-comment frames it as "the narrow countermodel to two-calibration forcing all prime calibrations": if only two prime axes are fixed, a nontrivial automorphism of the remaining primes can still move the cost. The $3$-adic valuation $v_3(x)$ on $\mathbb{Q}$ is the usual exponent of $3$ in the prime factorization of $x$ (negative for denominators).
The unit value $r(1)=1$ is the first axiom needed to promote this rational map to a full ratio character in the PRC sense.
proof idea
Unfold the definition: the claim is $1\cdot(5/3)^{v_3(1)}=1$. A short norm_num argument with padicValRat.of_int and padicValInt.eq_zero_of_not_dvd shows $v_3(1)=0$. Rewrite and finish by norm_num, since any nonzero base to the power $0$ is $1$.
why it matters
Downstream, threeToFiveRebaseCharacter_ratio_character installs the full PRCRatioCharacter instance for the rebased character; its unit field rewrites through toRat and applies exactly this lemma against RatioOrbit.one_toRat.
In the Recognition foundation stack this is a small but necessary gate on the countermodel side of native-cost uniqueness: it shows that a two-axis calibration need not force every prime calibration, so uniqueness arguments must use the full native cost hypotheses (doubled-trace d'Alembert structure, cross-equation matching) rather than a thin two-prime skeleton. It sits inside the PRC native-cost uniqueness module that underwrites J-cost uniqueness (forcing-chain T5) at the rational-character layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.