abs_mul_eq_zero_iff_of_balanced
plain-language theorem explainer
Under the signed-orbit balance relation, the absolute value of a product vanishes for one pair of factors if and only if it vanishes for any balanced pair. Order and integrality lemmas in the primitive recognition calculus cite this to transport zero-product facts across equivalent integer displays. The proof rewrites absolute value and multiplication into the integer display, then substitutes equal toInt values.
Claim. Let $a,a',b,b'$ be signed orbits. If $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|=0$ if and only if $|a'\cdot b'|=0$, where $|\cdot|$ is the absolute value as a distinction-orbit position.
background
In the primitive recognition calculus, integers are carried by signed orbits: pairs of distinction-orbit positions (positive and negative legs). Absolute value of a signed orbit is the absolute difference of those legs, landing in DistinctionNat. Two signed orbits are balanced when their leg lengths satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal PRC integer relation, defined entirely on $\delta$-orbit positions.
The bridge to the conservative $\mathbb{Z}$ view is the characterization that balance holds exactly when the integer displays agree: $\mathrm{balanced}(a,b)\leftrightarrow a.\mathrm{toInt}=b.\mathrm{toInt}$. Multiplication of signed orbits is defined so that the display is a ring homomorphism: $(a\cdot b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$. Absolute value vanishes precisely when the integer display is zero.
This module builds the order surface on those internal displays. The present statement is the zero-product transport law for absolute values under balance.
proof idea
Term-mode rewrite chain. First replace both sides' $|\cdot|=0$ goals by the corresponding $\mathrm{toInt}=0$ statements via abs_eq_zero_iff_toInt_eq_zero. Then apply mul_toInt on each product so the goals become $a.\mathrm{toInt}\cdot b.\mathrm{toInt}=0$ and $a'.\mathrm{toInt}\cdot b'.\mathrm{toInt}=0$. Rewrite the balance hypotheses with balanced_iff_toInt_eq to obtain $a.\mathrm{toInt}=a'.\mathrm{toInt}$ and $b.\mathrm{toInt}=b'.\mathrm{toInt}$, substitute, and the two sides coincide.
why it matters
Closes a small but necessary congruence fact for the signed-orbit order surface: zero absolute value of a product is invariant under replacing factors by balanced partners. The immediate consumer is the dual non-vanishing form abs_mul_ne_zero_iff_of_balanced, obtained by contraposing this iff. Both feed the package theorem integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
In the Recognition foundation this sits inside the ledger/forcing layer that builds integers from distinction orbits before the forcing chain (T0–T8) and the J-cost calculus. It does not itself force $\phi$ or dimension; it keeps the internal integer arithmetic coherent so later recognition identities can quote order and zero facts without leaving the orbit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.