cmp_mul_ofOrbit_left_of_ne_zero
plain-language theorem explainer
Left-multiplication by a nonzero nonnegative orbit element preserves signed-orbit comparison: cmp(d·z, d·w) equals cmp(z, w). Order theorists building the integer-order certificate cite it to show positive scaling is order-faithful. The proof chains balanced-congruence of cmp with the already-proved scaleByNat invariance.
Claim. Let $d$ be a nonzero distinction natural and let $z,w$ be signed orbits. Then $\mathrm{cmp}(\widehat{d}\cdot z,\,\widehat{d}\cdot w)=\mathrm{cmp}(z,w)$, where $\widehat{d}$ is the nonnegative signed orbit with positive part $d$ and zero negative part, and $\mathrm{cmp}$ is the internal signed-orbit comparison (equality on balanced pairs, otherwise the sign of the difference).
background
Signed orbits are the K4.6 difference type: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$. The map $\mathrm{ofOrbit}$ embeds a distinction natural $d$ as the nonnegative orbit $(d,0)$. Internal comparison $\mathrm{cmp}$ is not the verifier integer display; it returns equality when the two orbits are balanced, otherwise orders by the nonnegativity flag of the difference.
Multiplication of signed orbits interacts with natural scaling: $\mathrm{ofOrbit}(d)\cdot z$ is balanced with $z.\mathrm{scaleByNat},d$. The companion lemma $\mathrm{cmp_scaleByNat_of_ne_zero}$ already states that scaling both arguments by a nonzero distinction natural leaves $\mathrm{cmp}$ unchanged. Balanced pairs may be substituted under $\mathrm{cmp}$ by $\mathrm{cmp_congr_of_balanced}$.
This module builds the order surface on those primitives so that the later integer-order certificate can close without appealing to external $\mathbb{Z}$ order.
proof idea
Term-mode equality chain. First apply $\mathrm{cmp_congr_of_balanced}$ to the two balanced identities $\mathrm{ofOrbit_mul_balanced_scaleByNat},d,z$ and $\mathrm{ofOrbit_mul_balanced_scaleByNat},d,w$, which rewrites $\mathrm{cmp}(\widehat{d}\cdot z,\widehat{d}\cdot w)$ into $\mathrm{cmp}(z.\mathrm{scaleByNat},d,,w.\mathrm{scaleByNat},d)$. Then transitively apply $\mathrm{cmp_scaleByNat_of_ne_zero},z,w,d,hd$, using $d\neq 0$, to recover $\mathrm{cmp}(z,w)$.
why it matters
Feeds the single downstream parent $\mathrm{integer_order_certificate}$, whose doc-comment states that "the internal signed-orbit order surface is closed." Without left-multiplication invariance for nonzero orbit factors, the certificate could not treat positive scaling as order-preserving on the primitive recognition calculus side.
In the Recognition foundation stack this sits under PrimitiveRecognitionCalculus: it is bookkeeping that makes the signed-orbit order a genuine ordered monoid fragment before any appeal to the forcing chain (T0–T8) or the J-cost. It does not itself force $\phi$ or dimension; it only seals that the integer-order display is faithful under left multiplication by nonzero nonnegative orbits, a prerequisite for later ladder and mass constructions that read order off signed orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.