lt_mul_right_iff_of_nonnegFlag_of_not_balanced_zero
plain-language theorem explainer
Right-multiplication by a strictly positive signed orbit preserves strict order on signed orbits: za < wa iff z < w. Anyone assembling the ordered-ring laws for PRC integers cites this lemma. The proof pushes both sides through the toInt embedding and closes by linear arithmetic on ℤ.
Claim. Let $a,z,w$ be signed orbits. If $a$ is nonnegative and not balanced with zero (so its integer image is strictly positive), then $z\cdot a < w\cdot a$ if and only if $z < w$.
background
Signed orbits are the internal integer carriers of the Primitive Recognition Calculus: each carries a pair of δ-orbit lengths (pos, neg). Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$, the PRC-native equality relation; balanced with zero means the orbit is the zero class. The flag nonnegFlag records nonnegativity of the recovered integer image.
Order and arithmetic are defined so that they commute with the recovery map toInt : SignedOrbit → ℤ. In particular, strict order on signed orbits is equivalent to ordinary < on those integers, and multiplication of orbits maps to ordinary integer multiplication. The present lemma is the positivity half of the ordered-ring cancellation law under that embedding.
Upstream characterizations used here are the flag-to-integer equivalence for nonnegativity, the balanced-iff-toInt-equal criterion, and the toInt homomorphism for multiplication.
proof idea
Translate the flag hypothesis into $0 \le a.\mathrm{toInt}$. From $\neg\mathrm{balanced}(a,0)$ and the balanced-iff-toInt criterion (with zero mapping to $0$), deduce $a.\mathrm{toInt}\ne 0$. Combined, omega yields $0 < a.\mathrm{toInt}$.
Rewrite both sides of the claimed biconditional via lt_iff_toInt_lt and replace each product by mul_toInt. The resulting integer statement is $z\cdot a < w\cdot a \leftrightarrow z < w$ under a strictly positive multiplier, which both directions discharge by nlinarith.
why it matters
This is a core ordered-multiplication law for the internal PRC integers. It is consumed directly by cmp_mul_right_of_nonnegFlag_of_not_balanced_zero, which lifts the same positivity hypothesis from strict order to the three-way comparison function, and by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
Closing that certificate is part of the Foundation stack that rebuilds arithmetic and order from recognition primitives rather than importing classical ℤ. The lemma sits downstream of the forcing chain's arithmetic layer (integers recovered from logic) and supplies the positivity half of cancellation needed before mass-ladder and ledger constructions can treat signed quantities as an ordered ring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.