add_mul'
plain-language theorem explainer
The theorem establishes left distributivity of multiplication over addition for the integers obtained as the Grothendieck completion of logic-derived naturals. Foundational physicists or number theorists constructing arithmetic step-by-step from primitive distinctions would cite it when verifying ring axioms before ascending to rationals. The argument reduces both sides via the canonical embedding to the standard integers and invokes the ring axioms there.
Claim. Let $Z$ be the Grothendieck completion of the naturals arising from logical distinctions. For all $a,b,c$ in $Z$, $(a+b)c = ac + bc$.
background
LogicInt is the quotient of pairs of logic naturals under the equivalence that identifies $(p,q)$ with $(r,s)$ precisely when $p+s=q+r$, yielding the integers as the Grothendieck group completion under addition. The canonical map to the standard integers preserves both addition and multiplication, and the transfer principle states that an equality holds in LogicInt if and only if it holds after applying this map. These preservation and transfer results are the immediate upstream lemmas used here.
proof idea
The proof first invokes the transfer theorem to replace the LogicInt equality by the corresponding equality of standard integers. It then substitutes the additivity and multiplicativity of the embedding map on each occurrence of addition and multiplication. The resulting identity is discharged by the ring tactic.
why it matters
This supplies the distributive law required for the ring structure on the logic integers, which is invoked verbatim to obtain the identical law first for the logic rationals and then for the logic reals. It therefore closes one link in the chain that lifts arithmetic from the primitive distinction through integers to the reals used in the Recognition Science mass ladder and forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.