le_of_product_factors_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (integer-equivalent), then inequality against a fixed left factor is preserved under replacing either product by its balanced twin. Anyone building the internal integer order on δ-orbits cites this when products appear as right-hand sides. The proof is a one-line composition of right-congruence of ≤ under balance with balance of products under balanced factors.
Claim. Let $c,a,a',b,b'$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e. $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$ and likewise for $b,b'$), then $c \le a\cdot b$ if and only if $c \le a'\cdot b'$, where $\le$ means the difference of the right factor minus the left is nonnegative.
background
In the Primitive Recognition Calculus, integers are represented as signed orbits: pairs of nonnegative orbit lengths (positive and negative parts). Two signed orbits are balanced when their lengths satisfy $a.pos + b.neg = b.pos + a.neg$; this is the internal equivalence that recovers ordinary integer equality after mapping to $\mathbb{Z}$ via net length.
The order on signed orbits is defined by $a \le b$ iff the difference $b - a$ is nonnegative (nonnegativity of the signed orbit). Multiplication of signed orbits is the internal product that corresponds to integer multiplication on the net-length map.
Upstream, mul_congr_of_balanced shows that if both factor pairs are balanced then the products are balanced. Separately, le_congr_right_of_balanced shows that $\le$ is invariant when the right-hand argument is replaced by a balanced twin. The present result simply chains those two facts.
proof idea
Term-mode one-liner. First apply product-balance congruence: balanced factors $a\sim a'$ and $b\sim b'$ yield $a\cdot b \sim a'\cdot b'$. Then apply right-hand order congruence: if the two right-hand sides are balanced, $c \le a\cdot b$ iff $c \le a'\cdot b'$. No case analysis or induction; pure composition of the two prior congruences.
why it matters
Feeds the integer-order certificate (integer_order_certificate), which asserts that the internal signed-orbit order surface is closed: display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags all line up. Without product-side invariance of $\le$ under balance, the order would not be well-defined on the integer quotient, and the certificate could not close.
This sits in the foundation layer that reconstructs arithmetic from recognition primitives (δ-orbits and ledger balance), before the forcing chain T0–T8 is applied. It is bookkeeping rather than a landmark forcing step, but it is required scaffolding for any later use of ordered integers inside PRC.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.