lt_mul_left_iff_of_negativeFlag
plain-language theorem explainer
Left multiplication by a strictly negative signed orbit reverses the internal strict order: a·z < a·w if and only if w < z. Order and comparison lemmas on SignedOrbit cite it when the multiplier is known negative. The proof reduces both sides to ℤ via toInt, then finishes by linear arithmetic on the product inequality.
Claim. Let $a,z,w$ be signed orbits. If $a$ is strictly negative (its negative flag is true), then $a\cdot z < a\cdot w$ in the internal signed-orbit order if and only if $w < z$.
background
Signed orbits are the internal integer model in Primitive Recognition Calculus: each carries a pair of nonnegative orbit positions and a structural nonnegative flag. The negative flag is the Boolean negation of that flag, so negativeFlag = true means the orbit is strictly negative. Strict order on signed orbits is defined as nonnegative difference with nonzero (non-balanced) difference.
The bridge to classical integers is the recovery map toInt, which sends a signed orbit to an ordinary Int. Upstream, lt_iff_toInt_lt states that internal strict order is exactly the usual order on images under toInt, and mul_toInt states that multiplication is preserved: (a·b).toInt = a.toInt * b.toInt. The negativity hypothesis likewise transports: negativeFlag = true iff toInt a < 0.
This module builds the ordered-ring surface on that model. The local goal is the standard sign-sensitive multiplication laws for < and for the three-way comparison cmp, so that the integer-order certificate can close.
proof idea
Term-mode proof in three moves. First apply negativeFlag_eq_true_iff_toInt_neg to turn the Boolean hypothesis into a.toInt < 0. Rewrite both sides of the biconditional with lt_iff_toInt_lt and both multiplications with mul_toInt, so the claim becomes the classical fact
$$a_{\mathbb{Z}}\cdot z_{\mathbb{Z}} < a_{\mathbb{Z}}\cdot w_{\mathbb{Z}} \iff w_{\mathbb{Z}} < z_{\mathbb{Z}}$$
under $a_{\mathbb{Z}} < 0$. Split the biconditional and discharge each direction by nlinarith.
why it matters
This is the negative-multiplier half of order-compatibility for signed-orbit multiplication. It feeds cmp_mul_left_of_negativeFlag, which lifts the same sign flip to the three-way comparison function, and is listed among the ingredients of integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
In the Recognition foundation stack, integers and their order are recovered from logic rather than assumed. Closing left-multiplication laws for both nonnegative and negative multipliers is required before the ordered ring can support later arithmetic used in the forcing chain and mass-ladder constructions. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.