mul_assoc'

The ambient type is the primitive-recognition rational: a quotient of ratio-orbit displays by the cross-multiplication setoid on orbit-level numerator and denominator (nonzero denominator). Multiplication is the induced operation on those classes, already shown well-defined upstream.

This module packages the field axioms for that type. Sibling lemmas cover additive associativity, zero laws, and positivity; the present statement is the multiplicative counterpart. Parallel associativity results exist one level down on the integer and distinction-nat carriers, and one level up on the logic-rational and logic-real carriers, each proved by transport to a classical ring and a ring identity.

One-line wrapper: apply the existing mul_assoc lemma on PRCRat to the three arguments. No new algebra is performed here; the work sits in the upstream proof, which injects into the integer carrier and invokes ordinary integer associativity.

The declaration is a named field of the rational-field certificate in the same module, which bundles commutativity, associativity, units, and inverses into a single structure. Downstream, the same pattern is mirrored for logic integers, logic rationals, logic reals, and the Loom matrix core, so the certificate can be reused when lifting the recognition calculus toward the real continuum and the forcing chain. It does not itself touch J-cost, phi, or the eight-tick octave; it only secures the multiplicative monoid law required before those analytic layers.