lt_add_left_iff
plain-language theorem explainer
Left-addition by a fixed signed orbit is an order automorphism for the strict order: $c+a<c+b$ if and only if $a<b$. Anyone assembling the ordered abelian group structure on PRC integers cites this. The proof pushes both sides through the integer embedding and closes by linear arithmetic.
Claim. For signed orbits $a,b,c$ (each a pair of distinction-naturals meaning $\mathrm{pos}-\mathrm{neg}$), writing $+$ for componentwise addition and $<$ for the internal strict order (nonnegative difference that is not balanced), one has $c+a < c+b$ if and only if $a < b$.
background
Signed orbits are the PRC stand-in for integers: a structure with positive and negative distinction-natural parts, intended as $\mathrm{pos}-\mathrm{neg}$. Addition is componentwise on those parts. The map $\mathrm{toInt}$ sends a signed orbit to an ordinary integer difference of the underlying natural values; upstream, addition is compatible with that map: $(\mathrm{add},a,b).\mathrm{toInt}=a.\mathrm{toInt}+b.\mathrm{toInt}$.
Strict order on signed orbits is defined internally as the weak order together with failure of balance (equal $\mathrm{toInt}$ images). The bridge lemma states that this coincides with ordinary integer comparison: $a<b$ iff $a.\mathrm{toInt}<b.\mathrm{toInt}$. The ambient module builds the ordered arithmetic surface on these objects from the logic-native natural numbers upward.
proof idea
Rewrite both occurrences of signed-orbit strict order via the bridge to integer comparison. Rewrite both left-additions via the addition-toInt identity, so the goal becomes $c.\mathrm{toInt}+a.\mathrm{toInt}<c.\mathrm{toInt}+b.\mathrm{toInt}$ iff $a.\mathrm{toInt}<b.\mathrm{toInt}$. Finish with omega on $\mathbb{Z}$.
why it matters
This is the cancellation/translation invariance step for the strict order under left addition. Downstream, the one-direction monotonicity lemma is exactly the reverse implication of this biconditional, and the comparison-function identity under left addition cases on the three-way compare and invokes the same fact. Both feed the integer-order certificate, whose doc-comment records that "the internal signed-orbit order surface is closed." In the Recognition foundation stack this is ordinary ordered-group hygiene on the integers reconstructed from distinction orbits, not a physics forcing step (T5--T8), but it is required scaffolding before rationals, Cauchy reals, and cost calculus sit on a certified ordered base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.