divides_zero
plain-language theorem explainer
Every finite distinction orbit divides the zero orbit under native orbit multiplication. Anyone building divisibility or prime factorization on the δ-orbit will cite this absorption law. The proof is a one-line existential witness: multiply by zero and invoke the mul-zero identity.
Claim. For every finite distinction orbit $a$, $a$ divides the zero orbit: there exists an orbit $k$ such that $a \cdot k = 0$.
background
DistinctionNat is the inductive type of base-neutral finite orbits of repeated distinction (K2.12), with constructors zero and succ. It is the carrier for the Primitive Recognition Calculus arithmetic developed in this module family.
Native orbit divisibility is the relation divides a b, defined as existence of an orbit $k$ with $a \cdot k = b$. Multiplication on orbits is the arithmetic imported from OrbitArithmetic; in particular the identity $a \cdot 0 = 0$ holds definitionally for every $a$.
The local setting is the divisibility layer on top of that arithmetic: units, nontrivial factorizations, and prime orbits are sibling notions in the same file.
proof idea
One-line wrapper. The existential in the definition of divides is witnessed by $k = 0$. The required equality $a \cdot 0 = 0$ is exactly mul_zero_eq a, supplied by exact.
why it matters
Closes the zero-absorption half of orbit divisibility. The immediate parent is zero_divides_iff_eq_zero, which uses this fact (together with the dual zero-mul identity) to prove that zero divides $a$ if and only if $a$ is zero. That characterization keeps the later prime-orbit and factorization predicates from treating zero as a nontrivial factor. In the Recognition foundation stack this is pure arithmetic scaffolding under the Primitive Recognition Calculus, not yet a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.