le_mul_ofOrbit_right_iff_of_ne_zero
plain-language theorem explainer
Right-multiplication by a nonzero nonnegative orbit preserves the signed-orbit order in both directions: z ≤ w if and only if z·ofOrbit(d) ≤ w·ofOrbit(d) whenever d ≠ 0. Order theorists building the integer lattice from recognition orbits cite this cancellation law. The proof reduces multiplication to scale-by-nat via a balanced equivalence, then applies the existing scale-by-nat order iff.
Claim. For signed orbits $z,w$ and a nonzero distinction $d$, one has $z \cdot \mathrm{ofOrbit}(d) \le w \cdot \mathrm{ofOrbit}(d)$ if and only if $z \le w$, where $\mathrm{ofOrbit}(d)$ is the nonnegative signed orbit with magnitude $d$, and $\le$ means the difference is nonnegative.
background
In the primitive recognition calculus, integers are realized as signed orbits: pairs of distinction-nats encoding positive and negative parts. The internal order is defined by nonnegativity of the difference: $a \le b$ means $\mathrm{sub}(b,a)$ is nonnegative. The embedding $\mathrm{ofOrbit}$ sends a distinction-nat $d$ to the nonnegative signed orbit $\langle d, 0\rangle$.
Multiplication of signed orbits interacts with a simpler scaling operation $\mathrm{scaleByNat}$. The lemma $\mathrm{mul_ofOrbit_balanced_scaleByNat}$ records that $z \cdot \mathrm{ofOrbit}(d)$ is balanced with $z.\mathrm{scaleByNat}(d)$ (same integer value under the toInt map). Balanced pairs are interchangeable for the order: $\mathrm{le_congr_of_balanced}$ says $a \le b$ iff $a' \le b'$ whenever $a$ is balanced with $a'$ and $b$ with $b'$.
Separately, $\mathrm{le_scaleByNat_iff_of_ne_zero}$ already gives cancellation for scaling: when $d \ne 0$, $z.\mathrm{scaleByNat}(d) \le w.\mathrm{scaleByNat}(d)$ iff $z \le w$. The present theorem lifts that fact to genuine right-multiplication by a nonnegative orbit.
proof idea
Term-mode composition of two prior facts. First apply $\mathrm{le_congr_of_balanced}$ to the two balanced identities $\mathrm{mul_ofOrbit_balanced_scaleByNat}, z, d$ and $\mathrm{mul_ofOrbit_balanced_scaleByNat}, w, d$. That rewrites the desired comparison of products into a comparison of scale-by-nat images. Then transitively apply $\mathrm{le_scaleByNat_iff_of_ne_zero}, z, w, d, hd$, which cancels the nonzero scale factor. No new case analysis is introduced.
why it matters
This is one of the order-cancellation laws needed to close the internal signed-orbit order surface. Downstream it is consumed by $\mathrm{integer_order_certificate}$, whose doc-comment states that the certificate packages the closed order surface (nonnegativity displays, leq display, absdiff, signed nonneg flags). Without right-multiplication cancellation, the order would not behave like the standard integer order under the orbit embedding of positive magnitudes.
In the Recognition foundation stack this sits inside Arithmetic-from-Logic and the Primitive Recognition Calculus: integers and their order are not postulated but derived from distinction orbits. The result is pure order algebra; it does not itself invoke the forcing chain (T5–T8) or the J-cost, but it supplies the integer substrate those later layers quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.