zero_toRat
plain-language theorem explainer
The distinguished zero ratio orbit displays as the rational number 0 under the verifier map. Cost, gauge-orbit, and real-character lemmas cite it whenever a native cost is zero-calibrated or a case split hits the zero ratio. The proof is a short unfold-and-simp on the definitions of the zero orbit and the display map.
Claim. The distinguished zero ratio orbit $z$ (integer numerator zero over a nonzero orbit denominator) satisfies the verifier display $\mathrm{display}(z) = 0$ in $\mathbb{Q}$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator (a signed orbit) over a nonzero distinction-natural denominator. It is the internal carrier for rational comparisons before any transport to classical $\mathbb{Q}$.
The verifier display sends a ratio orbit $q$ to $(q.\mathrm{num}\text{ as }\mathbb{Z}):\mathbb{Q}$ divided by $(q.\mathrm{den}\text{ as }\mathbb{N}):\mathbb{Q}$. Spec tag A5 records this as a transport wrapper; internal equality is characterized by cross-multiplication, not by the display itself.
The zero ratio orbit is the canonical unit of that carrier with vanishing numerator. Parallel infrastructure already has zero_toInt for signed orbits; this lemma is the rational-display counterpart.
proof idea
One-line tactic proof: unfold the definitions of the zero ratio orbit and of the verifier display, then simp. The numerator becomes the integer 0, so the quotient in $\mathbb{Q}$ is 0. No external lemmas beyond definitional reduction are required.
why it matters
This is a simp-tagged calibration fact in the K4 integer/rational orbit layer. Downstream cost work depends on it heavily: signedPowerNativeCost_toRat and signGaugeNativeCost_toRat rewrite zero-cost branches through it; the zero-calibrated doubled-trace lemmas for signed-power and sign-gauge native costs use it to discharge the unit case; traceDisplay_one simplifies the doubled trace at the unit orbit via zero_toRat together with one_toRat and two_toRat.
It also feeds nondegeneracy statements such as strict_somewhere_iff_charges_at_two, which compare positive ratio displays against a cost that may vanish only at the sign sector. In the broader RS stack this keeps the PRC native-cost uniqueness and gauge-orbit classification honest at the zero point of the ratio ladder, before J-cost and the forcing chain (T5–T8) are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.