nonnegFlag_sub_eq_of_balanced
plain-language theorem explainer
Balanced signed orbits have subtraction that preserves the computable nonnegativity flag: if a ~ a' and b ~ b', then (a−b).nonnegFlag equals (a'−b').nonnegFlag. Anyone building the internal integer order on δ-orbits cites this congruence. The proof is a one-line composition of subtraction congruence with flag invariance under balance.
Claim. Let $a,a',b,b'$ be signed orbits (pairs of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e.\ $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$ and likewise for $b,b'$), then the structural nonnegativity flag of $a-b$ equals that of $a'-b'$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as the formal difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the internal PRC integer equivalence, defined only on $\delta$-orbit positions.
The nonnegativity flag is the computable Boolean $\mathrm{leq}(z.\mathrm{neg},z.\mathrm{pos})$: structural comparison of the two sides, not an external $\mathbb{Z}$ embedding. Subtraction of signed orbits is defined so that balance is a congruence (via addition and negation congruences).
Upstream, nonnegFlag_eq_of_balanced already shows the flag is invariant under balance of a single pair, and sub_congr_of_balanced shows $a\sim a'$, $b\sim b'$ imply $a-b\sim a'-b'$. This lemma only packages those two facts for differences.
proof idea
One-line term proof. First apply subtraction congruence: from $a\sim a'$ and $b\sim b'$ obtain $\mathrm{sub},a,b\sim\mathrm{sub},a',b'$ via sub_congr_of_balanced (itself built from addition and negation congruences). Then feed that balanced pair into nonnegFlag_eq_of_balanced, which equates the nonnegativity flags of any two balanced signed orbits. No case analysis appears at this layer.
why it matters
The integer-order surface on signed orbits must treat balanced representatives as interchangeable for every order primitive, including the flag that decides nonnegativity of a difference. This lemma closes that gap for subtraction, so order comparisons of differences do not depend on which balanced witness is chosen.
It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate bundles display lemmas (truncated subtraction, $\mathrm{leq}$, absolute difference, signed nonnegativity) into a single closed interface for the PRC integer layer.
In the broader Recognition foundation this sits under ledger and orbit forcing: integers arise as balanced signed $\delta$-orbits before rationals and the J-cost calculus. It does not itself touch T5–T8 or the RCL, but it is part of the discrete substrate those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.