le_congr_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer value under the PRC equivalence), their order relation is preserved: a ≤ b if and only if a' ≤ b'. Anyone proving that ≤ descends to the integer quotient, or that products and differences respect balanced representatives, cites this. The proof is a one-line composition of the left- and right-sided congruence lemmas.
Claim. Let $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 $a\le b$ if and only if $a'\le b'$, where $\le$ is the internal order ($b-a$ 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 $a.pos + b.neg = b.pos + a.neg$; this is the internal equivalence that identifies representatives of the same integer (K4.9).
The order on signed orbits is defined by $a \le b$ iff the difference $b - a$ is nonnegative. Upstream, this order is also characterized via the integer embedding: $a \le b$ iff $\mathrm{toInt}(a) \le \mathrm{toInt}(b)$, and balanced pairs are exactly those with equal $\mathrm{toInt}$ images.
The module builds the full order surface on these internal representatives (reflexivity, transitivity, totality, trichotomy, and congruence under arithmetic). The one-sided lemmas already show that replacing the left or right argument by a balanced partner preserves $\le$; this declaration packages both sides.
proof idea
Term-mode one-liner. Apply le_congr_left_of_balanced to the left pair $(a,a')$ to get $a \le b \leftrightarrow a' \le b$, then chain with le_congr_right_of_balanced on the right pair $(b,b')$ to get $a' \le b \leftrightarrow a' \le b'$. The two Iffs compose by Iff.trans.
Each one-sided lemma rewrites $\le$ through le_iff_toInt_le and substitutes equal toInt values from balanced_iff_toInt_eq. No new arithmetic is done here.
why it matters
Congruence of $\le$ under balanced replacement is the bridge from representative-level order to a well-defined order on the integer quotient. Downstream it feeds le_products_iff_of_balanced and le_subtractions_iff_of_balanced (order of products and differences is independent of balanced choice of factors), and the scaling lemmas le_mul_ofOrbit_left_iff_of_ne_zero / le_mul_ofOrbit_right_iff_of_ne_zero.
It also sits under integer_order_certificate, which closes the internal signed-orbit order surface for the foundation stack. Without two-sided congruence, the order would not be a relation on equivalence classes, and later arithmetic comparison lemmas would have to carry explicit representatives. This is pure foundation scaffolding for the PRC integer layer, not a physics forcing step (T0–T8), but it is required before mass-ladder or ledger comparisons can treat integers abstractly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.