nonnegFlag_mul_eq_of_balanced_right
plain-language theorem explainer
Right-multiplication by a fixed signed orbit preserves the nonnegative flag when the right factor is replaced by any balanced partner. Anyone building the internal integer order on δ-orbits cites this to know sign bits of products are well-defined on balance classes. The proof is a two-step term: congruence of multiplication under balance, then flag equality on balanced pairs.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$, then the computable nonnegative flags of the products agree: $(a\cdot b).\mathrm{nonnegFlag}=(a\cdot b').\mathrm{nonnegFlag}$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the integer difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their lengths match across sides: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the internal PRC integer equality, defined only on δ-orbit positions.
The nonnegative flag is the Boolean leq neg pos, a structural comparison that decides nonnegativity without leaving the orbit language. Multiplication of signed orbits is the ring operation lifted from those positions; the companion lemma mul_congr_of_balanced_right shows that right-multiplication by a fixed factor sends balanced pairs to balanced pairs (via equality of the underlying toInt values).
This module builds the order surface on those signed orbits: reflexivity, totality, trichotomy, and sign-flag exclusivity all sit as siblings. The present statement is the right-factor stability of the sign bit under balance.
proof idea
Pure term composition of two prior results. First apply right-multiplication congruence: from $b\sim b'$ one gets $a\cdot b\sim a\cdot b'$ (proved by rewriting balance to toInt equality and using multiplicativity of toInt). Then apply flag equality on balanced pairs: any two balanced signed orbits share the same nonnegFlag. No case split or rewriting is needed at this site.
why it matters
Feeds the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, leq, absolute difference, and the signed nonnegative flag; well-definedness of the flag under multiplication is part of making the order a genuine quotient structure on balance classes rather than a representative-dependent gadget.
In the Recognition foundation this sits inside the Primitive Recognition Calculus integer layer that underwrites ledger arithmetic before the forcing chain (T0–T8) and the Recognition Composition Law are applied. It does not itself force $\varphi$ or dimension; it keeps the discrete sign of products coherent so later mass-ladder and cost constructions can treat integers as balance classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.