le_scaleByNat_iff_of_ne_zero
plain-language theorem explainer
Scaling both sides of a signed-orbit comparison by a nonzero natural distinction preserves the order in both directions. Anyone assembling the ordered integer surface from recognition orbits cites this cancellation law. The proof pushes the relation through the integer embedding, records that the scale factor is a positive integer, and closes both directions by linear arithmetic.
Claim. Let $z,w$ be signed orbits and let $d$ be a nonzero distinction natural. Then $\mathrm{scale}(z,d)\le\mathrm{scale}(w,d)$ if and only if $z\le w$, where $\le$ is the internal signed-orbit order (nonnegative difference) and $\mathrm{scale}(\cdot,d)$ multiplies the underlying integer by the natural value of $d$.
background
In the primitive recognition calculus, integers are realized as signed orbits: an orbit of distinctions together with a sign. The internal order on signed orbits declares $a\le b$ precisely when the difference $b-a$ is nonnegative. Distinction naturals supply the nonnegative magnitudes; each carries a toNat reading that recovers an ordinary natural number, with zero mapping to $0$.
Scaling a signed orbit by a distinction natural multiplies its integer image by that natural value. The companion characterization le_iff_toInt_le states that the internal order agrees exactly with the standard order on the embedded integers. The local module builds the ordered-ring surface on these orbits; the present lemma is the cancellation step for positive natural scaling.
Upstream arithmetic-from-logic supplies the nonnegative order on logic naturals (existence of a summand) and the zero law for toNat, which together let a nonzero distinction natural be recognized as a strictly positive integer coefficient.
proof idea
First convert the hypothesis $d\neq 0$ into $d.\mathrm{toNat}\neq 0$ by injectivity of toNat and the zero law toNat_zero. Cast that natural inequality to obtain $0<(d.\mathrm{toNat}:\mathbb{Z})$.
Rewrite both sides of the desired biconditional via le_iff_toInt_le, then expand each scaled orbit with scaleByNat_toInt. The claim becomes the elementary integer statement
$$d_\mathbb{Z}\cdot z_\mathbb{Z}\le d_\mathbb{Z}\cdot w_\mathbb{Z}\iff z_\mathbb{Z}\le w_\mathbb{Z}$$
with $d_\mathbb{Z}>0$. Both directions finish by nlinarith.
why it matters
Positive-scale cancellation is a structural axiom of any ordered abelian group; here it is proved rather than assumed, from the integer embedding of signed orbits. Downstream it is applied directly by the left and right multiplication lemmas le_mul_ofOrbit_left_iff_of_ne_zero and le_mul_ofOrbit_right_iff_of_ne_zero, which treat multiplication by a nonzero pure orbit as order-reflecting. Those facts feed the closed certificate integer_order_certificate, whose doc-comment records that "the internal signed-orbit order surface is closed."
In the Recognition foundation this sits beneath the forcing chain: once integers carry a total order compatible with scaling, the later construction of rationals, the J-cost calculus, and the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ have a coherent ordered substrate. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.