recip_mul_cancel
plain-language theorem explainer
For any nonzero PRC rational a, the product of its reciprocal with a equals one. Algebraists building the field structure on ratio-orbit quotients cite this as the left inverse law. The proof is a one-line commute-and-apply of the already-proved right cancellation.
Claim. If $a$ is a nonzero PRC rational (a ratio-orbit quotient class with nonzero denominator), then $\mathrm{recip}(a)\cdot a = 1$.
background
PRC rationals are the quotient of ratio orbits by the cross-multiplication setoid: two displays represent the same class when their orbit-level numerators and denominators cross-multiply equally. The zero class is the class of the zero orbit over a nonzero denominator; one is the class of equal nonzero orbits.
Reciprocal and multiplication are defined on these classes so that they mirror ordinary rational arithmetic at the orbit level. The companion right-cancellation law (multiply then take reciprocal) is already available; this declaration supplies the opposite order.
The local module builds integer and rational arithmetic from primitive recognition orbits, without assuming classical $\mathbb{Q}$ as a primitive type.
proof idea
Rewrite the goal by commutativity of multiplication on PRC rationals, then apply the already-proved right reciprocal cancellation under the same nonzero hypothesis. No new orbit-level reasoning is introduced.
why it matters
K4.12 closes the inverse side of structural reciprocal cancellation for PRC rationals. Together with right cancellation it gives both one-sided inverse laws needed for a field (or division-ring) interface on the ratio-orbit quotient.
In the Recognition foundation this sits under the primitive recognition calculus that eventually feeds the forcing chain: clean rational arithmetic on orbits is prerequisite scaffolding for cost functionals, ladder arithmetic, and later uniqueness results (T5 J-uniqueness and the RCL). No downstream consumers are wired in the current graph, so the lemma is presently a local algebraic completeness step rather than a direct cite in T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.