canonicalSelectedNativeCost_crossEq_onRatioOrbit
plain-language theorem explainer
On every ratio orbit the canonically selected native cost agrees with the canonical J-cost under cross-multiplication equivalence. Cost-selection and minimality packages cite this to certify that the selected witness is non-vacuous and lands on J. The proof is a three-step rewrite through rational displays.
Claim. For every ratio orbit $q$, the canonically selected native cost of $q$ is cross-equivalent to the canonical cost on $q$: writing $\mathrm{crossEq}$ for the internal cross-multiplication relation on ratio orbits, $\mathrm{crossEq}(C_{\mathrm{sel}}(q),\,J_{\mathrm{orb}}(q))$ holds, equivalently their rational displays agree.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator (the internal rational display). Two orbits are related by crossEq when cross-multiplication balances as signed orbits; by K4.10 this is equivalent to equality of the verifier rationals (crossEq_iff_toRat_eq).
The canonical cost on ratio orbits is the orbit-level J-cost (the unique cost forced by the Recognition Composition Law and T5: $J(x)=(x+x^{-1})/2-1$). The selected native cost is the witness chosen for the native cost-selection package: a map on ratio orbits meant to satisfy the native-cost hypotheses and coincide with that J-cost.
This lemma sits in the native-cost selection module, after uniqueness infrastructure and the public spine. It only needs the two toRat evaluations of the selected witness and of the orbit J-cost.
proof idea
Short rewrite proof. First replace crossEq by equality of rational displays via crossEq_iff_toRat_eq. Then rewrite the left display with canonicalSelectedNativeCost_toRat and the right with onRatioOrbit_toRat. Both sides reduce to the same rational, so the goal closes.
why it matters
Native cost selection must exhibit a concrete witness that meets the hypothesis class and matches the unique J-cost; otherwise the selection package is vacuous. This pointwise crossEq identity is exactly that matching clause.
Downstream, costSelectionPackageNative_holds and costSelectionPackageNativeSlim_holds pack it into the non_vacuous field alongside the full or slim hypothesis bundles for canonicalSelectedNativeCost. The same fact feeds canonicalSelectedNativeCost_native_hypotheses and canonicalSelectedNativeCost_full_hypotheses, and appears in the RCL-spike certificate path.
In the forcing chain this locks the selected ledger cost onto T5 J-uniqueness at the PRC rational layer, before minimality and uniqueness targets discharge the rest of the native package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.