abs_mul_ofOrbit_right_ne_zero_iff
plain-language theorem explainer
Absolute value of a signed orbit multiplied on the right by a nonnegative orbit embedding is nonzero exactly when both factors are nonzero. Anyone assembling the signed-orbit integer order cites this as the nonzero product rule. The proof is the De Morgan dual of the matching zero-product characterization, via constructor on both directions.
Claim. For a signed orbit $z$ and a distinction-orbit position $d$, writing $\iota(d)$ for the nonnegative signed orbit with positive part $d$ and negative part $0$, one has $|\mathrm{mul}(z,\iota(d))| \neq 0$ if and only if $|z| \neq 0$ and $d \neq 0$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction-orbit positions (pos, neg), read as the formal difference pos - neg. Its absolute value is the absolute difference of those two positions, again an orbit position. The map ofOrbit embeds a nonnegative orbit position $d$ as the signed orbit $\langle d, 0\rangle$.
Multiplication of signed orbits is defined so that, after passage to the integer interpretation, it matches ordinary integer multiplication. The companion zero-product lemma states that $|\mathrm{mul}(z,\iota(d))| = 0$ if and only if $|z| = 0$ or $d = 0$. The present statement is the complementary nonzero form of that rule, needed when the order surface must certify that a product stays away from zero.
The local module builds the internal order on these signed orbits (reflexivity, totality, trichotomy, sign flags) without leaving the orbit language.
proof idea
One-line appeal to the zero-product companion abs_mul_ofOrbit_right_eq_zero_iff, then constructor on the biconditional. Forward direction: if the product absolute value is nonzero, neither factor can be zero, else the companion would force the product absolute value to zero. Reverse direction: if the product absolute value were zero, the companion yields a disjunction; each disjunct contradicts one of the two nonzero hypotheses. No new arithmetic is performed.
why it matters
Feeds the single downstream certificate integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, the order predicate, absolute difference, and nonnegativity flags; the nonzero product rule is part of keeping multiplication compatible with the order and with the zero element.
Within Recognition Science this sits in the foundation layer that reconstructs integer arithmetic from distinction orbits before the forcing chain (T0–T8) and the Recognition Composition Law are applied. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only seals the algebraic order surface those later steps rely on when they speak of integer rungs and signed gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.