dvdZ
plain-language theorem explainer
Divisibility of signed orbits: $a$ divides $b$ when some product $a\cdot c$ is balanced-equivalent to $b$. Cited by anyone building the integer layer of Primitive Recognition Calculus (reflexivity, transitivity, additivity). The body is a one-line existential over the balanced relation after multiplication.
Claim. For signed orbits $a,b$, write $a\mid b$ when there exists a signed orbit $c$ such that $a\cdot c$ is balanced with $b$: $(a\cdot c)_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+(a\cdot c)_{\mathrm{neg}}$.
background
Signed orbits are the PRC stand-in for integers: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-naturals, read as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their orbit lengths match under swap of signs, $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$; that is the internal equality relation on the integer layer (K4.9).
Multiplication of signed orbits is already available from the IntegerRational module. Divisibility is then the usual existential: $a$ divides $b$ if $b$ is balanced-equivalent to some multiple of $a$. The surrounding Grow.IntegerDivisibility module packages the elementary ring-of-integers facts needed before rationals and the forcing chain can talk about integer structure.
proof idea
Pure definition: unfold to an existential quantifier over a multiplier $c$, requiring that the product $a\cdot c$ stand in the balanced relation to $b$. No tactics or lemmas are invoked at the definition site; later theorems discharge the existential by exhibiting concrete multipliers (unit, zero, sums, products) and reducing via balanced-to-integer equalities.
why it matters
This is the divisibility predicate on which the whole IntegerDivisibility layer hangs. Downstream it is used by reflexivity ($a\mid a$ via the unit), transitivity (compose multipliers), additivity ($a\mid b$ and $a\mid c$ imply $a\mid b+c$), the unit divides everything, and everything divides zero. Those facts are the minimal algebraic skeleton before PRC can treat integers as a Euclidean domain and feed the later recognition calculus. It sits in Foundation, upstream of the forcing chain landmarks, and does not itself invoke $J$, $\varphi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.