inv_mul_cancel
plain-language theorem explainer
Nonzero PRC rationals satisfy left inverse cancellation: the multiplicative inverse times the element recovers the unit. Field-certificate authors cite this when packing the multiplicative laws for the ratio-orbit quotient. The proof is a short transport of the nonzero hypothesis into the orbit-level reciprocal cancellation lemma via the verifier display map.
Claim. Let $a$ be a PRC rational (a cross-multiplication quotient class of ratio orbits). If the verifier display of $a$ in $\mathbb{Q}$ is nonzero, then $a^{-1}\cdot a=1$.
background
PRC rationals are the K4.8 quotient of ratio orbits by the cross-multiplication setoid: pairs of integer numerator and nonzero natural denominator, identified when cross products agree. The verifier map toRat sends a ratio orbit to an ordinary rational by dividing the integer numerator by the natural denominator; its internal characterization is cross-multiplication, and it descends to the quotient.
The zero ratio orbit displays as $0$ under this map. Multiplicative structure on the quotient, including a reciprocal on classes whose display is nonzero, is inherited from orbit-level operations. This module assembles the field axioms for that quotient as part of the primitive recognition calculus foundation, before J-cost is lifted from representatives to classes.
proof idea
Apply the orbit-level reciprocal cancellation lemma recip_mul_cancel₀. The residual goal is that the underlying ratio orbit is not the zero orbit. Assume it is zero, rewrite the display by zero_toRat, and contradict the hypothesis that the verifier image of $a$ is nonzero.
why it matters
Supplies the left-inverse law consumed by RationalFieldCertificate and rational_field_certificate, which package the field axioms for PRC rationals. Those certificates sit under the lift of J-cost from ratio-orbit representatives to the rational quotient, so multiplicative cancellation must be settled before cost identities can be stated on classes rather than displays. In the Recognition foundation this is arithmetic infrastructure beneath the forcing chain (T5 J-uniqueness, RCL), not a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.