constantZeroNativeCost
plain-language theorem explainer
Defines the constant-zero map on rational orbits: every ratio is sent to the zero orbit. It is the first decoy cost in the native cost-selection ledger, used to prove that the trivial cost fails two-calibration and therefore cannot be a native recognition cost. Citation is for exclusion lemmas that clear the uniqueness class around the canonical J-cost.
Claim. Let $F_0$ be the map on rational orbits sending every orbit $r$ to the zero orbit: $F_0(r) = 0$. This is the constant-zero decoy cost on the PRC ratio-orbit display.
background
In the Primitive Recognition Calculus, costs act on RatioOrbit displays: integer numerator over a nonzero orbit denominator. The native selection program asks which maps $F : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ can serve as recognition costs under an itemized hypothesis ledger (two-calibration, prime-pair products, signed unit, zero orbit, and optionally all-prime axes).
The genuine cost is the quotient-level PRC $J$-cost (the RS cost $J(x) = (x+x^{-1})/2-1$ lifted to orbits). Upstream modules already treat cost as $J$ on recognition events and as derived comparator cost for multiplicative recognizers. This definition supplies the trivial competitor: the map that ignores its argument and returns the zero orbit.
The module sits in the $\delta$-native counterpart of the public cost-selection spine: uniqueness of the native cost under frozen hypotheses, with explicit decoys ruled out before the uniqueness theorem is stated.
proof idea
Pure definition: the constant function fun _ => RatioOrbit.zero. No proof obligations. Downstream exclusion proofs unfold this definition, reduce cross-equality of orbits to equality of rational values, and compare against the canonical cost of the two-orbit, which is $1/4$ rather than $0$.
why it matters
Native $J$-uniqueness (the T5 landmark in the forcing chain) needs a clean class: every map satisfying the ledger must agree pointwise with the canonical orbit cost. The constant-zero decoy is the first counterexample cleared from that class. It feeds constantZeroNativeCost_not_native_hypotheses (fails base two-calibration), then the full and slim exclusion theorems, and finally both CostSelectionPackageNative and CostSelectionPackageNativeSlim, whose uniqueness clauses quantify over the surviving native costs only.
Without excluding $F\equiv 0$, the uniqueness statement would be false or vacuous. The decoy therefore anchors the non-vacuity and minimality side of the preregistered native cost-selection packages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.