le_sub_right_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits are balanced (integer-equivalent), swapping the right operand of subtraction for its twin leaves the order relation to a third orbit unchanged: a−b ≤ c iff a−b′ ≤ c. Anyone assembling the PRC integer order or rewriting under balance would cite this. The proof is a one-line composition of left-order congruence with right-subtraction balance preservation.
Claim. Let $a,b,b',c$ be signed orbits. If $b$ and $b'$ are balanced, meaning $b_{\mathrm{pos}}+b'_{\mathrm{neg}}=b'_{\mathrm{pos}}+b_{\mathrm{neg}}$, then $a-b\le c$ if and only if $a-b'\le c$, where $\le$ is the internal order ($x\le y$ iff $y-x$ is nonnegative).
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg) standing for a directed count. Two signed orbits are balanced when their lengths satisfy $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$; this is the internal equivalence that identifies the same integer without leaving the $\delta$-orbit language.
Order is defined internally: $a\le b$ means the difference $b-a$ is nonnegative. Subtraction is the corresponding signed-orbit operation. The module builds a full order theory on these carriers so that later certificates can treat the integer surface as closed.
Upstream, right-subtraction preserves balance: if $b\sim b'$ then $a-b\sim a-b'$. Separately, left congruence of order says balanced left operands may be swapped under $\le$. Those two facts are the only inputs here.
proof idea
One-line term proof. First apply right-subtraction balance congruence to the hypothesis $b\sim b'$, obtaining $a-b\sim a-b'$. Feed that balanced pair into left-order congruence, which rewrites $x\le c$ under a balanced change of the left operand $x$. The result is exactly $a-b\le c\leftrightarrow a-b'\le c$.
why it matters
This is a small but necessary rewrite lemma in the signed-orbit order toolkit. It lets later arguments replace a right subtraction operand by any balanced representative without reopening the order goal. Downstream it is consumed by the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed": the certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags. Without right-input stability of $\le$ under balance, that closure package would have a hole whenever subtraction appears on the left of an order atom. In the broader foundation stack this sits under Arithmetic-from-Logic and Ledger forcing, where balanced ledgers and LogicNat order are the coarser ancestors of the signed-orbit relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.