sub_not_balanced_zero_iff_of_balanced_right
plain-language theorem explainer
If two signed orbits are balanced (internally equivalent), then subtracting either from a fixed orbit yields a nonzero difference exactly when the other does. Order and certificate authors cite this to transport nonzeroness across equivalent right operands. The proof is a one-line rewrite of the positive balanced-zero equivalence under the same hypothesis.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction lengths meaning $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$, then $a-b$ fails to balance with zero if and only if $a-b'$ fails to balance with zero.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: a structure with two distinction-length components, read as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal PRC integer relation, defined entirely on $\delta$-orbit positions (K4.9).
Subtraction of signed orbits is the natural difference on those components. Balancing against the zero orbit is the internal test that a difference is the zero integer. The companion result states that if the right operands are balanced, then $a-b$ balances with zero exactly when $a-b'$ does.
This module builds the order surface on those signed orbits (reflexivity, transitivity, antisymmetry up to balance, trichotomy, and sign-flag characterizations). The present lemma is the negated form of right-operand invariance for the zero test.
proof idea
One-line wrapper. Rewrite the goal with the positive companion sub_balanced_zero_iff_of_balanced_right at the same balanced-right hypothesis. Negation of both sides of a biconditional is definitional once that equivalence is in place; no further case split or arithmetic is required.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). Nonzeroness of differences must be stable under replacing a right operand by any balanced representative; without that, order and sign flags would depend on presentation rather than on the integer class.
In the Recognition foundation this sits inside the ledger and PRC integer layer that underwrites later forcing (T0–T8). It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only seals a presentation-invariance step needed for a coherent integer order before those landmarks are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.