balanced_mul_right_iff_of_not_balanced_zero
plain-language theorem explainer
If a signed orbit is nonzero, right-multiplication by it cancels in the balanced relation: za is balanced with wa exactly when z is balanced with w. Anyone building comparison or order laws for PRC integers cites this cancellation step. The proof bridges balanced to integer equality via toInt, then applies ordinary right-cancellation on ℤ.
Claim. Let $a,z,w$ be signed orbits. If $a$ is not balanced with the zero orbit, then the product $z\cdot a$ is balanced with $w\cdot a$ if and only if $z$ is balanced with $w$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg) recording how far a distinction has run in each polarity. Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; that is the internal equality relation on the PRC integer surface (K4.9).
The display map toInt recovers an ordinary integer from a signed orbit. The bridge theorem states that balanced holds exactly when the two displays agree: balanced $a,b$ iff $a.toInt = b.toInt$. Multiplication of signed orbits is defined so that it intertwines with integer multiplication: $(z\cdot a).toInt = z.toInt \cdot a.toInt$.
This module develops the order structure on that surface (reflexivity, totality, trichotomy, sign flags). The present lemma is the multiplicative cancellation law needed before comparison can be pushed through a right factor.
proof idea
First convert the hypothesis that $a$ is not balanced with zero into $a.toInt \neq 0$, using the balanced-to-toInt bridge and the fact that zero displays as $0$. Rewrite both sides of the claimed iff via the same bridge and the multiplication-display law, so the goal becomes
$$z.toInt \cdot a.toInt = w.toInt \cdot a.toInt \quad\leftrightarrow\quad z.toInt = w.toInt.$$
The forward direction is mul_right_cancel₀ on ℤ with the nonzero factor already established. The reverse direction is substitution.
why it matters
Right-cancellation under nonzero multiplication is the algebraic hinge for order-compatibility of multiplication on PRC integers. Downstream it is invoked by the two comparison-transport lemmas: one for a negative right factor (comparison reverses) and one for a nonnegative nonzero right factor (comparison preserves). Both feed the closed integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
Within the Recognition foundation this sits under Integers-from-Logic and Ledger forcing: balanced is the ledger-native equality, and the certificate packages the order display for later forcing and mass-ladder work. It does not itself touch T5–T8 or the RCL; it is pure integer-surface hygiene required before those layers can treat ordered rung arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.