le_of_sub_right_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits b and b' represent the same integer (they are balanced), then for any c and a the inequality c ≤ a−b holds exactly when c ≤ a−b'. Order theorists working on the PRC integer surface cite this to move the right input of a difference under the order relation. The proof is a two-step term: right-subtraction preserves balance, then right-congruence of ≤ under balance finishes it.
Claim. Let $c,a,b,b'$ be signed orbits. If $b$ and $b'$ are balanced (i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$), then $c \le a-b$ if and only if $c \le a-b'$, where $\le$ is the internal signed-orbit order ($x\le y$ means $y-x$ is nonnegative).
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (positive and negative parts). Two signed orbits are balanced when their lengths match under swap of signs: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the internal integer equality on δ-orbit positions (K4.9).
The internal order is defined by differences: $a\le b$ means the signed-orbit difference $b-a$ is nonnegative. Subtraction itself is an operation on signed orbits; the companion lemma sub_congr_of_balanced_right records that if $b\sim b'$ then $a-b\sim a-b'$.
The module builds a closed order surface on these objects (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations). The present statement is the right-input stability of $\le$ under balanced replacement inside a difference.
proof idea
Pure term proof, two applications. First apply sub_congr_of_balanced_right to the hypothesis that $b$ and $b'$ are balanced; this yields that $a-b$ and $a-b'$ are themselves balanced. Feed that balance witness into le_congr_right_of_balanced, which states that if $x\sim x'$ then $c\le x$ iff $c\le x'$. Instantiating $x:=a-b$ and $x':=a-b'$ gives the claimed biconditional.
No case splits or rewrites appear at this layer; the work is already done in the two upstream congruence lemmas (the latter reduces via toInt equality).
why it matters
Feeds the single downstream consumer integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas (truncated subtraction, $\le$ flags, absolute difference, nonnegativity) used to export the PRC integer order to the rest of the foundation stack.
Within Recognition Science this sits in the arithmetic-from-logic layer that underwrites ledger balance and the forcing chain's discrete counting structure. It does not itself touch T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$), but it is part of making the integer order a proved, not assumed, surface so later mass-ladder and tick-count arguments can treat $\le$ on signed orbits as a stable relation under balanced representatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.