zeroFlatNativeCost_crossEq_onRatioOrbit_of_nonzero
plain-language theorem explainer
For every nonzero ratio orbit q, the zero-flat native cost of q is cross-multiplication equivalent to the standard ratio-orbit cost display of q. Used when packaging the zero-flat countermodel as a native-cost hypothesis bundle and when ruling out character-trace realizations. Proof is a classical case split on the unit orbit: toRat transport at one, reflexivity off one.
Claim. Let $q$ be a ratio orbit whose verifier display is a nonzero rational. Then the zero-flat native cost of $q$ is equivalent, under cross-multiplication of signed numerator/denominator orbits, to the standard cost of $q$ on the ratio-orbit display.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator. Its verifier display toRat is the ordinary rational quotient; the internal equality relation is cross-multiplication (crossEq), which balances scaled signed orbits and agrees with rational equality of the displays (K4.10).
The ambient module studies uniqueness of native cost functionals on these orbits. The standard cost display on a ratio orbit is the PRC J-cost transport onRatioOrbit (vanishing at the unit orbit, as $J(1)=0$). The zero-flat native cost is a deliberately flat countermodel: it coincides with that standard display off zero and the unit, and is arranged to be zero at the unit.
Upstream, crossEq_iff_toRat_eq identifies cross-multiplication with equality of verifier rationals, and crossEq_refl supplies reflexivity. Those two facts, plus the unit and zero toRat simplifications, are the only external ingredients.
proof idea
Classical case split on whether $q$ is the unit ratio orbit.
If $q$ is the unit: substitute, rewrite the zero-flat cost at one, then transport via crossEq_iff_toRat_eq. The left display is zero (zero_toRat); the right is the standard cost at one, whose toRat is $0$ because the unit has display $1$ and the cost vanishes there. Close by norm_num.
If $q$ is not the unit: unfold the zero-flat definition, discharge both if guards with the nonzero hypothesis and the case assumption, and finish by crossEq_refl (the two sides are definitionally the same orbit).
why it matters
This lemma is a local agreement fact for the zero-flat countermodel: off the zero orbit, zero-flat native cost matches the standard ratio-orbit cost under the PRC internal equality. Downstream it is consumed by zeroFlatNativeCost_hypotheses (the full native-cost hypothesis bundle), by zeroFlatNativeCost_no_character_trace (no ratio character whose doubled trace recovers this cost), and by the prime-signed strengthened ledger package in PRCNativeCostSelection.
In the Recognition forcing picture this sits under native-cost uniqueness for the J-cost (T5 landmark: $J(x)=(x+x^{-1})/2-1$). The zero-flat object is the standard countermodel showing which calibration axioms are load-bearing: it satisfies a large fragment of the native-cost interface yet admits no character-trace realization. The present lemma is the crossEq bridge that lets those hypothesis packages quote agreement with onRatioOrbit wherever the display is nonzero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.