threeToFiveRebaseCharacter_two_calibrated
plain-language theorem explainer
At the ratio orbit 2, the cost built from the three-to-five rebase character agrees with the native PRC J-cost under cross-multiplication equality. Anyone checking calibration of rational characters against J at the integer 2 would cite this. The proof unfolds the character-cost definition and applies J-congruence under cross-equality, using that the rebase character fixes 2.
Claim. Let $\chi$ be the three-to-five rebase character on ratio orbits, and let $J$ be the PRC rational cost $J(q)=((q+q^{-1})/2)-1$. Then the character-generated cost $J(\chi(2))$ is cross-equivalent (via balanced scaled numerators and denominators) to the native cost $J(2)$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed numerator orbit over a nonzero distinction-nat denominator. Equality of two such displays is internal cross-multiplication equality: the scaled products of num and den balance as signed orbits (K4.10), not a real-field identity.
The native PRC J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$, built from orbit add, mul, recip, and half. A rational character $\chi$ generates a cost by post-composing with $J$: $\mathrm{cost}_\chi(q)=J(\chi(q))$. The canonical cost is the identity-character case.
The three-to-five rebase character is one non-identity character under study in native cost uniqueness. Two-calibration means that character-generated cost matches native $J$ at the ratio orbit $2$. Congruence of $J$ under cross-equality is already available upstream.
proof idea
Term-mode, two steps. Unfold the definition of cost-from-character so the goal is cross-equality of $J(\chi(2))$ with $J(2)$. Apply the congruence theorem for $J$ under cross-equality, feeding the prior identity that the three-to-five rebase character fixes the ratio orbit $2$ up to cross-equality. No further arithmetic is needed.
why it matters
This pins two-calibration for the three-to-five rebase character: at $2$, character-cost and native $J$ agree. Downstream it is the calibration hypothesis fed into the refutation that two-calibration forces the prime-calibration target: the parent theorem shows that claim is false by exhibiting this character as two-calibrated yet not three-prime-calibrated.
In the broader Recognition stack this sits inside native uniqueness of the PRC cost, the discrete precursor to T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). It separates weak calibration at a single integer point from stronger prime-calibration demands, so uniqueness arguments cannot silently upgrade two-calibration to a rigid prime target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.