negativeFlag_mul_eq_of_balanced
plain-language theorem explainer
Balanced pairs of signed orbits have products with identical negativity flags. Anyone assembling the internal integer order from δ-orbit data cites this for sign well-definedness under multiplication. The proof is a one-line composition: product congruence under balance, then flag invariance under balance.
Claim. Let $a,a',b,b'$ be signed orbits (pairs of distinction lengths meaning $\mathrm{pos}-\mathrm{neg}$). If $a$ is balanced with $a'$ and $b$ with $b'$ (i.e. $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$, and likewise for $b,b'$), then the negativity flag of the product $a\cdot b$ equals that of $a'\cdot b'$.
background
In the Primitive Recognition Calculus, 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 $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal PRC integer equivalence, defined only on δ-orbit positions (K4.9).
The negativity flag is the Boolean negation of the structural nonnegative flag: strict negativity as failure of nonnegativity. Multiplication of signed orbits is the ring product on these 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. Upstream, flag equality under balance is already known for a single pair; the present statement lifts that invariance through the product.
proof idea
One-line term proof. First apply product congruence under balance: if $a\sim a'$ and $b\sim b'$, then $a\cdot b\sim a'\cdot b'$. Then apply negativity-flag equality under balance to that product pair. No extra case analysis; the two lemmas compose directly.
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, $\le$, absolute difference, and signed nonnegativity; well-defined sign of products is part of making the order and ring structure descend to balance classes.
In the Recognition foundation this sits inside the PRC integer layer that supports ledger forcing and later mass/gap bookkeeping. It does not itself invoke T5–T8 or the RCL, but it is infrastructure those chains rely on once integers are reconstructed from distinction orbits rather than postulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.