abs_mul_ofOrbit_left_ne_zero_iff
plain-language theorem explainer
Absolute value of a nonnegative orbit times a signed orbit is nonzero exactly when both factors are nonzero. Anyone building the signed-orbit order or a zero-divisor-free integer surface cites this. The proof is a short De Morgan dual of the companion zero-product characterization.
Claim. For a distinction count $d$ and a signed orbit $z$, writing $|\cdot|$ for the absolute orbit and $\widehat{d}$ for the nonnegative signed orbit built from $d$, one has $|\widehat{d}\cdot z|\neq 0$ if and only if $|z|\neq 0$ and $d\neq 0$.
background
In the primitive recognition calculus, a DistinctionNat is an orbit position (a nonnegative count of distinctions). A SignedOrbit is a pair (pos, neg) of such positions, read as the formal difference pos - neg. The map ofOrbit embeds a nonnegative count $d$ as the signed orbit $\langle d, 0\rangle$. Absolute value sends a signed orbit to the orbit position absDiff pos neg.
Multiplication of signed orbits is defined so that it matches integer multiplication after the toInt interpretation. The companion lemma abs_mul_ofOrbit_left_eq_zero_iff already records the zero-product law: $|\widehat{d}\cdot z|=0$ iff $|z|=0$ or $d=0$. The present statement is the logical dual needed when one reasons about nonzero (invertible-scale) factors on the order surface.
The module builds an internal total order and sign calculus on these signed orbits without importing classical Int order axioms as primitives; zero and nonzero characterizations of products are the algebraic backbone of that surface.
proof idea
One-line appeal to the companion zero-product theorem abs_mul_ofOrbit_left_eq_zero_iff, then a pure propositional dualization.
Forward: if the product absolute value is nonzero, neither disjunct of the zero law can hold, so both $|z|\neq 0$ and $d\neq 0$. Each subgoal is by contradiction: feeding Or.inl or Or.inr into the reverse direction of the zero law would force the product absolute value to vanish.
Reverse: if both factors are nonzero and the product absolute value vanished, the forward direction of the zero law would yield $|z|=0$ or $d=0$, contradicting the two conjuncts. The proof is pure constructor/intro/rcases over that biconditional; no new arithmetic is introduced.
why it matters
Feeds the aggregate 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; nonzero product control is required so the order and sign flags behave like a genuine integral domain order rather than a ring with zero divisors.
In the Recognition Science foundation layer this sits under the primitive recognition calculus that precedes the forcing chain (T0–T8). Integers and their order are reconstructed from distinction orbits and signed differences before J-cost uniqueness, $\varphi$, the eight-tick octave, or $D=3$ are forced. Closing the zero/nonzero product laws is a small but mandatory algebraic step toward that certificate: without it, trichotomy and nonnegativity flags on products would not be trustworthy.
No open scaffold remains here; the claim is fully proved and only the dual of an already-proved zero law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.