le_add_right_iff
plain-language theorem explainer
Right-translation by a fixed signed orbit preserves the internal order: a+c ≤ b+c if and only if a ≤ b. Anyone assembling the integer-order certificate, or checking that signed-orbit order matches ℤ-order, cites this. The proof bridges both sides to integer comparison via toInt, then closes with linear arithmetic.
Claim. Let $a,b,c$ be signed orbits (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$). Writing $\le$ for the internal order ($b-a$ nonnegative), one has $a+c \le b+c$ if and only if $a \le b$.
background
Signed orbits are the integer layer of the primitive recognition calculus: a structure with two distinction-natural components, intended as $\mathrm{pos}-\mathrm{neg}$. Addition and subtraction act componentwise on those parts; the bridge toInt sends a signed orbit to an ordinary integer difference of the underlying natural values.
Internal order is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative. An upstream lemma equates this with the ordinary integer comparison of the images under toInt. Another upstream fact states that addition is respected by toInt: $(a+b).\mathrm{toInt} = a.\mathrm{toInt}+b.\mathrm{toInt}$.
The ambient module builds the order theory on this signed-orbit carrier so that the recognition foundation can treat integers without importing classical $\mathbb{Z}$ as a primitive.
proof idea
Term-style proof in three steps. Rewrite both occurrences of signed-orbit $\le$ into integer $\le$ via the bridge lemma that equates internal order with toInt comparison. Rewrite both additions via the lemma that toInt preserves addition, obtaining $a.\mathrm{toInt}+c.\mathrm{toInt} \le b.\mathrm{toInt}+c.\mathrm{toInt}$ on the left-hand side. Finish with omega, which cancels the common integer summand.
why it matters
This is one of the elementary order-arithmetic laws needed to certify that the internal signed-orbit order surface is closed. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the signed-orbit order surface is closed and packages display lemmas for nonnegativity, flags, and related order primitives.
In the Recognition foundation stack, integers are not assumed; they are reconstructed from distinction naturals and signed orbits. Translation-invariance of $\le$ under addition is part of matching that reconstruction to ordinary integer order, so later forcing and mass-ladder work can treat integer comparisons as already settled rather than axiomatic. It sits among sibling facts (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations) that together discharge the order certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.