Name for this algebraic structure?

Question

I've found myself looking at a structure $\mathbb{M}$ whose important properties are:

1. $\mathbb{M}$ is a discretely ordered additive monoid.
2. $\mathbb{M}$ has a least element, and this least element is the additive identity $0\in\mathbb{M}$.
3. All elements $m\in\mathbb{M}$ have unique additive decompositions once we choose some $n<m$ in $\mathbb{M}$ as one additive factor of $m$. That is, for all $n\in\mathbb{M}$ such that $n<m$, there exists exactly one $l\in\mathbb{M}$ such that $n+l=m$.

Does this structure have a name\has it been studied at all? A simple example is the natural numbers $\mathbb{N}$ under standard addition and ordering, another example is the non-negative part of the ordered Grothendieck group $\mathfrak{G}^+(\omega^\alpha)$ of a $\gamma$-number $\omega^\alpha$ under natural addition and standard ordinal ordering for $\alpha\in O_n$ fixed, or a proper-class sized example is $\mathfrak{G}^+(O_n).$

Answer 1

As Emil Jeřábek correctly suggests in the comments above, $\mathbb{M}$ is exactly the non-negative part of a discretely ordered group -- I humbly offer a proof to close the thread. The proof that the non-negative part of a discretely ordered group satisfies the above requirements is trivial.

For the opposite direction, we prove that $\mathbb{M}$ uniquely determines (up to isomorphism) a discretely ordered group whose set of non-negative elements is isomorphic to $\mathbb{M}$ as a discretely ordered monoid. Let $+$ and $\leq$ denote the addition and ordering in $\mathbb{M}$, and consider $\mathbb{M}\times\mathbb{M}$ with the binary operation $+_{_\mathbb{M}}:(\mathbb{M}\times\mathbb{M})\times(\mathbb{M}\times\mathbb{M})\rightarrow\mathbb{M}\times\mathbb{M}$ and the unary operation $-_{_\mathbb{M}}:\mathbb{M}\times\mathbb{M}\rightarrow\mathbb{M}\times\mathbb{M}$ given by: $$(m_0,m_1)+_{_\mathbb{M}}(m_2,m_3)=(m_0+m_2,m_1+m_3),$$ $$-_{_\mathbb{M}}(m_0,m_1)=(m_1,m_0),$$ and additive identity $0_{_\mathbb{M}}=(0,0)$, together with the ordering $\leq_{_\mathbb{M}}\subseteq\mathbb{M}^4$ given by: $$(m_0,m_1)\leq_{_\mathbb{M}}(m_2,m_3)\iff m_0+m_3\leq m_1+m_2.$$ We then mod out by the congruence relation $\equiv\subseteq\mathbb{M}^4$ defined by $$(m_0,m_1)\equiv(m_2,m_3)\iff m_0+m_3=m_1+m_2$$ to handle the fact that we want to forget the multiple coordinate representations of a given group element. We now have that $\mathbb{G}_{_\mathbb{M}}=\big\langle(\mathbb{M}\times\mathbb{M})\setminus\equiv,+_{_\mathbb{M}},-_{_\mathbb{M}},\leq_{_\mathbb{M}},0_{_\mathbb{M}}\big\rangle$ is a discretely ordered group, and $$\mathbb{G}_{_\mathbb{M}}^+=\{(m,0):m\in\mathbb{M}\}$$ is isomorphic to $\mathbb{M}$ as a discretely ordered monoid under the first factor projection $\pi_0:\mathbb{M}\times\mathbb{M}\rightarrow\mathbb{M}$. We could easily treat the first factor as being negative instead of positive by tweaking the definition of $\leq_{_\mathbb{M}}$, however the construction would still obviously be isomorphic to $\mathbb{G}_{_\mathbb{M}}$.