abs_sub_eq_of_balanced_right
plain-language theorem explainer
Absolute value of a signed-orbit difference is invariant when the subtracted operand is replaced by any balanced (integer-equivalent) representative. Order and certificate lemmas cite this so that |a−b| depends only on the integer class of b. The proof is a one-line composition of right-subtraction congruence with absolute-value invariance under balance.
Claim. Let $a,b,b'$ be signed orbits (each a pair of nonnegative orbit positions, read as $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, meaning $p_b+n_{b'}=p_{b'}+n_b$, then $|a-b|=|a-b'|$, where absolute value is the absolute difference of the two orbit positions of the difference.
background
In the Primitive Recognition Calculus, integers are not postulated: they are signed orbit differences. A SignedOrbit is a pair of distinction-nat positions $(\mathrm{pos},\mathrm{neg})$, intended as $\mathrm{pos}-\mathrm{neg}$. Two such pairs are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal PRC integer-equivalence relation, defined only on $\delta$-orbit positions.
Absolute value of a signed orbit is the distinction-nat absolute difference of its two legs. Subtraction of signed orbits is the corresponding componentwise operation. The local module builds the order surface on these objects: reflexivity, totality, trichotomy, and sign flags all live here.
Upstream, balance of the right operands lifts through subtraction: if $b\sim b'$ then $a-b\sim a-b'$. Separately, balanced signed orbits have equal absolute values. Those two facts are the only inputs.
proof idea
Term-mode one-liner. First apply right-subtraction congruence: balance of $b$ and $b'$ yields balance of $a-b$ and $a-b'$. Then feed that balanced pair into absolute-value invariance under balance, which concludes $|a-b|=|a-b'|$. No case splits and no arithmetic beyond those two lemmas.
why it matters
This is a small but load-bearing congruence for the internal integer order. Downstream it discharges the zero and nonzero absolute-difference equivalences under right balance, so vanishing of $|a-b|$ is well-defined on integer classes of $b$. It is also listed among the ingredients of the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the broader Recognition stack this sits in Foundation, under the ledger and forcing layer that eventually feeds the T0–T8 chain. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only keeps the signed-orbit model of $\mathbb{Z}$ coherent so later forcing steps can treat integer order as already certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.