canonicalSelectedNativeCost_toRat
plain-language theorem explainer
On every ratio orbit the selected native-cost witness displays as the classical J-cost: $(r+r^{-1})/2-1$, with both sides zero on the unit orbit. Anyone proving native-cost hypotheses, cross-equality to the canonical cost, or the structural ledger identity $F=J$ cites this evaluation lemma. The proof unfolds the selection definition and case-splits on whether the displayed ratio is 1.
Claim. For every ratio orbit $q$, the rational display of the canonically selected native cost at $q$ equals $(r + r^{-1})/2 - 1$, where $r$ is the rational display of $q$. When $r = 1$ both sides are $0$.
background
In the Primitive Recognition Calculus, costs on ratio orbits are maps $F : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ whose rational displays encode recognition cost. The classical J-cost is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced uniquely by the Recognition Composition Law in the T5 step of the unified forcing chain.
The selected witness canonicalSelectedNativeCost is the native-cost candidate chosen in this module: it returns the zero orbit when the display is the unit ratio, and otherwise the orbit-level lift of $J$ (onRatioOrbit). The companion evaluation onRatioOrbit_toRat already identifies that lift with the J formula off the unit.
This lemma is the display-level bridge: it says the selected witness, after .toRat, is pointwise the J formula on every orbit, including the unit branch where both sides collapse to zero.
proof idea
Unfold the definition of the selected witness (an if on whether $q.\mathrm{toRat} = 1$). On the unit branch, rewrite with if_pos, apply RatioOrbit.zero_toRat, substitute $r = 1$, and finish by norm_num (both sides are $0$). Off the unit, rewrite with if_neg and apply the already-proved evaluation onRatioOrbit_toRat, which supplies the J formula directly.
why it matters
This is the evaluation identity that lets the selected witness stand in for canonical $J$ everywhere downstream. It is the first rewrite in canonicalSelectedNativeCost_crossEq_onRatioOrbit (selected witness is crossEq-pointwise the canonical cost), and it discharges the reciprocal and display obligations in canonicalSelectedNativeCost_native_hypotheses and the full zero-calibrated prime-signed strengthened class in canonicalSelectedNativeCost_full_hypotheses.
The structural ledger re-exports it as canonicalSelectedNativeCost_jq: $(F q).\mathrm{toRat} = J(q.\mathrm{toRat})$. The minimality certificate's spiked competitor rclSpikeNativeCost_toRat is proved by the same pattern, comparing against this baseline. Framework-wise it pins T5 J-uniqueness at the native PRC layer: the selected cost is not an abstract placeholder but literally the forced $J$ on displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.