abs_sub_eq_zero_iff_of_balanced_right
plain-language theorem explainer
If two signed orbits are balanced (internally equivalent), then the absolute difference of a third orbit from either of them vanishes under the same condition. Order and certificate authors cite it to transfer zero-distance facts across balanced representatives. The proof is a one-line rewrite of the stronger absolute-value equality for balanced right arguments.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction-orbit positions, read as $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$, then $|a-b|=0$ if and only if $|a-b'|=0$, where absolute value is the absolute difference of the two orbit components.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is a pair of such positions, intended as $\mathrm{pos}-\mathrm{neg}$. Absolute value of a signed orbit is the absolute difference of those two components, landing again in DistinctionNat.
Two signed orbits are balanced when their lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That is the internal PRC integer relation (K4.9), defined entirely on $\delta$-orbit positions, not on external integers.
The immediate upstream fact is absolute-value equality under balanced right arguments: if $b\sim b'$, then $|a-b|=|a-b'|$ as distinction orbits. The present statement only needs the zero case of that equality.
proof idea
One-line wrapper. Rewrite the goal with abs_sub_eq_of_balanced_right hb, which already gives $(a-b).\mathrm{abs}=(a-b').\mathrm{abs}$. Equality of the two absolute values immediately yields the biconditional that either equals zero. No further case analysis or induction.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). Zero absolute difference is the equality witness in that order surface; transferring it across balanced representatives keeps the certificate independent of which balanced form is chosen.
Locally this sits in the IntegerOrder layer of PRC foundation work: building a total order and absolute-value calculus on signed distinction orbits before external $\mathbb{Z}$ is introduced. It does not itself touch T5–T8 or the Recognition Composition Law; it is ledger-side scaffolding for integer structure forced from recognition primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.