abs_sub_eq_zero_iff_of_balanced
plain-language theorem explainer
Absolute value of a signed-orbit difference vanishes exactly when it vanishes for any balanced pair of representatives. Authors of the Primitive Recognition Calculus integer-order surface cite this when transporting zero-difference across the internal integer equivalence. The proof is a one-line rewrite of the absolute-value congruence already proved for balanced pairs.
Claim. Let $a,a',b,b'$ be signed orbits (each a pair of distinction-orbit positions, read as $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ in the sense $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$ (and likewise for $b,b'$), then $|a-b|=0$ if and only if $|a'-b'|=0$, where $|\cdot|$ is the distinction-orbit absolute difference of the two parts.
background
In the Primitive Recognition Calculus, integers are built from distinction orbits rather than from a primitive $\mathbb{Z}$. A DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A signed orbit is a pair of such positions, intended as $\mathrm{pos}-\mathrm{neg}$. Its absolute value is the absolute difference of those two positions, again a distinction orbit.
Two signed orbits are balanced when their lengths match under swap of signs: $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$. That relation is the internal PRC integer equivalence (K4.9), defined entirely on $\delta$-orbit positions. Subtraction of signed orbits is the natural difference of those pairs.
The immediate upstream fact is that absolute value of a difference is invariant under balanced replacement of both arguments: if $a\sim a'$ and $b\sim b'$, then $|a-b|=|a'-b'|$. The present statement specializes that equality to the zero case as a biconditional.
proof idea
One-line wrapper. Rewrite the goal with the upstream congruence abs_sub_eq_of_balanced applied to the two balance hypotheses. That lemma already shows $|a-b|=|a'-b'|$ by composing subtraction-congruence for balanced pairs with absolute-value congruence for balanced pairs; equality of the two absolute values immediately yields the zero-iff-zero form.
why it matters
The declaration sits in the integer-order layer of the Primitive Recognition Calculus and is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, order predicates, absolute difference, and nonnegativity flags on signed orbits.
Without a transport of the zero-absolute-difference predicate across balance, the order surface could not treat balanced representatives as interchangeable when testing whether two signed orbits coincide. The result is pure foundation bookkeeping: it does not invoke the forcing chain (T5–T8), the Recognition Composition Law, or the $\varphi$-ladder, but it keeps the internal integer model coherent so later recognition calculus can sit on a closed order theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.