rclSpikeNativeCost
plain-language theorem explainer
The RCL-spike native cost equals the canonical J-cost on every rational orbit except the displays of 5 and 1/5, which it forces to the zero representative. Uniqueness and minimality arguments cite it as a counterexample when the Recognition Composition Law is omitted. It is a one-branch conditional on the rational display of the input orbit.
Claim. For a rational orbit $q$, define the RCL-spike native cost by sending $q$ to the zero orbit whenever its rational display equals $5$ or $5^{-1}$, and otherwise returning the canonical selected native cost of $q$ (the $J$-cost with the unit orbit mapped to zero).
background
A ratio orbit is an integer-numerator over nonzero-denominator display of a rational (K4.7). The verifier map toRat recovers the ordinary rational by integer division; equality of displays is cross-multiplication.
The canonical selected native cost is the $J$-cost $J(x)=(x+x^{-1})/2-1$ on ratio orbits, with the unit orbit forced to the literal zero representative. It is the non-vacuity witness for the zero-calibrated prime-signed strengthened hypothesis class.
This module builds certificates that native-cost uniqueness fails unless the Recognition Composition Law (RCL) is kept among the hypotheses. The spike is the explicit witness used for that necessity argument.
proof idea
Plain definition by cases: if the rational display of the input equals $5$ or $5^{-1}$, return the zero ratio orbit; otherwise return the canonical selected native cost. No lemmas are applied in the body; downstream lemmas rewrite through this definition and the corresponding toRat identity.
why it matters
The spike is the concrete counterexample that refutes uniqueness for the slim hypothesis package with RCL removed. Downstream, PRCSlimSansRclUniquenessTarget_refuted applies it at the orbit of $5$ and concludes that the RCL field cannot be dropped. Companion facts record that the spike still satisfies the slim-sans-RCL hypotheses, that its display is $0$ exactly on ${5,5^{-1}}$ and $J$ elsewhere, and that it differs from the true $J$-display at $5$.
In the forcing chain this supports T5 $J$-uniqueness: the RCL functional equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ is what pins $J$ and rules out such spikes. Without RCL, a cost that is $J$ almost everywhere but zero at the $5$-pair still meets the remaining axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.