le_of_sub_left_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits represent the same integer, left-substituting either into a difference does not change comparisons from a fixed lower bound: c ≤ a−b holds exactly when c ≤ a′−b. Order theorists building the PRC integer lattice cite this when transporting ≤ across balanced left inputs. The proof is a one-line composition of right-congruence of ≤ with left-congruence of subtraction under balance.
Claim. Let $c,a,a',b$ be signed orbits. If $a$ and $a'$ are balanced (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$), then $c \le a-b$ if and only if $c \le a'-b$, where $\le$ means the difference is nonnegative.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (positive and negative legs). Two signed orbits are balanced when their lengths satisfy $a.pos + b.neg = b.pos + a.neg$; this is the internal equality relation on PRC integers, defined only on $\delta$-orbit positions.
Order is defined internally: $a \le b$ means the signed-orbit difference $b-a$ is nonnegative. The underlying nonnegative order on bare logic naturals is the usual witness form $\exists k,, n+k=m$. The local module develops the full order surface on signed orbits (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations) needed before rationals and the forcing chain can treat integer comparison as closed.
Upstream, sub_congr_of_balanced_left shows that if $a$ balances $a'$, then $a-b$ balances $a'-b$. Separately, le_congr_right_of_balanced says $\le$ is insensitive to replacing the right argument by a balanced twin (proved by reducing both sides to integer comparison via toInt).
proof idea
One-line term proof. First apply left-subtraction congruence under balance: from $a$ balanced with $a'$, conclude $a-b$ balanced with $a'-b$. Feed that balance witness into right-congruence of $\le$: for fixed left argument $c$, $c \le a-b$ iff $c \le a'-b$. No further case splits or toInt rewriting appear at this layer; those live inside the two cited lemmas.
why it matters
This is a transport lemma for the signed-orbit order: subtraction on the left may replace any balanced representative without changing lower-bound comparisons. It feeds the module's integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging display equalities for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
Closing that surface is foundation work beneath Arithmetic-from-Logic and the later forcing chain (T0–T8). Without stable $\le$ under balanced rewriting, rung comparisons on the $\varphi$-ladder and mass-formula inequalities would not sit on a certified integer order. The result is pure order algebra; it does not itself force $\varphi$, eight-tick structure, or $D=3$, but it is part of the integer substrate those steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.