abs_sub_ne_zero_iff_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (internally equivalent), then subtracting a third orbit yields a nonzero absolute value for one if and only if it does for the other. Order and certificate machinery cites this to treat balanced representatives interchangeably when testing nonzero residual. The proof is a one-line rewrite through absolute-value equality under left-balanced subtraction.
Claim. Let $a$, $a'$, and $b$ be signed orbits (pairs of distinction-orbit positions, read as $\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|\neq 0$ if and only if $|a'-b|\neq 0$, where $|\cdot|$ is the absolute value on signed orbits (absolute difference of the two legs) and $0$ is the zero distinction orbit.
background
In the Primitive Recognition Calculus, integers are not postulated; they are built from distinction orbits. DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is a pair of such orbits, intended as $\mathrm{pos}-\mathrm{neg}$. Absolute value maps a signed orbit to a plain distinction orbit via absolute difference of the two legs.
Balance is the internal PRC integer relation: two signed orbits $a,a'$ are balanced when $a.pos+a'.neg=a'.pos+a.neg$. That is the equivalence that makes the signed-orbit surface behave like integers without importing $\mathbb{Z}$. Subtraction of signed orbits is defined so that congruence under balance is available on the left argument.
The immediate upstream fact is absolute-value equality under left-balanced subtraction: if $a$ and $a'$ are balanced, then $|(a-b)|=|(a'-b)|$. The present statement is the nonzero-test form of that equality, which order lemmas need when they only care whether a residual vanishes.
proof idea
One-line wrapper. Rewrite the goal with abs_sub_eq_of_balanced_left applied to the balance hypothesis. That lemma already gives $|(a-b)|=|(a'-b)|$ via abs_eq_of_balanced after left-congruence of subtraction under balance; once the absolute values are definitionally equal, the two inequalities against distinction-orbit zero are identical.
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). Without transport of the nonzero residual across balanced left representatives, the certificate could not treat equivalent signed orbits as interchangeable in order tests.
In the Recognition foundation stack this sits inside the Primitive Recognition Calculus integer layer: building order and residual tests on $\delta$-orbits before ledger forcing and the T0–T8 chain. It is local plumbing, not a forcing landmark, but it closes a congruence gap that the order certificate packages for downstream integer-order use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.