lt_add_right_iff
plain-language theorem explainer
Strict order on signed orbits is invariant under right translation: a+c < b+c if and only if a < b. Anyone building the ordered-group laws for the PRC integer layer cites this. The proof reduces both sides to ℤ via toInt, uses additivity of toInt, and finishes with omega.
Claim. For signed orbits $a,b,c$ (each a difference $\mathrm{pos}-\mathrm{neg}$ of distinction naturals), $a+c < b+c$ if and only if $a < b$, where $<$ is the internal strict order (nonnegative nonzero difference).
background
Signed orbits are the PRC stand-in for integers: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$. Addition is componentwise on the two legs. The map $\mathrm{toInt}$ sends a signed orbit to an ordinary integer difference of natural values.
Strict order on signed orbits is defined internally as "$a \le b$ and not balanced," i.e. a nonnegative nonzero difference. The bridge lemma $\mathrm{lt_iff_toInt_lt}$ equates that internal order with ordinary $<$ on $\mathrm{toInt}$. Separately, $\mathrm{add_toInt}$ states that addition commutes with $\mathrm{toInt}$: $(\mathrm{add},a,b).\mathrm{toInt} = a.\mathrm{toInt}+b.\mathrm{toInt}$.
This module develops the ordered arithmetic surface for those signed orbits, feeding the integer-order certificate that closes the layer.
proof idea
Rewrite both occurrences of signed-orbit $<$ via $\mathrm{lt_iff_toInt_lt}$, so the goal becomes an ordinary integer comparison of $\mathrm{toInt}$ values. Rewrite both additions with $\mathrm{add_toInt}$, obtaining $a.\mathrm{toInt}+c.\mathrm{toInt} < b.\mathrm{toInt}+c.\mathrm{toInt}$ iff $a.\mathrm{toInt} < b.\mathrm{toInt}$. Discharge the integer cancellation identity with $\mathrm{omega}$.
why it matters
Right-invariance of $<$ is the bidirectional form of translation monotonicity for the signed-orbit ordered group. Downstream, $\mathrm{add_lt_add_right}$ is the one-direction corollary (apply $\mathrm{mpr}$), and $\mathrm{cmp_add_right}$ lifts the same fact to the three-way comparison function. Both feed $\mathrm{integer_order_certificate}$, whose doc-comment states that "the internal signed-orbit order surface is closed."
In the Recognition stack this sits in the Primitive Recognition Calculus foundation: integers are reconstructed from distinction orbits before rationals and Cauchy reals. Closing translation invariance is a standard ordered-group axiom needed before mass-ladder and forcing-chain material can treat integer ranks as ordered without ad hoc side conditions. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.