mul_recip_cancel
plain-language theorem explainer
Any nonzero PRC rational multiplies with its structural reciprocal to the unit class. Field-axiom assemblers for the primitive recognition calculus cite it, as do the rational-field and kernel first-pass certificates. The proof is quotient induction on the representative, exclusion of a balanced numerator from the structural nonzero hypothesis, then cross-multiplication after unfolding mul/recip with a sign split closed by ring.
Claim. For every PRC rational $a$ outside the zero class, $a \cdot a^{-1} = 1$, where product and reciprocal are the structural operations on ratio-orbit quotient classes and the nonzero hypothesis is the class disequality $a \neq 0$ (not a statement about the $\mathbb{Q}$ display).
background
PRC rationals (K4.8) are quotient classes of ratio orbits with nonzero denominators, identified by cross-multiplication of orbit-level numerators and denominators. A ratio orbit pairs a signed-orbit numerator with a distinction-nat denominator. The zero class is the class of the zero ratio orbit; structural disequality $a \neq 0$ lives at the quotient, not on the verifier map to $\mathbb{Q}$.
Reciprocal on ratio orbits is total (K4.12): a balanced (zero) numerator is sent to zero, otherwise the reciprocal swaps numerator and denominator with sign handling via a decidable nonnegativity flag. Multiplication of classes is induced by componentwise orbit multiplication. The module builds integer and rational arithmetic from primitive recognition orbits without classical choice.
Upstream, recip branches on balancedness against signed-orbit zero; toRat is only a transport/display wrapper whose internal characterization remains cross-multiplication.
proof idea
Quotient induction on $a$ reduces to a representative ratio orbit $q$. From the structural hypothesis $a \neq 0$ one shows the numerator of $q$ is not balanced with signed-orbit zero (else the class would be the zero class via the cross-equality criterion and toInt), hence its integer image is nonzero.
The goal becomes class equality of $q$ times its reciprocal with the unit ratio orbit, discharged by mk_eq_mk_of_crossEq and the integer cross-product form. Unfolding mul and recip, the balanced branch is excluded (dif_neg). After simplifying with mul_toInt, toNat_mul, and the unit numerator/denominator identities, a case split on the numerator nonnegativity flag handles both signs: positive uses ofOrbit_toInt and the abs-toNat identity; negative uses negate_toInt likewise. Each branch reduces to an integer identity closed by ring.
why it matters
This is K4.12, structural reciprocal cancellation on the product-with-reciprocal side. It supplies the multiplicative inverse law on the nonzero locus for the rational-field certificate, which packages the field axioms (commutativity, associativity, units, additive inverses) for PRC rationals. The kernel first-pass certificate also sits downstream, relying on a working rational judgment surface.
In the Recognition Science stack the primitive recognition calculus is the discrete arithmetic substrate beneath continuum completion and the forcing chain (T5 J-uniqueness and the Recognition Composition Law). Keeping cancellation choice-free, with nonzero as class inequality rather than a classical $\mathbb{Q}$ witness, matches the constructive stance of the monolith.
Without this lemma the rational layer cannot certify that every nonzero class has a two-sided inverse against the structural unit, blocking the field certificate and any later continuum or cost-functional development that assumes a field of scalars.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.