abs_mul_ne_zero_iff_of_balanced_right
plain-language theorem explainer
If two signed orbits are balanced under the internal PRC integer relation, right-multiplication by a fixed signed orbit preserves non-vanishing of absolute value: |a·b|≠0 iff |a·b'|≠0. Anyone assembling the signed-orbit order or the integer-order certificate cites this. The proof dualizes the corresponding zero-equality iff by constructor and contraposition on both directions.
Claim. Let $a,b,b'$ be signed orbits and suppose $b$ is balanced with $b'$ (i.e. the orbit lengths satisfy $b_{\mathrm{pos}}+b'_{\mathrm{neg}}=b'_{\mathrm{pos}}+b_{\mathrm{neg}}$). Then the absolute value of the product $a\cdot b$ is nonzero if and only if the absolute value of $a\cdot b'$ is nonzero, where absolute value is the distinction-orbit absolute difference of the positive and negative legs.
background
In the Primitive Recognition Calculus, integers are realized as signed orbits: pairs of distinction-orbit positions (positive and negative legs). Absolute value of a signed orbit is the distinction-orbit absolute difference of those legs, landing in DistinctionNat. Two signed orbits are balanced when their leg lengths satisfy the internal integer relation $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$ (K4.9); this is the PRC stand-in for integer equality, defined entirely on $\delta$-orbit positions.
The local module builds the order surface on these signed orbits: reflexivity, transitivity, antisymmetry under balance, trichotomy, and sign-flag characterizations of nonnegativity and negativity. Multiplication of signed orbits is the monoid operation used to transport magnitude statements.
The immediate upstream fact is the zero-equality twin: under the same right-balance hypothesis, $|a\cdot b|=0$ if and only if $|a\cdot b'|=0$. That lemma reduces absolute vanishing to the integer image being zero and uses balance to equate the two products' integer values.
proof idea
One-line dualization of the zero-equality twin. Instantiate abs_mul_eq_zero_iff_of_balanced_right at $a,b,b'$ with the given balance hypothesis to obtain $|a\cdot b|=0\leftrightarrow|a\cdot b'|=0$. Then constructor on the desired non-equality biconditional: each direction is an intro that feeds the opposite vanishing hypothesis through the zero-iff (.mpr / .mp) and discharges the assumed non-vanishing. No new arithmetic is performed.
why it matters
This lemma is a small but necessary brick in closing the internal signed-orbit order surface. Downstream it is consumed by integer_order_certificate, whose doc-comment states that surface is closed and packages display lemmas for truncated subtraction, the $\le$ flag, absolute difference, and signed nonnegativity.
Within Recognition Science the PRC integer layer sits under the forcing chain: once signed orbits carry a coherent order and absolute value compatible with balance, one can speak rigorously of rung indices, mass-ladder exponents, and the eight-tick octave counting without smuggling classical $\mathbb{Z}$. The non-vanishing form is the version needed when ruling out zero divisors or when stating that a product remains a genuine distinction after right-multiplication by balanced representatives.
No open scaffold remains here; the claim is fully proved and only packages the zero-case twin for order-certificate consumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.