div
plain-language theorem explainer
Division on ratio orbits is multiplication by the reciprocal orbit. Anyone writing the Recognition Composition Law or doubled-trace identities on RatioOrbit cites this. The body is a one-line composition of mul and recip, matching the field pattern used for PRC rationals.
Claim. For ratio orbits $q$ and $r$ (signed-orbit numerator over nonzero distinction-nat denominator), define $q/r := q \cdot r^{-1}$, where $r^{-1}$ is the total reciprocal that sends the zero orbit to itself.
background
A RatioOrbit is the primitive-recognition display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Reciprocal on these orbits is total, sending the zero orbit to zero as in $\mathbb{Q}$ (K4.12). Multiplication of orbits is already available in the same layer.
The module builds the native $J$-cost calculus on these orbits. Division is the missing field operation needed to state the Recognition Composition Law in orbit language: expressions such as $F(xy)+F(x/y)$ require a well-defined $x/y$ before any uniqueness or d'Alembert argument can run.
Upstream, the same pattern appears for PRC rationals (a * b⁻¹) and for the real reciprocal involution $\iota(x)=x^{-1}$ that encodes dual-recognition symmetry. The orbit-level div is the corresponding total operation on the discrete display.
proof idea
One-line definitional wrapper: div q r is RatioOrbit.mul q (RatioOrbit.recip r). No separate proof obligations; totality of reciprocal (zero maps to zero) makes the composite total on all pairs of orbits.
why it matters
This is the division used throughout the real-character factorization layer. Downstream, the doubled-trace form of the composition law is stated with F (mul x y) and F (div x y) side by side (doubledTrace_dAlembert_of_rcl, and the native / sans-anchor specializations). The RCL pack structures (BaseSansTwo and related hypothesis packs) quantify over maps on ratio orbits and need this operation to write the canonical RCL identity without leaving the orbit type.
In the forcing chain, the composition law is the algebraic skeleton that forces $J(x)=\cosh(\log x)-1$ (T5) once reciprocity and normalization are fixed. Having division as a first-class orbit operation keeps those identities inside the primitive calculus rather than jumping to $\mathbb{R}$ early. It also feeds dimensioned-quantity and scalar-certificate code that manipulates ratios of orbit-valued costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.