mul_add'
plain-language theorem explainer
The theorem establishes left distributivity of multiplication over addition on the integers obtained as the Grothendieck completion of the logic naturals. Foundation developers in Recognition Science cite it when verifying that the constructed integer type satisfies ring axioms. The proof is a one-line wrapper that transfers the identity to standard integers via the toInt map and applies ring normalization.
Claim. For all $a, b, c$ in the Grothendieck completion of the logic naturals, $a(b + c) = ab + ac$.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of pairs of logic naturals by the relation that equates (p, q) with (r, s) precisely when p + s = q + r. The transfer theorem states that an equality holds between two elements of LogicInt if and only if the images under the canonical map to the standard integers coincide. The supporting lemmas establish that this map preserves both addition and multiplication.
proof idea
One-line wrapper that invokes the transfer principle to reduce the goal to an equality in the integers, rewrites each operation via the preservation lemmas for addition and multiplication, and closes with the ring tactic.
why it matters
The result is invoked by the distributivity statements for the logic rationals and logic reals. It supplies the missing ring axiom at the integer layer of the foundation, enabling the arithmetic structures required for the phi-ladder and the mass formula. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.