mul_comm'
plain-language theorem explainer
Multiplication commutes on LogicInt, the Grothendieck completion of LogicNat under addition. Researchers constructing the arithmetic hierarchy in Recognition Science cite this to confirm the ring axioms before lifting to rationals and reals. The proof is a one-line wrapper that transfers the claim via eq_iff_toInt_eq and toInt_mul then closes with the ring tactic.
Claim. For all $a, b$ in the Grothendieck completion of the natural numbers under addition, $a · b = b · a$.
background
LogicInt is the quotient of pairs of LogicNat under the equivalence (a,b) ~ (c,d) iff a + d = b + c, realizing the Grothendieck completion under addition. The module IntegersFromLogic builds these integers directly from logical naturals to support the Recognition Science derivation of arithmetic operations. The key upstream results are eq_iff_toInt_eq, stating that an equation holds in LogicInt iff it holds after applying toInt, and toInt_mul, showing that toInt preserves multiplication.
proof idea
The proof is a one-line wrapper. It rewrites the goal using eq_iff_toInt_eq to reduce to an equality of ordinary integers, applies toInt_mul on both sides to reach toInt a * toInt b = toInt b * toInt a, and invokes the ring tactic to conclude commutativity.
why it matters
This theorem supplies the commutativity axiom for the ring structure on LogicInt and is invoked directly by the corresponding mul_comm' statements in RationalsFromLogic and RealsFromLogic. It forms part of the chain that embeds standard arithmetic into the logic-derived number systems, supporting the forcing chain from T0 to T8. No open questions attach to this specific result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.