cmp_of_product_factors_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same internal integer), comparing any fixed orbit c against the product of the first pair equals comparing c against the product of the second pair. Order-certificate authors cite this to show multiplication is well-defined on the quotient by balance before the integer-order surface is closed. The proof is a two-lemma glue: self-balance of c plus product congruence into comparison congruence.
Claim. Let $c,a,a',b,b'$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (equal orbit-length integers), then the internal comparison $\mathrm{cmp}(c, a\cdot b)$ equals $\mathrm{cmp}(c, a'\cdot b')$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg). Two orbits are balanced when a.pos + b.neg = b.pos + a.neg; by K4.9 this is equivalent to equal verifier integers toInt. Balance is the internal equivalence used before any external $\mathbb{Z}$ display is trusted.
Multiplication of signed orbits is defined on the orbit data and descends to integers via mul_toInt. The internal comparison selector cmp returns equality when the two arguments are balanced, otherwise reads the nonnegativity flag of their difference; it is deliberately not defined from the verifier integer display.
Upstream, mul_congr_of_balanced shows that balanced factors yield balanced products, and cmp_congr_of_balanced shows that cmp is invariant when both arguments are replaced by balanced partners. The present lemma specializes that invariance to a fixed left argument and a product on the right.
proof idea
First obtain self-balance of $c$ by rewriting with balanced_iff_toInt_eq (reflexivity of integer equality). Next apply mul_congr_of_balanced to the two factor-balance hypotheses to conclude that $a\cdot b$ is balanced with $a'\cdot b'$. Feed self-balance of $c$ and that product balance into cmp_congr_of_balanced to finish. No case split on the ordering value is needed here; the work sits in the two named congruences.
why it matters
This is a well-definedness step for the internal signed-orbit order under multiplication. It feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity.
In the Recognition foundation stack, PRC builds integers and their order from $\delta$-orbit positions before ledger forcing and the T0–T8 chain. Keeping cmp congruent under balanced products ensures the order used downstream does not depend on orbit representatives. Without this, the certificate could not treat products as stable on the balance quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.