zeroFlatNativeCost_slim_excluded
plain-language theorem explainer
The zero-flat native cost fails the slim native-cost hypothesis class, and fails it only at zero-orbit calibration. Layer-discrimination arguments for the slim cost-selection package cite this exclusion. The proof reduces the doubled-trace zero-calibration field to a rational identity and obtains a numerical contradiction.
Claim. The zero-flat native cost does not satisfy the slim hypothesis class: base native-cost axioms (reciprocity, normalization invariance, nonzero RCL, unit-zero, two-calibration), prime-pair products, signed unit, and zero-orbit doubled-trace calibration.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits. The slim hypothesis class is the round-1 ledger with the all-prime axis field deleted: signed-strengthened native-cost axioms plus a zero-orbit calibration on the doubled trace of $F$. That zero field asks the doubled-trace native cost to match the canonical zero calibration on the zero orbit (cross-equality of ratio-orbit values).
The zero-flat cost is the frozen known-wrong candidate that is identically zero in the relevant native-cost presentation. Round-1 already places it in the larger prime-signed class; the slim package isolates whether the extra zero-orbit field does real work. The local module builds the slim cost-selection package (prereg j-free minimality): uniqueness under the slim ledger, non-vacuity of the canonical witness, and explicit exclusions of frozen wrong costs.
proof idea
Assume the slim hypotheses for the zero-flat cost. Project to the zero-calibration field. Unfold doubled-trace zero-calibration into a cross-equality of ratio-orbit values, then rewrite cross-equality as equality of rational images. Simplify the doubled-trace native cost of the zero-flat map (using that it evaluates to zero, together with the additive/multiplicative toRat rules for the orbit arithmetic and the constants $0,1,2$). The resulting rational identity is false by norm_num.
why it matters
This is the exclusion half of the layer-discrimination pair for the slim package: zero-flat passes every slim field except the zero orbit, and fails exactly there, so the slim class's zero field is not decorative. Downstream, costSelectionPackageNativeSlim_holds packages uniqueness, non-vacuity, and the frozen exclusions (including this one) into the slim native cost-selection certificate.
In the broader Recognition chain this sits under native J-cost rigidity on the countable ratio-orbit carrier: the Recognition Composition Law and T5 J-uniqueness force the canonical cost once the ledger is strong enough. Slimming the ledger (finite data on generators $2$ and $-1$, pair products, and the zero orbit) is only honest if each remaining field excludes a real counter-model; this theorem discharges that obligation for zero calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.