nonnegFlag_mul_eq_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced-equivalent, the nonnegative flags of their products agree. Order-surface and integer-certificate authors cite it to show multiplication respects the structural sign bit under the internal PRC equivalence. The proof is a one-line composition of product 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 computable nonnegative flag of the product $a\cdot b$ equals that of $a'\cdot b'$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the 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 nonnegative flag is the structural Boolean $\mathrm{leq}(z.\mathrm{neg},z.\mathrm{pos})$: true precisely when the positive side is at least the negative side. Multiplication of signed orbits is the corresponding product on those pairs; the companion lemma mul_congr_of_balanced shows that balance is a congruence for that product (via equality of the underlying integer images).
This module builds the order surface on those signed orbits: reflexivity, transitivity, antisymmetry under balance, trichotomy, and the various flag characterizations of $\le 0$ and $<0$. The present statement is the multiplicative stability of the nonnegative flag under balance.
proof idea
One-line term proof. First apply product congruence: if $a$ balances $a'$ and $b$ balances $b'$, then $a\cdot b$ balances $a'\cdot b'$ (mul_congr_of_balanced, proved by rewriting balance to equality of toInt images and using multiplicativity of toInt). Then apply flag invariance: balanced signed orbits have identical nonnegFlag (nonnegFlag_eq_of_balanced). Compose the two.
why it matters
Feeds the integer-order certificate (integer_order_certificate), whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\mathrm{leq}$, absolute difference, and the signed nonnegative characterizations; multiplicative stability of the nonnegative flag is part of making the order surface algebraically coherent under the PRC product.
In the broader Recognition stack this sits in Foundation, under the primitive recognition calculus that supplies integer structure before ledger forcing and the T0–T8 chain. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it keeps the signed-orbit order well-defined so later forcing and mass-ladder constructions can treat integer signs as balance-invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.