threeToFiveRebaseCharacter_two_identity
plain-language theorem explainer
The three-to-five rebase character fixes the ratio orbit 2 under cross-multiplication equivalence. Anyone calibrating native PRC cost characters against the doubled-trace or J-cost normalization cites this identity. The proof rewrites cross-equivalence to rational equality and applies the corresponding rational fixed-point fact for 2.
Claim. Let $\chi_{3\to5}$ be the three-to-five rebase character on ratio orbits, and let $2$ denote the ratio orbit with numerator orbit $2$ and denominator $1$. Then $\chi_{3\to5}(2)$ is cross-multiplication equivalent to $2$ (equivalently, their verifier rationals agree).
background
In the Primitive Recognition Calculus, rationals are carried as RatioOrbit displays: a signed integer orbit numerator over a nonzero distinction-nat denominator. Two such displays are related by cross-equivalence when the scaled numerators balance as signed orbits; that relation is exactly equality of the verifier rationals toRat.
The constant ratio orbit two is the display of the integer $2$ (numerator orbit $2$, denominator $1$), so two.toRat = 2. The three-to-five rebase character sends a ratio orbit $q$ to the ratio-orbit lift of a rational map threeToFiveRebaseRat applied to $q.toRat`. It is the character used when rebasing cost data between the three-tick and five-tick presentations inside native cost uniqueness.
Local setting is the PRC native-cost uniqueness development: characters on ratio orbits are turned into costs, then matched against doubled-trace and J-cost structure. Fixing the value $2$ is the calibration anchor for that matching.
proof idea
Term-mode rewrite chain. First replace cross-equivalence by equality of toRat via crossEq_iff_toRat_eq. Unfold the character with threeToFiveRebaseCharacter_toRat and simplify the right-hand side with two_toRat, reducing the goal to the rational identity threeToFiveRebaseRat 2 = 2. Discharge that with the already-proved rational lemma threeToFiveRebaseRat_two.
why it matters
Native cost uniqueness needs characters that preserve the calibration point $2$, so that costFromCharacter agrees with the on-orbit cost at that point. The immediate parent is threeToFiveRebaseCharacter_two_calibrated, which unfolds costFromCharacter and applies orbit congruence to this identity, obtaining cross-equivalence of the character-cost of $2$ with the native on-orbit cost of $2$.
That calibration step sits inside the PRC path toward uniqueness of the native cost functional (the J-cost side of the forcing chain: T5 uniqueness of $J(x)=(x+x^{-1})/2-1$). Without a fixed point at $2$, the doubled-trace d'Alembert and character-trace matching lemmas cannot lock the cost scale. The result is a small but load-bearing identity in that uniqueness spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.