le_congr_right_of_balanced
plain-language theorem explainer
If two signed orbits are balanced (same integer value), the internal order against any fixed left operand is unchanged on the right. Anyone transporting inequalities across equivalent integer displays cites this. The proof rewrites both sides to the ℤ comparison and substitutes equality of the integer displays.
Claim. Let $a,b,b'$ be signed orbits. If $b$ and $b'$ are balanced, i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$ (equivalently $b$ and $b'$ have the same integer display), then $a\le b$ if and only if $a\le b'$, where $\le$ is the internal signed-orbit order ($b-a$ nonnegative).
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (positive and negative legs). Two orbits are balanced when those legs match crosswise, $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equality; the bridge theorem states it is equivalent to equality of the conservative $\mathbb{Z}$ displays.
The internal order is defined without leaving the orbit language: $a\le b$ means the difference $b-a$ is nonnegative. A companion lemma identifies this with ordinary inequality of the integer displays. The present result is the right-operand half of order congruence under that balance relation, inside the IntegerOrder surface that packages the closed order theory for signed orbits.
proof idea
Term-mode, three rewrites. Both sides of the desired biconditional are rewritten by the display bridge for order, so the goal becomes $a.\mathrm{toInt}\le b.\mathrm{toInt}$ iff $a.\mathrm{toInt}\le b'.\mathrm{toInt}$. The balance hypothesis is turned into $b.\mathrm{toInt}=b'.\mathrm{toInt}$ via the balance-to-display equivalence, and substitution finishes. No case split and no omega at this layer; the arithmetic work lives in the two upstream bridges.
why it matters
This is the right half of order congruence under integer equivalence. It is composed with the left half into full two-sided congruence, and is the workhorse for every product- and difference-factor transport lemma in the same module (order against a product or difference is invariant when factors are replaced by balanced partners). Those lemmas feed the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. In the Recognition foundation stack this is bookkeeping on the arithmetic layer beneath the forcing chain: once integers and their order are internal and congruence-stable, later constructions (mass ladder, ledger forcing) can treat $\le$ as a well-defined relation on equivalence classes rather than on raw orbit representatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.