abs_sub_eq_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer value), the absolute values of their differences agree. Order and certificate lemmas cite this to transport |a−b| across balanced representatives. The proof is a one-line composition of difference-congruence with absolute-value invariance under balance.
Claim. Let $a,a',b,b'$ be signed orbits (pairs of distinction-nat positions meaning $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $a'$ and $b$ with $b'$ (i.e. $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$ and likewise for $b,b'$), then $|a-b|=|a'-b'|$ as distinction-nat absolute values.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-nat positions, read as the formal difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal PRC integer equality, defined only on $\delta$-orbit positions (K4.9).
Absolute value of a signed orbit is the distinction-nat absolute difference of its positive and negative legs. Subtraction of signed orbits is the usual add-of-negate construction on those legs. The local module builds the order surface on these objects: reflexivity, totality, trichotomy, and flag characterizations of nonnegativity.
Upstream, balance is already known to be a congruence for subtraction (sub_congr_of_balanced), and absolute value depends only on the balanced class (abs_eq_of_balanced, via injectivity of the toNat embedding and equality of underlying integers).
proof idea
One-line term proof. First apply sub_congr_of_balanced to the two balance hypotheses to obtain that $a-b$ is balanced with $a'-b'$. Then feed that witness into abs_eq_of_balanced, which converts balance of signed orbits into equality of their absolute values. No further case analysis or unfolding is required.
why it matters
This is the transport law for absolute differences across balanced representatives. Downstream it discharges the rewrite steps in abs_sub_eq_zero_iff_of_balanced and abs_sub_ne_zero_iff_of_balanced, so zero/nonzero status of $|a-b|$ is invariant under balance. Those facts feed the closed integer-order surface certificate (integer_order_certificate: "The internal signed-orbit order surface is closed"), which packages display lemmas for truncated subtraction, $\le$, abs-diff, and signed nonnegativity.
In the Recognition foundation stack this sits under the ledger/forcing layer that eventually supports the forcing chain (T0–T8). It does not itself force $\phi$ or dimension; it hardens the integer arithmetic substrate on which later recognition calculus sits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.