threeToFiveRebaseCharacter_toRat
plain-language theorem explainer
Transport lemma: the orbit-level 3→5 rebase character, after conversion to ℚ, equals the rational 3→5 rebase of the orbit's rational value. Cited when checking that the rebase is a ratio character, fixes the 2-axis, and sends the 3-prime direction to 5. Proof unfolds the character definition and applies the round-trip identity for ratioOrbitOfRat.
Claim. For every rational orbit $q$, converting the three-to-five rebase character of $q$ back to a rational yields the same value as applying the rational three-to-five rebase map to the rational display of $q$: $(\mathrm{rebase}_{3\to 5}(q))^{\mathbb{Q}} = \mathrm{rebase}_{3\to 5}^{\mathbb{Q}}(q^{\mathbb{Q}})$.
background
In the primitive recognition calculus, a RatioOrbit is a display of a rational as a signed-orbit numerator over a nonzero distinction-nat denominator. The map toRat is the verifier transport of that display into $\mathbb{Q}$ (spec tag A5: internal equality is cross-multiplication).
The rational map threeToFiveRebaseRat multiplies $x$ by $(5/3)^{v_3(x)}$, rebasing the native prime-3 axis onto 5 while leaving the 2-axis fixed. It is documented as the narrow countermodel to the claim that two-calibration forces all prime calibrations. The orbit-level character is defined by transporting through $\mathbb{Q}$: apply toRat, rebase, then rebuild an orbit via ratioOrbitOfRat.
The upstream identity ratioOrbitOfRat_toRat states that rebuilding an orbit from a rational and converting back recovers the original rational. That round-trip is the only nontrivial input here.
proof idea
One-line reduction. Unfold threeToFiveRebaseCharacter, which is definitionally ratioOrbitOfRat (threeToFiveRebaseRat q.toRat). The goal becomes (ratioOrbitOfRat _).toRat = _, discharged by ratioOrbitOfRat_toRat.
why it matters
This transport is the bridge from the rational countermodel to the orbit-level character interface. Three immediate parents use it: threeToFiveRebaseCharacter_ratio_character (the rebase is a PRCRatioCharacter, via unit and cross-equality through toRat), threeToFiveRebaseCharacter_two_identity (the 2-axis is fixed), and threeToFiveRebaseCharacter_three_to_five (the 3-prime direction lands on 5).
In the native-cost uniqueness thread, the point is negative: calibrating only the 2-axis does not force the full prime character of the cost. The 3→5 rebase is a concrete ratio character that agrees on 2 yet moves 3, so uniqueness arguments must impose more than two-point calibration. The lemma itself is pure transport; the framework content lives in those parent character theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.