nonnegFlag_sub_eq_of_balanced_left
plain-language theorem explainer
If two signed orbits represent the same integer, subtracting a third orbit on the left leaves their nonnegative flags equal. Order-surface and certificate authors cite it when showing that the structural nonnegativity bit is invariant under left subtraction of balanced pairs. The proof is a two-step term application: left-sub congruence of balance, then flag equality on balanced pairs.
Claim. Let $a$, $a'$, and $b$ be signed orbits (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$). If $a$ and $a'$ are balanced, i.e. $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$, then the computable nonnegative flag of $a-b$ equals that of $a'-b$.
background
In the Primitive Recognition Calculus, integers are not postulated; they arise as signed orbit differences. A SignedOrbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$. Two such orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$, the internal PRC integer relation defined entirely on $\delta$-orbit positions.
The nonnegative flag is the structural Boolean leq neg pos: it reports whether the orbit is nonnegative without leaving the distinction-nat layer. The IntegerOrder module builds the order surface on these flags and on the balanced relation, so that comparison is well-defined on equivalence classes of orbits.
Upstream, balance is already known to force equal nonnegative flags, and left subtraction preserves balance: if $a\sim a'$ then $a-b\sim a'-b$. The present result packages those two facts for the flag of a difference.
proof idea
Pure term proof, two applications. First invoke left-sub congruence of balance: from $a\sim a'$ obtain $(a-b)\sim(a'-b)$. Then apply the lemma that balanced signed orbits share the same nonnegative flag. No case split or rewriting is needed at this site; both lemmas do the work.
why it matters
The integer-order certificate asserts that the internal signed-orbit order surface is closed, packaging display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity (including the flag form). This theorem supplies the left-subtraction invariance of the nonnegative flag under balance, so the certificate can treat the flag as a well-defined class function on differences.
Within Recognition Science foundation work, that closure is part of forcing an integer order from recognition structure alone, before continuum or classical $\mathbb{Z}$ is assumed. It sits with the sibling order laws (reflexivity, transitivity, antisymmetry on balanced pairs, totality, trichotomy, and the zero/sign flag characterizations) that make the PRC integer layer usable downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.