abs_mul_eq_zero_iff_of_balanced_right
plain-language theorem explainer
If two signed orbits represent the same integer, then multiplying either by a fixed signed orbit yields a product of absolute value zero in exactly the same cases. Order and certificate lemmas cite this to transport zero-product facts across the balanced equivalence. The proof is a short rewrite chain through the integer display of absolute value and multiplication.
Claim. Let $a,b,b'$ be signed orbits. If $b$ and $b'$ are balanced (i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$), then $|a\cdot b|=0$ if and only if $|a\cdot b'|=0$, where $|\cdot|$ is the absolute-value orbit and $\cdot$ is signed-orbit multiplication.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-orbit positions (pos, neg). Their integer display is $\mathrm{toInt}=\mathrm{pos}-\mathrm{neg}$. Absolute value is the distinction-nat $\mathrm{absDiff}(\mathrm{pos},\mathrm{neg})$, and multiplication is defined so that $\mathrm{toInt}$ is a ring homomorphism.
Two signed orbits are balanced when $\mathrm{pos}$ and $\mathrm{neg}$ lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. Upstream, balanced_iff_toInt_eq states this internal relation is exactly equality of integer displays: "the bridge from the internal PRC relation to the conservative $\mathbb{Z}$ view." Likewise abs_eq_zero_iff_toInt_eq_zero and mul_toInt identify vanishing absolute value with $\mathrm{toInt}=0$ and send products to ordinary integer products.
This module builds the order surface on those displays; the present lemma is a transport fact for the zero locus of absolute values under right multiplication by balanced partners.
proof idea
Term-mode rewrite proof. Rewrite both sides of the goal with abs_eq_zero_iff_toInt_eq_zero, then replace each product absolute value by the corresponding mul_toInt identity, so the claim becomes $a.\mathrm{toInt}\cdot b.\mathrm{toInt}=0$ iff $a.\mathrm{toInt}\cdot b'.\mathrm{toInt}=0$. Apply balanced_iff_toInt_eq to the hypothesis to get $b.\mathrm{toInt}=b'.\mathrm{toInt}$, substitute, and the two sides coincide.
why it matters
Feeds the companion non-vanishing form abs_mul_ne_zero_iff_of_balanced_right (same hypotheses, $\neq 0$) and is listed among the ingredients of integer_order_certificate, whose doc-comment records that "the internal signed-orbit order surface is closed."
Within Recognition Science foundation work, signed orbits are the choice-free integer layer under ledger forcing and the primitive recognition calculus. Closing absolute-value and order facts on that layer is prerequisite scaffolding for later forcing-chain material (T0–T8) that needs a coherent integer display, not a classical $\mathbb{Z}$ import. The lemma itself is elementary algebra once the display bridges exist; its value is that zero-detection for products is invariant under the balanced equivalence used everywhere in the order certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.