threeToFiveRebaseRat_inv
plain-language theorem explainer
The rational three-to-five rebase map sends multiplicative inverses to inverses on all of Q. Anyone verifying that this map is a ratio character (or building the corresponding PRC character) cites this identity. The proof is a short zero/nonzero case split using the 3-adic valuation rule v_3(x^{-1})=-v_3(x) and field simplification.
Claim. Let $r:\mathbb{Q}\to\mathbb{Q}$ be the three-to-five rebase $r(x)=x\cdot(5/3)^{v_3(x)}$, where $v_3$ is the $3$-adic valuation on rationals. Then for every $x\in\mathbb{Q}$, $r(x^{-1})=r(x)^{-1}$.
background
In the primitive recognition calculus, native cost uniqueness is probed by rational characters on ratio orbits. The three-to-five rebase is the explicit map $r(x)=x\cdot(5/3)^{v_3(x)}$. It moves the native prime-$3$ axis onto prime $5$ while leaving the $2$-axis fixed. The module presents it as a narrow countermodel: two-calibration need not force calibration at every prime.
A ratio character must respect the group law on $\mathbb{Q}^\times$, so inversion is a basic check. The $3$-adic valuation satisfies $v_3(x^{-1})=-v_3(x)$ off zero, which is the algebraic engine behind the identity. The zero case is handled separately because valuation and inversion both need a convention there.
Upstream, the definition of the rebase is local to this uniqueness module; the only external name in the dependency list is a generic inverse-closure fact from the recognition core, not used as the main step here.
proof idea
Unfold the definition of the rebase. Split on whether $x=0$. If $x=0$, both sides simplify directly. If $x\neq 0$, rewrite with the identity $v_3(x^{-1})=-v_3(x)$ from padicValRat.inv, note that $(5/3)^{v_3(x)}\neq 0$, convert the negative exponent via zpow_neg, and finish by field_simp.
why it matters
This is a structural lemma for the three-to-five rebase character. Downstream, threeToFiveRebaseCharacter_ratio_character packages the rebase into a PRCRatioCharacter, and the unit and ratio axioms of that instance rely on inversion and related rational identities of this form.
In the Recognition foundation stack, native cost uniqueness and J-cost forcing (T5, RCL) need tight control of which multiplicative characters can arise from calibration data. The rebase is the designed countermodel showing that calibrating two primes does not automatically calibrate all primes. Proving it preserves inversion is a necessary step before it can sit inside the ratio-character interface used by doubled-trace and cost-matching arguments later in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.