mul_balanced_zero_iff
plain-language theorem explainer
Product of two signed orbits is balanced against zero exactly when at least one factor is. Anyone assembling the integer ring laws on δ-orbit differences cites this as the no-zero-divisors statement. The proof rewrites both sides through the toInt bridge and applies the corresponding zero-divisor law on LogicInt.
Claim. For signed orbits $z$ and $w$, writing $\mathrm{bal}$ for the internal balance relation on orbit lengths, $\mathrm{bal}(z\cdot w,\,0)$ if and only if $\mathrm{bal}(z,\,0)$ or $\mathrm{bal}(w,\,0)$.
background
Signed orbits are pairs of distinction-naturals (pos, neg), read as the formal difference pos - neg. Their internal equality is the balance relation of K4.9: two orbits balance when a.pos + b.neg = b.pos + a.neg. That relation is the PRC-native integer equality, defined only on δ-orbit positions.
The bridge theorem balanced_iff_toInt_eq identifies balance with equality of the conservative integer display toInt. Multiplication of signed orbits is defined so that toInt is a ring homomorphism: (mul a b).toInt = a.toInt * b.toInt. Zero is the orbit with both legs empty, and zero.toInt = 0.
Upstream, LogicInt already has no zero divisors: a * b = 0 forces a = 0 or b = 0, forced by the ring isomorphism with ℤ. The present statement is the same law, stated entirely in the balance language of signed orbits.
proof idea
Term-mode rewrite of both sides of the biconditional. First replace every balanced _ zero by equality of toInt values, then replace (mul z w).toInt by z.toInt * w.toInt and zero.toInt by 0. The goal is then ordinary integer zero-divisors on the displays.
The forward direction applies mul_eq_zero.mp and packages each arm as a left or right disjunct. The reverse direction cases on the disjunction, rewrites the zero factor, and closes each arm by ring.
why it matters
This is the no-zero-divisors law for the signed-orbit presentation of the integers inside Primitive Recognition Calculus. It feeds the one-sided absorption lemmas (product balanced-zero when the left or right factor is) and the negated form used when both factors are nonzero. Those facts sit on the path to integer_order_certificate, which closes the internal signed-orbit order surface (nonnegativity flags, truncated subtraction, absolute difference displays).
In the broader RS foundation, integers arise from δ-orbit bookkeeping before the forcing chain reaches J-uniqueness (T5), φ (T6), the eight-tick octave (T7), and D = 3 (T8). A clean zero-divisor law is required before order, absolute value, and the later mass-ladder arithmetic can be trusted on the same carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.