abs_sub_ne_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 is nonzero under exactly the same conditions. Order and certificate authors cite it to transport non-vanishing of |a−b| across balanced representatives. The proof is a one-line rewrite of the equality form of the same fact.
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|\neq 0$ if and only if $|a-b'|\neq 0$, where absolute value is the absolute difference of the two orbit coordinates.
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 $(\mathrm{pos},\mathrm{neg})$ of such positions, intended as $\mathrm{pos}-\mathrm{neg}$.
Two signed orbits are balanced when their lengths match under cross-addition: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That is the internal PRC integer relation (K4.9), defined only on $\delta$-orbit positions. Absolute value of a signed orbit is the absolute difference of its two coordinates, landing again in DistinctionNat.
The module develops the order surface on these signed orbits. The immediate upstream fact is that balanced right operands leave the absolute difference unchanged: $|a-b|=|a-b'|$ whenever $b$ and $b'$ are balanced.
proof idea
One-line wrapper. Rewrite the goal with abs_sub_eq_of_balanced_right hb, which supplies $|a-b|=|a-b'|$ from the balanced hypothesis on the right operand. Equality of the absolute values immediately yields the biconditional on non-equality to zero. No further case analysis or arithmetic is required.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\leq$, absolute difference, and nonnegativity flags). Without transport of non-vanishing across balanced representatives, the order certificate could not treat balanced pairs as interchangeable integers.
In the Recognition foundation this sits under the ledger/forcing layer that builds discrete arithmetic before the forcing chain (T0–T8) and the J-cost calculus. It is a small but necessary congruence fact: absolute distance to a fixed orbit does not see the choice of balanced representative on the right. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.