dvdZ_zero
plain-language theorem explainer
Every signed orbit divides the zero orbit under balanced-multiplication divisibility. Algebraists building the Primitive Recognition Calculus integer layer cite this as the zero-absorption law for that relation. The proof supplies the zero multiplier and reduces balance to an integer identity via the multiplicative toInt map, closed by omega.
Claim. For every signed orbit $a$ (a difference of distinction naturals, intended as an integer), $a$ divides the zero orbit: there exists a signed orbit $c$ such that the product $a\cdot c$ is balanced with zero. Balance means equal integer images under the canonical map to $\mathbb{Z}$.
background
Signed orbits are the PRC stand-in for integers: a structure with positive and negative distinction-natural parts, read as $\mathrm{pos}-\mathrm{neg}$. The zero orbit is the pair with both parts zero, and its integer image is $0$.
Divisibility on this type is defined existentially: $a$ divides $b$ when some multiple $a\cdot c$ is balanced with $b$. Balance is the equality relation induced by the integer embedding (equal toInt values). Multiplication is compatible with that embedding: $(a\cdot b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$.
The local module assembles elementary divisibility facts (reflexivity, transitivity, additivity, unit divides everything) on top of the integer-rational and integer-order imports.
proof idea
Witness the existential with the zero orbit as multiplier. It remains to show $a\cdot 0$ is balanced with $0$. Apply the lemma that equal integer images imply balance, then rewrite the product image by the multiplicative toInt law and the fact that zero maps to $0$. The resulting integer goal $a.\mathrm{toInt}\cdot 0=0$ is discharged by omega.
why it matters
Closes the zero case in the PRC Grow integer-divisibility suite alongside reflexivity, transitivity, additivity, and the unit law. No downstream consumers are wired yet; the lemma is infrastructure for treating signed orbits as a divisibility monoid before rationals and the broader forcing chain. It does not itself touch J-uniqueness, phi, the eight-tick octave, or $D=3$, but supplies the arithmetic substrate those layers eventually rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.