negativeFlag_eq_of_balanced
plain-language theorem explainer
Balanced signed orbits share the same negativity flag. Anyone building the internal integer order on δ-orbits cites this when transporting sign data across the balance relation. The proof unfolds the flag as Boolean negation of the nonnegative flag and rewrites by the companion nonnegative-flag congruence.
Claim. If two signed orbits $z$ and $w$ are balanced, meaning $z_{\mathrm{pos}}+w_{\mathrm{neg}}=w_{\mathrm{pos}}+z_{\mathrm{neg}}$, then their negativity flags agree: $z$ is strictly negative if and only if $w$ is.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-natural lengths $(p,n)$, read as the formal difference $p-n$. Two signed orbits are balanced when their lengths satisfy the internal integer relation $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$. That relation is the PRC stand-in for equality of the underlying integers.
The nonnegative flag is a Boolean structural test on a signed orbit; the negativity flag is defined as its Boolean negation ("strict negativity as failure of the structural nonnegative flag"). The companion result already shows that balance preserves the nonnegative flag. This module builds the internal order surface on those flags so that $\le$ and sign behave like ordinary integer order without leaving the δ-orbit language.
proof idea
Term-mode, two steps. Unfold the negativity flag to the Boolean negation of the nonnegative flag. Rewrite by the companion theorem that balance preserves the nonnegative flag; the two negations then agree. No case split is needed here because the hard work sits in the nonnegative companion.
why it matters
This is the sign half of balance-invariance for the internal integer order. Downstream it is the workhorse for negativity-flag congruence under multiplication and subtraction: products and differences of balanced pairs keep the same negativity flag, and scaling by a nonzero pure orbit leaves the flag unchanged. Those lemmas feed the closed certificate that "the internal signed-orbit order surface is closed," which packages display equalities for truncated subtraction, $\le$, absolute difference, and the signed nonnegative tests. In the broader Recognition stack this sits in the foundation layer that forces integer arithmetic from δ-orbit data before the T0–T8 forcing chain attaches continuum structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.