abs_sub_eq_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (same integer value), subtracting a third orbit from each yields differences with equal absolute values. Order and certificate lemmas cite this to transport vanishing and non-vanishing of |a−b| across balanced representatives. The proof is a two-step term: left-subtraction preserves balance, then absolute value is invariant under balance.
Claim. Let $a,a',b$ be signed orbits (pairs of distinction-natural positions meaning $\mathrm{pos}-\mathrm{neg}$). If $a$ and $a'$ are balanced, i.e. $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$, then $|a-b|=|a'-b|$ as distinction-naturals.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-natural positions with intended meaning $\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, defined entirely on $\delta$-orbit positions. Absolute value of a signed orbit is the distinction-natural absolute difference of its positive and negative legs.
The IntegerOrder module builds the order surface on these signed orbits without leaving the orbit calculus. Balance is the equivalence that identifies representatives of the same integer. Upstream, left-subtraction is congruent for balance: if $a\sim a'$ then $a-b\sim a'-b$. Separately, absolute value depends only on the balanced class: balanced signed orbits have equal abs.
proof idea
Term-mode composition of two prior facts. First apply left-subtraction congruence for balance to $ha$, obtaining that $a-b$ is balanced with $a'-b$. Then feed that witness into the lemma that absolute value is invariant under balance. No further case analysis or rewriting is required.
why it matters
This is the transport law for $|\cdot-b|$ across balanced left arguments. Downstream it discharges the zero and nonzero iff forms: $|a-b|=0$ iff $|a'-b|=0$, and likewise for inequality, by a single rewrite. Those facts feed the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. In the Recognition foundation stack this keeps integer order internal to $\delta$-orbits before ledger forcing and the T0–T8 chain, so order comparisons do not smuggle external $\mathbb{Z}$ structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.