nonnegFlag_sub_eq_of_balanced_right
plain-language theorem explainer
If two signed orbits are balanced (same integer value), subtracting either from a fixed orbit yields differences with identical nonnegative flags. Authors of the internal integer-order certificate cite this to show the flag is invariant under right subtraction of equivalents. The proof is a one-line composition of right-subtraction congruence with flag equality under balance.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, meaning $b_{\mathrm{pos}}+b'_{\mathrm{neg}}=b'_{\mathrm{pos}}+b_{\mathrm{neg}}$, then the structural nonnegative flag of $a-b$ equals that of $a-b'$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ standing for the formal difference $\mathrm{pos}-\mathrm{neg}$. 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}}$; this is the PRC equivalence that identifies the same integer without leaving the $\delta$-orbit language.
The nonnegative flag is the computable Boolean obtained by structural comparison $\mathrm{leq}(\mathrm{neg},\mathrm{pos})$. It is the discrete stand-in for "$z\ge 0$" on signed orbits. The IntegerOrder module builds the order surface on these flags and on balance, so that later certificates can treat the order as closed and displayable.
Upstream, balance already implies equal nonnegative flags, and right subtraction preserves balance: if $b\sim b'$ then $a-b\sim a-b'$. Those two facts are the only inputs needed here.
proof idea
Term-mode one-liner. First apply right-subtraction congruence: balance of $b$ with $b'$ yields balance of $a-b$ with $a-b'$. Then apply the general fact that balanced signed orbits share the same nonnegative flag. No case split or rewriting beyond that composition.
why it matters
Feeds the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, $\mathrm{leq}$, absolute difference, and both the Prop-level and flag-level nonnegative characterizations. Without flag invariance under right subtraction of balanced partners, the flag could not be treated as a well-defined order predicate on integer classes.
In the broader Recognition stack this sits in Foundation, under the Primitive Recognition Calculus that supplies the discrete integer layer before continuous forcing (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$). It is bookkeeping rather than a forcing step, but the order surface must be closed before ledger and gap constructions can quote signed comparisons safely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.