balanced_subtractions_iff_of_balanced
plain-language theorem explainer
If four pairs of signed orbits are balanced (same integer display), then the difference of the first pair balances the difference of the third pair exactly when the primed differences do. Authors of the integer-order certificate cite this to move balance across subtraction without leaving the δ-orbit surface. The proof is a short rewrite chain through the toInt bridge and the subtraction display law.
Claim. Let $a,a',b,b',c,c',d,d'$ be signed orbits (each a pair of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). Write $x\sim y$ when $x$ and $y$ are balanced, i.e. $x.{\rm pos}+y.{\rm neg}=y.{\rm pos}+x.{\rm neg}$. If $a\sim a'$, $b\sim b'$, $c\sim c'$, and $d\sim d'$, then $a-b\sim c-d$ if and only if $a'-b'\sim c'-d'$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Balance of two signed orbits is the internal integer relation $a.{\rm pos}+b.{\rm neg}=b.{\rm pos}+a.{\rm neg}$ (K4.9): equal orbit lengths after swapping the negative legs. It is defined entirely on δ-orbit positions, with no external $\mathbb{Z}$ assumed a priori.
The bridge theorem states that balance agrees with equality of the verifier integer display: $a\sim b$ if and only if $a.{\rm toInt}=b.{\rm toInt}$. Subtraction of signed orbits is realized by adding the negation, and the display law $(a-b).{\rm toInt}=a.{\rm toInt}-b.{\rm toInt}$ holds by the add and negate display lemmas plus a ring identity.
This module builds the order surface on those signed orbits (reflexivity, transitivity, antisymmetry on balanced pairs, trichotomy, sign flags). The present lemma is the congruence of balance under pairwise subtraction, needed so that order facts stated on one representative transfer to any balanced twin.
proof idea
Term-mode rewrite proof. Unfold both sides of the target biconditional with the bridge balanced_iff_toInt_eq, then replace each of the four subtractions by the display law sub_toInt. That reduces the claim to
$(a.{\rm toInt}-b.{\rm toInt}=c.{\rm toInt}-d.{\rm toInt})\leftrightarrow(a'.{\rm toInt}-b'.{\rm toInt}=c'.{\rm toInt}-d'.{\rm toInt})$.
Rewrite the four balance hypotheses with the same bridge, then substitute those integer equalities into the reduced goal. No case split and no classical choice.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity; congruence of balance under subtraction is part of keeping those displays well-defined on equivalence classes of balanced orbits.
In the Recognition foundation this sits inside the Primitive Recognition Calculus integer layer: integers are not imported as a primitive type but recovered as balanced signed δ-orbits. Closing order and arithmetic on that surface is a prerequisite for later ledger and forcing arguments that treat net imbalance as canonical momentum (the balanced ground state being the $\sigma=0$ cost-vanishing point). The lemma does not itself force dimension or the J-cost; it is pure integer-surface hygiene.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.