threeToFiveRebaseCharacter_not_three_prime_calibrated
plain-language theorem explainer
The three-to-five rebase character fails three-prime calibration: the cost it induces at the three-prime direction is not cross-equal to the native ratio-orbit J-cost there. Used to refute the claim that two-point calibration forces the prime-calibration target. Proof pushes both sides to rational displays and closes by numerical contradiction.
Claim. Let $\chi_{3\to 5}$ be the three-to-five rebase character and $q_3$ the three-prime direction (as ratio orbits). Then the induced cost $J(\chi_{3\to 5}(q_3))$ is not cross-multiplication equivalent to the native PRC cost $J(q_3)=\frac{q_3+q_3^{-1}}{2}-1$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two such displays are identified by cross-multiplication (crossEq), which the library proves equivalent to equality of their rational verifier values.
The native PRC cost on a ratio orbit is the orbit-level J-object $J(q)=((q+q^{-1})/2)-1$. A rational character $\chi$ induces a cost by precomposition: $\mathrm{costFromCharacter}(\chi,q)=J(\chi(q))$. The identity character recovers the native cost; other characters are candidate alternatives in the uniqueness argument.
This module studies which characters are calibrated to the native cost at distinguished directions (here the three-prime direction). The three-to-five rebase character is one such candidate; the claim is that it fails calibration at that direction.
proof idea
Assume cross-equality of the two ratio-orbit costs. Rewrite via the bridge crossEq_iff_toRat_eq, then unfold both sides with costFromCharacter_toRat and onRatioOrbit_toRat. Specialize the character and the direction with threeToFiveRebaseCharacter_three_to_five and threePrimeDirection_toRat, obtaining an equality of concrete rationals. norm_num discharges the contradiction.
why it matters
Immediate parent is PRCTwoCalibrationForcesPrimeCalibrationTarget_refuted, which shows that two-point calibration does not force the prime-calibration target: the three-to-five rebase character is a ratio character that would have to be prime-calibrated under that hypothesis, and this lemma supplies the concrete failure.
In the broader Recognition chain this sits under native-cost uniqueness for the PRC J-object, the discrete precursor of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). Ruling out rebased characters keeps the cost pinned to the identity character on the ratio-orbit lattice, before the analytic uniqueness bridge.
No open scaffold: the claim is fully proved and only used as a negative witness inside the two-calibration refutation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.