lt_scaleByNat_iff_of_ne_zero
plain-language theorem explainer
Strict order on signed orbits is invariant under scaling by a nonzero natural distinction: z scaled by d is strictly below w scaled by d exactly when z is strictly below w. Comparison and multiplication-by-orbit lemmas on the integer order surface cite this, as does the closed-order certificate. The proof embeds both sides into ℤ via toInt, uses positivity of d, and finishes by linear arithmetic.
Claim. For signed orbits $z,w$ and a natural distinction $d\neq 0$, writing $\cdot$ for scaling a signed orbit by a natural distinction and $<$ for the internal strict order on signed orbits, one has $z\cdot d < w\cdot d$ if and only if $z < w$.
background
In the primitive recognition calculus, integers are realized as signed orbits: an orbit position together with a sign flag. The internal strict order on signed orbits is defined as the conjunction of the weak order with failure of balance (nonnegative nonzero difference). That order is characterized by the embedding into ordinary integers: $z < w$ iff the integer image of $z$ is strictly less than that of $w$.
Scaling by a natural distinction multiplies the underlying orbit magnitude by a DistinctionNat value. The companion lemma scaleByNat_toInt records that this operation becomes ordinary multiplication by d.toNat after the integer embedding. Distinction naturals themselves sit on the logic-derived natural numbers, with toNat reading off the iteration count and sending the zero distinction to $0$.
The local module assembles the order surface on these signed orbits (reflexivity, totality, trichotomy, sign-flag characterizations) needed before rationals and the recognition cost calculus can treat integer comparisons as internal data.
proof idea
First convert $d\neq 0$ into $d.\mathrm{toNat}\neq 0$ by injectivity of toNat against toNat_zero. Cast to integers to obtain the positivity hypothesis $0<(d.\mathrm{toNat}:\mathbb{Z})$.
Rewrite both sides of the claimed biconditional with lt_iff_toInt_lt and scaleByNat_toInt. The statement becomes: multiplication of the two integer images by the positive factor $d.\mathrm{toNat}$ preserves strict inequality. Both directions are discharged by nlinarith.
why it matters
This is the strict-order half of natural scaling compatibility on the signed-orbit integer surface. Downstream, cmp_scaleByNat_of_ne_zero lifts it to the three-way comparison function, and the left/right lemmas lt_mul_ofOrbit_left_iff_of_ne_zero and lt_mul_ofOrbit_right_iff_of_ne_zero specialize it to multiplication by a positive orbit (the bridge from scaling to the monoid structure).
It is also wired into integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, absolute difference, and nonnegativity flags so later layers can treat integer order as a finished primitive rather than an open interface.
In the broader Recognition stack this sits under Foundation arithmetic-from-logic: before J-cost, the forcing chain (T5–T8), or the phi-ladder mass formula can speak about integer comparisons, the signed-orbit order must be stable under the natural scalings that build those comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.