jcost_eq_forces_same_or_reciprocal
plain-language theorem explainer
Equal native J-cost displays on two nonzero ratio orbits force the orbits to be cross-equivalent or reciprocal. Calibration and uniqueness arguments for PRC cost characters cite this when collapsing same-cost pairs. The proof rewrites to rationals, extracts x+1/x equality, and factors (x-y)(xy-1)=0.
Claim. Let $a,b$ be ratio orbits with nonzero rational displays. If the native cost orbits of $a$ and $b$ are equal under cross-multiplication, then either $a$ is cross-equivalent to $b$, or $a$ is cross-equivalent to the reciprocal of $b$.
background
In the Primitive Recognition Calculus, ratios live as RatioOrbit data (numerator/denominator signed orbits). Cross-equivalence is the internal rational equality: two orbits match when cross-multiplication balances as signed orbits (K4.10), and this agrees with equality of verifier rationals toRat.
The native cost display on a ratio is the orbit-level avatar of the T5 J-cost $J(x)=(x+x^{-1})/2-1$. Equality of those displays is again stated by cross-equivalence. Classically $J(x)=J(y)$ iff $y=x$ or $y=x^{-1}$ on $\mathbb{R}_{\neq 0}$; this lemma is that dichotomy inside PRC rationals.
The module develops uniqueness and calibration of native cost characters. Upstream arithmetic supplies zero-divisor freeness and unit laws used when clearing denominators on $\mathbb{Q}$.
proof idea
Rewrite the cost-equality hypothesis via crossEq_iff_toRat_eq and the cost-display evaluation lemmas to obtain the rational identity $a+ a^{-1}=b+b^{-1}$.
Multiply through by $ab$ and rearrange to $(a-b)(ab-1)=0$. Split on mul_eq_zero. The first factor gives $a=b$ as rationals, hence cross-equivalence. The second gives $ab=1$; a short calculation with field_simp and the unit laws shows $a=b^{-1}$, i.e. cross-equivalence of $a$ with the reciprocal orbit of $b$.
All steps are elementary rational algebra after the display rewrites; no analysis beyond $\mathbb{Q}$.
why it matters
Native cost uniqueness needs that equal J-values do not spawn independent orientations: same cost means same ratio or its reciprocal. Downstream, character_pair_two_calibration_forces_prime_calibration uses this transport so that pair-product consistency plus the base two-point calibration force prime-axis calibration ("the all-prime family is not independent data"). The sibling discharge PRCPrimeCalibrationForcesLocalPrimeOrientationTarget_proved likewise case-splits local prime orientation against this dichotomy.
Framework-wise this is the PRC-rational shadow of T5 J-uniqueness and the Recognition Composition Law symmetry $J(x)=J(x^{-1})$. It closes a concrete gap in the native-cost uniqueness ledger rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.