Comment: I greatly shortened and simplified the question. As a drawback, some comments/answers might not make any sense anymore.
Assume we are using this set of axioms $A$ for plane euclidean geometry and some sensible definition of the length $\overline{ab}$ between two points $a$ and $b$. Then we can define the set $R$ to be a regular $n$-gon iff
- $R = \{x_j \mid j \in \mathbb{Z}_n \}$ (has $n$ elements)
- $\forall k \in \mathbb{Z}_n : ~\overline{x_{k-1}x_{k}} = \overline{x_{k}x_{k+1}}$ (is equilateral)
- $\forall k \in \mathbb{Z}_n: \angle ~x_{k-1}x_{k}x_{k+1} = \angle~ x_{k}x_{k+1}x_{k+2} $ (is equiangular)
Now imagine someone simply presented you the following construction of a $17$-gon, with an instruction of what he did. The construction yields $17$ points of interest you collect in a set $R$.
Can you prove (or is there a known proof) by only using the Axioms of $A$, that $R$ is a regular $17$-gon?
Comment: The linked construction is one by Herbert William Richmond which I found here, but my question would be the same for any other known construction which does the same job. The origins of the construction are of algebraic nature. Independantly of the origin, I want to know if the answer to my question is positiv, negative or not known.