constantZeroNativeCost_not_native_hypotheses
plain-language theorem explainer
The constant-zero cost function fails the base native-cost hypothesis ledger of the Primitive Recognition Calculus: two-calibration demands that the cost of the two-orbit equal the canonical display 1/4, not 0. Anyone excluding decoy costs from the PRC selection class cites this. The proof is a short contradiction: unpack two-calibration, reduce via the ratio-orbit rationalization, and finish by norm_num.
Claim. The constant-zero native cost does not satisfy the PRC native-cost hypotheses. In particular, the two-calibration clause fails: the cost assigned to the two-orbit must equal the canonical display value $1/4$, whereas the constant-zero cost assigns $0$.
background
In the Primitive Recognition Calculus, candidate native costs are filtered by a hypothesis ledger before uniqueness and minimality arguments run. The base package PRCNativeCostHypotheses includes two-calibration: the cost of the two-orbit must match the canonical display value fixed by the RS calibration spine (here $1/4$ after passage to the rationalized ratio-orbit coordinates).
The constant-zero cost is the trivial decoy that sends every ratio-orbit display to $0$. Sibling selection material also treats a linear decoy; both are ruled out at the same ledger layer. Ratio-orbit infrastructure supplies the bridge crossEq_iff_toRat_eq and the evaluations zero_toRat, two_toRat, so two-calibration becomes a concrete rational equality once the cost is specialized.
Local module setting is native-cost selection and decoy exclusion inside PRCNativeCostSelection, feeding the slim and full strengthened hypothesis stacks used downstream for minimality.
proof idea
Assume the constant-zero cost satisfies the native hypotheses and extract the two-calibration conjunct. Rewrite that conjunct through the ratio-orbit equivalence that turns cross-equality into equality of rationalized displays. Specialize the cost and the orbit maps with simp (constantZeroNativeCost, zero_toRat, onRatioOrbit_toRat, two_toRat), obtaining the false numerical claim $0 = 1/4$. Close with norm_num.
why it matters
This is decoy exclusion 1 at the base ledger: constant zero never enters the PRC native-cost class. Downstream, constantZeroNativeCost_excluded lifts the negation to the full frozen package (zero-calibrated, prime-signed, strengthened), and constantZeroNativeCost_slim_excluded does the same for the slim signed-strengthened class used in minimality. Both are one-line projections onto this theorem's native core.
In the Recognition framework this protects the forced J-cost selection path (T5 J-uniqueness and the RCL) from the trivial zero functional before uniqueness and minimality arguments identify the canonical native cost. Without it, the selection class would be contaminated by a cost that erases all recognition structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.