sub_congr_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (same integer value), subtracting a fixed third orbit from both preserves balance. Order and comparison lemmas for left-input subtraction cite this congruence. The proof is a short tactic: reflexivity of balance on the fixed operand, then the two-sided subtraction congruence.
Claim. Let $a$, $a'$, and $b$ be signed orbits (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $a'$ (equivalently $a$ and $a'$ have the same integer display), then $a-b$ is balanced with $a'-b$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the difference $\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; it agrees with equality of the conservative $\mathbb{Z}$ display via the bridge balanced_iff_toInt_eq.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags, and subtraction-stable comparisons). The two-sided predecessor states that if $a\sim a'$ and $b\sim b'$ under balance, then $a-b\sim a'-b'$. The present result is the left-input specialization: only the minuend varies, the subtrahend is fixed.
proof idea
Instantiate the two-sided subtraction congruence with the same right operand twice. Reflexivity of balance on $b$ is obtained by rewriting with the characterization that balance is equivalent to equal integer displays (so $b.\mathrm{toInt}=b.\mathrm{toInt}$). Then apply the two-sided lemma to the given left balance hypothesis and that reflexive right balance.
why it matters
Left-input stability of balance under subtraction is the workhorse for every order fact that treats $a-b$ while $a$ is only known up to balance. Downstream it feeds absolute-value equality of left-substituted differences, both directions of comparison and $\le$/$\lt$ congruence for left-input subtraction, and ultimately the closed integer-order certificate that packages the signed-orbit order surface.
In the Recognition foundation this sits inside the ledger/PRC integer layer that underwrites discrete counting before the forcing chain (T5–T8) and continuum structure. It does not itself force $\phi$ or dimension; it keeps the internal integer order coherent so later recognition calculus can treat differences without leaving the $\delta$-orbit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.