le_congr_left_of_balanced_cf
plain-language theorem explainer
If two signed orbits are balanced (same internal integer), left-hand comparison against any third orbit is invariant under that equivalence. Anyone building choice-free order facts on the PRC integer layer cites this. The proof rewrites balance and order to Nat equalities/inequalities and finishes with omega.
Claim. Let $a$, $a'$, and $b$ be signed orbits. If $a$ and $a'$ are balanced, meaning $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$, 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 represented as signed orbits: pairs of nonnegative $\delta$-orbit positions (positive and negative parts). Two signed orbits are balanced when their lengths match in the sense $a.pos+b.neg=b.pos+a.neg$; this is the internal PRC integer equality, characterized at the Nat level by equal sums of toNat components.
The order $a\le b$ means the difference $b-a$ is nonnegative. Upstream, le_iff_toNat_cf gives the choice-free characterization: $a\le b$ iff $b.neg.toNat+a.pos.toNat\le b.pos.toNat+a.neg.toNat$. That lemma is the Nat-level stand-in for the older toInt comparison and is what makes congruence arguments stay inside constructive arithmetic.
This module sits in the Grow layer that develops order and product facts without classical choice, feeding later ledger and forcing constructions that treat balanced orbits as the same integer.
proof idea
Term-style tactic proof. First rewrite the balanced hypothesis via balanced_iff_toNat_eq to an equality of Nat sums. Split the biconditional. In each direction, rewrite the order hypothesis and goal with le_iff_toNat_cf, which turns $\le$ into a four-term Nat inequality; the balanced equality makes the two inequalities identical up to rearrangement, so omega closes both sides.
why it matters
Left-congruence under balance is the first half of full order congruence for the PRC integer relation. Downstream, le_congr_of_balanced_cf composes this with the right-hand twin to get $a\le b\leftrightarrow a'\le b'$ whenever both pairs are balanced. The product-side lemma le_product_right_factor_iff_of_balanced_cf applies it after mul_balanced_congr_right_cf, so replacing a balanced right factor does not change product inequalities.
That package keeps the signed-orbit order a well-defined order on equivalence classes (the internal integers) without choice. In the broader Recognition stack this is foundation plumbing under ArithmeticFromLogic and ledger forcing: once order respects balance, later forcing-chain and mass-ladder arguments can treat balanced representatives interchangeably. No T5–T8 landmark is proved here; the result is pure order infrastructure for the choice-free integer layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.