abs_mul_ne_zero_iff_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (the internal integer equivalence), then the absolute value of either product with a third orbit is nonzero exactly when the other is. Order and certificate authors cite this to transfer nonvanishing of products across the balance relation. The proof is a two-direction constructor that contraposes the companion zero-iff lemma.
Claim. Let $a$, $a'$, and $b$ be signed orbits. If $a$ and $a'$ are balanced (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$), then $|a\cdot b|\neq 0$ if and only if $|a'\cdot b|\neq 0$, where $|\cdot|$ is the absolute value as a distinction-natural (absolute difference of positive and negative orbit positions).
background
In the Primitive Recognition Calculus, integers are represented as signed orbits: pairs of distinction-natural positions (pos, neg). Two signed orbits are balanced when their lengths match under swap of signs: $a.pos + a'.neg = a'.pos + a.neg$. That relation is the internal PRC integer equivalence (K4.9), defined entirely on $\delta$-orbit positions.
Absolute value of a signed orbit is the distinction-natural absDiff of its positive and negative legs, so vanishing absolute value means the two legs coincide (the zero integer). Multiplication of signed orbits is the internal product used to build the order surface.
The companion result abs_mul_eq_zero_iff_of_balanced_left already equates vanishing of $|a\cdot b|$ and $|a'\cdot b|$ under balance of $a$ with $a'$. The present statement is the nonvanishing dual of that equivalence, needed wherever the order certificate reasons about nonzero products rather than zeros.
proof idea
Term-mode proof that reuses the zero-iff companion. Instantiate abs_mul_eq_zero_iff_of_balanced_left at the same $a$, $a'$, $b$ and balance hypothesis to obtain
$|a\cdot b|=0 \leftrightarrow |a'\cdot b|=0$.
Then constructor builds both directions of the $\neq 0$ biconditional by contraposition: each direction assumes nonvanishing on one side and a vanishing hypothesis on the other, then applies the corresponding direction of the zero-iff to derive a contradiction with the assumed nonvanishing.
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; nonvanishing of products under balance is part of keeping absolute value and multiplication coherent on the quotient by balance.
In the Recognition foundation stack this sits inside the Primitive Recognition Calculus integer layer: before J-cost uniqueness (T5), $\varphi$ forcing (T6), or the eight-tick octave (T7), the ledger must already have a well-behaved integer order. Balance is the equality relation on that order; transferring $|\cdot\cdot|\neq 0$ across it prevents the product from depending on representative choice. No open scaffold remains here: the claim is fully proved and only packages the dual of an already-proved zero-iff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.