abs_mul_eq_zero_of_balanced_zero_right
plain-language theorem explainer
If a signed orbit is balanced against zero, its product with any other signed orbit has absolute value zero. Order and arithmetic lemmas in the primitive recognition calculus cite this to close the zero-divisor behaviour of the internal integer model. The proof reduces absolute value to the integer display, multiplies, substitutes the zero display, and finishes by ring.
Claim. For signed orbits $z,w$, if $w$ is balanced with the zero orbit (equivalently $w$ has integer display $0$), then $\lvert z \cdot w \rvert = 0$ as a distinction-natural.
background
Primitive Recognition Calculus builds integers from signed orbits: each orbit carries a positive and a negative distinction-natural position. Absolute value is the absolute difference of those positions. Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; by the K4.9 bridge this is equivalent to equal integer displays $a.\mathrm{toInt}=b.\mathrm{toInt}$.
Multiplication of signed orbits is defined so that the integer display is a ring homomorphism: $(zw).\mathrm{toInt}=z.\mathrm{toInt}\cdot w.\mathrm{toInt}$. Absolute value vanishes exactly when the integer display is zero. The local module develops the order surface on these orbits (reflexivity, totality, trichotomy, sign flags) before packaging a certificate that the surface is closed.
proof idea
Term-mode rewrite chain. First rewrite the goal via $\lvert u\rvert=0\Leftrightarrow u.\mathrm{toInt}=0$ and the multiplication homomorphism, so the claim becomes $(z.\mathrm{toInt})\cdot(w.\mathrm{toInt})=0$. Then rewrite the hypothesis with the balanced-to-display bridge and the fact that the zero orbit displays as $0$, obtaining $w.\mathrm{toInt}=0$. Substitute and close with ring.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (nonnegativity, absolute difference, truncated subtraction, and flag displays all match the conservative $\mathbb{Z}$ view). Without zero-absorption of absolute value under right-multiplication by a zero-balanced orbit, the order surface would not be consistent with the ring structure forced earlier in the ledger/PRC stack. This is foundation plumbing rather than a T0–T8 landmark: it keeps the internal integer model coherent so later forcing (J-uniqueness, $\varphi$, eight-tick, $D=3$) can treat discrete order as already settled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.