abs_mul_ne_zero_iff
plain-language theorem explainer
Absolute value of a product of signed orbits is nonzero exactly when both factors have nonzero absolute value. Anyone building the integer-order surface on signed orbits cites this as the nonzero half of the zero-product law. The proof is a short classical dual of the already-proved zero-product equivalence.
Claim. For signed orbits $z,w$ (each a pair of distinction-orbit positions meaning $\mathrm{pos}-\mathrm{neg}$), $|z\cdot w|\neq 0$ if and only if $|z|\neq 0$ and $|w|\neq 0$, where $|\cdot|$ is the absolute difference of the two orbit components and $0$ is the zero distinction orbit.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is a pair of such orbits, intended as $\mathrm{pos}-\mathrm{neg}$. Its absolute value is the absolute difference of those two components, landing back in DistinctionNat.
Multiplication of signed orbits is defined so that it matches integer multiplication after the embedding to $\mathbb{Z}$. The sibling lemma abs_mul_eq_zero_iff already states the zero-product law: the absolute value of a product vanishes exactly when at least one factor has vanishing absolute value.
This module develops the internal order on signed orbits (reflexivity, totality, trichotomy, sign flags). The nonzero product law is the dual form needed when one reasons by contraposition about nonvanishing magnitudes.
proof idea
One-step dual of SignedOrbit.abs_mul_eq_zero_iff. Bind that equivalence as hzero. The forward direction: if the product absolute value is nonzero, neither factor can be zero, else hzero.mpr with Or.inl/Or.inr would force the product absolute value to zero. The reverse: if both factors are nonzero and the product absolute value were zero, hzero.mp yields a disjunction, and each branch contradicts one of the factor hypotheses. Pure classical constructor/intro/rcases reasoning; no new arithmetic.
why it matters
Feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, $\leq$, absolute difference, and signed nonnegativity flags. The nonzero product law is the magnitude half of the ring-like structure underlying that order surface: without it, nonvanishing of products cannot be reduced to nonvanishing of factors when comparing signed orbits.
In the broader Recognition stack this sits in Foundation, before the forcing chain (T5 J-uniqueness through T8 $D=3$). It is bookkeeping for the integer model of distinction orbits, not a physics claim, but the certificate it supports is part of closing the primitive calculus that later layers assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.