abs_sub_eq_zero_iff_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (internally equivalent as pos/neg pairs), then the absolute residual after left subtraction vanishes for one representative exactly when it vanishes for the other. Certificate and order machinery cite this to treat zero absolute difference as well-defined on the balance class. The proof is a one-line rewrite from the stronger fact that left balance preserves the absolute residual entirely.
Claim. Let $a$, $a'$, and $b$ be signed orbits (each a pair of distinction-orbit positions, read as $\mathrm{pos}-\mathrm{neg}$). Suppose $a$ and $a'$ are balanced: $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\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 and $0$ is the zero distinction orbit.
background
Primitive Recognition Calculus builds integer-like structure from distinction orbits rather than classical Peano naturals. A distinction orbit 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}$.
Two signed orbits are balanced when $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$. That relation is the internal PRC integer equivalence, stated entirely on orbit positions. Absolute value of a signed orbit is the absolute difference of its positive and negative components, returning a distinction orbit.
This module develops the order surface on signed orbits. Upstream, left balance already preserves absolute residuals in full: if $a$ balances $a'$, then $|a-b|=|a'-b|$ for every $b$. The present statement is the zero-specialization of that invariance.
proof idea
One-line wrapper. Rewrite the biconditional goal with the upstream equality that left balance preserves absolute residual after subtraction. Once $|a-b|=|a'-b|$ is in place, either side equals the zero distinction orbit exactly when the other does; no further case analysis is required.
why it matters
Used by the integer-order certificate, which asserts that the internal signed-orbit order surface is closed. That certificate packages display facts for truncated subtraction, order comparison, absolute difference, and nonnegativity flags. Zero-detection of absolute residual must be stable under choice of balanced left representative, or the order surface would depend on orbit presentation rather than the integer class.
The result sits in the foundation layer that constructs integer structure from recognition orbits before the forcing chain (T0–T8), the recognition composition law, and the derived constants are applied. It does not itself touch mass ladders or coupling bands; it only seals a well-definedness step on the order surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.