negativeFlag_mul_eq_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (same integer value), left-multiplication by any third orbit preserves the negative flag of the product. Order and sign bookkeeping for the internal PRC integer surface cites this when products must not flip sign under equivalence. The proof is a two-lemma term composition: left-mul congruence of balance, then negative-flag invariance under balance.
Claim. Let $a,a',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 negative 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 naturals (pos, neg) with intended meaning pos - neg. Two signed orbits are balanced when their lengths satisfy the internal integer relation a.pos + b.neg = b.pos + a.neg; this is the PRC stand-in for equality of integers, defined only on δ-orbit positions.
The negative flag is the Boolean !nonnegFlag, i.e. strict negativity as failure of the structural nonnegative test. The module builds an internal order on these signed orbits (a ≤ b when b - a is nonnegative) without importing classical Int as primitive.
Upstream, mul_congr_of_balanced_left shows left multiplication preserves balance: if a ~ a' then a*b ~ a'*b, via the toInt reading of balance. Separately, negativeFlag_eq_of_balanced says balanced orbits share the same negative flag (by reducing to the nonnegative-flag congruence).
proof idea
One-line term proof. Apply mul_congr_of_balanced_left to the hypothesis ha : balanced a a' to obtain balanced (mul a b) (mul a' b). Feed that into negativeFlag_eq_of_balanced, which equates negative flags of any balanced pair. No case splits or unfolding of mul at this site.
why it matters
This is a small congruence lemma on the signed-orbit order surface: sign of a product is well-defined on balance classes under left multiplication. It feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; that certificate packages display lemmas for truncated subtraction, ≤, absolute difference, and signed nonnegativity flags.
In the broader Recognition foundation, integers and their order are reconstructed from distinction orbits rather than assumed. Closing sign-invariance under multiplication is part of making that reconstruction usable for later ledger and forcing steps, without smuggling classical integer sign into the primitive calculus. No T5–T8 landmark is discharged here; the result is infrastructure for the PRC integer order package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.