nonnegFlag_mul_eq_of_balanced_left
plain-language theorem explainer
If two signed orbits represent the same integer, right-multiplication by any third orbit leaves their nonnegative flags equal. Order and sign infrastructure for the Primitive Recognition Calculus integer layer cites this when showing the order surface is well-defined on equivalence classes. The proof is a one-line composition: left-multiplication congruence of balance, then flag equality under balance.
Claim. Let $a$, $a'$, and $b$ be signed orbits (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$). If $a$ and $a'$ are balanced, i.e. $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$, then the computable nonnegative flag of $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 $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal integer equivalence, defined only on $\delta$-orbit positions.
The nonnegative flag is the structural Boolean $\mathrm{leq},z.\mathrm{neg},z.\mathrm{pos}$. It is the computable stand-in for nonnegativity before the map to ordinary integers is invoked. Multiplication of signed orbits is the ring operation on this representation.
Upstream, balance is already known to be preserved by right-multiplication on the left factor (mul_congr_of_balanced_left), and balanced orbits share the same nonnegative flag (nonnegFlag_eq_of_balanced). This lemma packages those two facts for the multiplicative setting.
proof idea
Term-mode one-liner. Apply mul_congr_of_balanced_left to the given balance hypothesis to obtain balance of the two products $a\cdot b$ and $a'\cdot b$. Feed that balance witness into nonnegFlag_eq_of_balanced, which equates the nonnegative flags of any balanced pair. No case analysis or rewriting is local to this declaration.
why it matters
The parent consumer is integer_order_certificate, which asserts that the internal signed-orbit order surface is closed: displays for truncated subtraction, $\leq$, absolute difference, and signed nonnegativity all line up. Flag invariance under balanced left factors is required so that the order and sign surface descends to integer equivalence classes rather than raw orbit representatives.
Within Recognition Science foundation work this sits in the PRC integer-order stack that underwrites ledger arithmetic before the forcing chain (T0–T8) and the Recognition Composition Law are applied at the continuum level. It does not itself force $\varphi$ or dimension; it keeps the discrete signed-integer substrate coherent so later certificates can treat order as a property of integers, not of presentations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.