sub_not_balanced_zero_iff_of_balanced
plain-language theorem explainer
Under signed-orbit balance, non-vanishing of a difference is invariant when either operand is replaced by a balanced partner. Order work on the PRC integer layer cites this for the strict (nonzero) half of difference-balance transport. The proof is a one-line rewrite of the positive balance-to-zero equivalence.
Claim. Let $a,a',b,b'$ be signed orbits (each a pair of distinction lengths read as $\mathrm{pos}-\mathrm{neg}$). If $a$ balances $a'$ and $b$ balances $b'$ in the sense $x.\mathrm{pos}+y.\mathrm{neg}=y.\mathrm{pos}+x.\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 integer layer, a signed orbit is a pair of distinction lengths $(\mathrm{pos},\mathrm{neg})$, intended as the formal difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits balance when their lengths satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that relation is the internal PRC integer equivalence, defined entirely on $\delta$-orbit positions (K4.9).
Subtraction of signed orbits is the natural componentwise operation on those pairs. Balancing against the zero orbit is the internal test that a difference vanishes. The companion result sub_balanced_zero_iff_of_balanced already transports the positive statement: under balanced inputs, $a-b$ balances zero exactly when $a'-b'$ does. The present lemma is the negated form of that transport, needed wherever order or trichotomy arguments speak in terms of nonzero differences rather than zero ones.
The surrounding module builds the order surface on these signed orbits (reflexivity, transitivity, antisymmetry on the balance class, totality, sign flags). Ledger-level balance from LedgerForcing is a separate notion (balanced event lists) and is not used in the argument here.
proof idea
One-line wrapper. Rewrite the goal with the positive companion sub_balanced_zero_iff_of_balanced applied to the same balance hypotheses on the two pairs; classical negation then yields the stated biconditional. No new arithmetic on distinction lengths is performed.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\leq$, absolute difference, and signed nonnegativity flags; the nonzero-difference transport is part of keeping those order facts well-defined on balance classes rather than on raw orbit representatives.
In the Recognition foundation stack this sits inside the PRC integer/rational scaffolding that precedes the forcing chain (T0–T8). It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only stabilizes the integer order surface so later recognition calculus can treat signed differences up to balance without representative dependence. No open sorry is involved: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.