abs_mul_ne_zero_iff_not_balanced_zero
plain-language theorem explainer
The absolute value of a product of two signed orbits is nonzero exactly when neither factor is balanced against zero. Anyone assembling the internal integer-order surface from δ-orbit positions cites this as the nonzero-product gate. The argument is a short De Morgan dual of the already-proved zero-product characterization for the same multiplication.
Claim. For signed orbits $z$ and $w$, $(\mathrm{mul}(z,w)).\mathrm{abs} \neq 0$ if and only if $z$ is not balanced with the zero signed orbit and $w$ is not balanced with the zero signed orbit.
background
In the Primitive Recognition Calculus, integers appear as signed orbits: pairs of distinction-orbit positions. Two signed orbits $a,b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal PRC integer relation, defined entirely on $\delta$-orbit positions. Absolute value of a signed orbit is the absolute difference of its positive and negative lengths, valued in DistinctionNat.
Balance against the zero signed orbit is the native notion of being zero. The companion theorem states that the absolute value of a product vanishes exactly when at least one factor is balanced with zero. The present result is the complementary nonzero form used by order and trichotomy lemmas on the signed-orbit surface.
proof idea
Term-mode dual of the zero-product theorem. Instantiate abs_mul_eq_zero_iff_balanced_zero for the same pair, then constructor on the target biconditional. Forward: from product-abs nonzero, neither factor can balance with zero, else the zero-product direction would force product-abs to vanish. Reverse: from both non-balance hypotheses, if product-abs were zero the zero-product direction would yield a disjunction, contradicting one of the two conjuncts.
why it matters
Used by integer_order_certificate, which asserts that the internal signed-orbit order surface is closed and packages display lemmas for truncated subtraction, order flags, absolute difference, and signed nonnegativity. In the Recognition foundation stack this sits inside Primitive Recognition Calculus: integer arithmetic rebuilt from pure distinction orbits before ledger forcing and the T0–T8 chain. It is the algebraic gate that nonzero factors multiply to a nonzero absolute value, stated entirely in balance language rather than classical cancellation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.