linearNativeCost_excluded
plain-language theorem explainer
The linear cost is ruled out of the full zero-calibrated, prime-signed, strengthened native-cost class. Cost-selection and J-uniqueness arguments cite this as the second decoy kill against the frozen hypothesis bundle. The proof is a one-line projection: strip the full package down to its native fragment and reuse the native-level exclusion.
Claim. The linear native cost functional does not satisfy the full package of zero-calibrated, prime-signed, strengthened native cost hypotheses on the PRC ledger.
background
In the Primitive Recognition Calculus, candidate cost functionals on positive ratios are tested against a nested ledger of structural axioms: a native Recognition Composition Law fragment, strengthenings, a prime-signed layer, and zero-orbit calibration. The target cost is the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely under the full package (T5 in the forcing chain).
Two explicit decoys sit beside the canonical selection: the constant-zero cost and a linear cost. Sibling results already show that the linear cost fails even the weakest native fragment of the ledger. The present theorem lifts that failure to the full frozen class used by the selection package.
Upstream cost notions in the stack (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsened weighted sums) all point at the same J-shaped functional; the selection module freezes which hypothesis bundle is allowed to force it.
proof idea
Term-mode one-liner. Assume h asserts that the linear native cost meets the full zero-calibrated prime-signed strengthened native package. Project h along the nested structure fields
prime_signed.signed_strengthened.strengthened.native
to obtain only the native-fragment hypotheses. Discharge the goal by applying the sibling lemma that already proves the linear cost fails those native hypotheses. No new algebraic work is done here; the strength is purely in the projection from the full class to the fragment.
why it matters
This is decoy exclusion 2 against the full frozen class (paired with the constant-zero exclusion). Downstream it is consumed by costSelectionPackageNative_holds, which assembles the native cost-selection package: J-uniqueness under the zero-calibrated prime-signed strengthened target, plus a non-vacuity witness that the canonical selected native cost meets the package and the cross-equation on ratio orbits.
In the Recognition framework this sits under T5 (J-uniqueness) and the Recognition Composition Law: only the hyperbolic J-cost survives the ledger, so later constants and the mass ladder inherit a single native cost rather than a linear alternative. Without this kill, the selection package could not claim the frozen class forces the canonical choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.