abs_sub_ne_zero_iff_not_balanced
plain-language theorem explainer
The absolute value of a signed-orbit difference is nonzero exactly when the two signed orbits fail to balance. Order and certificate lemmas in the primitive recognition calculus cite this to separate the zero class from genuine distinctions. The proof is a one-line rewrite of the equality form of the same equivalence.
Claim. For signed orbits $a$ and $b$, $|a-b| \neq 0$ if and only if $a$ and $b$ are not balanced, where balance means $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$ and absolute value is the orbit-position absolute difference of the signed components.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction-orbit positions (pos, neg), read as the formal difference pos - neg. Two signed orbits are balanced when their lengths match under cross-addition: a.pos + b.neg = b.pos + a.neg. That relation is the internal integer equality on δ-orbit data (K4.9).
Absolute value of a signed orbit is the distinction-orbit absolute difference of its positive and negative legs. The zero of that absolute value is the base-neutral orbit zero. The sibling result states that |a - b| = 0 exactly when a and b are balanced; the present statement is the negated form of that biconditional.
The local module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Balance is the equality kernel of that order.
proof idea
One-line wrapper. Rewrite with the converse of the sibling biconditional |a - b| = 0 ↔ balanced a b, which itself reduces via absolute-value-to-integer, subtraction-to-integer, and balance-to-integer equalities, then closes by omega. Negating both sides of that equivalence yields the nonzero form.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, ≤, absolute difference, and nonnegativity flags). Without the nonzero characterization, the certificate cannot cleanly separate balanced pairs from strict order comparisons.
In the Recognition foundation stack this sits under the ledger and forcing layer: balance is the internal equality that ledger balance (event-list balance) eventually rests on. It is bookkeeping for the integer order used before the J-cost and forcing chain (T5–T8) appear, not a physics claim itself. It closes a small but necessary gap in the order surface rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.