abs_scaleByNat
plain-language theorem explainer
Absolute value on signed orbits commutes with positive scaling: scaling a signed orbit by a distinction multiplies its absolute value by that distinction. Developers of the internal integer-order surface cite it when assembling the order certificate. The proof is a short term rewrite: injectivity of the Nat display, then abs and scale lemmas plus Int.natAbs_mul.
Claim. For every signed orbit $z$ (pair of orbit positions, meaning $\mathrm{pos}-\mathrm{neg}$) and every distinction $d$, the absolute value of $z$ scaled by $d$ equals the product of $|z|$ with $d$: $|\mathrm{scale}(z,d)| = |z|\cdot d$.
background
In the primitive recognition calculus, integers are recovered as signed orbit differences. A SignedOrbit is a pair of distinction positions (pos, neg) with intended meaning $\mathrm{pos}-\mathrm{neg}$. Its absolute value is the orbit-level absolute difference of those two positions, displayed on $\mathbb{N}$ by $\mathrm{Int.natAbs}$ of the integer embedding.
Scaling by a (positive-only) distinction multiplies both legs: $\mathrm{scale}(z,d)=(\mathrm{pos}\cdot d,,\mathrm{neg}\cdot d)$. The companion lemma scaleByNat_toInt records that this is ordinary integer multiplication by $d$ under the embedding. Multiplication of distinctions itself recovers ordinary Nat multiplication via the ArithmeticFromLogic recovery theorem toNat_mul.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). Absolute-value compatibility with scaling is one of the arithmetic identities needed before the certificate can close.
proof idea
Term-mode proof. Apply injectivity of DistinctionNat.toNat so it suffices to check equality after the Nat display. Rewrite the left side with abs_toNat and scaleByNat_toInt, turning absolute value of the scaled orbit into $\mathrm{natAbs}(z.\mathrm{toInt}\cdot d)$. Expand the product with toNat_mul and the right-hand abs_toNat, then finish by Int.natAbs_mul and Int.natAbs_natCast (since $d$ is a cast natural). No induction; pure display transport.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (nonnegativity, flags, abs-diff and truncated-sub displays all match). Without $|zd|=|z|d$, absolute value would not be homogeneous under the positive monoid action that builds the integer lattice from orbit arithmetic.
In the Recognition foundation stack this sits under ArithmeticFromLogic and the primitive recognition calculus: integers and their order are not imported from Mathlib as primitives but reconstructed from distinction orbits. Homogeneity of abs under scaling is a small but necessary bridge between the multiplicative structure on distinctions and the ordered group structure on signed orbits, upstream of later forcing-chain material that needs a coherent integer layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.