inv_zero
plain-language theorem explainer
The multiplicative inverse of the zero PRC rational equals zero, matching the standard rational convention. Builders of the PRC rational field package cite this when recording inverse laws. The proof is a one-line wrapper of the structural reciprocal-zero lemma on ratio orbits.
Claim. For the zero class $0$ among PRC rationals (ratio-orbit quotient classes), $0^{-1} = 0$.
background
PRC rationals are the K4.8 quotient of ratio orbits with nonzero denominators, identified by cross-multiplication of orbit-level numerators and denominators. They sit in the Primitive Recognition Calculus foundation as the rational layer before real completion.
Reciprocal on a ratio orbit is defined by cases: when the numerator is balanced against the zero signed orbit, the construction takes an explicit zero branch. Upstream, recip_zero records the structural fact that this reciprocal fixes the zero class under the usual $\mathbb{Q}$ convention $0^{-1}=0$.
Field-style inverse notation on the quotient is induced from that orbit-level reciprocal, so the zero law must be restated at the PRCRat level for the operator-form field package.
proof idea
One-line wrapper that applies the upstream lemma stating the reciprocal of the zero ratio-orbit class is again zero. Because inverse notation on PRC rationals is defined via that reciprocal, the structural identity is exactly the claimed equality.
why it matters
Used by the RationalFieldCertificate structure and the rational_field_certificate theorem that assembles operator-form field laws for PRC rationals (associativity, units, negatives, and related inverse facts). Packaging $0^{-1}=0$ keeps the multiplicative structure coherent under the chosen rational convention before J-cost is lifted from ratio-orbit representatives to the rational quotient.
That rational layer supports the cost calculus underlying the forcing chain, in particular T5 J-uniqueness and the Recognition Composition Law, once the field operations are certified. The declaration itself is bookkeeping, not a deep forcing step, but the certificate it feeds is the gate for later PRC arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.