padicValRat_three_two_eq_zero

In the Primitive Recognition Calculus native-cost uniqueness development, rational rebase maps adjust denominators and numerators by powers of fixed primes (here 3 versus 5) so that cost characters and doubled-trace values can be compared on a common scale. The $p$-adic valuation $v_p(q)$ of a nonzero rational $q$ is the unique integer exponent of the prime $p$ in the prime factorization of $q$ (negative when $p$ divides the denominator).

For the integer $2$, the only prime factor is $2$ itself. Hence $v_3(2)=0$ already at the integer level, and the same holds after viewing $2$ as a rational. This elementary arithmetic fact is recorded so that later lemmas can rewrite rebase expressions without introducing spurious powers of $3$.

Cast $2:\mathbb{Q}$ back to the integer $2$, apply the library identity that $p$-adic valuation on rationals agrees with the integer valuation on integer casts, then invoke the criterion that $v_p(n)=0$ whenever $p$ does not divide $n$. The non-divisibility $3\nmid 2$ is discharged by norm_num. A final exact_mod_cast returns the integer equality to the rational statement.

Feeds threeToFiveRebaseRat_two, which proves that the three-to-five rational rebase fixes the integer $2$. That identity is a local arithmetic step inside the native-cost uniqueness chain: cost characters and doubled-trace d'Alembert data must remain consistent under prime-base changes when comparing candidate cost functionals. The result itself is pure number theory; its place in Recognition Science is only as scaffolding for the uniqueness argument that isolates the J-cost (and ultimately the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) among native recognition costs.