one_dvdZ
plain-language theorem explainer
The unit signed orbit divides every signed orbit under the recognition-integer divisibility relation. Anyone assembling the ordered ring structure on signed orbits cites this as the unit law for divisibility. The proof takes the cofactor to be the dividend itself and reduces balance to integer equality via the toInt homomorphism.
Claim. For every signed orbit $a$, the multiplicative unit $1$ divides $a$: there exists a signed orbit $c$ such that $1\cdot c$ is balanced with $a$ (i.e. they represent the same integer).
background
Signed orbits are the K4.6 model of recognition integers: a pair (pos, neg) of distinction-naturals, read as the difference pos - neg. The map toInt sends a signed orbit to that integer difference in $\mathbb{Z}$. Two signed orbits are balanced when they have the same toInt (equivalently the same underlying nonnegative magnitude after cancellation).
Divisibility dvdZ a b is the existence of a cofactor $c$ such that mul a c is balanced with $b$. Multiplication is compatible with toInt: (mul a b).toInt = a.toInt * b.toInt, and the unit satisfies one.toInt = 1. This module grows the usual divisibility lattice on that integer model, importing the signed-orbit arithmetic and order layers.
proof idea
Witness the cofactor as $a$ itself. It remains to show mul one a is balanced with $a. Apply balanced_of_toInt_eq, which reduces balance to equality of toIntvalues. Rewrite withmul_toIntandone_toIntto obtain1 * a.toInt = a.toInt, then close by omega`.
why it matters
This is the unit law in the divisibility theory of recognition integers: every element is a multiple of $1$. It sits beside the sibling facts dvdZ_refl, dvdZ_trans, dvdZ_add, and dvdZ_zero that assemble a preorder compatible with the additive structure. No downstream consumers are wired yet in the graph; the lemma is infrastructure for later unique factorization, gcd, and rung-arithmetic arguments in the Primitive Recognition Calculus. In the broader RS forcing chain it supports the integer substrate on which eight-tick and $\varphi$-ladder constructions eventually rest, without itself invoking T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.