mul_assoc_crossEq
plain-language theorem explainer
Associativity of multiplication on ratio orbits holds up to the internal cross-multiplication equivalence: ((a·b)·c) ~ (a·(b·c)). Anyone building the ordered field structure on PRC rational displays cites this. The proof rewrites cross-equivalence to rational equality, pushes multiplication through the verifier map, and finishes by ring on ℚ.
Claim. For any three ratio orbits $a,b,c$ (integer numerator over nonzero orbit denominator), the products $(a\cdot b)\cdot c$ and $a\cdot(b\cdot c)$ are equivalent under cross-multiplication: the signed orbits $((a\cdot b)\cdot c).\mathrm{num}\cdot(a\cdot(b\cdot c)).\mathrm{den}$ and $(a\cdot(b\cdot c)).\mathrm{num}\cdot((a\cdot b)\cdot c).\mathrm{den}$ are balanced.
background
In the Primitive Recognition Calculus, rationals are not taken as a primitive type. A ratio orbit is a pair of a signed orbit numerator and a nonzero distinction-nat denominator (K4.7). Equality of two such displays is internal: cross-multiplication equivalence says the scaled numerators balance as signed orbits (K4.10), without leaving the δ-orbit language.
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 compatible with ordinary rational multiplication. Those two bridges let algebraic identities on ℚ lift back to the internal relation.
This module builds the order surface on signed and ratio orbits. Associativity up to cross-equivalence is one of the algebraic laws needed before the order certificate can close.
proof idea
Rewrite the goal via crossEq_iff_toRat_eq, so it becomes equality of two rationals. Apply mul_toRat four times to expand both nested products into products of the three verifier values. The resulting identity on ℚ is then discharged by ring. No orbit-level case analysis is required; the verifier homomorphism does the work.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (truncated subtraction, ≤ display, absolute difference, and nonnegativity flags all match their integer readings). Without multiplication associative up to the native equivalence, the rational layer cannot support a coherent ordered-field interface inside PRC.
In the broader Recognition stack this sits in Foundation, beneath the forcing chain: the calculus that later forces J-uniqueness (T5), φ (T6), the eight-tick octave (T7), and D = 3 (T8) needs a clean internal arithmetic of ratios. The result is fully proved (no sorry); it is bookkeeping that keeps the certificate honest rather than a new physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.