negativeFlag_sub_eq_of_balanced
plain-language theorem explainer
Balanced signed orbits have subtraction that preserves the strict-negativity flag: if a ~ a' and b ~ b', then (a−b) is negative exactly when (a'−b') is. Order and certificate authors cite it to show the internal ≤ relation is well-defined on equivalence classes. 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 read as $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ in the sense $x.\mathrm{pos}+y.\mathrm{neg}=y.\mathrm{pos}+x.\mathrm{neg}$, then the strict-negativity flag of $a-b$ equals that of $a'-b'$.
background
In the Primitive Recognition Calculus, integers are represented internally by signed orbits: a structure SignedOrbit with fields pos and neg (distinction naturals), intended as the difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their lengths satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the PRC integer equivalence, defined only on $\delta$-orbit positions.
Strict negativity is the Boolean flag negativeFlag, defined as the negation of the structural nonnegative flag. The internal order is then $a\le b$ when $b-a$ is nonnegative, so well-definedness of order on balance classes needs the negativity (and nonnegativity) flags to be invariant under balanced subtraction.
Upstream, sub_congr_of_balanced shows subtraction preserves balance, and negativeFlag_eq_of_balanced shows balanced orbits share the same negativity flag (via the corresponding nonnegativity invariance).
proof idea
One-line term proof. Apply sub_congr_of_balanced to the two balance hypotheses to obtain that $a-b$ is balanced with $a'-b'$. Feed that witness into negativeFlag_eq_of_balanced, which equates negativity flags of any balanced pair. No further case analysis or unfolding is required at this site.
why it matters
This lemma is a well-definedness brick for the internal signed-orbit order. It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed": the certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity so the order API can be treated as finished.
In the Recognition foundation stack, signed orbits sit under the ledger and forcing layers that eventually feed the T0–T8 chain. Closing flag-invariance under arithmetic means the integer order used in primitive recognition calculus does not depend on representative choice inside a balance class, which is required before any later comparison of costs, ticks, or ladder rungs can be stated on integers rather than raw orbit pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.