Apex of a cyclically ordered group

Question

Does it make sense to introduce the new definition?

Definition 2.1. An element $\pi$ of a cyclically ordered group is an apex of the group iff $\pi = - \pi \ne 0$.

Considering an element $x$ of a cyclically ordered group is positive (negative) iff $[0, x, -x]$
($[0, -x, x]$) (Positive and negative elements of a cyclically ordered group),
an apex is not positive and not negative.

It looks like an apex has some interesting properties
(I am using the Cycle notation for cyclic orders wherever it is convenient):

Lemma 2.1 (well-known). An apex of a cyclically ordered group is unique.

Proof.

• Assuming there are two apexes $\pi$, $\pi'$, and $[0, \pi, \pi']$;
• Compatibility with $\pi$: $[\pi, 0, \pi + \pi']$;
• Compatibility with $\pi'$: $[\pi', \pi + \pi', 0]$;
• 4-Cycle: $[\pi, 0, \pi + \pi'] \land [\pi', \pi + \pi', 0] \iff [0, \pi', \pi + \pi', \pi]$;
• $[0, \pi', \pi + \pi', \pi] \implies [0, \pi', \pi]$, contradiction.

Corollary 2.1. An element of a cyclically ordered group is either $0$, positive, negative, or the apex.

Lemma 2.2. If $\pi$ is the apex of a cyclically ordered group, then an element $x$ is positive (negative) $\iff [0, x, \pi]$ ($[0, \pi, x]$).

Proof:

1. $[0, x, \pi] \implies [0, x, -x]$:
   • Negation: $[0, x, \pi] \iff [0, -\pi, -x] \iff [0, \pi, -x]$;
   • Transitivity: $[0, x, \pi] \land [0, \pi, -x] \implies [0, x, -x]$;
2. $[0, \pi, x] \implies [0, -x, x]$:
   • Negation: $[0, \pi, x] \iff [0, -x, -\pi] \iff [0, -x, \pi]$;
   • Applying 1: $[0, -x, \pi] \implies [0, -x, x]$;
3. $[0, x, -x] \implies [0, x, \pi]$:
   • Assuming $[0, \pi, x]$ ($x \ne 0$, $x \ne -x$);
   • Applying 2: $[0, \pi, x] \implies [0, -x, x]$, contradiction;
4. $[0, -x, x] \implies [0, \pi, x]$:
   • Assuming $[0, x, \pi]$ ($x \ne 0$, $x \ne -x$);
   • Applying 1: $[0, x, \pi] \implies [0, x, -x]$, contradiction.

Lemma 2.3. If $\pi$ is the apex of a cyclically ordered group, then an element $x$ is positive (negative) $\iff [\pi, -x, x]$ ($[\pi, x, -x]$).

Proof:

1. $[0, x, -x] \implies [\pi, -x, x]$:
   • Lemma 2.2: $[0, x, -x] \iff [0, x, \pi]$;
   • Negation: $[0, x, \pi] \iff [0, -\pi, -x] \iff [0, \pi, -x]$;
   • 4-Cycle: $[0, x, \pi] \land [0, \pi, -x] \iff [0, x, \pi, -x]$;
   • $[0, x, \pi, -x] \implies [\pi, -x, x]$;
2. $[0, -x, x] \implies [\pi, x, -x]$:
   • Applying 1: $[0, -x, x] \implies [\pi, x, -x]$;
3. $[\pi, -x, x] \implies [0, x, -x]$:
   • Assuming $[0, -x, x]$ ($x \ne -x$);
   • Applying 2: $[0, -x, x] \implies [\pi, x, -x]$, contradiction;
4. $[\pi, x, -x] \implies [0, -x, x]$:
   • Assuming $[0, x, -x]$ ($x \ne -x$);
   • Applying 1: $[0, x, -x] \implies [\pi, -x, x]$, contradiction.

Lemma 2.4. If $\pi$ is the apex of a cyclically ordered group, then $(x + \pi)$ is negative (positive) for any positive (negative) $x$.

Proof:

• Lemma 2.2: $x$ is positive $\iff [0, x, \pi]$;
• Cyclicity: $[0, x, \pi] \iff [\pi, 0, x]$;
• Compatibility with $\pi$: $[\pi, 0, x] \implies [0, \pi, x + \pi]$;
• Lemma 2.2: $[0, \pi, x + \pi] \iff (x + \pi)$ is negative.

Could somebody verify the statements, please?