mul_eq_zero
plain-language theorem explainer
LogicInt, the Grothendieck completion of LogicNat, has no zero divisors. Foundation researchers cite this when establishing ring properties for cost algebras, J-cost Laplacians, and frequency ladders. The tactic proof reduces both directions to the corresponding fact on Int via the toInt isomorphism, then invokes Int.mul_eq_zero and transfers back with eq_iff_toInt_eq.
Claim. Let $a, b$ be elements of LogicInt, the Grothendieck completion of LogicNat under addition. Then $a · b = 0$ if and only if $a = 0$ or $b = 0$.
background
LogicInt is the quotient of LogicNat × LogicNat by the setoid equivalence that completes LogicNat under addition. The map toInt recovers the corresponding element of Int, and eq_iff_toInt_eq states that an equality holds in LogicInt precisely when the images under toInt coincide. Upstream results supply toInt_mul, which preserves multiplication, and toInt_zero, which identifies the zero element. This theorem sits inside the IntegersFromLogic module that constructs arithmetic directly from the logic primitives.
proof idea
The tactic proof opens with constructor. The forward direction maps the hypothesis via toInt_mul and congrArg to obtain an integer equation, applies Int.mul_eq_zero, then transfers each case back with eq_iff_toInt_eq and toInt_zero. The reverse direction uses rintro on the disjunction, substitutes the zero cases, and simplifies the resulting products with toInt_mul followed by ring.
why it matters
This result supplies the integral-domain property required by downstream theorems including costRateEL_implies_const_one (Euler-Lagrange rigidity), J_eq_iff_eq_or_inv (level-set classification for J), laplacian_form_zero_imp (zero-form constancy), and phi_unique_self_similar (self-similar fixed point). It closes a necessary step in the ring structure that supports the Recognition forcing chain from T0 through T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.