negativeFlag_mul_eq_of_balanced_right
plain-language theorem explainer
Left multiplication by a fixed signed orbit preserves the negativity flag when the right factors are balanced (integer-equivalent). Order and sign bookkeeping for the internal PRC integer surface cites this. The proof is a two-lemma composition: balanced is a congruence for mul on the right, then balanced orbits share the same negativeFlag.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction lengths meaning $\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 strict-negativity flags of the products agree: $(\mathrm{mul}\,a\,b).\mathrm{negativeFlag}=(\mathrm{mul}\,a\,b').\mathrm{negativeFlag}$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction lengths $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their lengths satisfy the internal integer relation $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the PRC stand-in for equality of the underlying integers.
The negativity flag is the Boolean dual of the structural nonnegative flag: $\mathrm{negativeFlag}(z)=\neg z.\mathrm{nonnegFlag}$. The order surface on signed orbits is built from these flags and from the balanced relation, so sign data must be invariant under balanced replacement.
Upstream, right-balanced factors remain balanced after left multiplication (mul_congr_of_balanced_right), and any two balanced orbits already share the same negativity flag (negativeFlag_eq_of_balanced).
proof idea
Term-mode composition of two prior facts. First apply mul_congr_of_balanced_right to the hypothesis that $b$ and $b'$ are balanced; that yields balancedness of $\mathrm{mul},a,b$ with $\mathrm{mul},a,b'$. Then feed that balanced pair into negativeFlag_eq_of_balanced, which equates the negativity flags of any balanced pair. No extra case analysis or unfolding is required.
why it matters
This is a small congruence lemma for the signed-orbit order surface: left multiplication does not scramble the negativity flag when the right factor is replaced by an integer-equivalent orbit. It feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity.
In the Recognition foundation stack, integers and their order are not imported from classical $\mathbb{Z}$; they are reconstructed from distinction orbits and the balanced relation. Sign-stable multiplication is part of making that reconstruction usable as an ordered ring-like structure before later forcing steps (T5–T8) and ledger accounting rely on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.