abs_mul_eq_zero_iff_of_balanced_left
plain-language theorem explainer
If two signed orbits are balanced (same integer value), then the absolute value of either product with a third orbit vanishes exactly when the other does. Order and arithmetic lemmas on the PRC integer surface cite this to move zero-tests across balanced representatives. The proof rewrites absolute-value vanishing to integer vanishing, multiplies under toInt, and substitutes the balanced equality.
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}$, equivalently $a$ and $a'$ display the same integer), then $|a\cdot b|=0$ if and only if $|a'\cdot b|=0$, where $|\cdot|$ is the orbit absolute value (absolute difference of positive and negative legs) and $0$ is the zero distinction.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-orbit positions (positive and negative legs). Two signed orbits are balanced when $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equivalence; the bridge lemma states it agrees with equality of the conservative integer displays: balanced iff the two toInt values coincide.
Absolute value of a signed orbit is the distinction-nat absolute difference of its legs. Vanishing of that absolute value is equivalent to the integer display being zero. Multiplication of signed orbits is defined so that the integer display is a ring homomorphism: the display of a product is the product of the displays.
The local module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Zero-tests after multiplication must be independent of which balanced representative is chosen on the left factor.
proof idea
Term-mode rewrite chain. First replace both sides' absolute-value-equals-zero goals by the corresponding integer-display-equals-zero statements via the abs-vanishing characterization. Then replace each product display by the product of displays using the multiplication homomorphism. Finally rewrite the balanced hypothesis into equality of integer displays and substitute, so both sides become the same product-equals-zero statement.
why it matters
Well-definedness of left-multiplication zero-tests under balanced equivalence is a small but necessary arithmetic fact for the internal integer order. The immediate parent is the nonzero twin: absolute value of a left product is nonzero for one balanced representative iff for the other. Both feed the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, comparison, abs-diff, and nonnegativity flags).
In the broader Recognition stack this sits in foundation ledger/PRC arithmetic beneath the forcing chain, not yet at J-uniqueness or phi. It keeps integer order choice-free and representative-independent so later rung and mass constructions can treat signed-orbit integers as a stable ordered ring surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.