mul_congr_of_balanced_left
plain-language theorem explainer
Right-multiplication by a fixed signed orbit preserves the internal balance relation: if two signed orbits represent the same integer, so do their products with any third factor. Order and comparison lemmas for the PRC integer surface cite this congruence. The proof is a three-line rewrite through the toInt bridge and the multiplicative display of mul.
Claim. Let $a$, $a'$, and $b$ be signed orbits (pairs of distinction naturals read as $a = a_+ - a_-$). If $a$ and $a'$ are balanced, i.e. $a_+ + a'_- = a'_+ + a_-$, then $a \cdot b$ and $a' \cdot b$ are balanced.
background
In the Primitive Recognition Calculus, a signed orbit is a pair $(p,n)$ of distinction naturals, intended as the difference $p-n$. Two signed orbits are balanced when $a_+ + b_- = b_+ + a_-$; this is the internal integer equality, defined only on $\delta$-orbit positions (K4.9).
The bridge to the conservative integer view is the theorem that balance holds if and only if the integer displays agree: $a.\mathrm{toInt} = b.\mathrm{toInt}$. Multiplication of signed orbits is defined so that its integer display multiplies: $(\mathrm{mul}, a, b).\mathrm{toInt} = a.\mathrm{toInt}\cdot b.\mathrm{toInt}$.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). Congruence of multiplication under balance is the algebraic step that lets order and comparison ignore choice of balanced representative on a left factor.
proof idea
Term-mode rewrite proof. First rewrite the goal and the hypothesis with the characterization that balance is equivalent to equality of integer displays. Then rewrite both sides of the resulting equality by the multiplicative display of mul, so the goal becomes $a.\mathrm{toInt}\cdot b.\mathrm{toInt} = a'.\mathrm{toInt}\cdot b.\mathrm{toInt}$. Close by the rewritten hypothesis $a.\mathrm{toInt} = a'.\mathrm{toInt}$.
why it matters
This is the left-factor congruence for signed-orbit multiplication under the internal balance relation. Downstream it feeds the product-order transfer lemmas: $\le$ and $<$ on a product with fixed right factor are invariant under replacing the left factor by a balanced twin, and likewise for the three-way comparison $\mathrm{cmp}$. Those lemmas are applied inside the integer-order certificate that closes the signed-orbit order surface.
In the Recognition stack this sits in the foundation layer that reconstructs integer arithmetic from distinction orbits before the forcing chain (T0–T8) and the J-cost calculus. It does not itself force $\phi$ or dimension; it keeps the PRC integer model coherent so later ledger and cost constructions can treat balanced orbits as interchangeable under multiplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.