mul_ofOrbit_right_balanced_zero_iff
plain-language theorem explainer
Multiplying a signed orbit by the nonnegative embedding of a distinction natural is balanced with zero exactly when the orbit itself is zero-balanced or the natural is zero. Order and integrality arguments in the primitive recognition calculus cite this as the right-factor zero-divisor law. The proof reduces balancedness to integer equality via the toInt bridge, then applies the LogicInt no-zero-divisors theorem and reconstructs.
Claim. For any signed orbit $z$ and distinction natural $d$, writing $\iota(d)$ for the nonnegative signed-orbit embedding of $d$, one has $z\cdot\iota(d)$ balanced with zero if and only if either $z$ is balanced with zero or $d=0$. Balancedness means equality of the crossed orbit-length sums $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$.
background
In the Primitive Recognition Calculus, integers appear as signed orbits: pairs of distinction-natural lengths (positive and negative parts). Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that internal relation is the PRC stand-in for integer equality (K4.9). The display map sends a signed orbit to $\mathbb{Z}$, and balancedness is equivalent to equality of displays.
Multiplication of signed orbits is defined so that it is compatible with ordinary integer multiplication: the display of a product is the product of the displays. The embedding $\iota$ lifts a distinction natural to a nonnegative signed orbit. Upstream, the forced integer type LogicInt has no zero divisors, forced by the ring isomorphism with $\mathbb{Z}$.
This module assembles the order surface on signed orbits (nonnegativity flags, trichotomy, antisymmetry under balancedness) and packages it as a closed certificate.
proof idea
Rewrite the balancedness claim through the bridge to integer equality, the multiplication-display law, the embedding display, and the zero display. The goal becomes $z.\mathrm{toInt}\cdot(\mathrm{toNat},d)=0$ iff $z.\mathrm{toInt}=0$ or $d=0$.
Forward: apply the LogicInt zero-divisor law; the left disjunct rewrites back to balancedness of $z$ with zero, while the right uses injectivity of $\mathrm{toNat}$ together with $\mathrm{toNat},0=0$ to recover $d=0$. Reverse: case-split the disjunction; each arm substitutes and finishes by a ring identity that makes the product display vanish.
why it matters
This is the right-factor zero-divisor law for orbit embeddings, so positivity and order scale like the integers under multiplication by distinction naturals. Its immediate consumer is the negated companion, which rewrites the same fact for strictly-nonzero reasoning. Both feed the integer-order certificate, whose statement is that the internal signed-orbit order surface is closed: nonnegativity displays, flag displays, truncated subtraction, and absolute difference all line up with the conservative $\mathbb{Z}$ view.
In the Recognition foundation stack this sits inside the arithmetic reconstruction that makes ledger balance and integer structure available before continuum physics. It does not itself touch the forcing chain T0–T8, the J-cost, or $\varphi$, but it removes a gap between $\delta$-orbit combinatorics and the integer order used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.