le_scaleByNat_of_le
plain-language theorem explainer
If two signed orbits satisfy z ≤ w, scaling both by the same distinction count d preserves the inequality. Order theorists and anyone building the integer lattice from recognition orbits cite this monotonicity fact. The proof rewrites to ℤ via the toInt bridge, notes that d maps to a nonnegative integer, and finishes by linear arithmetic.
Claim. Let $z,w$ be signed orbits and let $d$ be a distinction count. If $z \le w$ in the internal signed-orbit order (equivalently $z$ maps to an integer no larger than $w$), then scaling both orbits by $d$ preserves the order: $z\cdot d \le w\cdot d$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: each carries a positive and a negative distinction count. The order le is defined by nonnegativity of the difference $b-a$, and is equivalent to the ordinary integer order after the toInt embedding (le_iff_toInt_le).
Scaling by a distinction count multiplies both the positive and negative legs by that count (scaleByNat). Distinction counts themselves come from the logic-native naturals (LogicNat / DistinctionNat), whose order is the usual existential-witness order $n \le m \Leftrightarrow \exists k., n+k=m$, and which embed into Nat via toNat.
The local module develops the full order surface on signed orbits (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations). This lemma is the monotonicity of scaling under that order.
proof idea
Rewrite the hypothesis and goal through le_iff_toInt_le, so both become ordinary integer inequalities. Replace each scaled orbit by its integer image via scaleByNat_toInt (so the goal is essentially $z_{\mathbb{Z}}\cdot d_{\mathbb{N}} \le w_{\mathbb{Z}}\cdot d_{\mathbb{N}}$). Cast Nat.zero_le to obtain $0 \le (d.\mathrm{toNat}:\mathbb{Z})$, then close with nlinarith.
why it matters
Monotonicity of scaling is part of the closed order surface on signed orbits. It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed" and packages display lemmas for truncated subtraction, comparison flags, absolute difference, and nonnegativity.
In the Recognition foundation stack this sits under Arithmetic-from-Logic: integers are recovered as signed orbits before rationals and the J-cost calculus. The lemma does not itself touch T5–T8 or the Recognition Composition Law, but it is infrastructure those layers rely on once magnitudes live on the integer lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.