mul_assoc
plain-language theorem explainer
Multiplication of PRC integers is associative. Anyone building ring or monoid structure on the signed-orbit quotient cites this. The proof is a short term argument: inject the equality into ℤ via the display map and invoke ordinary integer associativity.
Claim. For all PRC integers $a,b,c$ (quotient classes of signed orbits under the balanced-length relation), $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
background
PRC integers are the quotient of signed orbits by the internal balanced-length setoid. A signed orbit is a pair of positive/negative orbit lengths; the display toInt sends a representative to an ordinary integer difference of natural lengths. Multiplication is defined at the orbit level so that it respects the quotient, and the companion lemma mul_toInt records that the display intertwines PRC multiplication with Mathlib integer multiplication.
This module sits in the Primitive Recognition Calculus layer that rebuilds ℤ and ℚ from orbit arithmetic without classical choice at the integer level. Upstream, ArithmeticFromLogic.toNat_mul already recovers ordinary natural multiplication from the logic-native naturals; the signed and ratio constructions lift that recovery to ℤ and ℚ displays.
The local goal is the standard monoid/ring axioms on the quotient type, so that later cost algebra and φ-ring constructions can treat PRC integers as an ordinary associative multiplicative structure.
proof idea
One short term proof. Apply injectivity of the integer display toInt on the quotient, reducing the claimed equality of PRC products to an equality in ℤ. Then simp with Mathlib's Int.mul_assoc (and the intertwining lemmas such as mul_toInt already available in the namespace) finishes: the displayed products associate because ordinary integers associate.
why it matters
Associativity is the monoid axiom that every downstream multiplicative structure on PRC integers needs. It is used heavily: CostAlgebra builds CommSemigroup / CommMonoid instances for shifted carriers whose mul_assoc obligations route through this fact; PhiRing packages ℤ[φ] pairs whose integer coordinates inherit associative multiplication; CosmogenesisSim rewrites flow products with ← mul_assoc in conservation steps; GapWeight and AlphaGenesis resummation proofs multiply integer and real quantities that ultimately rest on this foundation.
In the Recognition chain this is scaffolding under the arithmetic layer that feeds J-cost algebra and the φ-ladder, not a forcing step (T5–T8) itself. It closes the K4.8 integer quotient as a genuine associative multiplicative type so later modules need not re-prove orbit-level association.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.