cmp_products_of_balanced
plain-language theorem explainer
Comparison of products of signed orbits is invariant under the balanced equivalence on each factor. Anyone building the internal integer order from δ-orbit data cites this when products must not depend on representative choice. The proof is a two-step term application: multiply factors congruently, then compare congruently.
Claim. Let $a,a',b,b',c,c',d,d'$ be signed orbits. If $a$ is balanced with $a'$, $b$ with $b'$, $c$ with $c'$, and $d$ with $d'$, then $\mathrm{cmp}(a\cdot b,\, c\cdot d)=\mathrm{cmp}(a'\cdot b',\, c'\cdot d')$, where $\mathrm{cmp}$ is the internal signed-orbit comparison (equality on balance, otherwise the sign of the difference).
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their lengths match in the internal sense $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the PRC integer equivalence, not a display-level integer identity.
The internal comparison $\mathrm{cmp}$ returns equality when the two orbits are balanced, otherwise orders by the nonnegativity flag of the difference. Multiplication of signed orbits is the operation whose integer image multiplies the corresponding integers. Upstream, multiplication preserves balance: if $a\sim a'$ and $b\sim b'$ then $a\cdot b\sim a'\cdot b'$. Separately, $\mathrm{cmp}$ itself is congruent under balance of both arguments.
This module builds the order surface on those primitives so that later certificates can treat signed-orbit comparison as a closed internal structure.
proof idea
One-line term proof. Apply multiplication-congruence twice: $\mathrm{mul_congr_of_balanced},ha,hb$ yields balance of $a\cdot b$ with $a'\cdot b'$, and likewise for $c\cdot d$ with $c'\cdot d'$. Feed those two balance witnesses into $\mathrm{cmp_congr_of_balanced}$, which states that balanced pairs may be substituted under $\mathrm{cmp}$. No case split on Ordering is needed here; that work lives in the congruence lemmas.
why it matters
Feeds the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. Without product-level comparison invariance, the order would depend on orbit representatives and could not certify a stable integer layer under multiplication.
In the Recognition foundation this sits inside the ledger and distinction calculus that underwrite the forcing chain: integers and their order must arise from balanced δ-orbit data before mass ladders, eight-tick structure, or continuum limits are attached. It is a small but necessary congruence step so that the certificate can package display lemmas (truncated subtraction, absolute difference, nonnegativity flags) without reopening representative choice for products.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.