cmp_add_left

Signed orbits are the internal carriers of integer-like data in the primitive recognition calculus. Their comparison selector cmp is not the verifier integer display: it returns Ordering.eq when the two orbits are balanced (same signed length), Ordering.lt when the difference is nonnegative and unbalanced, and Ordering.gt otherwise.

Balance is the equality case of the order. Upstream, balanced_add_left_iff states that $c+a$ is balanced with $c+b$ if and only if $a$ is balanced with $b$, proved by transporting through the integer display and omega. Strict order likewise admits a left-add characterization (lt_add_left_iff).

The module builds a closed integer-order surface from these primitives (reflexivity, totality, trichotomy, sign flags) without leaning on external Int order as the definitional source.

Case-split on hcmp : cmp a b.

• If lt: convert via cmp_eq_lt_iff to lt a b, push across left addition with lt_add_left_iff, then rebuild cmp = lt by cmp_eq_lt_of_lt.
• If eq: convert via cmp_eq_eq_iff to balance, push with balanced_add_left_iff, rebuild with cmp_eq_eq_of_balanced.
• If gt: convert via cmp_eq_gt_iff to lt b a, push with lt_add_left_iff on the swapped pair, rebuild with cmp_eq_gt_of_gt.

Each branch is a two-step transport: Ordering decode, left-add iff, Ordering encode.

Translation invariance of comparison is a required algebraic law for any integer-like order. It feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging display lemmas for truncated subtraction, leq, absolute difference, and nonnegativity flags.

In the Recognition foundation stack this sits under the arithmetic-from-logic and ledger-forcing layer: order must be forced from recognition structure (balance and sign flags on orbits) rather than imported from classical Int. The result is local bookkeeping, not a T0–T8 forcing step, but without it the certificate cannot assert that the signed-orbit order behaves as a genuine ordered group under addition.