negativeFlag_mul_of_negativeFlag_of_nonnegFlag_of_not_balanced_zero
plain-language theorem explainer
If a signed orbit is negative and another is strictly positive (nonnegative and not balanced with zero), their product is negative. Order and sign-flag lemmas for the PRC integer surface cite this. The proof reduces flags to the integer display via toInt, then closes with nlinarith on the product of a negative and a positive integer.
Claim. Let $z$ and $w$ be signed orbits. If the negative flag of $z$ is true, the nonnegative flag of $w$ is true, and $w$ is not balanced with the zero orbit, then the negative flag of the product $z \cdot w$ is true.
background
In Primitive Recognition Calculus, integers are recovered from signed orbits: pairs of nonnegative orbit lengths (pos, neg) with an internal balance relation $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. The map $\mathrm{toInt}$ sends a signed orbit to an ordinary integer; balance is equivalent to equal $\mathrm{toInt}$ values (K4.9 bridge).
Sign is tracked by Boolean flags rather than classical trichotomy on $\mathbb{Z}$. The negative flag means $\mathrm{toInt}<0$; the nonnegative flag means $\mathrm{toInt}\ge 0$. Not being balanced with the zero orbit means the display integer is nonzero. Multiplication of signed orbits is defined so that $\mathrm{toInt}(z\cdot w)=\mathrm{toInt}(z)\cdot\mathrm{toInt}(w)$.
This module builds the order surface on those flags: reflexivity, totality, trichotomy, and the dictionary between flags and comparisons with zero. The present lemma is the mixed-sign product rule for the negative flag.
proof idea
Rewrite the goal with $\mathrm{negativeFlag}=\mathrm{true}\Leftrightarrow\mathrm{toInt}<0$ and the multiplicative law for $\mathrm{toInt}$. From the hypotheses, obtain $z.\mathrm{toInt}<0$ and $0\le w.\mathrm{toInt}$. The non-balance hypothesis plus $\mathrm{balanced}\Leftrightarrow\mathrm{toInt}$ equality and $\mathrm{zero}.\mathrm{toInt}=0$ give $w.\mathrm{toInt}\ne 0$, hence $0<w.\mathrm{toInt}$ by omega. Then nlinarith yields $(\mathrm{toInt},z)\cdot(\mathrm{toInt},w)<0$, which is the rewritten goal.
why it matters
Closes one direction of the product rule for negative flags on signed orbits, feeding $\mathrm{negativeFlag_mul_iff}$ (the full iff characterizing when a product is negative). That rule is part of the internal signed-orbit order surface packaged by $\mathrm{integer_order_certificate}$, whose doc states the surface is closed.
In the Recognition foundation stack, integers and their order are not imported as a black box: they are forced from ledger/orbit structure (IntegersFromLogic, IntegerRational). Correct sign behavior under multiplication is required before the order certificate can stand as a complete PRC integer interface. This is local foundation work beneath the forcing chain (T0–T8), not a physics constant claim; it secures the algebraic substrate those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.