zeroFlatNativeCost
plain-language theorem explainer
Native zero-spike cost on ratio orbits: the canonical J-cost everywhere except the zero orbit, where it returns the zero orbit. Serves as the principal countermodel showing that native-cost uniqueness fails without zero-orbit calibration. Defined by a classical case split on the rational display and the unit orbit.
Claim. Define the zero-flat native cost $F$ on ratio orbits by $F(q)=0$ when the rational display of $q$ is $0$ or when $q$ is the unit orbit, and $F(q)=J(q)=\frac{q+q^{-1}}{2}-1$ (as a ratio-orbit object) otherwise.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-denominator display of a rational (K4.7). The verifier map toRat recovers the ordinary rational $\mathbb{Q}$ value by transport; internal equality is cross-multiplication.
The canonical PRC J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$, realized as the ratio-orbit object onRatioOrbit. The Recognition Composition Law (RCL) only quantifies over nonzero inputs, so a cost that agrees with $J$ off zero can still satisfy the native cost interface.
This module builds native-cost uniqueness and selection packages. The zero-flat map is the standard decoy: it matches $J$ on every nonzero orbit (and $J(1)=0$ already), but spikes the zero orbit to $0$ instead of the canonical display $-1$.
proof idea
Definition by classical case split, not a derived theorem. On input $q$: if the rational display is $0$, return the zero orbit; else if $q$ equals the unit orbit, return zero (matching $J(1)=0$); otherwise return the canonical ratio-orbit J-cost onRatioOrbit q. Noncomputable only because the classical decision on rationals is used.
why it matters
This is the working countermodel for native-cost uniqueness in the PRC ledger. Downstream, it refutes the signed-strengthened uniqueness target (no zero field): every hypothesis lives on nonzero orbits, so zero-flat inhabits the class while disagreeing with canonical $J$ at zero. The same object refutes the prime-signed strengthened target and is excluded exactly by zero-orbit calibration in the slim selection package.
In the Recognition forcing chain this sits under T5 J-uniqueness: RCL forces $J(x)=\cosh(\log x)-1$ on the multiplicative group, but the discrete native interface needs an explicit zero-calibration axiom to kill this flat spike. The slim package CostSelectionPackageNativeSlim records that with zero calibration restored, every native cost is crossEq-pointwise the canonical cost, and zero-flat is the witness that the axiom is irreducible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.