abs_mul_ofOrbit_left_eq_zero_iff
plain-language theorem explainer
Absolute value of a nonnegative orbit times a signed orbit vanishes exactly when either factor is zero. Order and integrality lemmas in the primitive recognition calculus cite this left-ofOrbit zero-divisor law. The proof reduces both sides to integer images via toInt, then applies the no-zero-divisors property of LogicInt and injectivity of toNat.
Claim. For every nonnegative distinction count $d$ and every signed orbit $z$, $|\,d\cdot z\,|=0$ if and only if $|z|=0$ or $d=0$, where $d$ is embedded as the nonnegative signed orbit $\langle d,0\rangle$ and $|\cdot|$ is absolute value on signed orbits.
background
In the primitive recognition calculus, integers appear as signed orbits: pairs of distinction-nat positions (pos, neg). Absolute value is the orbit position absDiff(pos, neg). The embedding ofOrbit sends a nonnegative DistinctionNat $n$ to the signed orbit $\langle n,0\rangle$. Multiplication is defined so that toInt is a ring homomorphism: $(\mathrm{mul},a,b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$.
Absolute value vanishes exactly when the integer image is zero (abs_eq_zero_iff_toInt_eq_zero). Upstream, LogicInt has no zero divisors: "$a*b=0$ iff $a=0$ or $b=0$. Forced by the ring isomorphism with Int." DistinctionNat.toNat_zero records that the zero distinction maps to the natural $0$.
This module assembles the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags).
proof idea
Rewrite both sides with abs_eq_zero_iff_toInt_eq_zero, then expand mul_toInt and ofOrbit_toInt. The claim becomes $(\mathrm{toNat},d:\mathbb{Z})\cdot z.\mathrm{toInt}=0$ iff $z.\mathrm{toInt}=0$ or $d=0$.
Forward: apply mul_eq_zero. If the left factor is zero, DistinctionNat.toNat_inj plus toNat_zero recovers $d=\mathrm{zero}$; if the right factor is zero, that is $|z|=0$. Reverse: case-split on the disjunction and reduce each product to zero by ring.
why it matters
Direct parent of the complementary nonvanishing form abs_mul_ofOrbit_left_ne_zero_iff, which rewrites this biconditional under negation. Also consumed by integer_order_certificate, whose doc states "The internal signed-orbit order surface is closed," packaging nonneg flags, absdiff display, and truncated subtraction.
In the Recognition foundation stack this sits under arithmetic-and-order-from-logic, before the forcing chain (T0–T8), J-uniqueness, and the phi ladder. It is a fully proved integrality lemma, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.