abs_mul_eq_zero_iff_balanced_zero
plain-language theorem explainer
The absolute value of a product of two signed orbits vanishes exactly when at least one factor is balanced with zero. Order and integrality arguments in the primitive recognition calculus cite this as the no-zero-divisors law at the orbit level. The proof rewrites absolute value and balance to the integer display, then applies the LogicInt zero-divisor law and closes the reverse direction by ring.
Claim. For signed orbits $z,w$, one has $|z \cdot w| = 0$ if and only if $z$ is balanced with the zero orbit or $w$ is balanced with the zero orbit. Balance means $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; absolute value is the distinction-nat absolute difference of positive and negative orbit positions.
background
In the primitive recognition calculus, integers are carried by signed orbits: each SignedOrbit pairs a positive and a negative distinction-nat position. Two orbits are balanced when their lengths match under swap of signs, $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equality; the bridge theorem states it is equivalent to equality of the conservative $\mathbb{Z}$ displays toInt.
Absolute value of a signed orbit is the distinction-nat absolute difference of its two positions, and vanishes exactly when toInt is zero. Multiplication of signed orbits is compatible with integer multiplication via mul_toInt. Upstream, LogicInt (the ledger-forced integer type) has no zero divisors: $a\cdot b=0$ forces $a=0$ or $b=0$, by the ring isomorphism with Int.
This module builds the order surface on those signed orbits. The present statement is the product form of vanishing absolute value, phrased entirely in balance and distinction-nat zero rather than in toInt.
proof idea
Term-mode proof by rewriting and a two-way constructor. First rewrite the goal with four bridges: absolute value zero iff toInt zero; product toInt equals product of toInts; balance with zero iff toInt equals zero's toInt; and zero.toInt = 0. The goal becomes $z.\mathrm{toInt}\cdot w.\mathrm{toInt}=0$ iff $z.\mathrm{toInt}=0$ or $w.\mathrm{toInt}=0$.
Forward direction: apply mul_eq_zero from IntegersFromLogic and case-split the resulting disjunction. Reverse direction: case-split the balance hypothesis, rewrite the vanishing factor, and finish each case by ring.
why it matters
Closes the no-zero-divisors law for the internal signed-orbit product, so absolute value of a product is a faithful zero test. The immediate consumer is the negated form abs_mul_ne_zero_iff_not_balanced_zero, which packages the same fact for nonzero product tests in order arguments.
It is also wired into integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate aggregates display lemmas (truncated subtraction, leq, abs-diff, nonneg flags) that make the PRC integer order self-contained without escaping to classical Int at use sites.
In the broader Recognition foundation this sits under the ledger-forced integer layer that feeds later forcing steps; it is not itself a T0–T8 landmark, but it keeps the integer substrate choice-free and orbit-native before those steps are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.