threeToFiveRebaseCharacter_ratio_character
plain-language theorem explainer
The three-to-five rebase map on ratio orbits is a genuine ratio character: it fixes the unit, preserves multiplication and inversion up to cross-equivalence, is invariant under normalization, and never sends a nonzero orbit to zero. Anyone building or refuting uniqueness claims for PRC cost factorizations cites it. The proof reduces each structure field through the toRat display and applies the corresponding rational rebase lemmas.
Claim. The three-to-five rebase map $\chi_{3\to 5}$ on ratio orbits is a PRC ratio character: $\chi_{3\to 5}(1)\sim 1$; $\chi_{3\to 5}(xy)\sim\chi_{3\to 5}(x)\,\chi_{3\to 5}(y)$; $\chi_{3\to 5}(x^{-1})\sim\chi_{3\to 5}(x)^{-1}$; $\chi_{3\to 5}$ is invariant under ratio normalization; and $\chi_{3\to 5}$ sends nonzero orbits to nonzero orbits (all equivalences are cross-equivalence of ratio orbits).
background
In the Primitive Recognition Calculus, costs factor in a d'Alembert style through ratio characters. A ratio character is a map $\chi$ on ratio orbits that fixes the unit, is multiplicative and reciprocal up to cross-equivalence, respects normalization, and preserves nonzeroness. Cross-equivalence is the quotient-native equality on orbits: two orbits are cross-equivalent exactly when their rational displays agree (crossEq_iff_toRat_eq).
Ratio orbits carry a multiplicative monoid structure with unit, multiplication, and reciprocal, all compatible with the rational display (one_toRat, mul_toRat, recip_toRat). The three-to-five rebase character is the orbit-level lift of a rational map that rewrites base-3 place values into base-5 place values; the rational lemmas threeToFiveRebaseRat_one, _mul, _inv, and _ne_zero already establish the character axioms at the $\mathbb{Q}$ level.
This module sits in the native-cost uniqueness development: characters feed doubled-trace d'Alembert factorizations and calibration targets for the unique PRC cost.
proof idea
Five independent structure fields, each discharged by the same pattern. For unit, multiplicative, reciprocal, and normalized_invariant: rewrite the goal with crossEq_iff_toRat_eq, push threeToFiveRebaseCharacter_toRat through the orbit operations via one_toRat / mul_toRat / recip_toRat / normalizeRatio_toRat, then apply the matching rational lemma (threeToFiveRebaseRat_one, _mul, _inv). For nonzero_preserving: reduce by threeToFiveRebaseCharacter_toRat and apply threeToFiveRebaseRat_ne_zero. No global induction; pure transport along the toRat display.
why it matters
Feeds the refutation PRCTwoCalibrationForcesPrimeCalibrationTarget_refuted: the three-to-five rebase character is a concrete ratio character that is not three-prime calibrated, so two calibration conditions do not force the prime calibration target. That blocks an over-strong uniqueness route for native PRC costs and forces the uniqueness argument to use the full doubled-trace / d'Alembert package rather than a short calibration shortcut.
In the broader Recognition chain this sits under cost uniqueness for the J-cost forced at T5 ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. A wrong character class would pollute the factorization that pins the native cost; exhibiting a non-prime rebase character that still satisfies the ratio-character axioms keeps the uniqueness hypotheses honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.