zero_mul
plain-language theorem explainer
Zero times any element of the natural numbers forced by the Law of Logic equals zero. Arithmetic developers in the Recognition framework cite this when establishing ring structure on the logic-derived naturals. The proof is a direct induction on the second factor that reduces the successor case via the multiplication successor rule and the zero addition identity.
Claim. For every element $n$ of the natural numbers forced by the Law of Logic, the product of the zero element with $n$ equals the zero element.
background
The module derives natural-number arithmetic from the Recognition functional equation. The natural numbers forced by the Law of Logic form an inductive type whose identity constructor is the zero-cost element and whose step constructor iterates the generator, mirroring the orbit under multiplication by the self-similar fixed point. The zero element is this identity constructor. Multiplication is defined so that the successor rule rewrites a product involving a successor as the prior product plus the first factor.
proof idea
The proof applies induction on the second argument. The identity base case holds by reflexivity. The successor case rewrites the left-hand side with the multiplication successor theorem, replaces the recursive product by the induction hypothesis, and finishes with the zero addition theorem.
why it matters
Nineteen downstream results invoke this lemma, among them the PhiInt structure in the algebra layer and d'Alembert classification theorems in the cost axioms. It supplies a basic ring axiom needed to reach the phi-ladder and the eight-tick octave from the Recognition Composition Law. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.