sub_balanced_zero_iff_of_balanced_left
plain-language theorem explainer
If two signed orbits are balance-equivalent, subtracting a third orbit hits zero for one representative exactly when it hits zero for the other. Order and certificate lemmas cite this to move zero-difference facts across the balance relation. The proof is a one-line specialization of the general left-input balance transport for subtraction, fixing the right-hand side to zero.
Claim. Let $a$, $a'$, and $b$ be signed orbits (each a pair of distinction-natural lengths, read as $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $a'$, meaning $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$, then $a-b$ is balanced with zero if and only if $a'-b$ is balanced with zero.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: a structure SignedOrbit with two distinction-natural components pos and neg, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are related by the internal balance predicate when their lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the PRC integer equivalence, defined entirely on $\delta$-orbit positions (K4.9).
Subtraction of signed orbits is the natural difference operation on those pairs. Being balanced with zero means the difference is the zero class in this internal arithmetic: the orbit is equivalent to the zero signed orbit under balance.
The immediate upstream fact is the general left-input transport lemma: if $a$ is balanced with $a'$, then for any right operand $b$ and any comparison target $c$, $a-b$ is balanced with $c$ exactly when $a'-b$ is. The present statement is that lemma with $c$ fixed to zero. (A separate ledger-level balanced predicate on event lists is in scope via imports but is not the relation used here.)
proof idea
One-line term wrapper. Instantiate the general theorem balanced_sub_left_input_iff_of_balanced at comparison target $c=\mathrm{zero}$, feeding the given balance hypothesis on the left inputs. No extra rewriting is needed: the general lemma already rewrites both sides through balanced_iff_toInt_eq and sub_toInt, so the zero specialization inherits that integer-level equality transport automatically.
why it matters
This is a small but load-bearing transport fact for the signed-orbit order surface. It is used directly by the companion negation form (sub_not_balanced_zero_iff_of_balanced_left), which rewrites non-balance-with-zero across left balance, and it sits in the dependency cone of integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation stack, PRC integer order is scaffolding for later forcing and ledger structure: zero-tests after subtraction are how nonnegativity, sign flags, and trichotomy are expressed on orbits. Without left-input invariance of the zero class under balance, those order displays would depend on the choice of representative. The lemma closes that gap for the zero target specifically, matching the certificate's signed-nonneg and flag display obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.