le_mul_left_iff_of_negativeFlag
plain-language theorem explainer
Left multiplication by a strictly negative signed orbit reverses the internal order: a z ≤ a w if and only if w ≤ z. Order-theory and arithmetic-from-logic work cite this when building the signed-orbit total order. The proof reduces both sides to ℤ via toInt and finishes with linear arithmetic on a negative multiplier.
Claim. Let $a,z,w$ be signed orbits. If $a$ is strictly negative (its negative flag is true), then $a\cdot z \le a\cdot w$ if and only if $w \le z$, where $\le$ is the internal signed-orbit order ($b-a$ nonnegative).
background
Signed orbits are the internal integer model in the primitive recognition calculus: each carries a pair of nonnegative distinction-nat components and recovers an ordinary integer via toInt. The internal order is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative. The boolean negativeFlag is the structural dual of the nonnegative flag; it is true precisely when toInt is strictly negative.
Multiplication of signed orbits is compatible with ordinary integer multiplication: (mul a b).toInt = a.toInt * b.toInt. The bridge lemma le_iff_toInt_le states that the internal order coincides with the standard order on recovered integers. Together these facts let order statements about signed orbits be decided in ℤ.
This module assembles the order surface (reflexivity, transitivity, totality, trichotomy, sign-flag exclusivity) needed before the recognition calculus can treat integers as an ordered ring.
proof idea
Convert the hypothesis a.negativeFlag = true into a.toInt < 0 by the flag-to-integer equivalence. Rewrite both sides of the claimed biconditional with le_iff_toInt_le, then replace each product by its integer image via mul_toInt. The goal becomes the elementary fact that for $A < 0$ one has $A Z \le A W \Leftrightarrow W \le Z$. Both directions are discharged by nlinarith.
why it matters
The integer-order certificate that closes the signed-orbit order surface lists the display lemmas for nonnegativity, absolute difference, and truncated subtraction; the present inequality-reversal rule is one of the algebraic order facts that certificate depends on (via the module's order package). Without left-multiplication by negatives reversing order, the signed orbits would not behave as an ordered ring under the internal operations.
In the broader Recognition foundation this sits under arithmetic-from-logic and integers-from-logic: once LogicNat and LogicInt are recovered, the signed-orbit layer must match classical ordered-integer arithmetic before later forcing-chain steps (T5–T8) can treat discrete structure as given. It is a proved local lemma, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.