balanced_negate_iff
plain-language theorem explainer
Negating both signed orbits preserves balance: the negated pair is balanced exactly when the original pair is. Order and integer-display lemmas in the Primitive Recognition Calculus cite this when comparisons are pushed through a global sign flip. The proof rewrites both sides to integer equality, applies the negate-to-integer identity, and closes with omega.
Claim. For signed orbits $a$ and $b$ (each a pair of distinction-natural lengths with intended value $\mathrm{pos}-\mathrm{neg}$), the pair $(-a,-b)$ is balanced if and only if $(a,b)$ is balanced, where balance means $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$ (equivalently $a$ and $b$ display the same integer).
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-natural lengths with intended meaning $\mathrm{pos}-\mathrm{neg}$. Pointwise negation swaps the two components, so the integer display of the negated orbit is the ordinary additive inverse of the original display.
Two signed orbits are balanced when their orbit lengths satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equivalence; the bridge theorem states it agrees with equality of the conservative $\mathbb{Z}$ displays. The present module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags).
Upstream, the ledger-level balance notion is separate: a ledger is balanced when its event list is balanced. Here balance is the K4.9 orbit relation, not the ledger predicate.
proof idea
Term-mode rewrite proof. First rewrite both sides of the biconditional with the bridge that balance is equivalent to equality of integer displays. Then rewrite each display of a negated orbit via the identity that negation sends the integer display to its additive inverse. The goal reduces to $-x=-y\leftrightarrow x=y$ on $\mathbb{Z}$, which omega discharges.
why it matters
Sign-flip invariance of balance is a small but necessary coherence fact for the internal integer order. Downstream, the comparison-swap lemma uses it when relating $\mathrm{cmp}(-b,-a)$ to $\mathrm{cmp}(a,b)$, and the integer-order certificate packages the closed order surface (nonnegativity displays, truncated subtraction, absolute difference) that this family of lemmas supports.
In the Recognition foundation stack this sits under the Primitive Recognition Calculus integer layer that feeds ledger forcing and the later forcing chain, not under T5–T8 directly. It closes a local algebraic obligation so the signed-orbit order can be treated as a genuine $\mathbb{Z}$-like order under negation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.