abs_mul_ofOrbit_left
plain-language theorem explainer
Multiplying a signed orbit on the left by a nonnegative orbit embedding scales absolute value by that orbit's magnitude. Anyone building the internal integer order or verifying that signed-orbit multiplication respects the nonnegative cone cites this identity. The proof injects into natural numbers and rewrites through the toInt and abs display lemmas, finishing by ring.
Claim. For every distinction-orbit position $d$ and every signed orbit $z$, $\lvert \iota(d)\cdot z\rvert = \lvert z\rvert\cdot d$, where $\iota$ embeds a nonnegative orbit as a signed orbit with zero negative part, $\lvert\cdot\rvert$ is the absolute-value orbit (absolute difference of positive and negative parts), and multiplication is signed-orbit multiplication.
background
In the primitive recognition calculus, integers are realized as signed orbits: pairs of distinction-orbit positions (positive and negative parts). The embedding of a bare orbit position $d$ is the nonnegative signed orbit with positive part $d$ and zero negative part. Absolute value of a signed orbit is the distinction-orbit absolute difference of those two parts, recovering the usual magnitude when displayed as a natural number.
Signed-orbit multiplication is defined so that its integer display multiplies: $(\mathrm{mul},a,b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$. Distinction-orbit multiplication recovers ordinary $\mathrm{Nat}$ multiplication under $\mathrm{toNat}$. The local module develops the order surface on these internal integers (reflexivity, totality, trichotomy, sign flags) before packaging a closure certificate.
proof idea
Term-mode proof by injectivity of $\mathrm{toNat}$ on distinction orbits. After applying that injection, rewrite the left-hand absolute value via $\mathrm{abs_toNat}$, expand the product with $\mathrm{mul_toInt}$ and $\mathrm{ofOrbit_toInt}$, push multiplication through $\mathrm{toNat_mul}$, and apply $\mathrm{abs_toNat}$ again on $z$. The remaining integer identity is $\mathrm{Int.natAbs_mul}$ with $\mathrm{Int.natAbs_natCast}$, closed by $\mathrm{ring}$.
why it matters
Feeds the single downstream package $\mathrm{integer_order_certificate}$, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate aggregates display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags; left-scaling of absolute value by nonnegative embeddings is part of making absolute value and multiplication coherent on the order surface.
In the Recognition foundation stack this sits under arithmetic recovered from logic (LogicNat equivalence) and the signed-orbit model of integers, before higher forcing-chain physics. It is pure algebraic bookkeeping: no J-cost, phi-ladder, or dimensional claim is at stake, but the certificate it supports is a prerequisite for treating internal integers as an ordered ring in later recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.