zeroFlatNativeCost_zero
plain-language theorem explainer
The zero-flat native cost sends the zero ratio orbit to itself. Anyone building or refuting uniqueness for native costs on ratio orbits cites this fixed-point fact. The proof is a one-line rewrite: the definition branches on `toRat = 0`, and the zero orbit has rational value 0, so the first branch returns zero.
Claim. Let $C_0$ be the zero-flat native cost on ratio orbits (canonical on nonzero orbits, flattened to the zero orbit at rational value $0$). Then $C_0(0) = 0$, where $0$ denotes the zero ratio orbit.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator, carrying a rational value via toRat. The zero orbit is the distinguished orbit with rational value $0$ (proved by zero_toRat).
Native costs on ratio orbits are meant to satisfy the Recognition Composition Law (RCL) style interface. Because RCL only quantifies over nonzero inputs, one may alter the value at the zero orbit without breaking those axioms. The zero-flat native cost does exactly that: on every nonzero orbit it agrees with the canonical on-orbit cost, and at the zero orbit (and also at the unit orbit) it returns the zero orbit.
This module studies uniqueness and countermodels for such native costs. The zero-flat map is the standard countermodel when zero-orbit calibration is omitted from the hypothesis package.
proof idea
Term-mode rewrite under classical choice. Unfold the definition of the zero-flat cost: it is an if on whether q.toRat = 0. Apply the positive branch via if_pos, using the simp fact that the zero orbit has toRat = 0. The then-branch is definitionally the zero orbit, so equality holds.
why it matters
This fixed point is the algebraic hinge for every zero-flat countermodel argument in the native-cost uniqueness chain. Downstream, it feeds zeroFlatNativeCost_doubled_trace_zero (doubled-trace evaluation at zero) and zeroFlatNativeCost_no_character_trace (no ratio character can match the flattened cost).
It is also the witness used to refute uniqueness targets that omit zero calibration: PRCSignedStrengthenedNativeCostUniquenessTarget_refuted and PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted both instantiate the zero-flat cost and rely on its value at zero being $0$ rather than the canonical display. Layer discrimination (zeroFlatNativeCost_slim_excluded) likewise uses that the map fails zero-calibration exactly at the zero orbit.
In the broader Recognition forcing picture this is bookkeeping for T5-style J-uniqueness: RCL forces the cost shape on the multiplicative group of nonzero ratios, but the zero orbit is outside that group, so uniqueness needs an explicit zero-calibration axiom. This lemma records the countermodel's zero value cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.