sub_congr_of_balanced_right
plain-language theorem explainer
If two signed orbits agree under the internal balance relation, right-subtraction from a fixed signed orbit preserves that agreement. Order and comparison lemmas cite this to treat balanced right operands as interchangeable under subtraction. The proof is a one-line specialization of two-sided subtraction congruence after reflexivity of balance on the left operand.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$ (equivalently $b.\mathrm{toInt}=b'.\mathrm{toInt}$), then $a-b$ and $a-b'$ are balanced.
background
In the Primitive Recognition Calculus, a SignedOrbit is a pair of distinction naturals with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their orbit lengths satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equivalence; the bridge theorem states it is equivalent to equality of the conservative integer displays $a.\mathrm{toInt}=b.\mathrm{toInt}$.
Subtraction on signed orbits is defined via addition after negation. The two-sided congruence already shows that if both pairs of operands are balanced, the differences are balanced. The present statement is the right-operand specialization used throughout the integer-order surface: when only the subtrahend changes within a balance class, the difference stays in one balance class.
This sits in the IntegerOrder module, which builds the order, comparison, and absolute-value layer on signed orbits from the IntegerRational primitives, without classical choice on the balance-to-integer bridge.
proof idea
Reflexivity of balance on the left operand is obtained by rewriting with the characterization that balance is equivalent to equal integer displays, so $a$ is balanced with itself. The two-sided theorem is then applied: balanced left pair $(a,a)$ and the given balanced right pair $(b,b')$ yield balance of $\mathrm{sub},a,b$ with $\mathrm{sub},a,b'$. The two-sided result itself unfolds subtraction and chains addition congruence with negation congruence.
why it matters
Right-subtraction congruence is the workhorse that lets the order surface treat balanced subtrahends as interchangeable. Downstream it feeds absolute-value equality of right differences, both left and right comparison stability under right-subtraction, and the corresponding $\le$ and $<$ iff lemmas for right inputs. Those lemmas are part of closing the internal signed-orbit order surface recorded by the integer-order certificate.
In the Recognition foundation this is bookkeeping on the PRC integer layer (K4.6–K4.9), not a forcing-chain step. It keeps order and comparison well-defined on balance classes before any passage to $\mathbb{Z}$, so later ledger and gap constructions can use signed differences without depending on a particular representative of the right operand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.