abs_sub_eq_zero_iff_balanced
plain-language theorem explainer
The absolute value of a signed-orbit difference vanishes exactly when the two orbits are balanced (same integer display). Order and certificate lemmas cite this as the zero test for the internal PRC integer relation. The proof rewrites through the toInt bridge and finishes by omega on the integer equality.
Claim. For signed orbits $a,b$ (each a pair of distinction-orbit positions meaning $\mathrm{pos}-\mathrm{neg}$), $|a-b|=0$ if and only if $a$ and $b$ are balanced, i.e. $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$ (equivalently $a$ and $b$ have the same integer display).
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction-orbit positions with intended meaning $\mathrm{pos}-\mathrm{neg}$. Absolute value is the orbit-position absolute difference of those components. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$: the internal PRC integer relation, defined entirely on $\delta$-orbit positions (K4.9).
The bridge to the conservative $\mathbb{Z}$ view is that balance holds exactly when the integer displays agree: $\mathrm{balanced},a,b\leftrightarrow a.\mathrm{toInt}=b.\mathrm{toInt}$. Separately, a signed orbit has absolute value zero iff its integer display is zero. Subtraction of signed orbits is compatible with $\mathrm{toInt}$ via $\mathrm{sub_toInt}$.
This module builds the order surface on those signed orbits; the present lemma is the zero characterization of the difference absolute value in that surface.
proof idea
Term-mode rewrite chain, then omega. First rewrite the left side with $\mathrm{abs_eq_zero_iff_toInt_eq_zero}$, so $|a-b|=0$ becomes $(a-b).\mathrm{toInt}=0$. Then apply $\mathrm{sub_toInt}$ to replace the difference display by $a.\mathrm{toInt}-b.\mathrm{toInt}$. Finally rewrite the right side with $\mathrm{balanced_iff_toInt_eq}$, turning balance into $a.\mathrm{toInt}=b.\mathrm{toInt}$. The remaining integer goal $a.\mathrm{toInt}-b.\mathrm{toInt}=0\leftrightarrow a.\mathrm{toInt}=b.\mathrm{toInt}$ is discharged by omega.
why it matters
Closes the zero test for signed-orbit differences on the internal order surface. Immediate consumers are the negated form ($|a-b|\neq 0$ iff not balanced) and the reflexivity fact $|a-a|=0$. Both feed the broader integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation stack this is bookkeeping for the PRC integer layer (K4.6–K4.9), not a forcing-chain step: it ensures the absolute-difference display is a faithful null test for the balance relation before order and certificate lemmas rely on it. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.