mul_not_balanced_zero_iff
plain-language theorem explainer
For signed orbits, the product is unbalanced against zero exactly when both factors are. Anyone building the internal integer order or zero-divisor facts on the PRC signed-orbit layer cites this. The proof is a short De Morgan dual of the existing product-zero characterization.
Claim. For signed orbits $z,w$, the product $z\cdot w$ is not balanced with zero if and only if $z$ is not balanced with zero and $w$ is not balanced with zero.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ standing for the formal difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits $a,b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; balancing against the zero orbit is the internal notion of being zero.
Multiplication of signed orbits is defined so that the integer image multiplies in the usual way. The sibling theorem already records that the product is balanced with zero precisely when at least one factor is. The present statement is the complementary non-zero form needed for order and trichotomy facts on the same surface.
The surrounding module develops the internal order on signed orbits (reflexivity, transitivity, antisymmetry up to balance, totality, sign flags) entirely from $\delta$-orbit data, without external $\mathbb{Z}$.
proof idea
One rewrite applies the sibling product-zero characterization: balanced$(z\cdot w,0)\leftrightarrow$ balanced$(z,0)\lor$ balanced$(w,0)$. The rest is pure propositional De Morgan. Forward: if the product is not zero-balanced, neither disjunct can hold, so both factors are non-zero. Backward: if both factors are non-zero and the product were zero-balanced, the disjunction would force one factor zero, a contradiction. No arithmetic beyond the rewrite is used.
why it matters
This closes the non-zero half of the product law on signed orbits, matching the classical fact that $\mathbb{Z}$ is an integral domain at the PRC layer. Downstream it feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; that certificate packages display lemmas for nonnegativity, flags, and truncated subtraction used by the broader foundation stack.
In Recognition Science terms this sits under the ledger and forcing infrastructure that later supports the T0–T8 chain: clean zero and order facts on the integer surface are prerequisites for counting, eight-tick structure, and dimension forcing. It does not itself invoke $J$, $\varphi$, or the RCL; it is pure internal arithmetic hygiene.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.