lt_congr_right_of_balanced
plain-language theorem explainer
Right-congruence for the strict order on signed orbits: if two right-hand sides are balanced (same integer value), then a < b holds exactly when a < b'. Order theorists and anyone building integer arithmetic from δ-orbits cite it. The proof is a two-line rewrite through the toInt characterizations of lt and balanced.
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}$), then $a < b$ if and only if $a < b'$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit positions (pos, neg) that encode a signed length. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal PRC equality relation on δ-orbit data, and it agrees with equality of the conservative integer display toInt.
Strict order is defined internally as nonnegative difference with nonzero difference (le and not balanced). The bridge lemma lt_iff_toInt_lt states that this internal order is exactly the usual order on the integer displays. The present result is the right-hand half of order-congruence under that equivalence.
The module builds a closed integer-order surface on these orbits, feeding the broader Arithmetic-from-Logic and ledger-forcing stack in Foundation.
proof idea
Term-mode proof by two rewrites. First replace both sides of the biconditional by the integer-display form via lt_iff_toInt_lt. Then apply balanced_iff_toInt_eq to the hypothesis, so the right-hand integers coincide and the ordinary < goals match. No case split or omega is needed at this layer; the work sits in the two characterization lemmas.
why it matters
This is the right-factor of order congruence under balanced equivalence. Downstream it is composed with the left version to give full lt_congr_of_balanced, and it is the workhorse for product and difference stability: lt_of_product_factors_iff_of_balanced, the one-sided product variants, and the subtraction-input variants all invoke it after a mul/sub congruence. Comparison congruence cmp_congr_of_balanced and the closing integer_order_certificate ("the internal signed-orbit order surface is closed") sit above it.
In the Recognition stack this is pure Foundation scaffolding: it makes the PRC integer order well-defined on equivalence classes before the forcing chain (T0–T8) and the J-cost calculus ever see a number. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.