toRat_mul
plain-language theorem explainer
The verifier display from PRC rationals to ordinary rationals preserves multiplication. Anyone assembling ring laws on logic-built rationals, or transporting order and continuity facts down to Mathlib ℚ, cites this. Proof is double quotient induction that reduces to the orbit-level identity mul_toRat.
Claim. For PRC rationals $a,b$ (quotient classes of ratio orbits), the ordinary-rational display of the product equals the product of the displays: $\mathrm{toRat}(a\cdot b)=\mathrm{toRat}(a)\,\mathrm{toRat}(b)$.
background
PRC rationals (K4.8) are the quotient of ratio orbits by the cross-multiplication setoid. A ratio orbit (K4.7) is a signed-orbit numerator over a nonzero distinction-nat denominator. The display toRat on a ratio orbit is the ordinary fraction $(\mathrm{num.toInt}:\mathbb{Q})/(\mathrm{den.toNat}:\mathbb{Q})$; it descends to the quotient as a conservative verifier map (spec tag A5: transport wrapper, internal content is cross-multiplication).
Multiplication on ratio orbits multiplies numerators and denominators componentwise. The orbit-level theorem mul_toRat already records that this product is preserved by the display, using SignedOrbit.mul_toInt and DistinctionNat.toNat_mul together with nonzero denominator casts. The present result lifts that identity through the quotient.
proof idea
Term-style tactic proof. Apply Quot.induction_on to both arguments, reducing to representatives a,b : RatioOrbit. The show step rewrites quotient multiplication as RatioOrbit.mul. The goal is then exactly RatioOrbit.mul_toRat a b, which is applied directly. No further algebra is done at the quotient level.
why it matters
Supplies the multiplicative half of the A5 transport so PRC rationals can talk to Mathlib ℚ while staying internally cross-multiplicative. Downstream, RationalsFromLogic uses it (with the additive twin) to discharge ring laws such as mul_assoc', mul_comm', mul_add', and add_mul' via eq_iff_toRat_eq. On the real side it is simp-fuel for PRCBoundednessDelta_toRat (evaluating the 1/8 bound), for order-congruence lemmas in RealOrderCongruence, and for the bounded-continuity target in RealProductContinuity. Those continuity and order facts sit under the foundation ladder that later supports J-cost geometry (T5 uniqueness of $J$, RCL) once reals are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.