lt_mul_ofOrbit_right_iff_of_ne_zero
plain-language theorem explainer
Right-multiplication by a nonzero nonnegative orbit preserves and reflects strict order on signed orbits. Anyone closing the integer-order surface for the primitive recognition calculus cites this. The proof is a two-step term: balanced-congruence reduces multiplication to natural scaling, then the nonzero scaling lemma finishes.
Claim. For signed orbits $z,w$ and a distinction-natural $d\neq 0$, writing $\iota(d)$ for the nonnegative signed orbit built from $d$, one has $z\cdot\iota(d)<w\cdot\iota(d)$ if and only if $z<w$.
background
In the primitive recognition calculus, integers are carried by signed orbits: pairs of distinction-naturals with a balanced-equivalence that identifies opposite presentations of the same integer. The internal strict order is the nonnegative-difference relation with a nonzero (non-balanced) difference: $a<b$ means $a\le b$ and $a$ is not balanced with $b$.
The map $\iota$ (ofOrbit) embeds a distinction-natural $d$ as the nonnegative signed orbit $\langle d,0\rangle$. Right-multiplication by $\iota(d)$ is the orbit-level avatar of scaling by $d$. An upstream lemma records that this product is balanced with the explicit scale-by-nat operation on the same signed orbit, so the two presentations agree as integers.
The local module builds the full order theory (reflexivity, totality, trichotomy, sign flags) needed before the integer-order certificate can close. The key comparison lemmas already proved are congruence of $<$ under balanced equivalence, and the iff that scale-by-nat by nonzero $d$ preserves and reflects $<$.
proof idea
Term-mode composition of two prior results. First apply balanced-congruence of strict order to both sides: multiplying $z$ (resp. $w$) on the right by $\iota(d)$ is balanced with scaling $z$ (resp. $w$) by $d$, so the product comparison is equivalent to the scaled comparison. Then chain the nonzero scale-by-nat lemma, which states that scaling both sides by $d\neq 0$ preserves and reflects $<$. The hypothesis $d\neq 0$ is threaded only into that second step.
why it matters
This is one of the multiplicative comparison laws that let the signed-orbit order behave like the usual order on $\mathbb{Z}$ under positive scaling. Downstream it is consumed by the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed": the certificate packages display lemmas for truncated subtraction, absolute difference, nonnegativity, and the signed order flags.
In the Recognition foundation stack this sits under Arithmetic-from-Logic: distinction-naturals and signed orbits are the pre-numeric carriers from which ordinary integer arithmetic is recovered. Closing order under right-multiplication by nonzero orbits is a necessary step before later forcing-chain material can treat integer comparisons as settled infrastructure rather than open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.