mul_assoc'
plain-language theorem explainer
Multiplication is associative on the integers obtained as the Grothendieck completion of logic naturals. Researchers constructing the rational and real rings from the same logic base cite this result to close the ring axioms at the integer level. The proof is a one-line wrapper that transfers the claim via the toInt embedding and hands the resulting integer identity to the ring tactic.
Claim. For all elements $a, b, c$ in the Grothendieck completion of the logic naturals, multiplication satisfies $(a b) c = a (b c)$.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of pairs of logic naturals by the equivalence $(p, q) ~ (r, s)$ when $p + s = q + r$. Multiplication is defined on this quotient so that the structure becomes a ring. The transfer principle eq_iff_toInt_eq states that an equality holds in LogicInt precisely when the images under the canonical map toInt coincide in the ordinary integers. The companion lemma toInt_mul shows that toInt preserves multiplication, making it a ring homomorphism.
proof idea
The proof is a one-line wrapper. It rewrites the goal with eq_iff_toInt_eq, applies toInt_mul four times to push every product inside toInt, and lets the ring tactic discharge the resulting associativity statement on ordinary integers.
why it matters
This result is invoked by the mul_assoc' theorems for LogicRat and LogicReal, completing the ring axioms at each successive number system. It supplies the arithmetic foundation required for the Recognition Science constructions that lift operations from logic naturals through integers to support the J-function, phi fixed point, and eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.