abs_sub_ne_zero_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced under the internal integer relation, the absolute difference of the first pair is nonzero exactly when that of the second pair is. Integer-order and order-certificate arguments cite this to move non-vanishing of absolute differences across balanced representatives. The proof is a one-line rewrite from equality of those absolute differences under balance.
Claim. Let $a,a',b,b'$ be signed orbits (each a pair of distinction-orbit positions, read as positive minus negative). If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$ and likewise for $b,b'$), then $|a-b|\neq 0$ if and only if $|a'-b'|\neq 0$, where absolute value is the orbit-position absolute difference of the two components.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A signed orbit is a pair of such positions, intended as positive minus negative. Absolute value of a signed orbit is the absolute difference of those two components, again as a distinction-orbit position.
Two signed orbits are balanced when their lengths match under swap of signs: $a.pos + b.neg = b.pos + a.neg$. That is the internal PRC integer equivalence, defined only on $\delta$-orbit positions (K4.9). Subtraction of signed orbits is the corresponding componentwise difference operation used to form $|a-b|$.
The immediate upstream fact is that balanced pairs have equal absolute differences after subtraction: if $a$ balances $a'$ and $b$ balances $b'$, then $|a-b|=|a'-b'|$. The present statement is the non-vanishing form of that equality.
proof idea
One-line wrapper. Rewrite the goal with the upstream equality abs_sub_eq_of_balanced applied to the two balance hypotheses. Equality of the absolute differences immediately yields the biconditional for inequality with zero; no further case split is needed.
why it matters
This lemma sits in the integer-order layer of Primitive Recognition Calculus: it lets non-vanishing of $|\cdot|$ travel across balanced representatives, so order and sign facts do not depend on which balanced lift is chosen.
It 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, $\leq$, absolute difference, and signed nonnegativity flags. Without transport of $|a-b|\neq 0$ under balance, the certificate could not treat balanced signed orbits as interchangeable for order.
In the broader Recognition stack this is foundation scaffolding for integer structure on distinction orbits, not yet a forcing-chain (T0–T8) step; it underwrites the discrete order surface that later mass and rung constructions sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.