negativeFlag_mul_of_nonnegFlag_of_not_balanced_zero_of_negativeFlag
plain-language theorem explainer
If a signed orbit is strictly positive (nonnegative and not balanced with zero) and another is negative, their product is negative. Order and sign lemmas in the primitive recognition calculus cite this for the multiplicative sign law. The proof bridges to ordinary integers via the toInt display and finishes by linear arithmetic.
Claim. Let $z,w$ be signed orbits. If $z$ is nonnegative, $z$ is not balanced with the zero orbit, and $w$ is negative, then the product orbit $zw$ is negative.
background
In the primitive recognition calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (positive and negative parts). Two orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; that internal relation is the PRC equality of integers. The display map toInt sends a signed orbit to an ordinary $\mathbb{Z}$ value, and balancedness is equivalent to equality of those integers.
Nonnegative and negative status are recorded by Boolean flags on the orbit. The nonnegative flag holds exactly when toInt is $\ge 0$; the negative flag holds exactly when toInt < 0. Not being balanced with the zero orbit means the integer is nonzero, so nonnegative plus not-balanced-zero is strict positivity.
Multiplication of signed orbits is defined so that it intertwines with integer multiplication: the toInt of a product is the product of the toInts. That bridge lets sign facts on orbits reduce to ordinary inequalities on $\mathbb{Z}$.
proof idea
Rewrite the goal with the characterization that the negative flag is true iff toInt is negative, and replace the product's toInt by the product of the factors' toInts.
From the nonnegative flag on $z$, obtain $0 \le z.toInt$. From not-balanced-with-zero, obtain $z.toInt \ne 0$ by the balanced-iff-toInt bridge and the fact that zero has toInt $0$; omega upgrades this to $0 < z.toInt$. From the negative flag on $w$, obtain $w.toInt < 0$. Then nlinarith closes $z.toInt \cdot w.toInt < 0$.
why it matters
This is one directed arm of the multiplicative sign law for signed-orbit flags. It is consumed by negativeFlag_mul_iff, which packages the full biconditional for when a product is negative, and it contributes to the closed integer-order surface recorded by integer_order_certificate (the certificate that the internal signed-orbit order display is complete).
In the Recognition foundation stack, signed orbits are the PRC presentation of integers before rationals and the cost calculus. Correct product signs are needed so the order and absolute-value layer on the ledger stays faithful to $\mathbb{Z}$. The result is local bookkeeping rather than a forcing-chain landmark (T5–T8), but without it the integer-order certificate cannot claim a closed sign surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.