negativeFlag_mul_eq_false_of_balanced_zero_left
plain-language theorem explainer
If a signed orbit is balanced with zero, its product with any signed orbit is not strictly negative. Order and arithmetic developers in the primitive recognition calculus cite this when closing sign behaviour of multiplication at zero. The proof is a short case split: nonnegativity of the product forces the negative flag false via the exclusive sign-flag equivalence.
Claim. Let $z,w$ be signed orbits. If $z$ is balanced with the zero orbit (i.e. $z.\mathrm{pos}+0.\mathrm{neg}=0.\mathrm{pos}+z.\mathrm{neg}$), then the product $z\cdot w$ has negative flag equal to false: it is not strictly negative.
background
In the primitive recognition calculus, integers are represented as signed orbits: pairs of nonnegative distinction counts (pos, neg). Two orbits are balanced when a.pos + b.neg = b.pos + a.neg; this is the internal equivalence that plays the role of integer equality. The zero orbit is the balanced class of the empty difference.
Sign is read off computable Boolean flags. The nonnegative flag is the structural comparison leq z.neg z.pos. The negative flag is its Boolean negation: strict negativity is failure of nonnegativity. Multiplication of signed orbits is defined so that it descends to the usual product on the balanced quotient.
The sibling lemma nonnegFlag_mul_of_balanced_zero_left already shows that if $z$ is balanced with zero then $(z\cdot w)$ is nonnegative. The present result is the matching negative-flag statement needed for a closed order surface.
proof idea
Term-mode proof by cases on the product's negative flag.
First apply nonnegFlag_mul_of_balanced_zero_left to obtain that (mul z w).nonnegFlag = true. Case-split on (mul z w).negativeFlag. The false branch is immediate by rfl. In the true branch, negativeFlag_eq_true_iff_nonnegFlag_eq_false converts negativity into nonnegFlag = false, which rewrites against the earlier nonnegativity fact and yields a contradiction.
why it matters
This lemma is one of the arithmetic sign facts assembled into integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, leq, absolute difference, and signed nonnegativity so downstream modules can treat the PRC integer order as a finished interface rather than an open construction.
In the Recognition foundation stack, signed-orbit integers sit under the ledger and forcing layers that eventually feed the T0–T8 chain. Closing multiplication-at-zero sign behaviour is routine classical arithmetic, but here it must be proved from δ-orbit positions alone, without importing ℤ. The result therefore discharges a concrete obligation on the path from primitive recognition data to a usable ordered ring of integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.