mul_congr_of_balanced
plain-language theorem explainer
Multiplication of signed orbits respects the internal balance relation: if a is balanced with a' and b with b', then a·b is balanced with a'·b'. Order and comparison lemmas for products cite this congruence. The proof is a three-line rewrite through the integer display of orbits.
Claim. Let $a,a',b,b'$ be signed orbits (pairs of distinction naturals interpreted as $pos-neg$). If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (equivalently, their integer displays agree), then the product orbit $a\cdot b$ is balanced with $a'\cdot b'$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair $(pos,neg)$ of distinction naturals, intended as the difference $pos-neg$. Two signed orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; this is the internal PRC integer relation, defined entirely on $\delta$-orbit positions (K4.9).
The bridge to ordinary integers is the display map $toInt$: balance holds if and only if $a.toInt=b.toInt$. Multiplication of signed orbits is defined so that it matches integer multiplication on the display: $(a\cdot b).toInt=a.toInt\cdot b.toInt$.
This module builds the order surface on those signed orbits. Congruence of multiplication under balance is the algebraic step needed before product comparisons and $\le$ statements can be rewritten across balanced representatives.
proof idea
Term-mode rewrite proof. First rewrite both the hypotheses and the goal with $balanced_iff_toInt_eq$, turning balance into equality of integer displays. Then rewrite both product displays with $mul_toInt$, so the goal becomes $a.toInt\cdot b.toInt=a'.toInt\cdot b'.toInt$. Substitute the rewritten hypotheses $ha$ and $hb$ to finish.
why it matters
This is the multiplicative congruence lemma for the internal signed-orbit equivalence. Downstream it feeds every product-order rewrite in the module: $\le$ and $cmp$ for one or both factors, and the four-factor product comparison $cmp_products_of_balanced$. Those lemmas in turn support the closed integer-order certificate ($integer_order_certificate$), which records that the signed-orbit order surface is closed.
In the Recognition foundation stack this sits under the ledger/PRC integer layer that precedes forcing of $\phi$, the eight-tick octave, and $D=3$. It does not itself force physical constants; it keeps the internal $\mathbb{Z}$-view of orbits coherent under multiplication so later order and gap arguments can treat balanced representatives interchangeably.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.