div_toRat
plain-language theorem explainer
Division of ratio orbits transports to ordinary rational division under the verifier map toRat. Anyone checking RCL surface identities or native-cost reciprocal laws on ratio orbits cites this lemma. The proof unfolds orbit-division as multiply-by-reciprocal and rewrites with the already-proved multiplication and reciprocal transport facts.
Claim. For ratio orbits $q$ and $r$, the rational display of their orbit-division equals the ordinary quotient of their rational displays: $\mathrm{display}(q \mathbin{/}_{\mathrm{orb}} r) = \mathrm{display}(q)/\mathrm{display}(r)$ in $\mathbb{Q}$.
background
A ratio orbit is the PRC display of a rational: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). The map toRat sends such a display to the ordinary rational $(n:\mathbb{Z})/(d:\mathbb{N})$; its doc tags it as a transport wrapper whose internal equality is cross-multiplication.
Orbit division is not primitive. In this module it is defined by multiplying by the reciprocal: $\mathrm{div},q,r := \mathrm{mul},q,(\mathrm{recip},r)$. The same pattern appears on the PRC rational field, where division is $a\cdot b^{-1}$.
Two upstream transport lemmas already exist: multiplication of ratio orbits becomes ordinary product after toRat, and reciprocal becomes ordinary inverse. Together they reduce any statement about orbit-division on the rational surface to ordinary field arithmetic in $\mathbb{Q}$.
proof idea
One short tactic proof. Unfold the definition of orbit-division to expose multiplication by the reciprocal. Rewrite with the multiplication transport lemma (mul_toRat) and the reciprocal transport lemma (recip_toRat). The resulting equality is definitional in $\mathbb{Q}$, closed by rfl. No case splits and no denominator bookkeeping beyond what those two lemmas already discharge.
why it matters
This is the rational-surface transport step for division inside the PRC J-cost module. The immediate parent is canonical_rcl_surface, which states that the canonical PRC J-cost satisfies the Recognition Composition Law algebraically on nonzero ratio orbits (the rational surface of RCL, not the continuous uniqueness theorem T5). That proof rewrites both sides through toRat and needs division to match ordinary quotients.
Downstream native-cost certificates reuse the same pattern: signed-power, sign-gauge, Liouville-twist, and the selected canonical native cost all discharge reciprocal (and related) hypotheses by moving to toRat, applying this division identity or its reciprocal sibling, and returning via cross-equality. Real-character factorization also uses it inside the d'Alembert identity for rational traces, $T(xy)+T(x/y)=T(x)T(y)$.
In the forcing chain this sits under the RCL algebra that forces $J(x)=\cosh(\log x)-1$ (T5) and the self-similar fixed point $\varphi$ (T6). It does not itself prove uniqueness; it keeps the discrete rational ledger honest so those uniqueness arguments can quote field identities without leaving the orbit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.