le_congr_left_of_balanced
plain-language theorem explainer
Balanced signed orbits may be substituted on the left of the internal order: if a and a' balance, then a ≤ b holds exactly when a' ≤ b. Congruence lemmas for products and differences, and the integer-order certificate, cite this fact. The proof rewrites both sides through the toInt order bridge and substitutes equality of the integer displays.
Claim. Let $a$, $a'$, and $b$ be signed orbits. If $a$ and $a'$ are balanced (i.e. $a_{+}+a'_{-}=a'_{+}+a_{-}$), then $a\le b$ if and only if $a'\le b$, where the internal order means that the signed-orbit difference is nonnegative.
background
In Primitive Recognition Calculus, integers appear as signed orbits: pairs of nonnegative orbit lengths (a positive part and a negative part). Two signed orbits are balanced when $a_{+}+b_{-}=b_{+}+a_{-}$. That internal relation is the PRC integer equivalence; the upstream bridge states it agrees with equality of the conservative $\mathbb{Z}$ display (toInt).
Internal order is defined by $a\le b$ when $b-a$ is nonnegative. A second upstream bridge identifies this with ordinary integer comparison of the displays. The IntegerOrder module assembles these bridges so later arithmetic (products, differences) can transport inequalities along balance classes rather than particular orbit representatives.
proof idea
Short term-mode rewrite. Both sides of the biconditional are rewritten by the characterization that internal $\le$ is ordinary $\le$ on the integer displays. The balance hypothesis is turned, via the balanced-iff-toInt-equality bridge, into equality of the two left-hand displays; the two integer inequalities therefore coincide and the biconditional follows.
why it matters
This is the left half of order congruence on balance classes. It is composed into the two-sided congruence, and is the transport step in the product-factor and sub-input families (left/right factor and joint versions). Those lemmas help close the internal signed-orbit order surface recorded by the integer-order certificate.
In the Recognition foundation stack the point is definitional hygiene: order becomes a property of the integer value, not of a chosen orbit representative. That is required before ledger and forcing constructions can treat PRC integers as ordered without tracking representatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.