dvdZ_add
plain-language theorem explainer
If a signed orbit divides two others in the balanced-product sense, it divides their sum. Anyone assembling the integer ring laws on signed orbits (or the divisibility preorder used later in the Grow layer) cites this. The proof takes the two quotient witnesses, adds them, and checks the product identity after transporting balancedness through the integer embedding.
Claim. Let $a,b,c$ be signed orbits (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$). Write $a\mid b$ when there exists a witness $w$ such that $a\cdot w$ is balanced with $b$ (same integer value under the embedding). If $a\mid b$ and $a\mid c$, then $a\mid (b+c)$.
background
Signed orbits are the K4.6 integer carrier in the Primitive Recognition Calculus: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the difference $\mathrm{pos}-\mathrm{neg}$. The map toInt sends such a pair to $\mathbb{Z}$, and addition and multiplication on signed orbits are defined componentwise so that they intertwine with ordinary integer arithmetic (add_toInt, mul_toInt).
Two signed orbits are balanced when they represent the same integer. The local divisibility relation dvdZ is existential: $a$ divides $b$ when some witness $c$ makes $a\cdot c$ balanced with $b$. The companion lemmas balanced_toInt_eq and balanced_of_toInt_eq identify balancedness with equality of toInt images, so divisibility statements can be checked after embedding into $\mathbb{Z}$.
This module sits in the Grow layer of the foundation stack and builds the usual divisibility facts (refl, trans, add, one, zero) on that carrier before higher arithmetic is available.
proof idea
Unpack the two divisibility hypotheses to witnesses $w$ and $v$ with $a\cdot w$ balanced to $b$ and $a\cdot v$ balanced to $c$. Propose $w+v$ as the witness for $a\mid(b+c)$. Reduce the required balancedness goal to an equality of toInt values via balanced_of_toInt_eq. Convert the two balanced hypotheses the other way with balanced_toInt_eq, rewrite both sides using mul_toInt and add_toInt, and finish by linear_combination of the two integer identities (distributivity $a(w+v)=aw+av$ in $\mathbb{Z}$).
why it matters
This is one of the elementary closure laws for the signed-orbit divisibility preorder (dvdZ_refl, dvdZ_trans, one_dvdZ, dvdZ_zero are siblings). It is pure foundation arithmetic: no Recognition Composition Law, J-cost, or forcing-chain step is invoked. The parent use sites are not yet wired (used_by is empty), so the lemma presently exists to complete the standard divisibility toolkit on the K4.6 carrier before later Grow constructions consume it. In the broader RS stack it is scaffolding for integer structure underneath the phi-ladder and mass formulas, not a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.