constantZeroNativeCost_excluded
plain-language theorem explainer
The constant-zero map on ratio orbits fails the full zero-calibrated, prime-signed, strengthened native-cost hypothesis package. Anyone building the native cost-selection package cites this as decoy exclusion 1. The argument is a one-line projection: the full package implies the base native hypotheses, which constant-zero already violates via two-calibration.
Claim. The constant-zero cost $F\equiv 0$ on ratio orbits does not satisfy the zero-calibrated prime-signed strengthened native-cost hypotheses (the full frozen native-cost interface).
background
In the primitive recognition calculus, candidate native costs are maps $F$ from ratio orbits to ratio orbits. The constant-zero decoy sends every orbit to the zero orbit. Base native-cost hypotheses already demand two-calibration: the cost of the distinguished two-orbit must match a fixed rational display equal to $1/4$, not $0$.
The full frozen interface packages several layers: prime-axis and prime-pair calibration, signed-unit recognition, a strengthened native ledger, and zero-trace calibration of the doubled native cost at the zero orbit. Satisfying that interface therefore implies the base native hypotheses.
Local setting is native cost selection: exclude trivial competitors before asserting that the canonical selected cost is the unique map meeting the frozen class.
proof idea
Term-mode reductio. Assume the full zero-calibrated prime-signed strengthened package holds for the constant-zero map. Project the nested structure fields down to the base native-cost hypotheses (prime_signed.signed_strengthened.strengthened.native). Apply the upstream lemma that constant-zero already fails those base hypotheses: two-calibration rewrites to an equality of rationals, and simplifying the constant-zero evaluation yields $0 = 1/4$, a contradiction.
why it matters
Feeds costSelectionPackageNative_holds, which assembles the native cost-selection package: uniqueness of the zero-calibrated prime-signed strengthened native cost together with a non-vacuous witness (the canonical selected cost and its cross-equation on ratio orbits). Doc-comment labels this decoy exclusion 1 against the full frozen class.
In the Recognition forcing chain this sits under T5 J-uniqueness: the cost $J(x)=(x+x^{-1})/2-1$ is the unique native selection once decoys are ruled out. Constant-zero is the most trivial competitor; excluding it is a necessary step before claiming the selection package is inhabited only by the canonical cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.