balanced_sub_left_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits represent the same integer, subtracting a fixed third orbit from either yields results that balance against any fourth orbit in lockstep. Order and certificate lemmas cite this to treat balanced pairs as interchangeable left operands under subtraction. The proof rewrites both sides through the toInt bridge and the subtraction identity, then substitutes the hypothesis.
Claim. Let $a,a',b,c$ be signed orbits (each a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$). If $a$ and $a'$ are balanced, i.e. $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$ (equivalently $a$ and $a'$ display the same integer), then $a-b$ is balanced with $c$ if and only if $a'-b$ is balanced with $c$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction-nats with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their orbit lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equality, defined only on $\delta$-orbit positions.
The bridge theorem states that balance agrees with equality of the conservative integer display: balanced $a,b$ iff $a.\mathrm{toInt}=b.\mathrm{toInt}$. Subtraction on signed orbits is addition of the negation, and the display identity $(a-b).\mathrm{toInt}=a.\mathrm{toInt}-b.\mathrm{toInt}$ holds by the add and negate display lemmas plus ring arithmetic.
This module builds the order surface on those signed orbits (reflexivity, transitivity, antisymmetry on balanced pairs, trichotomy, sign flags). The present lemma is a left-congruence fact for subtraction under balance, needed before specializing to comparisons against zero.
proof idea
Term-mode rewrite proof. Rewrite both sides of the goal with the balance-to-toInt characterization, then apply the subtraction display identity on each side, so the goal becomes $(a.\mathrm{toInt}-b.\mathrm{toInt}=c.\mathrm{toInt})\leftrightarrow(a'.\mathrm{toInt}-b.\mathrm{toInt}=c.\mathrm{toInt})$. Rewrite the hypothesis with the same characterization to obtain $a.\mathrm{toInt}=a'.\mathrm{toInt}$, then substitute that equality. No case splits or omega.
why it matters
Feeds the specialization that $(a-b)$ balances zero iff $(a'-b)$ does, whenever $a$ balances $a'$. That zero case is the natural language of nonnegativity and order comparisons after a difference. Both sit inside the IntegerOrder development whose certificate theorem asserts that the internal signed-orbit order surface is closed (truncated-sub, leq, absdiff, and signed-nonneg displays all wired).
In the broader Recognition stack this is bookkeeping on the integer layer beneath ledger forcing and the forcing chain, not a T5–T8 landmark itself. It keeps the PRC integer relation a congruence for subtraction so later order and mass-ladder arguments can swap balanced representatives without leaving the internal $\delta$-orbit vocabulary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.