recip_zero
plain-language theorem explainer
The reciprocal operation on PRC rationals fixes the zero class, matching the conventional rule 0⁻¹ = 0. Anyone wiring field or division instances for PRCRat cites this. The proof is a short structural case split: the zero representative’s numerator balances the zero orbit, so RatioOrbit.recip takes its zero branch and the quotient map preserves equality.
Claim. On the PRC rational quotient, $\mathrm{recip}(0) = 0$. Equivalently, the reciprocal of the zero class is again the zero class (the standard $0^{-1}=0$ convention).
background
Primitive Recognition Calculus builds rationals from ratio-orbits: a RatioOrbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. PRC rationals are the quotient of these displays under the structural equivalence that identifies balanced presentations.
Reciprocal on a ratio-orbit swaps numerator and denominator when the numerator is balanced against a nonzero orbit; otherwise it falls into a zero branch. The zero class is the image of the zero ratio-orbit under the quotient map mk. Ledger-level reciprocal (swap source/target and invert the ratio) is the physical ancestor; here the same idea is realized on the integer/orbit arithmetic layer that underwrites $\mathbb{Q}$.
The local module develops integer and rational arithmetic for the recognition calculus so that later field instances can quote structural identities rather than floating-point or classical $\mathbb{Q}$ axioms alone.
proof idea
Reduce both sides to the quotient: show mk (RatioOrbit.recip RatioOrbit.zero) = mk RatioOrbit.zero. Reflexivity of balance gives that the zero orbit’s numerator is balanced against the zero signed orbit. Unfolding RatioOrbit.recip and rewriting with the positive dif branch (the balanced case) collapses the reciprocal of the zero representative to the zero representative itself, so the classes agree.
why it matters
K4.12 pins the zero convention for reciprocal so the $\mathbb{Q}$-facing API is coherent. Downstream, RationalField.inv_zero is literally (0 : PRCRat)⁻¹ = 0 by this theorem, which is required for a lawful Inv/Field-style instance on PRC rationals. Without a structural zero branch, division-by-zero would be an undefined hole rather than a closed total operation on the quotient. In the broader Recognition stack this is bookkeeping on the arithmetic substrate (not a T5–T8 forcing step), but it keeps the ledger-derived rational layer closed under the same reciprocal that appears in cost algebra and recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.