balanced_mul_left_iff_of_not_balanced_zero
plain-language theorem explainer
Left multiplication by a nonzero signed orbit preserves the balanced (integer-equality) relation: a·z ~ a·w if and only if z ~ w. Anyone building comparison or cancellation laws for the PRC integer order cites this. The proof reduces balanced to equality of toInt images and applies ordinary left cancellation in ℤ.
Claim. Let $a,z,w$ be signed orbits. If $a$ is not balanced with the zero orbit (equivalently $a.\mathrm{toInt}\neq 0$), then $a\cdot z$ is balanced with $a\cdot w$ if and only if $z$ is balanced with $w$.
background
In Primitive Recognition Calculus, integers are recovered as signed orbits: pairs of nonnegative δ-orbit lengths with a sign presentation. 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.
The bridge to classical integers is the recovery map $\mathrm{toInt}$. The upstream lemma balanced_iff_toInt_eq states that balanced holds exactly when the two orbits display the same integer. Multiplication of signed orbits is defined so that it intertwines with ordinary multiplication on $\mathbb{Z}$ via mul_toInt.
This module develops the order surface on those signed orbits (nonneg/negative flags, comparison, trichotomy). Cancellation under left multiplication is the algebraic step needed before comparison can be pushed through products.
proof idea
First convert the hypothesis that $a$ is not balanced with zero into $a.\mathrm{toInt}\neq 0$, using balanced_iff_toInt_eq and the fact that zero has toInt $0$. Rewrite both sides of the claimed iff via balanced_iff_toInt_eq and replace products by mul_toInt, so the goal becomes $a.\mathrm{toInt}\cdot z.\mathrm{toInt}=a.\mathrm{toInt}\cdot w.\mathrm{toInt}$ iff $z.\mathrm{toInt}=w.\mathrm{toInt}$. The forward direction is mul_left_cancel₀ on the nonzero integer; the reverse is substitution.
why it matters
Without left-cancellation of balanced under nonzero multipliers, the signed-orbit comparison cannot be transported across products. Downstream, cmp_mul_left_of_nonnegFlag_of_not_balanced_zero and cmp_mul_left_of_negativeFlag use this (or the same pattern) to flip or preserve cmp when multiplying on the left by a positive or negative factor. Those comparison laws feed the closed integer_order_certificate, which packages the internal order surface as a finished certificate for the foundation layer.
In the broader Recognition stack this sits under the integers-from-logic construction: once orbits carry a genuine ordered ring structure, later forcing steps (ledger balance, rung arithmetic on the φ-ladder) can treat integer inequalities as native rather than imported. No T5–T8 landmark is proved here; the lemma is pure algebraic scaffolding for that certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.