sub_not_balanced_zero_iff_not_balanced
plain-language theorem explainer
Negation form of the signed-orbit balance identity: a−b fails to balance zero exactly when a fails to balance b. Order and certificate lemmas cite it when they need the unbalanced case without unfolding subtraction. Proof is a one-line rewrite of the positive biconditional.
Claim. For signed orbits $a,b$ (each a pair of distinction-natural lengths meaning $\mathrm{pos}-\mathrm{neg}$), $\neg\,\mathrm{balanced}(a-b,0)$ if and only if $\neg\,\mathrm{balanced}(a,b)$, where $\mathrm{balanced}(x,y)$ means $x_{\mathrm{pos}}+y_{\mathrm{neg}}=y_{\mathrm{pos}}+x_{\mathrm{neg}}$.
background
In the Primitive Recognition Calculus integer layer, a SignedOrbit is a difference of two distinction-natural orbit lengths (intended meaning $\mathrm{pos}-\mathrm{neg}$). Two signed orbits are balanced when their lengths match under the internal PRC integer relation $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$; that is the equality that later becomes integer equality after the toInt embedding.
The sibling theorem sub_balanced_zero_iff_balanced already states the positive form: $a-b$ balances zero exactly when $a$ balances $b$. That identity is proved by transporting both sides through balanced_iff_toInt_eq, using sub_toInt and zero_toInt. The present declaration is the negated biconditional needed by order facts that speak in terms of strict inequality or unbalanced pairs.
Local setting is the IntegerOrder module: building a closed order surface on signed orbits (reflexivity, totality, trichotomy, sign flags) entirely from δ-orbit data, without external ℤ axioms.
proof idea
One-line wrapper. Rewrite the goal with the positive sibling sub_balanced_zero_iff_balanced a b; classical negation of both sides of a proved iff is then definitional. No further case splits or toInt unfolding occur here.
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, ≤, absolute difference, and nonnegativity flags; the unbalanced-subtraction form is the dual needed when order proofs reason about failure of balance rather than success.
In the Recognition foundation stack this sits under the ledger/forcing layer that eventually supports the T0–T8 chain: balanced ledgers and integer order on distinction orbits are the discrete substrate before J-cost uniqueness (T5), φ (T6), the eight-tick octave (T7), and D=3 (T8). The lemma itself is pure integer-order plumbing, not a physics claim, but it closes a dual case so the certificate can assert a complete order surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.