sub_balanced_zero_iff_balanced
plain-language theorem explainer
Two signed orbits balance exactly when their difference balances against zero. Order lemmas and the integer-order certificate in the primitive recognition calculus cite this to turn vanishing-difference checks into the native balance relation. The proof rewrites both sides through the integer display bridge and closes by linear arithmetic on ℤ.
Claim. For signed orbits $a$ and $b$ (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), the difference $a-b$ is balanced with the zero orbit if and only if $a$ is balanced with $b$.
background
In the primitive recognition calculus, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That is the internal PRC integer relation (K4.9), stated entirely on $\delta$-orbit positions.
A bridge theorem equates this relation with equality of verifier integer displays: balance holds iff the two orbits map to the same integer. Subtraction is compatible with that display, $(a-b).\mathrm{toInt}=a.\mathrm{toInt}-b.\mathrm{toInt}$, and the zero orbit displays as $0$.
This module builds the order surface on signed orbits. The lemma translates "the difference vanishes" into the native balance predicate, so later order facts need not leave the internal representation.
proof idea
Rewrite both sides with the bridge that balance is equality of integer displays. The left side becomes $(a-b).\mathrm{toInt}=\mathrm{zero}.\mathrm{toInt}$. Apply the subtraction display identity to replace the left with $a.\mathrm{toInt}-b.\mathrm{toInt}$, and the zero display to replace the right with $0$. Apply the bridge again on the right-hand claim so it reads $a.\mathrm{toInt}=b.\mathrm{toInt}$. Finish with omega on the resulting integer equality.
why it matters
Used by the integer-order certificate that closes the internal signed-orbit order surface, by the negated form that rewrites non-balance of a difference, and by the self-difference identity (any orbit minus itself balances zero). In the Recognition foundation stack this is PRC integer bookkeeping: it keeps equality-to-zero checks choice-free and internal to $\delta$-orbit data before any external $\mathbb{Z}$ is trusted. It is not itself a forcing-chain step (T0–T8), but it stabilizes the integer layer those later constructions sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.