le_subtractions_iff_of_balanced
plain-language theorem explainer
If four pairs of signed orbits are balanced-equivalent, then the order relation between the two differences is invariant under that equivalence: a−b ≤ c−d if and only if a′−b′ ≤ c′−d′. Anyone building the internal integer order on Primitive Recognition Calculus orbits cites this congruence. The proof is a two-step term: subtract-congruence on each pair, then order-congruence on the resulting differences.
Claim. Let $a,a',b,b',c,c',d,d'$ be signed orbits. Suppose $a\sim a'$, $b\sim b'$, $c\sim c'$, and $d\sim d'$ under the balanced relation ($x.pos+y.neg=y.pos+x.neg$). Then $a-b\le c-d$ if and only if $a'-b'\le c'-d'$, where $\le$ means the difference is nonnegative.
background
In Primitive Recognition Calculus, integers are represented as signed orbits: pairs of nonnegative orbit lengths (pos, neg). Two signed orbits are balanced-equivalent when their lengths match crosswise: $a.pos + b.neg = b.pos + a.neg$. That relation is the internal integer equality, defined entirely on $\delta$-orbit positions (K4.9).
The internal order is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative. Subtraction itself is addition after negation. The local module develops the order surface on these representatives: reflexivity, transitivity, totality, trichotomy, and congruence lemmas that show order and arithmetic ignore balanced rewrites.
Upstream, sub_congr_of_balanced shows subtraction preserves balanced pairs, and le_congr_of_balanced shows the order relation is invariant under balanced rewrites of both sides. The present statement packages those two facts for difference-to-difference comparisons.
proof idea
Term-mode composition, no tactics. Apply subtract-congruence to (a,b) and (a',b') to obtain that $a-b$ is balanced with $a'-b'$; likewise for (c,d) and (c',d'). Feed those two balanced hypotheses into order-congruence, which yields the biconditional $a-b \le c-d \leftrightarrow a'-b' \le c'-d'$.
why it matters
The integer-order certificate asserts that the internal signed-orbit order surface is closed. This lemma is one of the congruence bricks that certificate depends on: without difference-order invariance under balanced rewrites, the order would depend on the choice of representative rather than on the integer class.
In the broader Recognition stack, signed orbits are the PRC realization of integers built from pure recognition structure (orbit lengths on the ledger), not from an external $\mathbb{Z}$. Congruence of order under balanced equivalence is required before one can safely treat $\le$ as a well-defined relation on the quotient. It sits with the sibling order laws (reflexivity, transitivity, antisymmetry on balanced pairs, totality, trichotomy) that close the order surface used downstream by display and certificate theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.