abs_mul_ofOrbit_right
plain-language theorem explainer
Absolute value is homogeneous under right-multiplication by a nonnegative orbit embedding: |z · ι(d)| equals |z| · d as distinction-orbit positions. Order and certificate authors cite it when reducing signed products to unsigned arithmetic. The proof injects through toNat and rewrites via the integer display of mul and abs.
Claim. For every signed orbit $z$ and every distinction-orbit position $d$, if $\iota(d)$ is the nonnegative signed orbit with positive part $d$ and zero negative part, then $|z \cdot \iota(d)| = |z| \cdot d$ as distinction-orbit positions.
background
In the primitive recognition calculus, integers are recovered as signed orbits: pairs of distinction-orbit positions (positive and negative parts). DistinctionNat is the unsigned orbit type; SignedOrbit packages a pair and exposes toInt as the difference of the two toNat displays.
Absolute value on a signed orbit is the orbit-level absolute difference of the two parts, and abs_toNat states that this display equals Int.natAbs of toInt. Nonnegative embeddings are ofOrbit d := ⟨d, 0⟩, with ofOrbit_toInt simplifying to d.toNat.
Multiplication of signed orbits is defined so that mul_toInt recovers ordinary integer multiplication. Upstream, toNat_mul is the recovery theorem that LogicNat multiplication agrees with Nat multiplication under the equivalence.
proof idea
Term-mode proof. Apply injectivity of DistinctionNat.toNat, then rewrite both sides into integer arithmetic: abs_toNat on the product, mul_toInt and ofOrbit_toInt to expose z.toInt * (d.toNat : ℤ), then toNat_mul and a second abs_toNat, finishing with Int.natAbs_mul and Int.natAbs_natCast. 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). Homogeneity of abs under right-multiplication by nonnegative embeddings is a basic compatibility fact needed so order and magnitude stay coherent when scaling by orbit positions.
In the Recognition foundation stack this sits below the forcing chain (T0–T8): it is arithmetic infrastructure for the integer layer built from distinction orbits, not yet a physics forcing step. It closes a small but necessary gap between signed multiplication and the unsigned abs used in order lemmas (siblings include trichotomy, sign-flag exclusivity, and zero-comparisons).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.