le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero
plain-language theorem explainer
Right-multiplication by a strictly positive signed orbit preserves the internal order: za ≤ wa if and only if z ≤ w. Anyone building the PRC integer-order surface cites this cancellation law. The proof reduces both sides to ℤ via toInt, obtains a.toInt > 0 from the nonneg flag and non-balance hypotheses, then finishes by linear arithmetic.
Claim. Let $a,z,w$ be signed orbits. If $a$ is nonnegative ($a.\mathrm{nonnegFlag}=\mathrm{true}$) and $a$ is not balanced with zero, then $za \le wa$ if and only if $z \le w$, where $\le$ and multiplication are the internal signed-orbit order and product.
background
Signed orbits are the PRC carrier for integers: each orbit records a pair of nonnegative distinction lengths (pos, neg). Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; balance with zero is the internal zero test. The recovery map toInt sends a signed orbit to an ordinary integer, and balance is equivalent to equal images under toInt.
The nonneg flag marks orbits whose toInt image is nonnegative. Order on signed orbits is defined so that $x \le y$ iff $x.\mathrm{toInt} \le y.\mathrm{toInt}$. Multiplication of signed orbits is compatible with toInt in the usual way: $(xy).\mathrm{toInt}=x.\mathrm{toInt}\cdot y.\mathrm{toInt}$.
This lemma lives in the IntegerOrder module, which closes the ordered-ring surface on the internal PRC integers before the certificate packages the display equalities.
proof idea
Translate the nonneg flag into $0 \le a.\mathrm{toInt}$. From non-balance with zero and balanced_iff_toInt_eq together with zero_toInt, deduce $a.\mathrm{toInt}\ne 0$, hence $0 < a.\mathrm{toInt}$ by omega. Rewrite both order statements via le_iff_toInt_le and both products via mul_toInt, obtaining the ordinary integer claim $z\cdot a \le w\cdot a \leftrightarrow z \le w$ under a positive multiplier. Each direction is discharged by nlinarith.
why it matters
The parent consumer is integer_order_certificate, which asserts that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, Boolean leq, absolute difference, and the nonneg flag/toInt bridge; the present cancellation law is one of the algebraic order facts the surface must hold before the certificate can be assembled.
In the broader Recognition stack this sits under Foundation: integers and their order are forced from the primitive recognition calculus rather than imported from Mathlib's Int. Positive-multiplier order preservation is the standard ordered-ring axiom needed so later mass-ladder and ledger comparisons can cancel strictly positive scale factors without leaving the internal carrier. It does not itself touch T5–T8 or the RCL; it is pure arithmetic infrastructure those layers rely on once integers are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.