negativeFlag_mul_iff
plain-language theorem explainer
The product of two signed orbits is negative exactly when the factors have opposite strict signs: one nonnegative and nonzero, the other negative. Anyone building the integer order or sign calculus on SignedOrbit cites this biconditional. The proof splits on exhaustive sign flags, reduces via the toInt embedding and nlinarith, and closes the converse with the two one-sided multiplication lemmas.
Claim. For signed orbits $z,w$, the product $z\cdot w$ is flagged negative if and only if either ($z$ is nonnegative, $z\neq 0$, and $w$ is negative) or ($z$ is negative, $w$ is nonnegative, and $w\neq 0$).
background
In the primitive recognition calculus, integers are recovered as signed orbits. Each SignedOrbit carries boolean sign flags: nonnegFlag and negativeFlag, together with a balance relation that identifies the zero orbit. Multiplication is the orbit product, and toInt is the recovery map into classical Int (from IntegersFromLogic), so flag statements can be read as ordinary inequalities on integers.
Sibling facts already pin the dictionary: negative flag true iff toInt < 0, nonnegative flag true iff toInt ≥ 0, and balance with zero iff toInt = 0. Sign flags are exhaustive and exclusive, so every orbit is either nonnegative or negative. The local module builds the full order surface on these flags before packaging it as a certificate.
Two directed lemmas sit immediately upstream: product is negative when the left factor is nonnegative nonzero and the right is negative, and when the left is negative and the right is nonnegative nonzero. This theorem is the if-and-only-if packaging of those directions.
proof idea
Bidirectional constructor. Forward: assume the product flag is negative, rewrite via negativeFlag_eq_true_iff_toInt_neg and mul_toInt to get z.toInt * w.toInt < 0. Case-split on signFlags_exhaustive z. If $z$ is nonnegative, deduce $z\neq 0$ (else the product integer is zero, contradicting strict negativity by nlinarith), force $w.toInt < 0$, and reassemble the left disjunct. If $z$ is negative, force $w.toInt > 0$ (hence nonnegative and nonzero) and take the right disjunct.
Converse: case-split the disjunction and apply the two one-sided lemmas negativeFlag_mul_of_nonnegFlag_of_not_balanced_zero_of_negativeFlag and negativeFlag_mul_of_negativeFlag_of_nonnegFlag_of_not_balanced_zero directly.
why it matters
This closes the multiplicative sign law for the internal integer order on signed orbits. Downstream, nonnegFlag_mul_iff_not_strict_opposite_sign is the complementary nonnegative product criterion (literally the negation of this opposite-sign pattern). Both feed the order surface that integer_order_certificate packages: that certificate records that the signed-orbit order display is closed, including nonnegative and negative flag displays tied to toInt.
In the Recognition foundation stack, integers-from-logic and the ledger balance relation are prerequisites for any later rung arithmetic on the phi-ladder. A clean sign-of-product rule is bookkeeping, not a forcing step (T5–T8), but without it the order certificate cannot claim a closed multiplicative sign calculus. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.