linearNativeCost_not_native_hypotheses
plain-language theorem explainer
The linear decoy cost on ratio orbits fails the base PRC native-cost hypotheses at two-calibration. Cost-classification proofs cite it to kill the linear candidate before stronger ledgers. The argument reduces two-calibration to a rational equality and obtains the numerical contradiction $1 \neq 1/4$.
Claim. The linear native cost $F$ on ratio orbits does not satisfy the PRC native-cost hypotheses. In particular the two-calibration field fails: the display of $F$ at $2$ equals $1$ in $\mathbb{Q}$, not the canonical value $1/4 = J(2)$.
background
In the primitive recognition calculus, costs are maps $F$ on RatioOrbit (integer numerator over a nonzero orbit denominator), compared by cross-multiplication equality of displays. The rational display map sends each orbit to $\mathbb{Q}$.
PRCNativeCostHypotheses is the base ledger for later discrete cost classification. Its two_calibrated field forces the cost at the orbit for $2$ to match the canonical $J$-display; the upstream doc states it "rules out the identically-zero cost on the discrete rational surface, playing the role of the continuous theorem's unit log-curvature calibration." The canonical $J$ on orbits satisfies
$(J(q)).\mathrm{toRat} = (q + q^{-1})/2 - 1$, so $J(2) = 1/4$.
The linear decoy is the sibling map that subtracts the unit orbit rather than applying $J$. Cross-equality of displays is equivalent to equality of rational displays (crossEq_iff_toRat_eq).
proof idea
Assume PRCNativeCostHypotheses for the linear decoy and extract two_calibrated. Rewrite that cross-equality as rational equality via crossEq_iff_toRat_eq. Unfold the linear decoy and simplify with sub_toRat, one_toRat, onRatioOrbit_toRat, and two_toRat to obtain the equality $1 = 1/4$ in $\mathbb{Q}$. Close by norm_num.
why it matters
This is decoy exclusion 1 against the full frozen class: the linear candidate dies already at the base two-calibration gate, before reciprocal, RCL, or strengthened signed hypotheses are checked. Downstream, linearNativeCost_excluded and linearNativeCost_slim_excluded wrap it to exclude the linear decoy from the full and slim strengthened ledgers ("dies at the base two-calibration").
In the Recognition framework this supports discrete selection of the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ (forcing-chain T5 / RCL), by showing that the obvious linear alternative is not even two-calibrated on the rational surface. It pairs with the constant-zero exclusion in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.