linearNativeCost_slim_excluded

In the Primitive Recognition Calculus, candidate native costs are maps $F$ on ratio orbits. The slim hypothesis class packages the round-1 ledger without the all-prime axis field: reciprocity, normalization invariance, nonzero Recognition Composition Law, unit-zero, and two-calibration, strengthened by prime-pair products, a signed unit condition, and zero-orbit calibration of the doubled trace.

The linear map $F(q)=q-1$ is listed as decoy 2 in the native-cost selection module. It is the obvious additive alternative to the canonical $J$-type cost. Upstream, a dedicated lemma already shows that this decoy fails the base native hypotheses (specifically two-calibration against the canonical two-orbit value).

The local module closes decoy exclusions so that uniqueness of the selected native cost can be stated over the slim ledger rather than the full prime-axis package.

Term-mode one-liner. Assume the slim hypotheses hold for the linear decoy. Project to the nested base native field via signed_strengthened.strengthened.native, then apply the upstream lemma linearNativeCost_not_native_hypotheses, which already refutes those base hypotheses for $F(q)=q-1$. Contradiction.

Feeds costSelectionPackageNativeSlim_holds, which assembles the slim cost-selection package: uniqueness of the native cost on the slim ledger plus a non-vacuous witness (the canonical selected cost). Without excluding the linear decoy, the uniqueness target would be vacuous or false.

This is decoy exclusion 2 against the slim class; the doc-comment notes it dies at base two-calibration. In the broader forcing chain it supports the T5 $J$-uniqueness story: only the hyperbolic cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) survives the native ledger, not additive linear competitors. The slim package is the lighter uniqueness surface used before the full prime-axis field is restored.