zero_divides_iff_eq_zero
plain-language theorem explainer
In the finite distinction orbit, the zero position divides an orbit element a exactly when a itself is zero. Anyone building native divisibility or prime-orbit structure on DistinctionNat cites this. The proof is a two-line biconditional: left-to-right collapses via zero multiplication, right-to-left reuses that everything divides zero.
Claim. For every finite distinction-orbit position $a$, the zero orbit divides $a$ if and only if $a$ equals the zero orbit.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, carrying the native arithmetic of the primitive recognition calculus.
Native orbit divisibility is existential multiplication: $a$ divides $b$ when there exists an orbit position $k$ with $a \cdot k = b$. Upstream arithmetic already gives $0 \cdot a = 0$ for every $a$, and the companion fact that every orbit position divides zero (witnessed by the zero multiplier).
This module develops the divisibility surface on that arithmetic so it can later display as ordinary Nat divisibility while remaining native to the orbit.
proof idea
Split the biconditional. Forward: unpack the witness $k$ from divides zero $a$, rewrite the product by zero_mul_eq to obtain $0 = a$, and symmetrize. Backward: substitute $a = 0$ and apply divides_zero at zero. No induction; pure rewriting against the two zero-multiplication facts.
why it matters
Closes the zero case of native orbit divisibility, which the package theorem orbit_divisibility_certificate needs when it asserts that the divisibility surface is closed (reflexive, transitive, and displayable as Nat dvd). Without the zero-divides characterization, the native prime-orbit and nontrivial-factorization predicates would be ill-behaved at the origin of the orbit. Sits in the Foundation layer under PrimitiveRecognitionCalculus, upstream of any continuum or ledger bridge that consumes certified orbit arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.