rclSpikeNativeCost_toRat
plain-language theorem explainer
On every rational orbit, the RCL-spike native cost displays as zero at the five and one-fifth points and as the classical J-cost elsewhere. Certificate authors cite this when comparing the spiked witness to the canonical cost or when discharging slim PRC hypotheses without RCL. The proof unfolds the spike definition, splits on the branch, and applies the zero-display and selected-cost J-display lemmas.
Claim. For every rational orbit $q$, writing $r$ for its rational display, the rational display of the RCL-spike native cost at $q$ equals $0$ if $r=5$ or $r=5^{-1}$, and equals $\frac{r+r^{-1}}{2}-1$ otherwise.
background
A ratio orbit is an integer-numerator over nonzero-orbit-denominator display of a rational (K4.7). Its verifier display toRat is the ordinary quotient in $\mathbb{Q}$; the zero orbit displays as $0$.
The Recognition Composition Law forces the native cost $J(x)=\frac{x+x^{-1}}{2}-1$ (T5). The selected native-cost witness already displays as this $J$ formula on every orbit (and as $0$ on the unit branch). The RCL-spike witness is the same selection everywhere except at the $5$ and $5^{-1}$ displays, which are sent to the zero representative.
This module builds minimality certificates for that spiked witness inside the Primitive Recognition Calculus, working over ratio orbits rather than bare rationals.
proof idea
One short case split. Rewrite by the spike definition, then split_ifs on whether the orbit displays as $5$ or $5^{-1}$. On the true branch the spike is the zero orbit, so zero_toRat gives display $0$. On the false branch the spike is the selected native cost, so canonicalSelectedNativeCost_toRat supplies the $J$ formula.
why it matters
This is the display identity that makes the spike usable as a certificate object. Downstream, rclSpikeNativeCost_five_not_canonical uses it (via cross-equality iff equal toRat) to prove the spike differs from the canonical cost at the five-orbit. The companion rclSpikeNativeCost_sans_rcl_hypotheses rewrites reciprocal and related slim-PRC fields through the same identity, so the spike satisfies the PRC package without assuming the full RCL hypotheses.
In the forcing chain this sits under T5 $J$-uniqueness and the RCL functional equation: the spike is the canonical $J$ with a deliberate zero puncture at ${5,5^{-1}}$, isolating those two points as the only places where a competing native cost could deviate while still matching $J$ elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.