div
plain-language theorem explainer
Division of PRC rationals is multiplication by the reciprocal. Anyone building field operations, cost composition, or d'Alembert forms of the Recognition Composition Law on the PRC rational field cites this. The body is a one-line definition: a times b inverse.
Claim. For PRC rationals $a,b$, define division by $a/b := a \cdot b^{-1}$, using the already-constructed multiplicative structure on the ratio-orbit quotient.
background
PRC rationals (PRCRat) are the K4.8 quotient of ratio orbits by the cross-multiplication setoid: nonzero-denominator pairs identified when numerators and denominators cross-multiply equal at the orbit level. They carry the field operations needed before real completion.
The sibling module on ratio orbits already defines orbit-level division as multiplication by reciprocal. The present definition lifts that pattern to the quotient type. Reciprocal and multiplication on PRCRat are presupposed; this only packages them as a binary division operator.
Local setting is the primitive recognition calculus: rationals as the discrete carrier on which J-cost, RCL identities, and later real character factorizations are stated before passing to completeness.
proof idea
One-line definitional wrapper. No tactics: div a b is definitionally a * b⁻¹. Parallel to the orbit-level RatioOrbit division, which is mul q (recip r).
why it matters
Field division is the primitive that lets the Recognition Composition Law be written in the familiar form $J(xy)+J(x/y)=\cdots$. Downstream, the doubled-trace d'Alembert theorems (doubledTrace_dAlembert_of_rcl, _of_native, _of_sansAnchor) and rational-trace identities invoke this operator when stating RCL without the two-point anchor. Cost factorization structures (BaseSansTwo) and scalar derivative certificates also consume it. In the forcing chain this sits under the algebraic substrate for T5 J-uniqueness and the RCL, not a chain step itself, but without quotient-level division those identities cannot be stated on PRCRat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.