abs_mul_ne_zero_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (internally equivalent), the absolute value of their products is nonzero on one pair exactly when it is nonzero on the other. Anyone building the PRC integer order or proving that multiplication respects the balanced equivalence will cite this. The proof is a short constructor flip of the corresponding zero-equality lemma.
Claim. Let $a,a',b,b'$ be signed orbits. Suppose $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$ and likewise for $b,b'$). Then $|a\cdot b|\neq 0$ if and only if $|a'\cdot b'|\neq 0$, where $|\cdot|$ is the absolute orbit position $\mathrm{absDiff}(\mathrm{pos},\mathrm{neg})$.
background
In the Primitive Recognition Calculus, integers are represented as signed orbits: pairs of distinction-orbit positions (positive and negative legs). Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; that is the internal PRC integer relation, defined entirely on $\delta$-orbit positions, and it is the equivalence used in place of ordinary integer equality.
Absolute value of a signed orbit is the distinction-nat $\mathrm{absDiff}(z.pos, z.neg)$. Multiplication of signed orbits is the internal product on this representation. The companion result abs_mul_eq_zero_iff_of_balanced already shows that, under balanced pairs, the product absolute value is zero on one side exactly when it is zero on the other. This module develops the order surface on those signed orbits (reflexivity, transitivity, trichotomy, sign flags) toward a closed integer-order certificate.
proof idea
One-step reduction from the zero form. Instantiate abs_mul_eq_zero_iff_of_balanced on the same balanced hypotheses to obtain
$|a\cdot b|=0 \leftrightarrow |a'\cdot b'|=0$.
Then constructor splits the desired biconditional on the negated predicates. Each direction is pure contrappositive: from $\neq 0$ on one side and $=0$ on the other, feed the zero-iff arrow (mpr or mp) to derive $=0$ on the first side and contradict the nonzero hypothesis. No new arithmetic on orbits is required.
why it matters
The result is a small but necessary closure step for the signed-orbit order surface. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; that certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the Recognition Science foundation stack this sits inside Primitive Recognition Calculus integer structure: before mass ladders, eight-tick cadence, or forcing-chain landmarks (T5 J-uniqueness, T6 $\phi$, T7 octave, T8 $D=3$) can be stated over integers, multiplication and absolute value must respect the balanced equivalence. The nonzero form is the natural interface for invertibility and cancellation arguments that the zero form alone does not phrase cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.