le_congr_of_balanced_cf
plain-language theorem explainer
If two pairs of signed orbits are balanced (same internal integer value), the order relation a ≤ b is invariant under replacing either argument by its balanced partner. Anyone building the PRC integer order from δ-orbit data cites this. The proof is a one-line Iff.trans of the left and right 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_{+} + a'_{-} = a'_{+} + a_{-}$ and likewise for $b,b'$), then $a \le b$ if and only if $a' \le b'$, where $\le$ means the difference is nonnegative.
background
In the Primitive Recognition Calculus, integers are not postulated; they arise as signed orbits of δ-steps. A signed orbit records a positive and a negative orbit length. Two signed orbits are balanced when $a_{+} + b_{-} = b_{+} + a_{-}$: their net displacements agree. That is the internal PRC integer equality (K4.9), defined only on orbit positions.
The order $a \le b$ is defined by nonnegativity of the difference $b - a$ in the signed-orbit monoid. The left and right congruence lemmas already show that balancing the left (resp. right) argument alone preserves $\le$. This module sits in the Grow layer that lifts those one-sided facts to a two-sided congruence, so the order descends to the quotient by balance.
proof idea
One-line term proof. Apply le_congr_left_of_balanced_cf to ha to get $a \le b \leftrightarrow a' \le b$, then chain with le_congr_right_of_balanced_cf on hb to replace $b$ by $b'$, yielding $a \le b \leftrightarrow a' \le b'$. Composition is ordinary Iff.trans.
why it matters
Balance is the PRC stand-in for integer equality; without two-sided order congruence, $\le$ would not be well-defined on the integer quotient. This closes the left/right pair into a single congruence theorem for signed-orbit order, which is required before rationals and the φ-ladder can inherit a coherent comparison from orbit data. No downstream consumers are wired yet in the graph, so it is presently a leaf that packages the two one-sided Grow lemmas for later arithmetic and ledger-forcing use. It does not itself touch T5–T8 or the RCL; it is pure foundation plumbing under ArithmeticFromLogic and IntegerRational.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.