cmp_congr_of_balanced

Signed orbits are the primitive integer carriers in the recognition calculus: each carries a signed distinction orbit rather than a bare verifier integer. Two orbits are balanced when they represent the same integer (same length and sign data under the ledger balance relation). The internal comparison selector cmp is defined from that balance test and the nonnegativity flag of the difference: equal when balanced, otherwise ordered by whether $b-a$ is nonnegative.

This lives in the IntegerOrder layer of PrimitiveRecognitionCalculus, which builds a total order on signed orbits without appealing to the display integer. Upstream, cmp_eq_eq_iff and cmp_eq_eq_of_balanced pin the equality case of cmp exactly to balance; companion lt congruence lemmas (left and right under balance) move strict inequalities across balanced replacements. The arithmetic-from-logic strict order on LogicNat is the distant ancestor of the orbit-level lt used here.

Tactic proof by cases on cmp a b.

• If lt: unpack via cmp_eq_lt_iff to get lt a b, push the inequality across hb then ha with lt_congr_right_of_balanced and lt_congr_left_of_balanced, and repack with cmp_eq_lt_of_lt.
• If eq: unpack balance of $a$ with $b$, chain balanced_symm ha, that balance, and hb by balanced_trans to get balance of $a'$ with $b'$, then apply cmp_eq_eq_of_balanced.
• If gt: dual of the lt case, swapping sides and using cmp_eq_gt_iff / cmp_eq_gt_of_gt with the congruence lemmas on the reversed pair.

This is the basic congruence lemma for the signed-orbit comparison: once balance is an equivalence, cmp descends to the quotient. Downstream it is the workhorse for product and difference stability: cmp_of_product_factors_of_balanced, the one-sided product factor variants, and cmp_of_sub_inputs_of_balanced (plus left/right sub variants) all reduce to replacing balanced factors inside cmp. Multiplicative cancellation forms cmp_mul_ofOrbit_left_of_ne_zero and cmp_mul_ofOrbit_right_of_ne_zero likewise rely on transporting comparisons across balanced rewrites.

In the Recognition foundation this keeps integer order internal to the orbit calculus (not the verifier display), so later forcing and ledger steps can treat order as a recognition primitive. It does not itself touch T5–T8 or the J-cost; it is pure order infrastructure under the arithmetic-from-logic stack.