lt_sub_right_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits are balanced (integer-equivalent), swapping the right operand of subtraction leaves the strict comparison against any third orbit unchanged: a−b < c iff a−b′ < c. Builders of the PRC integer order surface cite this when transporting inequalities across representatives. The proof is a one-line composition of left-congruence for strict order with right-congruence of subtraction under balance.
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 < c$ if and only if $a-b' < c$, where $<$ is the internal strict order (nonnegative difference and not balanced).
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit positions encoding positive and negative parts. Two signed orbits are balanced when their lengths match crosswise, $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$. That relation is the internal integer equality, defined entirely on $\delta$-orbit positions (K4.9).
Strict order on signed orbits is the conjunction of the weak order with failure of balance: $a < b$ means $a \le b$ and $\neg,\mathrm{balanced}(a,b)$. Subtraction is the corresponding signed-orbit difference. The IntegerOrder module develops the order laws needed so that these representatives behave like ordinary integers under comparison.
Upstream, right-congruence of subtraction under balance already yields that $a-b$ is balanced with $a-b'$ whenever $b$ is balanced with $b'$. Separately, left-congruence of strict order says balanced left operands may be swapped in any $<$ comparison. This lemma joins those two facts.
proof idea
One-line term proof. First apply right-congruence of subtraction under balance to the hypothesis that $b$ is balanced with $b'$, obtaining that $a-b$ is balanced with $a-b'$. Feed that balanced pair into left-congruence of strict order, which rewrites the left operand of $<$ and yields the desired biconditional against $c$.
why it matters
The declaration is a transport lemma on the signed-orbit order surface: inequalities involving a difference remain stable when the subtracted representative is replaced by any balanced partner. It is consumed by the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display and flag lemmas (nonnegativity, absolute difference, truncated subtraction) into a single closure witness for the PRC integer layer.
In the broader Recognition foundation, integers and their order are not imported from classical arithmetic; they are forced from ledger balance and orbit structure. Congruence lemmas of this kind are the glue that lets later forcing steps (T5–T8 and the mass ladder) treat signed-orbit comparisons as well-defined integer facts rather than representative-dependent accidents. Without right-input stability of $<$ under subtraction, the certificate could not honestly claim a closed order surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.