zeroFlatNativeCost_one
plain-language theorem explainer
The zero-flat native cost sends the unit ratio orbit to the zero orbit. Anyone verifying that this flattened cost meets the PRC native-cost interface cites this base evaluation. The argument is a short classical case split on the definition: the unit orbit is nonzero as a rational, so the second branch returns zero.
Claim. Let $C_{\mathrm{flat}}$ be the zero-flat native cost on ratio orbits (canonical on nonzero orbits, forced to zero at the zero orbit, and also forced to zero at the unit orbit). Then $C_{\mathrm{flat}}(1)=0$, where $1$ and $0$ are the unit and zero ratio orbits.
background
In the Primitive Recognition Calculus, ratio orbits package an integer numerator over a nonzero distinction-nat denominator. The display map toRat sends a ratio orbit to an ordinary rational by integer division; the unit orbit maps to $1$ and the zero orbit to $0$.
Native cost uniqueness works with cost functionals valued in ratio orbits that obey the Recognition Composition Law on nonzero inputs. The zero-flat native cost is the canonical on-orbit cost, except it is forced to the zero orbit whenever the input is the zero orbit (so the RCL, which only quantifies over nonzero inputs, still holds) and also forced to zero at the unit orbit.
This lemma records the unit-orbit evaluation of that flattening. Upstream, one_toRat supplies the verifier fact that the unit orbit displays as the rational $1$.
proof idea
Term-mode classical proof by unfolding the definition of the zero-flat cost. The first branch is the zero-rational test: rewrite with one_toRat and close 1 ≠ 0 by norm_num, so that branch is discarded. The second branch is the unit-orbit test; rfl fires it and returns the zero orbit.
why it matters
This is a base evaluation inside the native-cost uniqueness development for the Primitive Recognition Calculus. Downstream it is used by the cross-equality lemma that identifies the flattened cost with the on-orbit cost on every nonzero ratio orbit, and by the package that assembles the full PRCNativeCostHypotheses instance for the flattened cost (reciprocal symmetry and the remaining interface axioms).
In the broader Recognition forcing chain this sits under T5 J-uniqueness and the Recognition Composition Law: native costs are the discrete precursors of the continuous J-cost $J(x)=(x+x^{-1})/2-1$. Flattening at zero (and at the unit) is the bookkeeping step that lets a single orbit-valued functional satisfy the interface while remaining canonical away from those points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.