mul_congr_of_balanced_right
plain-language theorem explainer
Left multiplication by a fixed signed orbit preserves the balanced relation on the right factor: if b and b' display the same integer, so do a·b and a·b'. Order and comparison lemmas for products cite this as the congruence step. The proof is a three-line rewrite through the toInt bridge and multiplicativity of the integer display.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$ (equivalently $b$ and $b'$ have the same integer display), then $a\cdot b$ and $a\cdot b'$ are balanced.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their orbit lengths match crosswise: $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 theorem states that balance is equivalent to equality of the conservative integer displays: $\mathrm{balanced},a,b \leftrightarrow a.\mathrm{toInt}=b.\mathrm{toInt}$. Multiplication of signed orbits is defined so that the display is a ring homomorphism: $(\mathrm{mul},a,b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$.
This module builds the order surface on those signed orbits. Congruence of balance under arithmetic is the prerequisite for transporting $\le$, $<$, and $\mathrm{cmp}$ across product factors.
proof idea
Term-mode rewrite proof. First rewrite the goal and the hypothesis with the characterization that balance iff equal integer displays. The goal becomes $(\mathrm{mul},a,b).\mathrm{toInt}=(\mathrm{mul},a,b').\mathrm{toInt}$. Apply multiplicativity of the display on both sides, then substitute the rewritten hypothesis $b.\mathrm{toInt}=b'.\mathrm{toInt}$. No case splits or omega.
why it matters
This is the right-factor multiplication congruence for the PRC integer equivalence. Downstream it is the hypothesis discharged by the product order transport lemmas: $\mathrm{le}$ and $\mathrm{lt}$ iff statements for a product on the left or right of a comparison, and the corresponding $\mathrm{cmp}$ identities when the right factor is replaced by a balanced partner. Those feed the closed integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the foundation stack this keeps the signed-orbit arithmetic compatible with the integer view without leaving the distinction-nat presentation. It is local algebra, not a forcing-chain step, but it is load-bearing for any later use of ordered PRC integers in ledger or gap arguments that multiply signed quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.