balanced_mul_ofOrbit_right_iff_of_ne_zero
plain-language theorem explainer
Right-multiplication of two signed orbits by the same nonzero distinction orbit preserves the internal balance relation (the PRC integer equivalence). Anyone proving cancellation or order laws for signed-orbit integers cites this. The proof rewrites balance to integer equality via toInt, records that the multiplier is a positive integer, and closes both directions by nlinarith.
Claim. Let $z,w$ be signed orbits and let $d$ be a nonzero distinction natural. Write $\iota(d)$ for the nonnegative signed orbit of length $d$. Then $z\cdot\iota(d)$ is balanced with $w\cdot\iota(d)$ if and only if $z$ is balanced with $w$, where balance means $a_{+} + b_{-} = b_{+} + a_{-}$.
background
In Primitive Recognition Calculus, integers are represented as signed orbits: pairs of distinction-orbit lengths (positive and negative legs). Two signed orbits are balanced when $a_{+} + b_{-} = b_{+} + a_{-}$; equivalently, their integer readings toInt agree. That relation is the internal integer equality of the calculus, defined only on $\delta$-orbit positions.
DistinctionNat is the nonnegative counting type built from logic naturals; ofOrbit d embeds a distinction natural as a nonnegative signed orbit. Multiplication of signed orbits multiplies the underlying integer values (mul_toInt). The local module develops the order surface on these signed-orbit integers (reflexivity, totality, trichotomy, sign flags).
The nonzero hypothesis on $d$ is essential: right-multiplication by zero collapses every pair to the zero orbit, so balance would hold universally and cancellation would fail.
proof idea
Rewrite both sides of the biconditional with balanced_iff_toInt_eq, then expand mul_toInt twice and ofOrbit_toInt. The claim becomes
$$\mathrm{toInt}(z)\cdot n = \mathrm{toInt}(w)\cdot n \iff \mathrm{toInt}(z)=\mathrm{toInt}(w)$$
where $n = d.\mathrm{toNat}$.
From $d \neq 0$, injectivity of toNat and toNat_zero give $n \neq 0$, hence $0 < (n:\mathbb{Z})$ by Nat.pos_of_ne_zero and a cast. Both directions of the integer cancellation are then discharged by nlinarith (positive multiplier).
why it matters
This is a right-cancellation lemma for the PRC integer equivalence under nonzero nonnegative multipliers. It sits in the IntegerOrder development that closes the signed-orbit order surface.
The sole recorded consumer is integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\leq$, absolute difference, and nonnegativity flags; cancellation under nonzero scaling is part of making those order facts coherent with the multiplicative structure.
In the broader Recognition stack this is foundation arithmetic, not a forcing-chain landmark (T5–T8). It supports the claim that integers and their order arise internally from distinction orbits rather than being imported as primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.