add_lt_add_right

A signed orbit is a pair of distinction naturals (pos, neg), read as the difference pos − neg. Its internal strict order is defined as the weak order together with a nonzero (unbalanced) difference: $a < b$ means $a \le b$ and the two orbits are not balanced.

This module builds the order surface on those signed orbits inside Primitive Recognition Calculus, reconstructing integer comparison from logic-level arithmetic rather than importing classical $\mathbb{Z}$. The key upstream fact is the biconditional right-translation lemma: $a+c < b+c$ if and only if $a < b$. That lemma reduces both sides through the toInt embedding and finishes by omega on ordinary integers.

One-line wrapper. It applies the reverse direction of the biconditional right-translation lemma (lt_add_right_iff), feeding the hypothesis $a < b$ to obtain $a+c < b+c$. No new arithmetic is done here; the heavy lifting (rewrite through toInt, then omega) already lives in that iff.

Contributes one of the ordered-monoid laws collected by the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. Downstream it is also invoked in the electron-mass necessity lemma that pins gap 1332 between 13.953 and 13.954, where ordered arithmetic on the phi-ladder supports the mass-gap bounds. In the broader framework it sits in the PRC foundation that rebuilds integers before reals and constants, supplying the arithmetic substrate beneath the forcing chain rather than a single T-step.