lt_mul_ofOrbit_left_iff_of_ne_zero
plain-language theorem explainer
Left-multiplication by a positive orbit element preserves and reflects the strict order on signed orbits. Anyone building ordered-ring structure on the recognition integers cites this. The proof reduces multiplication to natural scaling via a balanced-identity, then applies the known scale-by-nonzero criterion.
Claim. Let $d$ be a nonzero distinction-natural and let $z,w$ be signed orbits. Then $\mathrm{ofOrbit}(d)\cdot z < \mathrm{ofOrbit}(d)\cdot w$ if and only if $z < w$, where $<$ is the internal strict order (nonnegative difference that is not balanced).
background
Signed orbits are the recognition-calculus model of integers: each is a pair of distinction-naturals recording positive and negative parts. The map $\mathrm{ofOrbit}$ embeds a nonnegative distinction-natural $d$ as the signed orbit $\langle d,0\rangle$. Strict order on signed orbits is defined internally as the conjunction of the weak order with failure of balance (equal integer value).
Balance is the equivalence that identifies representatives with the same integer content. The lemma $\mathrm{ofOrbit_mul_balanced_scaleByNat}$ states that left-multiplying by $\mathrm{ofOrbit}(d)$ is balanced with ordinary scaling of the orbit by $d$. Scaling by a nonzero distinction-natural already preserves and reflects strict order ($\mathrm{lt_scaleByNat_iff_of_ne_zero}$).
The ambient module builds the ordered arithmetic surface on these signed orbits from pure recognition primitives, feeding the integer-order certificate.
proof idea
Term-mode chain of two equivalences. First apply $\mathrm{lt_congr_of_balanced}$ to both sides, using $\mathrm{ofOrbit_mul_balanced_scaleByNat}$ on $z$ and on $w$: this rewrites left-multiplication by $\mathrm{ofOrbit}(d)$ into $\mathrm{scaleByNat},d$ up to balance, so the strict-order comparison is unchanged. Then transitively apply $\mathrm{lt_scaleByNat_iff_of_ne_zero}$ with the hypothesis $d\neq 0$, which yields the desired iff with the unscaled comparison $z<w$.
why it matters
This is one of the order-compatibility facts required to close the signed-orbit order surface. Downstream it is consumed by $\mathrm{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 flags, and related order primitives.
In the Recognition foundation stack, ordered integers sit under the arithmetic-from-logic layer that eventually supports the forcing chain. The result is pure order algebra (no physical constants), but it is load-bearing for any later claim that the recognition integers form an ordered ring compatible with the $\phi$-ladder and mass formulas. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.