mul_respects_balanced
plain-language theorem explainer
Multiplication of signed orbits preserves the balanced equivalence relation: if $a_1\sim a_2$ and $b_1\sim b_2$, then $a_1 b_1\sim a_2 b_2$. Anyone building PRC integers as a quotient of signed orbits cites this to justify that multiplication descends. The proof rewrites both sides through the integer display and uses multiplicativity of that display.
Claim. Let $a_1,a_2,b_1,b_2$ be signed orbits (pairs of distinction-nats, read as $\mathrm{pos}-\mathrm{neg}$). If $a_1$ is balanced with $a_2$ and $b_1$ is balanced with $b_2$ (i.e. $a_1.\mathrm{pos}+a_2.\mathrm{neg}=a_2.\mathrm{pos}+a_1.\mathrm{neg}$, and likewise for $b$), then the signed-orbit products $a_1\cdot b_1$ and $a_2\cdot b_2$ are balanced.
background
In the Primitive Recognition Calculus, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-nats, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the internal equivalence used to form PRC integers.
The verifier map $\mathrm{toInt}$ sends a signed orbit to an ordinary integer $\mathrm{pos}.\mathrm{toNat}-\mathrm{neg}.\mathrm{toNat}$. Upstream, $\mathrm{balanced}\leftrightarrow\mathrm{toInt}$ equality is already proved, and signed-orbit multiplication is defined by the usual difference-of-products formula $(p_1-n_1)(p_2-n_2)=(p_1p_2+n_1n_2)-(p_1n_2+n_1p_2)$, with $\mathrm{mul_toInt}$ stating that $\mathrm{toInt}$ is a ring homomorphism on that operation.
The local module builds integer and rational arithmetic on these orbit objects before quotienting.
proof idea
Short rewrite proof. First replace both balanced hypotheses and the goal by equality of $\mathrm{toInt}$ values via $\mathrm{balanced_iff_toInt_eq}$. Then apply $\mathrm{mul_toInt}$ on each product so the goal becomes $a_1.\mathrm{toInt}\cdot b_1.\mathrm{toInt}=a_2.\mathrm{toInt}\cdot b_2.\mathrm{toInt}$. Substitute the rewritten hypotheses $a_1.\mathrm{toInt}=a_2.\mathrm{toInt}$ and $b_1.\mathrm{toInt}=b_2.\mathrm{toInt}$. Done.
why it matters
This is the congruence lemma that lets signed-orbit multiplication descend to the quotient of balanced classes. Downstream it is the exact witness inside $\mathrm{Quot.lift}_2$ for PRC-integer multiplication (K4.8): each well-definedness obligation is an instance of this theorem plus reflexivity of balanced. Without it, PRC integers would have addition-level structure only.
In the broader Recognition stack, PRC integers sit under the primitive recognition calculus that feeds the forcing chain (T0–T8) and ledger constructions. The result is pure foundation arithmetic: it does not itself force $\phi$, the eight-tick octave, or $D=3$, but it is part of the integer substrate those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.