recip_zero_crossEq_zero
plain-language theorem explainer
The reciprocal of the zero ratio orbit is cross-equivalent to zero under the internal PRC cross-multiplication relation. Anyone building the signed-orbit order surface or the integer-order certificate cites this base identity. The proof rewrites cross-equivalence to rational equality, applies the reciprocal and zero display lemmas, and finishes by numeric simplification (Lean’s 0⁻¹ = 0).
Claim. Let $0$ be the zero ratio orbit. Then $\mathrm{recip}(0)$ is cross-equivalent to $0$: the cross-multiplication balance $a.n\cdot b.d \sim b.n\cdot a.d$ holds between $\mathrm{recip}(0)$ and $0$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Cross-equivalence (crossEq) is the internal rational relation: two ratio orbits match when the scaled numerators balance as signed orbits (K4.10). The verifier display toRat sends each ratio orbit to a rational, and cross-equivalence is proved equivalent to equality of those displays.
The total reciprocal on ratio orbits mirrors $\mathbb{Q}$: it sends the zero orbit to itself and otherwise swaps numerator and denominator with a sign adjustment. The companion lemmas record that the display of the reciprocal is the field inverse of the display, and that the zero orbit displays as $0$.
This module builds the internal order surface on signed and ratio orbits; the present fact is a zero-case identity needed for that surface to close under reciprocal.
proof idea
Term-mode rewrite chain. First replace cross-equivalence by equality of toRat displays via crossEq_iff_toRat_eq. Then rewrite the left display with recip_toRat and the right with zero_toRat, reducing the goal to $(0:\mathbb{Q})^{-1}=0$. norm_num discharges that arithmetic identity (Lean’s convention that the inverse of zero is zero).
why it matters
Closes the zero case of reciprocal under the internal rational relation, so the order surface treats $0$ and $\mathrm{recip}(0)$ as the same point. Downstream, zero_crossEq_recip_zero is the symmetric form obtained by crossEq_symm, and both feed integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. Within the foundation stack this is bookkeeping for the PRC integer/rational layer that later supports the forcing chain’s cost and dimension steps; it is not itself a T5–T8 claim, but a prerequisite identity those layers rely on when they talk about reciprocal generators and balanced orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.