negativeFlag_sub_eq_of_balanced_right
plain-language theorem explainer
Right-congruence of the strict-negativity flag under signed-orbit subtraction: if b and b' balance, then a−b and a−b' share the same negative flag. Order-surface and certificate authors cite it to show the internal ≤ relation is well-defined on balance classes. The proof is a two-lemma term: right-subtraction preserves balance, then balance preserves the negative flag.
Claim. For signed orbits $a,b,b'$, if $b$ and $b'$ are balanced (i.e. $b_{\mathrm{pos}}+b'_{\mathrm{neg}}=b'_{\mathrm{pos}}+b_{\mathrm{neg}}$), then the strict-negativity flag of $a-b$ equals that of $a-b'$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-natural lengths (pos, neg) with intended meaning pos − neg. Two signed orbits are balanced when their lengths satisfy the internal integer relation a.pos + b.neg = b.pos + a.neg; this is the PRC stand-in for equality of integer values without leaving the δ-orbit language.
The negative flag is the Boolean !nonnegFlag, recording strict negativity as failure of structural nonnegativity. Internal order is defined by a ≤ b iff b − a is nonnegative, so flags on differences must be invariant under replacing either operand by a balanced representative.
Upstream, sub_congr_of_balanced_right already shows that right-subtraction preserves balance when the right operands balance, and negativeFlag_eq_of_balanced shows that balanced orbits share the same negative flag (via the corresponding nonneg-flag equality).
proof idea
Term-mode composition of two prior lemmas. First apply right-subtraction congruence: balance of b with b' yields balance of a − b with a − b'. Then apply negative-flag equality of balanced orbits to that pair. No case split or unfolding is needed at this site.
why it matters
Feeds the integer-order certificate (integer_order_certificate), whose doc-comment states that the internal signed-orbit order surface is closed. Without right-invariance of the negative flag under balanced replacement, the order relation on balance classes would depend on representatives and the certificate's signed-nonneg displays would not be well-defined.
This sits in the foundation layer that builds an integer order purely from δ-orbit data before ledger forcing and the T0–T8 chain. It is a small but necessary congruence step so that later mass-ladder and recognition-cost constructions can treat signed differences as integers up to balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.