mul_balanced_zero_of_balanced_zero_right
plain-language theorem explainer
If a signed orbit is balanced against zero, its product with any other signed orbit is likewise balanced against zero. Order work on the primitive recognition calculus cites this as right-zero absorption for the balanced-zero predicate under multiplication. The proof is a one-line application of the multiplication-zero biconditional, selecting the right disjunct.
Claim. Let $z,w$ be signed orbits (pairs of distinction-natural lengths, read as $\mathrm{pos}-\mathrm{neg}$). If $w$ is balanced with the zero orbit, meaning $w.\mathrm{pos}+0=0+w.\mathrm{neg}$ in the internal orbit-length relation, then the product $z\cdot w$ is balanced with zero.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction-natural lengths intended as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits $a,b$ are balanced when their lengths satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal integer relation on $\delta$-orbit positions (K4.9), not a ledger-level balance predicate.
The zero orbit is the neutral element of that relation. Multiplication of signed orbits induces ordinary integer multiplication on the underlying $\mathrm{toInt}$ values. An upstream biconditional records that a product is balanced with zero exactly when at least one factor is: $z\cdot w\sim 0$ iff $z\sim 0$ or $w\sim 0$.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma is the right-factor absorption half of the zero-product law.
proof idea
One-line term proof. Apply the right-to-left direction of the multiplication-zero biconditional mul_balanced_zero_iff, and feed it the right disjunct Or.inr hw of the hypothesis that $w$ is balanced with zero. No further case analysis or arithmetic is required.
why it matters
The lemma is a small but necessary absorption fact for the signed-orbit multiplicative structure that underwrites the internal integer order. It is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags are packaged as a single certificate.
Within Recognition Science foundation work, that certificate is part of forcing an integer order from pure distinction-orbit data before the forcing chain reaches J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). Closing zero-product absorption keeps the order surface free of ad-hoc zero cases when products appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.