le_mul_ofOrbit_left_iff_of_ne_zero
plain-language theorem explainer
Left-multiplication by a nonzero nonnegative orbit element preserves the signed-orbit order in both directions: d·z ≤ d·w if and only if z ≤ w. Order theorists building the integer lattice from recognition orbits cite this as the positive-scaling monotonicity step. The proof reduces multiplication to natural scaling via a balanced equivalence, then applies the already-proved scale-by-nat order equivalence.
Claim. Let $d$ be a nonzero distinction natural and let $z,w$ be signed orbits. Write $\iota(d)$ for the nonnegative signed orbit built from $d$. Then $\iota(d)\cdot z \le \iota(d)\cdot w$ if and only if $z \le w$, where $\le$ is the internal signed-orbit order ($a\le b$ means $b-a$ is nonnegative).
background
In the primitive recognition calculus, integers are realized as signed orbits: pairs of distinction naturals encoding positive and negative parts. The order on signed orbits is internal: $a\le b$ means the difference $b-a$ is nonnegative. The embedding $\iota$ (ofOrbit) sends a distinction natural $d$ to the nonnegative signed orbit with positive part $d$ and zero negative part.
Multiplication of signed orbits interacts with this embedding. The key upstream fact is that $\iota(d)\cdot z$ is balanced-equivalent to scaling $z$ by the natural underlying $d$: the two signed orbits represent the same integer. Balanced equivalence is the kernel of the map to ordinary integers, so order is invariant under it (le_congr_of_balanced).
Separately, scaling both sides of an inequality by a nonzero distinction natural preserves order both ways (le_scaleByNat_iff_of_ne_zero). Together these reduce left-multiplication by $\iota(d)$ to ordinary positive scaling.
proof idea
Term-mode composition of two facts. First apply le_congr_of_balanced to both sides, using ofOrbit_mul_balanced_scaleByNat on $z$ and on $w$: this rewrites $\iota(d)\cdot z\le\iota(d)\cdot w$ into $z.\mathrm{scaleByNat},d\le w.\mathrm{scaleByNat},d$. Then chain (trans) with le_scaleByNat_iff_of_ne_zero, which under $d\ne 0$ equates that scaled comparison with $z\le w$. No further case analysis.
why it matters
Feeds integer_order_certificate, which asserts that "the internal signed-orbit order surface is closed." That certificate packages display lemmas and order facts needed to treat signed orbits as a genuine ordered integer structure inside the recognition calculus.
Without positive left-multiplication monotonicity, the order would not interact correctly with the multiplicative structure inherited from distinction orbits. This is foundational arithmetic infrastructure rather than a physics forcing step (T0–T8), but it underwrites later constructions that identify RS integers with ordinary $\mathbb{Z}$ before building rationals and the $\varphi$-ladder mass formula.
Sibling results (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations) form the rest of the order package; this theorem is the multiplicative compatibility piece for nonnegative orbit multipliers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.