constantZeroNativeCost_slim_excluded
plain-language theorem explainer
The constant-zero cost on ratio orbits is excluded from the slim native-cost hypothesis class. Anyone assembling uniqueness of the selected native cost over that slim ledger cites this decoy kill. The argument is a one-line projection: slim hypotheses imply the base native ledger, which constant-zero already fails at two-calibration (the two-orbit cost is 1/4, not 0).
Claim. The constant-zero map $F\equiv 0$ on ratio orbits does not satisfy the slim native-cost hypotheses: base ledger (reciprocity, normalization invariance, nonzero RCL, unit-zero, two-calibration) plus prime-pair products, signed unit, and zero-orbit calibration of the doubled trace.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ from ratio orbits to ratio orbits obeying a ledger of algebraic axioms that force the classical $J$-cost shape. The base ledger includes reciprocity, normalization invariance, a nonzero Recognition Composition Law, unit-zero, and two-calibration: the cost of the distinguished two-orbit must match the canonical display value.
The slim hypothesis class is that base ledger strengthened by prime-pair product laws, a signed unit condition, and zero-orbit calibration of the doubled trace, but without the all-prime axis field. The constant-zero map (send every orbit to the zero orbit) is the first decoy candidate against this class.
Upstream, constant-zero is already known to fail the base ledger alone: two-calibration demands that the cost of the two-orbit equal $1/4$ in rational display, not $0$.
proof idea
Term-mode one-liner. Assume the slim hypotheses hold for constant-zero. Project to the nested base native hypotheses via the signed-strengthened and strengthened fields of the structure. Apply the prior exclusion that constant-zero fails the base native ledger (two-calibration mismatch). Contradiction.
why it matters
This is decoy exclusion 1 against the slim class. It feeds the slim cost-selection package, which packages uniqueness of the canonical selected native cost over the slim ledger together with a non-vacuity witness. That package is the local uniqueness engine for the native $J$-cost under the reduced axiom set (round-1 minted ledger without the all-prime axis field), aligning with the T5 $J$-uniqueness landmark in the forcing chain. Closing the slim package keeps the uniqueness claim from being vacuous when the stronger all-prime field is dropped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.