toRat_div
plain-language theorem explainer
Division of primitive recognition calculus (PRC) rationals is compatible with the verifier map into ordinary rationals: the image of a quotient is the quotient of the images. Field-structure and cancellation lemmas on PRC rationals cite this homomorphism identity. The proof unfolds division as multiplication by inverse and rewrites with the already-proved mul and inv transport lemmas.
Claim. Let $a,b$ be PRC rationals (nonzero-denominator ratio-orbit quotient classes). Writing $(\cdot)^{\sim}$ for the verifier display into $\mathbb{Q}$, one has $(a/b)^{\sim} = a^{\sim}/b^{\sim}$.
background
PRC rationals are the quotient of ratio orbits by the cross-multiplication setoid: two orbit displays represent the same class when numerators and denominators cross-multiply equally. The verifier map sends a class to the ordinary rational formed by integer numerator over natural denominator (a pure transport wrapper; the internal equality is cross-multiplication).
Division on PRC rationals is not primitive: it is defined as multiplication by the multiplicative inverse, via the standard HDiv instance built from the module's div operation. Upstream, the verifier already preserves multiplication and inversion (toRat_mul', toRat_inv'), so the only remaining step for a field homomorphism is to check that the composite definition of division is likewise preserved.
This module sits in the Primitive Recognition Calculus foundation layer, assembling enough arithmetic on PRC rationals to support J-cost distance and increment identities used later in the forcing chain.
proof idea
Tactic proof. Unfold the hierarchy of division instances (HDiv.hDiv, Div.div, and the local div) so the left-hand side becomes multiplication by inverse. Rewrite with the upstream lemmas that the verifier preserves multiplication and inversion. The two sides of the goal are then definitionally equal, closed by rfl.
why it matters
This is a structural homomorphism lemma needed before PRC rationals can be treated as a field in verifier coordinates. Downstream it is applied directly in the cancellation laws (a/b)*b = a and a*b/b = a (under nonzero verifier image), and it is listed among the ingredients of the rational-field certificate that packages commutativity, associativity, and units.
It also appears in the proved J-cost distance-increment triangle target, where concrete PRC rationals such as $\rho = \varepsilon/(1+\varepsilon)$ are formed and compared after transport to $\mathbb{Q}$. Without division commuting with the verifier, those algebraic reductions cannot leave the quotient type. In the broader Recognition stack this is bookkeeping under the primitive calculus that later feeds cost identities (RCL, J-uniqueness), not a new physical forcing step by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.