mul_ofOrbit_left_not_balanced_zero_iff
plain-language theorem explainer
Left-multiplying a signed orbit by a nonnegative orbit from a distinction count yields a nonzero product (not balanced with zero) exactly when both factors are nonzero. Order and integer-arithmetic developments in the primitive recognition calculus cite this to control zero-divisors under orbit multiplication. The proof is a short De Morgan dual of the corresponding balanced-zero biconditional.
Claim. For every distinction count $d$ and signed orbit $z$, the product $\mathrm{ofOrbit}(d)\cdot z$ is not balanced with zero if and only if $z$ is not balanced with zero and $d\neq 0$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (Peano-style naturals built from zero and successor). A SignedOrbit is a pair of such orbits (pos, neg), read as the formal difference pos - neg.
Two signed orbits are balanced when their lengths match under the internal integer relation $a.pos + b.neg = b.pos + a.neg$ (K4.9). In particular, balance with zero means the signed orbit represents the integer zero. The embedding ofOrbit d builds the nonnegative signed orbit $\langle d, 0\rangle$.
The sibling theorem mul_ofOrbit_left_balanced_zero_iff already records the positive form: left-multiplying by ofOrbit d lands on zero exactly when $z$ is zero or $d = 0$. The present statement is the logical dual needed for nonzero product tests in the order layer.
proof idea
One-line rewrite by the positive biconditional mul_ofOrbit_left_balanced_zero_iff, which converts the goal into $\neg(P \lor Q) \leftrightarrow (\neg P \land \neg Q)$ with $P$ = "$z$ balanced with zero" and $Q$ = "$d = 0$".
The rest is pure propositional reasoning: the forward direction splits the conjunction and discharges each half by feeding the corresponding disjunct into the negated hypothesis; the reverse direction cases on the disjunction coming from the rewritten product-balance assumption and applies the matching conjunct.
why it matters
Feeds integer_order_certificate, which asserts that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity flags; nonzero product control under left multiplication by nonnegative orbits is part of keeping the order and sign-flag layer consistent with the integer interpretation of signed orbits.
Within Recognition Science foundation work, this sits in the ledger/orbit arithmetic that underwrites later forcing (T0–T8) rather than naming a forcing step itself. It closes a small but necessary zero-divisor fact: nonnegative left factors from distinction counts do not create accidental zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.