nonnegFlag_mul_of_negativeFlag_of_negativeFlag
plain-language theorem explainer
The product of two strictly negative signed orbits is nonnegative under the structural flag. Integer-order and sign-algebra developments in the primitive recognition calculus cite this when closing multiplicative sign rules. The proof bridges both flags to recovered integers, multiplies via the toInt homomorphism, and finishes by nonlinear arithmetic on two negative factors.
Claim. For signed orbits $z$ and $w$, if each has negative flag true (equivalently $z.{\rm toInt}<0$ and $w.{\rm toInt}<0$), then the product $z\cdot w$ has nonnegative flag true (equivalently $0\le(z\cdot w).{\rm toInt}$).
background
Signed orbits represent integers by a pair of distinction naturals (pos, neg), recovered by toInt = pos - neg (from the LogicInt quotient bridge). The nonnegative flag is the structural comparison neg ≤ pos; it is proved equivalent to 0 ≤ toInt. The negative flag is its Boolean negation and is equivalent to toInt < 0.
Multiplication on signed orbits is defined so that the recovery map is a ring homomorphism: (mul z w).toInt = z.toInt * w.toInt. This module equips those orbits with an internal order (difference nonnegative) as part of reconstructing classical integer arithmetic from recognition primitives, before continuum or ladder structure appears.
proof idea
Rewrite the goal with nonnegFlag_eq_true_iff to 0 ≤ (mul z w).toInt, then apply mul_toInt to obtain 0 ≤ z.toInt * w.toInt. Convert each hypothesis via negativeFlag_eq_true_iff_toInt_neg into z.toInt < 0 and w.toInt < 0. Close the resulting integer inequality by nlinarith.
why it matters
Used by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. Supplies one multiplicative sign law needed for that certificate's nonnegative and flag displays. Sits in the foundation layer that recovers ordered integers from recognition structure (IntegersFromLogic and PrimitiveRecognitionCalculus), the discrete substrate on which later forcing-chain and ladder constructions rest. Not itself a T0–T8 step; it is infrastructure under the integer order package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.