threeToFiveRebaseCharacter
plain-language theorem explainer
Defines the ratio-orbit character that multiplies each rational by (5/3) raised to its 3-adic valuation, then lifts back to a ratio orbit. It is the explicit countermodel showing two-calibration need not force every prime calibration. Construction is a one-line section–retract sandwich through verifier rationals.
Claim. The three-to-five rebase character sends each rational orbit $q$ to the rational orbit whose verifier rational is $q_{\mathbb{Q}}\cdot(5/3)^{v_3(q_{\mathbb{Q}})}$, where $v_3$ is the $3$-adic valuation on $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). The map toRat displays it as an ordinary rational by integer division; the reverse section ratioOrbitOfRat rebuilds a ratio orbit from a classical rational so that classical countermodels can be tested against the character interface.
The underlying rational map multiplies $x$ by $(5/3)^{v_3(x)}$. It therefore fixes every power of $2$ (and the unit $1$) while sending the native three-prime direction to five. The present definition merely packages that rational map as an endomorphism of ratio orbits via the section–retract pair.
The local module studies uniqueness of native cost characters under calibration hypotheses. This character is the narrow countermodel to the claim that calibrating the two-axis already forces every prime axis.
proof idea
One-line definitional wrapper: convert the input orbit to a rational, apply the already-defined three-to-five rational rebase, and re-embed via the verifier section ratioOrbitOfRat. No further proof obligations live on the definition itself; transport lemmas such as the companion toRat identity discharge later.
why it matters
This character is the concrete witness used to refute two-calibration forcing all prime calibrations. Downstream, it is shown to be a genuine ratio character, to fix the two-axis (two-calibrated and two-identity), to send the three-prime direction to five, and therefore not to be three-prime calibrated. Those facts assemble into the refutation theorem that the target statement "two-calibration forces prime calibration" is false.
In the Recognition forcing chain the native cost is forced to the unique J-cost (T5) with self-similar scale $\varphi$ (T6). The present countermodel clarifies that uniqueness cannot be obtained from two-axis calibration alone; full prime-axis (or equivalent) hypotheses are required before the native cost is pinned down. It therefore delimits the strength of calibration hypotheses inside PRC native-cost uniqueness rather than advancing a positive uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.