instDiv
plain-language theorem explainer
Registers ordinary division notation on PRC rationals by packaging the already-defined multiply-by-reciprocal operation as a Div instance. Anyone writing a/b on PRCRat, or proving that toRat intertwines that division with ordinary rational division, cites this. The body is a one-constructor typeclass registration of the local div map.
Claim. The type of primitive-recognition rationals (nonzero-denominator ratio-orbit quotient classes) carries a division operation, implemented as multiplication by the multiplicative inverse: $a/b := a \cdot b^{-1}$.
background
PRC rationals are the K4.8 quotient of ratio orbits by the cross-multiplication setoid: two displays represent the same class when their orbit-level numerators and denominators cross-multiply. The ambient module builds the field structure on that quotient from the orbit-level arithmetic already available in the primitive recognition calculus.
Division is not primitive. Upstream, ratio-orbit division is multiplication by the reciprocal; the local div on PRC rationals is the same pattern after descent: $a/b := a \cdot b^{-1}$. The present declaration only exposes that map through Lean's Div typeclass so the / notation and HDiv hierarchy become available.
The module sits in the foundation layer that reconstructs $\mathbb{Q}$ inside the recognition calculus before real completion and the J-cost calculus are attached.
proof idea
One-line typeclass instance: the Div structure is inhabited by the already-defined local division map (multiply by inverse). No algebraic obligations are discharged here; the instance is pure packaging.
why it matters
Without this instance, downstream proofs cannot write a / b on PRC rationals or unfold the hierarchy cleanly. The immediate consumer is the compatibility theorem that (a/b).toRat = a.toRat / b.toRat, which unfolds HDiv/Div through this instance and reduces to the already-proved toRat lemmas for multiplication and inversion. That bridge is part of identifying the PRC rational field with ordinary $\mathbb{Q}$ before the real-completion and J-cost stages of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.