mul_zero_eq
plain-language theorem explainer
Right-multiplication by the zero orbit annihilates every finite distinction orbit: a·0 = 0. Anyone building native arithmetic or divisibility on DistinctionNat cites this identity. The proof is pure definitional reflexivity from the recursive clause of orbit multiplication.
Claim. For every finite distinction orbit $a$, one has $a \cdot 0 = 0$, where $0$ is the zero orbit and $\cdot$ is the recursively defined multiplication of orbits.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, isomorphic in shape to the Peano naturals but carrying the Recognition-Science reading of successive distinction steps rather than bare counting.
This module equips those orbits with addition and multiplication defined by recursion on the second argument, parallel to the usual Nat arithmetic. The zero clause of multiplication is written so that any orbit times zero is definitionally zero; the successor clause accumulates repeated addition.
Upstream, only the inductive type itself is required. Sibling lemmas already establish the corresponding additive facts (add_zero_eq, zero_add_eq, and the cancellation and toNat bridge lemmas).
proof idea
One-line definitional proof: rfl. The recursive definition of orbit multiplication has the clause a * zero := zero, so the equality holds by reduction with no further lemmas or induction.
why it matters
This is the right-zero law that every later arithmetic and divisibility argument on orbits needs. Downstream it discharges the zero cases of mul_comm and succ_mul_eq, seeds the base step of toNat_mul (K4.7: verifier display of orbit multiplication matches Lean Nat), and supplies the witness in divides_zero. It also appears in mul_one_eq and in the zero-exclusion branch of unit_or_unit_of_mul_eq_prime ("if an orbit is prime, every native factorization has a unit factor").
In the broader Primitive Recognition Calculus, these orbit laws are the discrete substrate on which later forcing and cost structure sit; without a clean zero law the native ring-like structure and the prime-orbit theory cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.