abs_mul
plain-language theorem explainer
Absolute value is multiplicative on signed orbits: |z·w| = |z|·|w|. Anyone proving magnitude identities for integer-like orbit differences cites this. The proof reduces both sides to Nat via the toNat injection, then applies the classical |ab| = |a||b| identity after transporting through the signed-orbit integer embedding.
Claim. For any signed orbits $z,w$ (pairs of distinction-counts interpreted as $z = \mathrm{pos}-\mathrm{neg}$), the absolute value of the product equals the product of the absolute values: $|z\cdot w| = |z|\cdot|w|$, where absolute value is the nonnegative distinction-count $|z| = |\mathrm{pos}-\mathrm{neg}|$.
background
Signed orbits are the integer layer of the primitive recognition calculus: a pair (pos, neg) of DistinctionNat values, read as the difference pos − neg. DistinctionNat is the base-neutral finite orbit of repeated distinction (zero/succ), the RS stand-in for natural numbers before classical Nat is recovered.
Absolute value on a signed orbit is defined as the distinction-count absolute difference of the two legs, so it lands back in nonnegative orbit positions. Multiplication of signed orbits is the usual cross-term rule that makes the integer embedding a ring homomorphism: (mul z w).toInt = z.toInt * w.toInt.
Upstream, abs_toNat identifies the internal absolute value with classical Int.natAbs after display, and toNat_mul (from ArithmeticFromLogic and OrbitArithmetic) says multiplication of distinction-counts agrees with Nat multiplication under the equivalence. Those two bridges let magnitude facts on signed orbits inherit ordinary integer arithmetic.
proof idea
Term/tactic hybrid, four lines. Apply DistinctionNat.toNat_inj so it suffices to check equality after toNat. Rewrite the left side by abs_toNat, then mul_toInt to push the product into Int, then DistinctionNat.toNat_mul on the absolute values, then abs_toNat on each factor, and finish with the classical Int.natAbs_mul. No case split on signs: the integer embedding carries the sign bookkeeping.
why it matters
This is the magnitude homomorphism for the signed-orbit layer. Downstream it is the rewrite that turns product magnitudes into factor magnitudes throughout the stack.
In cosmology it powers the B0 sphaleron magnitude package: BfinalFromRelicBL_abs_lt_of_ne (strict contraction |B_final| < |B−L| via the 28/79 factor), sphaleron_cannot_amplify_magnitude and sphaleron_cannot_suppress_magnitude (the closed band |B_final| ∈ [|B−L|/3, |B−L|/2]), and sphaleron_source_floor (equilibrium baryon size forces a strictly larger B−L source). Those results treat sphaleron reprocessing as a pure magnitude map, not a relabel.
On the cost side it appears in small-strain J-cost expansions (Jcost_one_plus_eps_quadratic, Jcost_small_strain_bound) and gauge-orbit character work, where absolute values of products must factor cleanly. It is ordinary ring absolute-value multiplicativity, but proved on the RS-native integer type rather than assumed from Mathlib ℤ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.