linearNativeCost
plain-language theorem explainer
Defines the linear decoy cost on ratio orbits by F(q) = q − 1. Native cost-selection and minimality arguments cite it as the second explicit counterexample that already fails the base two-calibration ledger. The body is a one-line orbit subtraction against the unit orbit.
Claim. The linear native cost on a ratio orbit $q$ is the orbit difference $F(q) := q - 1$, where $1$ denotes the unit ratio orbit.
background
In the primitive recognition calculus, candidate costs are maps $F$ from ratio orbits to ratio orbits. The native selection program asks which such maps satisfy an itemized hypothesis ledger (two-calibration, prime-pair products, signed unit, zero orbit, and optionally all prime axes) and thereby coincide with the canonical cost on orbits.
The module builds explicit decoys that look plausible but fail early ledger items. The linear map $q \mapsto q-1$ is decoy 2. Upstream, recognition cost is ordinarily the $J$-cost $J(x)=(x+x^{-1})/2-1$ (or a derived comparator cost); here the ambient type is the discrete ratio-orbit surface rather than $\mathbb{R}_{>0}$, so candidates are orbit endomorphisms.
The sibling constant-zero decoy already fails because the canonical display of the two-orbit is $1/4$, not $0$. The linear decoy is the next natural polynomial trial.
proof idea
Pure definition: return the ratio-orbit subtraction of the input orbit from the unit orbit. No lemmas, no tactics; the meaning is exactly $F(q)=q-1$ on RatioOrbit.
why it matters
Feeds the native cost-selection package and its slim minimality counterpart. Downstream, linearNativeCost_not_native_hypotheses shows it fails the base ledger because $2-1=1$ is not the canonical two-orbit display $1/4$; the full and slim exclusion theorems then discharge decoy 2 against both frozen classes.
That exclusion is part of the $\delta$-native counterpart of the public cost-selection package: every native cost meeting the ledger is crossEq-pointwise the canonical on-orbit cost, and the class is non-vacuous. In the broader forcing chain this supports $J$-uniqueness (T5) on the discrete native surface without smuggling real-analytic assumptions. It does not itself force $\phi$ or the eight-tick structure; it only kills one competing linear ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.