dvdZ_trans
plain-language theorem explainer
Transitivity of divisibility on signed orbits: if a divides b and b divides c (up to balance), then a divides c. Cited when assembling the divisibility preorder on RS integers built from distinction naturals. Proof multiplies the two witnesses and reduces balance to an integer identity via toInt and a linear combination.
Claim. Let $a,b,c$ be signed orbits (integer-like pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). Write $a\mid_Z b$ when there exists a signed orbit $w$ such that $a\cdot w$ is balanced with $b$ (same recovered integer). If $a\mid_Z b$ and $b\mid_Z c$, then $a\mid_Z c$.
background
Signed orbits are the K4.6 integer carriers in the primitive recognition calculus: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as $\mathrm{pos}-\mathrm{neg}$. The recovery map toInt sends a signed orbit to an ordinary integer; two orbits are balanced when they recover the same integer (equivalently, the same underlying natural difference).
Divisibility dvdZ a b is existential: some witness $c$ makes $a\cdot c$ balanced with $b$. Multiplication of signed orbits is compatible with recovery: $(a\cdot b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$. The companion lemmas balanced_toInt_eq and balanced_of_toInt_eq convert freely between balance and equality of recovered integers.
This module sits in the Grow layer that equips those forced integers with order and divisibility structure, importing the integer-rational and integer-order developments.
proof idea
Unpack the two divisibility hypotheses to witnesses $w$ (for $a\mid b$) and $v$ (for $b\mid c$). The composite witness is the product $w\cdot v$. It remains only to show $a\cdot(w\cdot v)$ is balanced with $c$. Convert both balance hypotheses to integer equalities via balanced_toInt_eq, rewrite products with mul_toInt, then close by the integer identity obtained from the linear combination $v.\mathrm{toInt}\cdot h_w + h_v$. Finish with balanced_of_toInt_eq to return from integer equality to balance.
why it matters
Transitivity is the non-reflexive half of making dvdZ a preorder on the signed-orbit model of integers. Sibling facts in the same file (dvdZ_refl, dvdZ_add, one_dvdZ, dvdZ_zero) assemble the elementary divisibility calculus needed before rung arithmetic, mass ladders, or any number-theoretic forcing step can speak about multiples.
No downstream consumers are wired yet (used_by is empty), so the lemma is infrastructure rather than a cited link in T0–T8. It still belongs in the Foundation chain: integers are recovered from logic (IntegersFromLogic / ForcedIntegers), and divisibility is the first algebraic relation grown on top of that carrier. Without transitivity the later “divides on the phi-ladder” language cannot even be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.