lt_mul_right_iff_of_negativeFlag
plain-language theorem explainer
If a signed orbit is strictly negative, right-multiplication by it reverses strict order: za < wa holds exactly when w < z. Order and comparison lemmas for the internal integer surface cite this. The proof bridges both sides to ℤ via toInt, multiplies, and closes both directions by linear arithmetic.
Claim. Let $a,z,w$ be signed orbits. If $a$ is strictly negative (its negativity flag is true), then $z\cdot a < w\cdot a$ if and only if $w < z$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: each carries a pair of orbit positions and a structural nonnegative flag. Strict order is defined internally as nonnegative difference with nonzero (unbalanced) difference. The recovery map toInt sends a signed orbit to an ordinary integer and is a ring homomorphism for multiplication.
Negativity is the Boolean dual of the nonnegative flag: the flag is true exactly when toInt is negative. Upstream, strict order on signed orbits is characterized by ordinary integer comparison: $a < b$ iff $a.\mathrm{toInt} < b.\mathrm{toInt}$. Multiplication likewise descends: $(ab).\mathrm{toInt} = a.\mathrm{toInt}, b.\mathrm{toInt}$.
This module builds the ordered-ring surface on that model so the foundation can certify integer order without leaving the recognition calculus.
proof idea
Convert the negativity hypothesis to $a.\mathrm{toInt} < 0$ via the flag-to-integer equivalence. Rewrite both sides of the claimed biconditional with the order bridge ($\mathrm{lt}\leftrightarrow\mathrm{toInt},<$) and the multiplication bridge ($\mathrm{mul}_\mathrm{toInt}$). The goal becomes the elementary fact that multiplying a strict inequality of integers on the right by a negative integer reverses it. Both directions are discharged by nlinarith.
why it matters
Right-multiplication by a negative unit is the remaining orientation case for ordered multiplication on signed orbits. Downstream, the comparison form cmp_mul_right_of_negativeFlag reuses the same hypothesis and bridges to equate comparison values after right-multiplication. The bundle theorem integer_order_certificate then records that the internal signed-orbit order surface is closed (nonnegativity, flags, and display maps all match the recovered integers).
In the Recognition foundation this is bookkeeping on the integers-from-logic layer, not a forcing-chain step (T5–T8). It keeps the ordered arithmetic used by later recognition calculus honest: order and multiplication interact exactly as on ℤ, including sign reversal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.