mul_comm_crossEq
plain-language theorem explainer
Multiplication of ratio orbits is commutative up to the internal cross-multiplication equivalence. Anyone assembling the ordered-field layer on PRC rationals cites this. The proof rewrites through the rational display map and finishes by ring on ordinary rational products.
Claim. For any two ratio orbits $a$ and $b$ (integer numerator over nonzero orbit denominator), the products $a\cdot b$ and $b\cdot a$ are cross-equivalent: their cross-multiplied numerator-denominator pairs balance as signed orbits, equivalently their rational displays agree.
background
A ratio orbit is the PRC display of a rational: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence is the internal equality relation on these displays: two ratio orbits match when the scaled pairs $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ and $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ balance as signed orbits (K4.10).
The verifier map toRat sends each ratio orbit to an ordinary rational. Upstream, cross-equivalence is proved equivalent to equality of those displays, and multiplication of ratio orbits is proved to intertwine with ordinary rational multiplication.
This module builds the integer/rational order surface on those orbit displays. Commutativity of multiplication up to cross-equivalence is a basic algebraic identity needed before reciprocal and order certificates can close.
proof idea
Rewrite the goal with the bridge crossEq_iff_toRat_eq, so it becomes equality of rational displays. Apply mul_toRat on each side to replace the displays of the two products by ordinary products of displays. The resulting identity $a_{\mathbb{Q}}\cdot b_{\mathbb{Q}}=b_{\mathbb{Q}}\cdot a_{\mathbb{Q}}$ is discharged by ring.
why it matters
This is the commutativity law for the PRC rational product, stated entirely in orbit language. Downstream it is applied directly in recip_product_comm_crossEq_recip_product (reciprocal of a product commutes under cross-equivalence) and in several nonzero reciprocal-pair lemmas that rearrange products of reciprocals. Those identities feed the closed integer-order certificate, which packages the signed-orbit order surface as complete. Within Recognition Science this sits in the Primitive Recognition Calculus foundation: before J-cost uniqueness (T5) and the forcing chain can talk about ratios of costs, the internal rational arithmetic must already be commutative and well-defined on δ-orbit positions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.