cmp_add_right
plain-language theorem explainer
Right-addition by a fixed signed orbit leaves the internal comparison of two signed orbits unchanged: cmp(a+c,b+c)=cmp(a,b). Anyone assembling the integer-order certificate or proving translation invariance of the signed-orbit order cites this. The proof cases on the three Ordering values and routes each through the matching add-right equivalence for strict order or balance.
Claim. For any signed orbits $a$, $b$, and $c$, the internal comparison of $a+c$ with $b+c$ equals the internal comparison of $a$ with $b$: $\mathrm{cmp}(a+c,\,b+c)=\mathrm{cmp}(a,b)$.
background
Signed orbits are the internal carriers of integer-like order in the primitive recognition calculus. Their comparison selector cmp is defined from signed-orbit order and balanced length, not from the verifier integer display: it returns equality when the pair is balanced, otherwise strict less or greater according to the nonnegativity flag of the difference.
Balance of two signed orbits is the equality case of that selector. Upstream, balance is translation-invariant under right addition: $a$ is balanced with $b$ if and only if $a+c$ is balanced with $b+c$ (proved by reducing to integer equality via the toInt display and a short omega argument). Strict order likewise admits an add-right equivalence.
The local module builds a closed order surface on these carriers: reflexivity, totality, trichotomy, and the usual flag characterizations of nonnegativity and negativity. Translation invariance of cmp is the remaining algebraic glue that makes the order behave like the integers under addition.
proof idea
Term-mode case split on hcmp : cmp a b.
- If
lt: rewrite viacmp_eq_lt_iffto obtainlt a b, push the inequality across right addition withlt_add_right_iff, then reassemble withcmp_eq_lt_of_lt. - If
eq: rewrite viacmp_eq_eq_iffto balance of $a$ and $b$, transport withbalanced_add_right_iff, then reassemble withcmp_eq_eq_of_balanced. - If
gt: dual of theltbranch, usingcmp_eq_gt_iff,lt_add_right_iffon the swapped pair, andcmp_eq_gt_of_gt.
No new arithmetic is invented here; each branch is a pure transport along the already-proved add-right equivalences.
why it matters
This lemma is one of the algebraic closure facts consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." Without translation invariance of the comparison selector, the certificate could not treat signed-orbit order as a stable integer-like structure under addition.
In the broader Recognition foundation, integers and their order are not postulated: they are forced from recognition/ledger structure (balance, signed orbits, distinction naturals). Right-invariance of cmp is the concrete step that makes that forced order compatible with the additive monoid already present on signed orbits. It sits downstream of the balance and strict-order add-right equivalences and upstream of the single certificate that packages the whole order surface for later arithmetic and physics layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.