le_mul_right_iff_of_negativeFlag
plain-language theorem explainer
If a signed orbit $a$ is strictly negative, right-multiplication by $a$ reverses order: $z\cdot a\le w\cdot a$ iff $w\le z$. Anyone assembling the signed-orbit order certificate, or checking that internal integer order matches $\mathbb{Z}$, would cite this. The proof transports both sides to $\mathbb{Z}$ via the recovery map and closes with nonlinear arithmetic on a negative multiplier.
Claim. Let $a,z,w$ be signed orbits (internal integer carriers). If $a$ is strictly negative, then $z\cdot a \le w\cdot a$ if and only if $w \le z$.
background
Signed orbits are the internal integer type in the primitive recognition calculus: each carrier pairs nonnegative distinction-nat limbs for the positive and negative parts. The recovery map toInt sends a signed orbit to ordinary $\mathbb{Z}$, and multiplication is defined so that it intertwines with integer multiplication.
Order on signed orbits is defined internally: $a\le b$ means the difference $b-a$ is nonnegative (nonneg of the structural subtraction). The Boolean negativeFlag is the negation of the structural nonnegative flag; upstream it is equivalent to toInt a < 0.
The bridge lemmas used here are the order-transport le a b \leftrightarrow a.toInt \le b.toInt and the multiplicative transport (mul a b).toInt = a.toInt * b.toInt. Together they reduce signed-orbit order facts to ordinary integer inequalities.
proof idea
First convert the hypothesis negativeFlag a = true into a.toInt < 0 via the flag-to-integer characterization. Rewrite both order atoms with the order-transport lemma, and both multiplications with the multiplicative transport, so the goal becomes
$$z\cdot a\le w\cdot a ;\text{in};\mathbb{Z};\iff; w\le z;\text{in};\mathbb{Z}$$
with a strictly negative right factor. Both directions are then discharged by nlinarith on $\mathbb{Z}$.
why it matters
This is one of the order-algebra lemmas that close the internal signed-orbit order surface. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed (displaying nonnegativity, flags, truncated subtraction, and absolute difference against the distinction-nat layer).
In the Recognition foundation stack, integers are rebuilt from logic rather than assumed as a primitive. Multiplicative order-reversal for negative carriers is a standard $\mathbb{Z}$ axiom that must be recovered internally before the certificate can claim the order is fully assembled. It sits beside reflexivity, transitivity, totality, trichotomy, and the sign-flag exclusivity lemmas in the same module.
No forcing-chain landmark (T5–T8) is directly at stake; this is pure arithmetic infrastructure under the primitive recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.