sub_not_balanced_zero_iff_of_balanced_left
plain-language theorem explainer
If two signed orbits are equivalent under internal balance, then after subtracting a third orbit one difference fails to balance with zero exactly when the other does. Order and certificate constructions cite this to transfer non-zeroness across equivalent left inputs. The proof is a one-line rewrite of the positive balance-preservation sibling.
Claim. Let $a$, $a'$, and $b$ be signed orbits. If $a$ is balanced with $a'$ (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$), then $\neg\,\mathrm{balanced}(a-b,\,0)$ if and only if $\neg\,\mathrm{balanced}(a'-b,\,0)$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-naturals (pos, neg), read as the difference pos − neg (K4.6). Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; that is the internal PRC integer equivalence, defined entirely on δ-orbit positions (K4.9).
Balance with the zero orbit detects the zero class: an orbit balances with zero exactly when it represents integer zero. Signed-orbit subtraction is the group operation used to form differences in the IntegerOrder surface.
The sibling lemma already proves that, under left-input balance, the property "difference balances with zero" is invariant in the left operand. The present statement is the negated form of that same invariance, needed wherever non-zeroness (rather than zeroness) is the predicate in play.
proof idea
One-line wrapper. Rewrite the goal with the positive sibling sub_balanced_zero_iff_of_balanced_left applied to the given left-balance hypothesis. That sibling itself is a specialization of left-input balance congruence at the zero orbit. Negating both sides of a biconditional yields the biconditional of the negated predicates, so the rewrite closes immediately.
why it matters
Used by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, ≤, absolute difference, and signed nonnegativity. Transferring non-balance-with-zero across equivalent left inputs keeps strict-inequality and nonzero tests independent of the representative chosen for the left operand.
In the Recognition foundation stack this is a congruence fact inside the ledger/integer layer that underwrites order before higher forcing (T0–T8) and the Recognition Composition Law are applied. It does not itself force φ, dimension, or the eight-tick octave; it only seals representative-independence for the signed-orbit order certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.