zero_crossEq_recip_zero
plain-language theorem explainer
Zero as a ratio orbit is cross-equivalent to its reciprocal (also zero under the total reciprocal). Anyone proving order or rational-display facts that need both orientations of the zero–reciprocal identity cites this. The proof is a one-line symmetry wrapper on the reverse direction.
Claim. Under the internal cross-multiplication relation on ratio orbits, the zero orbit is equivalent to its reciprocal: $\mathrm{crossEq}(0,\,0^{-1})$, where the total reciprocal sends the zero orbit to itself (as on $\mathbb{Q}$).
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Equality of such displays is not raw structural equality; it is crossEq (K4.10): two orbits match when the scaled products of numerator and opposite denominator balance as signed orbits. That is the internal PRC stand-in for rational equality.
The total reciprocal on ratio orbits (K4.12) mirrors $\mathbb{Q}$: it inverts nonzero orbits and sends the zero orbit to zero. The dual-recognition reciprocal on positive reals is the continuum analogue; here the discrete display must close the same convention at zero.
The sibling theorem already shows the reverse orientation: reciprocal of zero is cross-equivalent to zero, by reducing through the rational verifier display and a numeric check. Symmetry of cross-equivalence then supplies the opposite arrow.
proof idea
One-line wrapper: apply symmetry of cross-equivalence (crossEq_symm) to the already-proved reverse fact recip_zero_crossEq_zero. No new arithmetic; only direction flip of the balanced signed-orbit products.
why it matters
Closes the zero–reciprocal identity in both directions on the ratio-orbit surface. Downstream it is consumed by integer_order_certificate, whose doc states the internal signed-orbit order surface is closed: truncated subtraction, $\le$, absolute difference, and nonnegativity displays all line up with their integer readings. Without both orientations of zero versus reciprocal-zero under cross-equivalence, the rational layer under that certificate would have a one-sided hole at the origin. This is foundation bookkeeping for the PRC integer/rational stack that later supports cost and forcing arguments, not a T5–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.