negativeFlag_sub_eq_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (same integer value), subtracting a third orbit on the right preserves the negativity flag of the difference. Order-theoretic work on the PRC integer surface cites this when showing the internal ≤ relation is well-defined on balance classes. The proof is a two-step term: left-subtraction congruence of balance, then flag invariance under balance.
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 negativity flags of $a-b$ and $a'-b$ agree: $(a-b)$ is strictly negative if and only if $(a'-b)$ is.
background
In the Primitive Recognition Calculus, integers are not postulated; they arise as signed orbits. A SignedOrbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.pos+b.neg=b.pos+a.neg$, the internal PRC integer relation defined entirely on $\delta$-orbit positions (K4.9).
The negativity flag is the Boolean dual of the structural nonnegative flag: negativeFlag z := !z.nonnegFlag. Internal order is then $a\le b$ when $b-a$ is nonnegative. For that order to descend to balance classes, flags of differences must be invariant under replacing either argument by a balanced partner.
Upstream, sub_congr_of_balanced_left shows that if $a\sim a'$ then $a-b\sim a'-b$. Separately, negativeFlag_eq_of_balanced says balanced orbits share the same negativity flag (via the corresponding fact for the nonnegative flag).
proof idea
Pure term-mode composition of two prior lemmas. First apply sub_congr_of_balanced_left to the hypothesis that $a$ and $a'$ are balanced; this yields that $a-b$ and $a'-b$ are balanced. Then feed that balance witness into negativeFlag_eq_of_balanced, which equates the negativity flags of any two balanced signed orbits. No case split or unfolding is needed at this site.
why it matters
This is a small but necessary congruence step on the path to a closed internal integer order. Downstream it is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity, tying the Boolean flag layer to the integer reading.
Within Recognition Science foundation work, the PRC integer surface is the discrete substrate on which later forcing (ledger balance, J-cost comparisons, and the T0–T8 chain) can speak about ordered magnitudes without importing classical $\mathbb{Z}$ as a primitive. The result does not itself force $\phi$ or dimension; it keeps the order relation well-defined on the balance quotient so those later steps can cite a coherent $\le$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.