le_of_sub_inputs_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (integer-equivalent), a fixed orbit sits below their difference exactly when it sits below the difference of the replacements. Order-surface builders in the primitive recognition calculus cite this when transporting ≤ across representatives. The proof is a one-line composition of right-congruence for ≤ with congruence of subtraction under balance.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$ and likewise for $b,b'$), then $c \le a-b$ if and only if $c \le a'-b'$, where $\le$ means the difference is nonnegative.
background
In the primitive recognition calculus, integers are carried by signed orbits: pairs of δ-orbit lengths (positive and negative parts). Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; that is the internal integer equivalence, defined only on orbit positions (K4.9).
The internal order is defined by $a \le b$ iff the difference $b-a$ is nonnegative. Subtraction is built from addition and negation on signed orbits. The local module develops the order laws needed so this surface is well-defined on equivalence classes, not just on raw representatives.
Upstream, right-congruence already says that if $b$ is balanced with $b'$ then $a \le b$ iff $a \le b'$. Separately, subtraction preserves balance: balanced inputs yield balanced differences. Those two facts are the only inputs here.
proof idea
Term-mode one-liner. First apply congruence of subtraction under balance to the two hypotheses, obtaining that $a-b$ is balanced with $a'-b'$. Feed that witness into right-congruence of $\le$: replacing the right-hand argument of $\le$ by a balanced partner yields an iff. No case split and no unfolding of toInt at this layer.
why it matters
This lemma is one of the transport laws that let the signed-orbit order descend to integer classes. 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 equalities for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the Recognition foundation stack, arithmetic is forced from logic rather than assumed. Closing order under balanced representatives is a necessary step before the φ-ladder mass formula and the forcing chain (T0–T8) can treat integers as unique up to the internal relation. Without this iff, inequalities involving differences would depend on which balanced representative was chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.