abs_mul_eq_zero_iff
plain-language theorem explainer
The absolute value of a product of two signed orbits vanishes exactly when at least one factor has vanishing absolute value. Foundation workers building the internal integer order on distinction orbits cite this to transfer the no-zero-divisors law from LogicInt onto the signed-orbit surface. The proof rewrites absolute-value vanishing into integer vanishing via the toInt bridge, applies the LogicInt zero-divisor law, and closes both directions by ring simplification.
Claim. For signed orbits $z,w$ (pairs of distinction-naturals read as $\mathrm{pos}-\mathrm{neg}$), $|z\cdot w|=0$ if and only if $|z|=0$ or $|w|=0$, where absolute value is the distinction-natural absolute difference of the two components and $0$ is the zero distinction-natural.
background
Signed orbits (K4.6) are pairs of distinction-naturals intended as the difference $\mathrm{pos}-\mathrm{neg}$. DistinctionNat (K2.12) is the base-neutral finite orbit of repeated distinction, the primitive natural carrier in the recognition calculus. Absolute value on a signed orbit is the absolute difference of its components, returning a DistinctionNat.
This module equips signed orbits with an internal order surface. Upstream, LogicInt has no zero divisors: from $a\cdot b=0$ one gets $a=0$ or $b=0$, forced by the ring isomorphism with $\mathbb{Z}$. Signed-orbit multiplication is compatible with the integer embedding: $(zw).\mathrm{toInt}=z.\mathrm{toInt}\cdot w.\mathrm{toInt}$. Absolute value vanishes exactly when the integer image vanishes.
proof idea
Rewrite every absolute-value-equals-zero atom via the bridge that abs vanishes iff toInt vanishes, and replace the product's toInt by the product of the toInts (mul_toInt). The biconditional collapses to the LogicInt statement $a\cdot b=0\leftrightarrow a=0\lor b=0$. Forward direction: apply mul_eq_zero and split the disjunction. Converse: substitute the zero factor and simplify each case by ring.
why it matters
Direct parent of the complementary non-vanishing form abs_mul_ne_zero_iff in the same module. Also consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed"; that certificate packages display lemmas for truncated subtraction, order flags, and nonnegativity, so the absolute-value zero-divisor law is part of algebraic coherence of the order surface. In the Recognition foundation stack this sits in the primitive recognition calculus that builds integers from distinction orbits, beneath the forcing chain (T0–T8) and the J-cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.