le_sub_left_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits a and a' are balanced (same integer), then a−b ≤ c if and only if a'−b ≤ c. Order theorists building the internal PRC integer lattice cite this when transporting inequalities across left-input replacements in a difference. The proof is a one-line term: left-congruence of ≤ under balance applied to the balanced pair (a−b, a'−b).
Claim. Let $a,a',b,c$ be signed orbits. If $a$ and $a'$ are balanced (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$), then $a-b\le c$ if and only if $a'-b\le c$, where $\le$ means the difference is nonnegative.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg). Two signed orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; this is the internal integer equality relation, defined only on $\delta$-orbit positions (K4.9).
The order on signed orbits is defined by $a\le b$ iff $b-a$ is nonnegative. Subtraction is the corresponding signed-orbit operation. The module builds a closed order surface on these internal integers, independent of any external $\mathbb{Z}$ embedding at the interface level.
Upstream, le_congr_left_of_balanced already says balanced left arguments may be swapped under $\le$. Separately, sub_congr_of_balanced_left says that if $a\sim a'$ then $a-b\sim a'-b$. The present lemma composes those two facts.
proof idea
One-line term proof. First apply sub_congr_of_balanced_left to the hypothesis $a\sim a'$ to obtain $a-b\sim a'-b$. Feed that balanced pair into le_congr_left_of_balanced with right argument $c$, which rewrites the left slot of $\le$ and yields the biconditional.
why it matters
This is a transport lemma for the internal signed-orbit order: inequalities involving a left difference are invariant under replacing the minuend by any balanced representative. It feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display and flag lemmas (nonnegativity, truncated subtraction, abs-diff) that seal the order layer of the PRC integer construction.
In the broader Recognition foundation, integers and their order arise from recognition calculus rather than being postulated. Closing congruence of $\le$ under balanced left subtraction is a small but necessary step toward a self-contained arithmetic substrate beneath the forcing chain (T0–T8) and the ledger calculus. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.