cmp_mul_ofOrbit_right_of_ne_zero
plain-language theorem explainer
Right-multiplication of two signed orbits by the same nonzero nonnegative orbit leaves their comparison unchanged. Anyone assembling the closed integer-order surface from signed-orbit primitives cites this invariance. The proof is a two-step term: balanced-congruence reduces the multiplications to scale-by-nat, then scale-invariance of the comparator finishes it.
Claim. Let $z,w$ be signed orbits and let $d$ be a nonzero distinction. Write $\iota(d)$ for the nonnegative signed orbit with positive part $d$ and zero negative part. Then $\mathrm{cmp}\bigl(z\cdot\iota(d),\, w\cdot\iota(d)\bigr)=\mathrm{cmp}(z,w)$, where $\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 primitive for integer differences: a pair $(\mathrm{pos},\mathrm{neg})$ of distinctions, read as $\mathrm{pos}-\mathrm{neg}$. The map $\iota$ (ofOrbit) embeds a bare distinction $d$ as the nonnegative signed orbit $\langle d,0\rangle$. Multiplication of signed orbits and the auxiliary scale-by-nat operation both act componentwise on these pairs.
The internal comparator $\mathrm{cmp}$ is defined from signed-orbit order and balanced length, not from any external integer display: it returns equality when the two arguments are balanced, otherwise reads the nonnegativity flag of their difference. A prior lemma records that multiplying by $\iota(d)$ is balanced with scaling by $d$, so the two operations agree up to the balanced relation.
The local module builds the order theory of these signed orbits (reflexivity, totality, trichotomy, sign flags) as the foundation layer beneath the integer-order certificate.
proof idea
Term-mode composition of two existing facts. First apply balanced-congruence of $\mathrm{cmp}$: because $z\cdot\iota(d)$ is balanced with $z$ scaled by $d$, and likewise for $w$, the comparator on the two products equals the comparator on the two scaled orbits. Then chain with the already-proved scale-invariance lemma: when $d\neq 0$, scaling both arguments by $d$ does not change $\mathrm{cmp}$. The composite equality is exactly the claim.
why it matters
This is one of the multiplicative stability facts needed to close the internal signed-orbit order surface. Downstream it is consumed by the integer-order certificate, whose doc-comment states that surface is closed and packages display lemmas for truncated subtraction, $\leq$, absolute difference, and signed nonnegativity flags.
In the Recognition foundation stack, signed orbits are the pre-display integer layer: order must be invariant under right-multiplication by nonzero nonnegative orbits before one can trust that the later integer display and the $\phi$-ladder mass bookkeeping see a coherent total order. The result is pure order algebra; it does not itself invoke J-cost, RCL, or the T0–T8 forcing chain, but it underwrites the integer substrate those landmarks sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.