le_product_factors_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (the internal PRC integer equivalence), then the product of the first pair is ≤ a third orbit exactly when the product of the second pair is. Anyone proving that multiplication is well-defined on the signed-orbit order cites this. The proof is a one-line composition of product-congruence of balanced with left-congruence of ≤.
Claim. Let $a,a',b,b',c$ 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 $a\cdot b\le c$ if and only if $a'\cdot b'\le c$, where $\le$ means the difference is nonnegative.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative $\delta$-orbit lengths with a sign. Two signed orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; that is the internal integer equivalence (K4.9), defined entirely on orbit positions.
The internal order is $a\le b$ when $b-a$ is nonnegative. Multiplication of signed orbits is the corresponding product on those positions. The module builds the ordered-integer surface from these primitives rather than from classical $\mathbb{Z}$.
Upstream, mul_congr_of_balanced shows balanced is a congruence for multiplication: if $a\sim a'$ and $b\sim b'$ then $a\cdot b\sim a'\cdot b'$. Separately, le_congr_left_of_balanced shows $\le$ depends only on the balanced class of the left argument: $a\sim a'$ implies $a\le c\Leftrightarrow a'\le c$. Both reduce through the toInt embedding.
proof idea
One-line term proof. Apply mul_congr_of_balanced to the two balanced hypotheses to obtain that $a\cdot b$ is balanced with $a'\cdot b'$. Feed that single balanced witness into le_congr_left_of_balanced against the fixed right-hand side $c$. The resulting biconditional is exactly the claim. No case split on signs or separate nonnegativity argument is needed.
why it matters
This lemma is one of the congruence steps that close the internal signed-orbit order. It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed": the certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
Without product-factor invariance of $\le$ under balanced, multiplication would not descend to a well-defined operation on the ordered quotient that PRC uses as integers. The result sits in the Foundation layer that reconstructs arithmetic from recognition primitives, upstream of the forcing chain (T0–T8) and the physical constants ladder. It does not itself force $\phi$ or dimension; it only seals the order-algebra interface those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.