threeToFiveRebaseCharacter_three_to_five
plain-language theorem explainer
Applying the three-to-five rebase character to the canonical prime-3 ratio orbit yields a ratio orbit whose rational display is exactly 5. Native-cost uniqueness arguments cite this as the concrete evaluation of that character on the first mixed-composite test direction. The proof is a two-rewrite transport to the already-proved rational identity threeToFiveRebaseRat 3 = 5.
Claim. Let $q_3$ be the canonical prime-3 ratio orbit. If $\chi_{3\to 5}$ is the character that rebases a ratio orbit by the three-to-five rational map on its verifier display, then $(\chi_{3\to 5}(q_3)).\mathrm{toRat} = 5$.
background
In the Primitive Recognition Calculus, ratio orbits are the discrete carriers of multiplicative comparison data. The verifier map toRat sends a ratio orbit to a rational by numerator/denominator transport (spec tag A5: internal equality is cross-multiplication). The canonical non-two prime direction is the prime-3 orbit, with display value 3.
The three-to-five rebase character lifts a rational map threeToFiveRebaseRat back to ratio orbits: evaluate the orbit, apply the rational rebase (built from the 3-adic valuation), and re-embed. Upstream, threeToFiveRebaseRat 3 = 5 is already proved by computing padicValRat 3 (3) = 1 and simplifying the rebase formula.
This module develops native-cost uniqueness: which multiplicative characters can match the native cost on prime directions. Concrete evaluations such as this one feed calibration and non-calibration lemmas for mixed-composite tests.
proof idea
Term-mode transport. Rewrite the left-hand side by threeToFiveRebaseCharacter_toRat, which unwraps the character to threeToFiveRebaseRat on the orbit's rational display. Then rewrite threePrimeDirection.toRat to 3 via the simp lemma threePrimeDirection_toRat. The goal is exactly threeToFiveRebaseRat 3 = 5, discharged by threeToFiveRebaseRat_three.
why it matters
Feeds the immediate parent threeToFiveRebaseCharacter_not_three_prime_calibrated, which shows that the cost built from this rebase character fails cross-equality with the native on-orbit cost at the prime-3 direction. That non-calibration step is part of the PRC native-cost uniqueness chain: only characters compatible with the native J-cost (and ultimately the Recognition Composition Law) survive on prime directions.
In the broader forcing picture, native cost uniqueness supports the identification of the unique cost functional J (T5: $J(x)=(x+x^{-1})/2-1$) before phi and the eight-tick structure are forced. This lemma is a small but concrete arithmetic pin in that uniqueness argument, not a physics endpoint by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.