toRat_mul'
plain-language theorem explainer
Multiplication of PRC rationals is preserved by the verifier display into ordinary rationals: the display of a product is the product of the displays. Field-identity and Cauchy/completion arguments on the PRC rational layer cite this homomorphism law. The proof is a one-line simp wrapper over the quotient and display definitions.
Claim. For any two PRC rationals $a$ and $b$ (nonzero-denominator ratio-orbit quotient classes), the verifier display into $\mathbb{Q}$ satisfies $\widetilde{a \cdot b} = \tilde{a} \cdot \tilde{b}$.
background
PRC rationals are the K4.8 quotient of ratio orbits by the cross-multiplication setoid: two displays represent the same class when numerators and denominators cross-multiply at the orbit level, with nonzero denominators. The type is Quot ratioOrbitSetoid.
The verifier display sends a ratio orbit to an ordinary rational by dividing the integer lift of the numerator by the natural lift of the denominator. Spec tag A5 treats this as a transport wrapper whose internal characterization is cross-multiplication; the same display lifts to the quotient of PRC rationals.
This module sits in the Primitive Recognition Calculus foundation, building integer and rational arithmetic from orbit data before real completion. Multiplicativity of the display is the bridge that lets ordinary rational field tactics certify PRC identities.
proof idea
One-line wrapper: simp unfolds the quotient multiplication and the display on representatives and reduces both sides to the same product of integer/natural lifts in $\mathbb{Q}$. No separate lemma application is required; the simp set already knows that the display respects the ratio-orbit setoid and that multiplication is defined pointwise on numerators and denominators.
why it matters
This is the multiplicative half of the display homomorphism used throughout the PRC rational field and real layers. Downstream, toRat_div rewrites division via this law and the inverse display; div_mul_cancel and mul_div_cancel apply injectivity of the display after rewriting with it and field_simp. PRCSquareGap_toRat expands the square-gap cost into ordinary rationals using the same multiplicativity. Real completion uses the dual ofRat_mul, and the J-cost distance-increment triangle target builds explicit PRC rationals whose displays must multiply correctly. In the broader RS stack this keeps the K4 rational layer honest before T5 J-uniqueness and the forcing chain rely on cost arithmetic over completed scalars.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.