zero_mul_eq
plain-language theorem explainer
Left multiplication by the zero orbit annihilates every finite distinction orbit: 0 · a = 0. Anyone building native arithmetic or divisibility on DistinctionNat cites this as the left-zero law. The proof is induction on a, reducing the successor case via the already-proved right-identity for addition.
Claim. For every finite distinction orbit $a$, the product of the zero orbit with $a$ equals the zero orbit: $0 \cdot a = 0$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ, the Recognition-native stand-in for the naturals (K2.12). Arithmetic on these orbits is defined recursively from the generators, not imported from Mathlib Nat.
Multiplication is the usual recursive product on that inductive structure (zero times anything is zero; successor multiplies by adding). The sibling lemma add_zero_eq already records the right-identity $a + 0 = a$ as definitional equality. Successor itself is one more application of the generator, matching the Peano-style structure developed in ArithmeticFromLogic.
This module sits in the Primitive Recognition Calculus foundation layer, where orbit arithmetic is built before divisibility and primality notions are stated.
proof idea
Induction on the orbit $a$.
- Base: $a = 0$. Both sides are zero by the recursive definition of multiplication;
rflcloses. - Step: $a = \mathrm{succ}, n$ with inductive hypothesis $0 \cdot n = 0$. Unfolding multiplication turns the goal into $0 \cdot n + 0 = 0$. Rewrite with add_zero_eq (right-identity for addition) and the IH to finish.
why it matters
Native multiplication needs a left-zero law before commutativity and divisibility can be stated cleanly. Downstream, mul_comm uses this theorem in its zero case (paired with the symmetric mul_zero_eq). In OrbitDivisibility, zero_divides_iff_eq_zero rewrites a factorization $0 \cdot k = a$ via this identity to conclude $a = 0$, and unit_or_unit_of_mul_eq_prime rules out a zero factor when an orbit is prime.
Within the Recognition foundation, this is ordinary Peano bookkeeping on distinction orbits: it does not touch the forcing chain (T5–T8), the J-cost, or the phi ladder, but it keeps the arithmetic substrate of the calculus free of external Nat assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.