mul_ofOrbit_left_balanced_zero_iff
plain-language theorem explainer
Left multiplication of a signed orbit by a pure positive orbit is balanced with zero exactly when the orbit itself is zero or the multiplier distinction is zero. Arithmetic and order developers in the Primitive Recognition Calculus cite this as the no-zero-divisors law for ofOrbit factors. The proof reduces balanced to integer equality via the toInt bridge, multiplies through the ring homomorphism, and applies the LogicInt zero-divisor theorem.
Claim. For any distinction natural $d$ and signed orbit $z$, the product of the pure positive orbit of $d$ with $z$ is balanced with the zero orbit if and only if either $z$ is balanced with zero or $d$ is the zero distinction.
background
In the Primitive Recognition Calculus, integers appear as signed orbits: pairs of distinction-nat positions recording positive and negative δ-orbit lengths. Two signed orbits $a,b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation (K4.9) is the PRC integer equivalence; the bridge theorem states it holds exactly when the display maps agree, $a.\mathrm{toInt}=b.\mathrm{toInt}$.
The pure positive embedding sends a distinction natural $d$ to the signed orbit with positive length $d$ and vanishing negative length. Signed-orbit multiplication is defined so that toInt is a ring homomorphism: $(\mathrm{mul},a,b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$.
Upstream, IntegersFromLogic already records that LogicInt has no zero divisors (forced by the ring isomorphism with $\mathbb{Z}$): $a\cdot b=0$ iff $a=0$ or $b=0$. The present lemma transports that fact onto the internal balanced relation for left factors of the form ofOrbit$(d)$.
proof idea
Rewrite the balanced claim through balanced_iff_toInt_eq, then expand mul_toInt, ofOrbit_toInt, and zero_toInt. The goal becomes the ordinary integer equality $(\mathrm{toNat},d)\cdot z.\mathrm{toInt}=0$.
Forward direction: apply mul_eq_zero from IntegersFromLogic and case-split. If $\mathrm{toNat},d=0$, injectivity of toNat together with toNat_zero recovers $d=\mathrm{zero}$. If $z.\mathrm{toInt}=0$, rewrite back via balanced_iff_toInt_eq to obtain balanced $z$ zero.
Converse: substitute either disjunct and simplify the product to zero by ring arithmetic (zero factor or zero multiplier).
why it matters
This is the left-factor zero-product criterion for pure positive orbits inside the signed-orbit model of the integers. Its immediate negation form (mul_ofOrbit_left_not_balanced_zero_iff) is a one-line rewrite of the same biconditional, and both feed integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
That certificate packages the display lemmas for nonneg flags, leq, truncated subtraction, and absolute difference, so ordered integer reasoning can stay inside PRC primitives rather than assuming classical $\mathbb{Z}$. In the broader Recognition foundation this sits beneath the forcing chain (T0–T8) but is required scaffolding wherever later tick-count, rung, or mass-ladder arguments need cancellation-free ordered arithmetic built from δ-orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.