1 Basic Constructions with Ruler and Compass

1.1 Defining lines, circles and the set of constructable points

First we need to define what construction using a ruler and compass means. We will use $\mathbb {C}$ as plane of drawing and $\mathcal{M} \subset \mathbb {C}$ as the set of constructed points.

Definition 1.1 Line

✓

A line $L := (x,y)$ is defined by two points $x,y\in \mathbb {C}$ with $x\ne y$ and a set

\[ l:=\{ \lambda x+(1-\lambda )y\mid \lambda \in \mathbb {R}\} . \]

We say two lines are equal if their generated set is equal.

Remark 1.2

To express lines in the most general way, they are stated without the requirement that $x\ne y$, which allows for trivial lines. The condition is only included in the lemmas that require it.

Definition 1.3 Circle

✓

A circle $C := (c,r)$ is defined by a center $c$ with $c\in \mathbb {C}$, a radius $r\in \mathbb {R}_{\ge 0}$ and the set:

\[ c:=\{ z\in \mathbb {C} \mid \| z-c\| =r\} . \]

We say two circles are equal if their underlying sets are equal.

Lemma 1.4

✓

If we have two circles $C_1 = (c_1,r_1)$, $C_2 = (c_2,r_2)$ and we have $c_1 \ne c_2$ or $r_1 \ne r_2 $ then the circles aren’t equal.

Definition 1.5 Set of lines

✓

$\mathcal{L(M)}$ is the set of all real straight lines $l$, with $| l\cap \mathcal{M} |\ge 2$. As a set this is:

\begin{equation*} \mathcal{L(M)} := \{ l \mid l = \{ x,y\} \text{ with }x,y \in \mathcal{M} \land x \neq y\} . \end{equation*}

Definition 1.6 Set of circles

✓

$\mathcal{C(M)}$ is the set of all circles in $\mathbb {C}$, with center in $\mathcal{M}$ and radius of $\mathcal{C}$ which is the distance of two points in $\mathcal{M}$. As an equation this is:

\[ \mathcal{C(M)}:=\{ c\mid c = \langle c, \text{ dist }r_1 r_2 \rangle \text{ with } c,r_1,r_2\in M\} . \]

Definition 1.7 Rules to construct a point

✓

We define operations that can be used to construct new points.

$(ILL)$ is the intersection of two different lines in $\mathcal{L(M)}$.
$(ILC)$ is the intersection of a line in $\mathcal{L(M)}$ and a circle in $\mathcal{C(M)}$.
$(ICC)$ is the intersection of two different circles in $\mathcal{C(M)}$.

$ICL(\mathcal{M})$ is the union of all points that can be constructed using the operations $(ILL)$, $(ILC)$ and $(ICC)$ and $\mathcal{M}$.

Definition 1.8 Set of constructable points

✓

We inductively define the chain

\begin{equation*} \mathcal{M}_0 \subseteq \mathcal{M}_1 \subseteq \mathcal{M}_2 \subseteq \dots \end{equation*}

with $\mathcal{M}_0 = \mathcal{M}$ and $\mathcal{M}_{n+1} = ICL(\mathcal{M}_n)$
and call $\mathcal{M}_{\infty } = \bigcup _{n \in \mathbb {N}} \mathcal{M}_n$ the set of all constructable points.

Remark 1.9

The set of lines, circles and their intersection $icc$, $ilc$, $icc$ are monoton, i.e. for $N\subseteq M$ is $\mathcal{L(N)} \subseteq \mathcal{L(M)}$,….

1.2 Properties of Lines

In light of the fact that a considerable proportion of the forthcoming project will entail the manipulation of lines and the absence of an existing formalisation from MathLib, it is imperative to illustrate the fundamental properties that will be utilised throughout the remainder of the project.

Lemma 1.10

✓

The set of points of a line $l$ is not defined by one position vector, i.e. for every $\alpha \in l$ $\{ \lambda x+(1-\lambda )y\mid \lambda \in \mathbb {R}\} = \{ \lambda x+\lambda y+\alpha \mid \lambda \in \mathbb {R}\} $.

Proof ▶

Two sets are equal if they have the same elements. Since $\alpha $ is in $l$, there exists a $\lambda _{\alpha }$ such that $\alpha = \lambda _{\alpha } x+(1-\lambda _{\alpha })y$.

"$\Rightarrow :$" Let $z=\lambda _0 x + (1-\lambda _0)y$ (i.e. $z\in \{ \lambda x+(1-\lambda )y\mid \lambda \in \mathbb {R}\} $), we have to show that $z\in \{ \lambda x+\lambda y+\alpha \mid \lambda \in \mathbb {R}\} $, which is equivalent to the existence of $\lambda $ such that $z = \lambda x+\lambda y+\alpha $. If we use $\lambda = \lambda _0 - \lambda _{\alpha } $ we get

\[ (\lambda _0 - \lambda _{\alpha }) x + ((\lambda _0 - \lambda _{\alpha }))y + \alpha \overset {\alpha = \lambda _{\alpha } x+(1-\lambda _{\alpha })y}{=} \lambda _0 x - \lambda _0 y + y = z \]

$\Leftarrow :$ Let $z$ be in $\{ \lambda x+(\lambda )y+\alpha \mid \lambda \in \mathbb {R}\} $, if we use $\lambda = \lambda _0 + \lambda _{\alpha } $ we get

\[ (\lambda _0 + \lambda _{\alpha }) x + (1 -(\lambda _0 + \lambda _{\alpha }))y = \lambda _0 x - \lambda _0 y + \lambda _{\alpha } x - \lambda _{\alpha } y + y \overset {\alpha = \lambda _{\alpha } x+(1-\lambda _{\alpha })y}{=} \lambda _0 (x - y) + \alpha = z \]

Definition 1.11 parallel

✓

Two lines $l_1$ and $l_2$ are parallel if they have the same slope, i.e. $\exists r\in \mathbb {C}: l_1 = \{ x + r \mid x\in l_2\} $.

Lemma 1.12 Parallel defined by basis

✓

If the basis of two lines is moved by the same amount, i.e $l_1.z_1 - l_2.z_1 = l_1.z_2- l_2.z_2$, then they are parallel.

Proof ▶

We have to lines $l_1, l_2$ with basis $z_1, z_2$ and $l_1.z_1 - l_2.z_1 = l_1.z_2- l_2.z_2$. To show that they are parallel we have to show that

\[ \exists r: l_1 = \{ z + r \mid z\in l_2\} . \]

To make it easier to read we define $a := l_1.z_1$, $b:= l_1.z_2$, $x:= l_2.z_1$ and $y:= l_2.z_2$.
Upon unravelling the definition, it becomes evident that we need to show that $\exists t: t \cdot a +(1-t)\cdot b=z \iff \exists s :s \cdot x+(1-s)y+(a-x)=z$.
$\Rightarrow :$ Claim $s = \frac{t(a-b)}{x-y}$ is a solution.

Proof ▶

\begin{align*} & & z & = s \cdot x+(1-s)y+(a-x)& & | z= t\cdot a+(1-t)\cdot b\\ & \Leftrightarrow & t\cdot a+(1-t)\cdot b & = s \cdot x+(1-s)y+(a-x)\\ & \Leftrightarrow & t\cdot a-t\cdot b +b & = s \cdot x-s\cdot y + y+(a-x)& & | -y\\ & \Leftrightarrow & t\cdot a-t\cdot b + b-y & = s \cdot x-s\cdot y+(a-x)-y& & | a-x =b-y\\ & \Leftrightarrow & t\cdot a-t\cdot b & = s \cdot x+s\cdot y\\ & \Leftrightarrow & t(a-b) & = s(x-y)& & |s:= \frac{t(a-b)}{x-y}\\ & \Leftrightarrow & t(a-b) & = \frac{t(a-b)}{x-y}(x-y)\\ & \Leftrightarrow & t(a-b) & = t(a-b) \end{align*}

"$\Leftarrow :$" Claim $t = \frac{s(x-y)}{a-b}$ is a solution.

Proof ▶

\begin{align*} & & t\cdot a+(1-t)b & = z& & | z:= s \cdot x+(1-s)y+(a-x)\\ & \Leftrightarrow & t\cdot a-t\cdot b+b & = s \cdot x-s\cdot y+y+(a-x)& & |-y;a-x =b-y\\ & \Leftrightarrow & t(a-b) & = s(x-y)& & |t:= \frac{s(x-y)}{a-b}\\ & \Leftrightarrow & \frac{s(x-y)}{a-b}(a-b) & = s(x-y) \end{align*}

Definition 1.13

✓

The direction vector of a line $l$ is the vector $l.z_1 - l.z_2$.

Definition 1.14

✓

Two lines $l_1$ and $l_2$ are parallel’ if there exists a $k$ such that $l_1.z_1 - l_1.z_2 = k \cdot (l_2.z_1 - l_2.z_2)$.

Lemma 1.15 Parallel imp parallel’

✓

If two lines $l_1$ and $l_2$ are parallel’ they are parallel.

Remark 1.16

The other direction holds as well, but is not needed.

Proof ▶

Let $l_1$ and $l_2$ be two lines with $l_1.z_1 - l_1.z_2 = k \cdot (l_2.z_1 - l_2.z_2)$. We have to show that $l_1 = \{ z + r \mid z\in l_2\} $, i.e. $\exists r: l_1 = \{ z + r \mid z\in l_2\} $.
First we remark that $k\ne 0$ since $l_1.z_1\ne l_1.z_2$. We define $r:= y_1 - y_2$ and show that $l_1 = \{ z + r \mid z\in l_2\} $. For $z$ to be in $l_1$ is equivalent to $z = \lambda x_1 + (1-\lambda )y_1$ for some $\lambda _0$. For $z$ to be in $\{ x + y_1-y_2 \mid z\in l_2\} $ is wquivalent to the existence of $\lambda $ such that

\[ z = \lambda x_2 + (1-\lambda )y_2 + y_1 - y_2 = \lambda (x_2 - y_2) + y_1 \overset {\lambda = \lambda _0 * k}{=} \lambda _0 k (x_2-x_2)-y_1\overset {x_1-y_1=k(x_2-y_2)}{=}\lambda _0(x_1-y_1)+y_1. \]

Lemma 1.17 Parallel imp equal

✓

If two lines $l_1$ and $l_2$ are parallel’ and intersect, then they are equal.

Proof ▶

Let $z\in l_1 \cap l_2$. Then we use lemma 1.10 to get $l_1 = l_2 \Leftrightarrow \{ \lambda (x_1-y_1)\mid \lambda \in \mathbb {R}\} = \{ \lambda (x_2- y_2)+z\mid \lambda \in \mathbb {R}\} $. Since for every $\lambda $ we have $\lambda (x_1-y_2) + x = \lambda \cdot k(x_2- y_2)+z$ we get $l_1 = l_2$.

1.3 The Set $M_{\infty }$

In order to work with the set of constructable points, it is necessary to have some basic lemmas at one’s disposal. While these may appear to be trivial on paper, they are invaluable when undertaking a formalisation.

Lemma 1.18 $\mathcal{M}\subseteq ICL(\mathcal{M})$

✓

Every set $M$ is included in the constructable points of $M$, i.e.

\[ M \subseteq ICL(M) \]

Proof ▶

Follows from the definition of $ICL(M)$.

Lemma 1.19 $\mathcal{M}_i$ Monoton

✓

The set $\mathcal{M}_i$ is monoton, i.e.

\[ \mathcal{M}_i \subseteq \mathcal{M}_{i+1}. \]

This can be generalised to

\[ \forall m :\forall n\le m : \mathcal{M}_n \subseteq \mathcal{M}_m. \]

Proof ▶

Follows from the definition of $\mathcal{M}_i$.

Lemma 1.20 $\mathcal{M}$ in $\mathcal{M}_i$

✓

The set $\mathcal{M}$ is in $\mathcal{M}_i$, i.e.

\[ \mathcal{M} \subseteq \mathcal{M}_i. \]

Proof ▶

Combining the fact that $\mathcal{M}_0 = \mathcal{M}$ 1.8 and the monotonity of $\mathcal{M}_i$ 1.19 we get the result.

Lemma 1.21 $\mathcal{M}_i$ in $\mathcal{M}_{\infty }$

✓

The set $\mathcal{M}_i$ is in $\mathcal{M}_{\infty }$, i.e.

\[ \mathcal{M}_i \subseteq \mathcal{M}_{\infty }. \]

Proof ▶

Follows from the definition of $\mathcal{M}_{\infty }$.

Lemma 1.22 $\mathcal{M}$ in $\mathcal{M}_{\infty }$

✓

The set $\mathcal{M}$ is in $\mathcal{M}_{\infty }$.

Proof ▶

Combining $\mathcal{M} \subseteq \mathcal{M}_i$ 1.20 and $\mathcal{M}_i \subseteq \mathcal{M}_{\infty }$ 1.21 we get the result.

Lemma 1.23 $\mathcal{M}_{\infty }$ iff $\mathcal{M}_i$

✓

A point $z$ is in $\mathcal{M}_{\infty }$ if and only if $z$ is in $\mathcal{M}_i$ for some $i$.

Proof ▶

Follows from the definition of $\mathcal{M}_{\infty }$.

Corollary 1.24 $L(\mathcal{M_{\infty }})$ iff $L(\mathcal{M_i})$

✓

A line $l$ is in $\mathcal{L(M_{\infty })}$ if and only if $l$ is in $\mathcal{L(M_i)}$ for some $i$.

Proof ▶

Follows from 1.23 and the fact that every line in $\mathcal{L(M_{\infty })}$ is defined by two points in $\mathcal{M_{\infty }}$.

Corollary 1.25 $C(\mathcal{M_{\infty }})$ iff $C(\mathcal{M_i})$

✓

A circle $c$ is in $\mathcal{C(M_{\infty })}$ if and only if $c$ is in $\mathcal{C(M_i)}$ for some $i$.

Proof ▶

Follows from 1.23 and the fact that every circle in $\mathcal{C(M_{\infty })}$ is defined by three points in $\mathcal{M_{\infty }}$.

To construct new points in the next section1.4 we still need to show that every intersection of lines and circles is in $\mathcal{M}_{\infty }$.

Lemma 1.26 Intersection of lines in $\mathcal{M}_{\infty }$

✓

For two lines $l_1, l_2 \in \mathcal{L(M_{\infty })}$ is $l_1 \cap l_2 \in \mathcal{M}_{\infty }$.

Proof ▶

By corollary 1.24 and the monotonity of $\mathcal{M}_i$ 1.19 we get that there exists an $n$ such that $l_1, l_2 \in \mathcal{L(M_n)}$. Therfore $l_1 \cap l_2 \in \mathcal{M}_{n+1} \stackrel{\ref{lem:M_i_in_M_inf}}{\subseteq } \mathcal{M}_{\infty }$.

Remark 1.27

To formalise the lemmas 1.23, 1.24 and 1.25 one should use filters in Lean.

Lemma 1.28 Intersection of line and circle in $\mathcal{M}_{\infty }$

✓

For a line $l \in \mathcal{L(M_{\infty })}$ and a circle $c \in \mathcal{C(M_{\infty })}$ is $l \cap c \in \mathcal{M}_{\infty }$.

Proof ▶

By corollary 1.24 and 1.25 we get that there exists an $n$ such that $l \in \mathcal{L(M_n)}$ and $c \in \mathcal{C(M_n)}$. Therfore $l \cap c \in \mathcal{M}_{n+1} \stackrel{\text{\ref{lem:M_i_in_M_inf}}}{\subseteq } \mathcal{M}_{\infty }$.

Lemma 1.29 Intersection of circles in $\mathcal{M}_{\infty }$

✓

For two circles $c_1, c_2 \in \mathcal{C(M_{\infty })}$ it follows that $c_1 \cap c_2 \in \mathcal{M}_{\infty }$.

Proof ▶

By corollary 1.25 we get that there exists an $n$ such that $c_1, c_2 \in \mathcal{C(M_n)}$. Therfore $c_1 \cap c_2 \in \mathcal{M}_{n+1} \stackrel{\ref{lem:M_i_in_M_inf}}{\subseteq } \mathcal{M}_{\infty }$.

1.4 Basic constructions

It is now possible to construct fundamental points in $M_{\infty }$ using a compass and ruler, which can subsequently be employed to create a field structure and special properties on $M_{\infty }$. Consequently, the following constructions are based on the assumption that $M\subseteq \mathbb {C}$ with $0,1 \in M$.

Lemma 1.30 Negative complex numbers

✓

For $z \in M_{\infty }$ it follows that $-z \in M_{\infty }$.

This construction is taken from [ 6 ] .
To get the point $-z$ we can use the second intersection of the line through $0$ and $z$ with the circle with center $0$ and radius $\| z\| $.1.1

Proof ▶

Define $l = \{ 0,z\} $ and $c = \{ 0,\text{ dist }(0, z)\} $.
By assumption $0, z \in M_{\infty }$, so $l \in \mathcal{L(M_{\infty })}$ and $c \in \mathcal{C(M_{\infty })}$.
Claim 1: $-z$ is in $l$.

Proof ▶

By the definition of $l:=\{ \lambda 0+(1-\lambda )z\mid \lambda \in \mathbb {R}\} $ with $\lambda = 2$ we get $2 \cdot 0 + (1-2)z = -z$.

Claim 2: $-z$ is in $c$.

Proof ▶

Unfolding the definition of $c:=\{ x\in \mathbb {C} \mid \| x-0\| =\text{ dist }(0\ z)\} $. By the definition of the distance we get $\| 0-(-z)\| = \text{ dist }(0\ z)$.

By claim 1 and 2 we get that $-z \in l \cap c$. Futhermore $-z $ is in $M_{\infty }$, after lemma 1.28.

\begin{tikzpicture}
\draw[->] (-1,0) -- (3,0) node[right] {$\Re$};
\draw[->] (0,-1) -- (0,3) node[above] {$\Im$};
\draw (0,0) -- (2,2) node[right] {$z$};
\draw (0,0) -- (-2,-2) node[left] {$-z$};
\draw (0,0) circle (2.8);
\end{tikzpicture} — Figure 1.1 Construction of $-z$

Lemma 1.31 Addition of complex numbers

✓

For $z_1, z_2 \in M_{\infty }$ it follows that $z_1 + z_2 \in M_{\infty }$.

This construction is taken from [ 6 ] .
One can construct the point $z_1 + z_2$ by drawing a circle with center $z_1$ and radius $\| z_2\| $ and a circle with center $z_2$ and radius $\| z_1\| $ and taking the intersection of the two circles.1.2

Proof ▶

First we have the case that $z_1 \ne z_2$.
Define $c_1 = \{ z_1,\text{ dist }(0\ z_2)\} $ and $c_2 = \{ z_2,\text{ dist }(0\ z_1)\} $.
By assumption $0, z_1, z_2 \in M_{\infty }$, so $c_1, c_2 \in \mathcal{C(M_{\infty })}$ and since $z_1 \ne z_2$ we get $c_1 \ne c_2$.
Claim 1: $z_1 + z_2$ is in $c_1$.

Proof ▶

By the definition of $c_1:=\{ x\in \mathbb {C} \mid \| x-z_1\| =\text{ dist }(0\ z_2)\} $ and of the distance we get $\| z_1-(z_1+z_2)\| = \text{ dist }(0\ z_2)$.

Claim 2: $z_1 + z_2$ is in $c_2$.

Proof ▶

Using that $c_2$ ia definded as $c_2:=\{ x\in \mathbb {C} \mid \| x-z_2\| =\text{ dist }(0\ z_1)\} $ and the definition of the distance we get $\| z_2-(z_1+z_2)\| = \text{ dist }(0\ z_1)$.

By claim 1 and 2 we get that $z_1 + z_2 \in c_1 \cap c_2$. Futhermore $z_1 + z_2 $ is in $M_{\infty }$, after lemma 1.29.

If we have $z_1 = z_2$ we can define $c_1 = \{ z_1,\text{ dist }(0\ z_1)\} $ and $l = \{ 0,z_1\} $ and get that $z_1 + z_2 = z_1 + z_1 \in c_1 \cap l$.

\begin{tikzpicture}
\draw[->] (-1,0) -- (3,0) node[right] {$\Re$};
\draw[->] (0,-1) -- (0,3) node[above] {$\Im$};
\draw (0,0) -- (1,2) node[above] {$z_1$};
\draw (0,0) -- (2,1) node[right] {$z_2$};
\draw (1,2) circle (2.2360679775);
\draw (2,1) circle (2.2360679775);
\draw[dashed,->] (1,2) -- (3,3);
\draw[dashed,->] (2,1) -- (3,3);
\draw (0,0) -- (3,3) node[right] {$z_1 + z_2$};
\end{tikzpicture} — Figure 1.2 Construction of $z_1 + z_2$

Corollary 1.32 Subtraction of complex numbers

✓

For $z_1, z_2 \in M_{\infty }$ it follows that $z_1 - z_2 \in M_{\infty }$.

Proof ▶

By lemma 1.30 and 1.31 we get $z_1 - z_2 = z_1 + (-z_2) \in M_{\infty }$.

Corollary 1.33 Construction of parallel lines

✓

For $l \in \mathcal{L(M_{\infty })}$ and $z \in M_{\infty }$ it follows that $\exists l' \in \mathcal{L(M_{\infty })}$ with $z\in l'$ and $l\| l'$.

Proof ▶

Let $l$ be a line through $x,y \in \mathcal{M_{\infty }}$ and $z \in \mathcal{M_{\infty }}$.
After corollary 1.32 we get $z - x \in \mathcal{M_{\infty }}$ and therfore $z-x + y \in \mathcal{M_{\infty }}$1.31.
Define $l' = \{ z, z-x+y\} $, then $l' \in \mathcal{L(M_{\infty })}$ and since a line is defined by two points and we moved them the same distance ($z-x$) $l'$ is parallel to $l$.1.12

Lemma 1.34 Complex conjugation

✓

For $z \in M_{\infty }$ it follows that $\overline{z} \in M_{\infty }$.

This construction is taken from [ 6 ] .
Draw two circles one with center $0$ and radius $\| z\| $ and a second with center $1$ and radius $\| z-1\| $ and take the intersection of the two circles.1.3

Proof ▶

Define $c_1 = \{ 0,\text{ dist }(0, z)\} $ and $c_2 = \{ 1,\text{ dist }(1, z)\} $.
By assumption $0, 1, z \in M_{\infty }$, so $c_1, c_2 \in \mathcal{C(M_{\infty })}$.
Claim 1: $\overline{z}$ is in $c_1$.

Proof ▶

The definition of $c_1$ can be written in the following form:

\[ \{ x\in \mathbb {C} \mid \| x-0\| = \text{ dist }(0\ z)\} . \]

Using the definition of the distance, we obtain the following result:

\[ \| 0 - \overline{z}\| = \| \overline{z}\| = \| z\| = \text{ dist }(0\ z). \]

Claim 2: $\overline{z}$ is in $c_2$.

Proof ▶

From the definition of $c_2:=\{ x\in \mathbb {C} \mid \| x-1\| =\text{ dist }(1\ z)\} $ and the definition of the distance, we can derive the following:

\[ \| 1-\overline{z}\| = \| \overline{z}-1\| = \sqrt{(\Re (\overline{z})-1)^2 + \Im (\overline{z})^2} = \sqrt{(\Re (z)-1)^2 + \Im (z)^2} = \| z-1\| =\text{ dist }(1\ z). \]

By claim 1 and 2 we get that $\overline{z} \in c_1 \cap c_2$. Futhermore $\overline{z} $ is in $M_{\infty }$, after lemma 1.29.

\begin{tikzpicture}
\draw[->] (-3,0) -- (3,0) node[right] {$\Re$};
\draw[->] (0,-2.5) -- (0,2.5) node[above] {$\Im$};
\draw[dashed] (0,0) -- (2,1) node[right] {$z$};
\draw[dashed] (0,0) -- (2,-1) node[right] {$\overline{z}$};
\draw (0,0) circle (2.2360679775);
\draw (1,0) circle (1.4142135624);
\end{tikzpicture} — Figure 1.3 Construction of $\overline{z}$

Lemma 1.35 Construction $\imath r\in \mathcal{M}_{\infty }$

✓

For $r \in \mathbb {R}\cap M_{\infty }$ it follows that $\imath\cdot r \in M_{\infty }$.

The first step is to construct the imaginary axis, which is achieved by drawing a line, designated as $l$, that passes through two circles with centres at $-1$ and $1$ and radii of $2$. The second step is to construct the point, designated as $\imath r$, which is achieved by drawing a circle with a centre at $0$ and a radius of $r$, and taking the intersection with the imaginary axis. (Fig1.4)

Proof ▶

First we construct the imaginary axis. Define $c_1 = \{ -1,2\} $ and $c_2 = \{ 1,2\} $.
Claim 1: $c_1, c_2 \in \mathcal{C(M_{\infty })}$

Proof ▶

By assumption and lemma 1.30 we get $-1, 1 \in M_{\infty }$. Using $\text{ dist }(-1 1)=2$ we get $c_1, c_2 \in \mathcal{C(M_{\infty })}$, by the definition of the circle.

Claim 2: $\imath\sqrt {3}$ and $-\imath\sqrt {3}$ are in $c_1 \cap c_2$.

Proof ▶

Unfolding the definition of $c_1:=\{ x\in \mathbb {C} \mid \| x+1\| =2\} $ and $c_2:=\{ x\in \mathbb {C} \mid \| x-1\| =2\} $. By the definition of the distance we get $\| -\imath\sqrt {3}+1\| = \sqrt{1 + 3} = 2$ and $\| \imath\sqrt {3}-1\| = \sqrt{1 + 3} = 2$.

Now we define $l = \{ \imath\sqrt {3}, -\imath\sqrt {3}\} $.
Claim 3: $l \in \mathcal{L(M_{\infty })}$

Proof ▶

By claim 2 and 1.29 we get $\imath\sqrt {3}, -\imath\sqrt {3} \in M_{\infty }$, so $l \in \mathcal{L(M_{\infty })}$.

To get $\imath r$ we define $c = \{ 0,|r|\} $.
Claim 4: $\imath r$ is in $c \cap l$.

Proof ▶

It is clear that $\imath r \in c$. Now using the definition of $l$ and $\lambda = \frac{r}{2\sqrt{3}+\frac{1}{2}}$ we get $(\frac{r}{2\sqrt{3}+\frac{r}{2}})\imath\sqrt {3} + (1-\frac{r}{2\sqrt{3}+\frac{r}{2}})(-\imath\sqrt {3}) = \imath r$.

Therfore $\imath r \in M_{\infty }$ after lemma 1.28.

\begin{tikzpicture}
\draw[->] (-3,0) -- (3,0) node[right] {$\Re$};
\draw[->] (0,-2.5) -- (0,2.5) node[above] {$\Im$};
\coordinate[label=-45:$1$] (one) at (1,0);
\coordinate[label=-135:$-1$] (mone) at (-1,0);
\fill[black] (one) circle (2pt);
\fill[black] (mone) circle (2pt);
\draw[dashed] (one) [carc=110:250:2];
\draw[dashed] (mone) [carc=70:-70:2];
\coordinate[label=45:$r$] (r) at (2,0);
\coordinate[label=135:$\imath r$] (ir) at (0,2);
\fill[black] (r) circle (2pt);
\fill[black] (ir) circle (2pt);
\draw (0,0) [carc=-10:100:2];
\end{tikzpicture} — Figure 1.4 Construction of $\imath r$

Corollary 1.36 Construction of

✓

$\imath\in M_{\infty }$.

Proof ▶

By lemma 1.35 with $r = 1$ and the definition of $\mathcal{M}$ we get $\imath\in M_{\infty }$.

Lemma 1.37 Construction of real part

✓

For $z \in M_{\infty }$ it follows that $z.re \in M_{\infty }$.

To get the point $z.re$ we draw a line through $z$ and $\overline{z}$. Then $z.re$ is the intersection with the real line, defined by $0$ and $1$.1.5

Proof ▶

Without loss of generality we can assume that $z \in \mathbb {C}\setminus \mathbb {R}$.
Define the lines $l = \{ z, \overline{z}\} $ and $l_{\Re } = \{ 1, 0\} $.
By using Lemma 1.34, they are in $\mathcal{L(M_{\infty })}$.
To show that $z.re \in l \cap l_{\Re }$ we use $t:= 1/2$ for $l$ and $t:= z.re$ for $l_{\Re }$.

\begin{tikzpicture}
\draw[->] (-0.5,0) -- (5,0) node[right] {$\Re$};
\draw[->] (0,-3) -- (0,3) node[above] {$\Im$};
\coordinate[label=135:$z$] (z) at (2,2);
\coordinate[label=-45:$z.re$] (zre) at (2,0);
\coordinate[label=135:$\overline{z}$] (oz) at (2,-2);
\coordinate[label=-135:$0$] (zero) at (0,0);
\coordinate[label=-90:$1$] (one) at (1,0);
\fill[black] (z) circle (2pt);
\fill[black] (zre) circle (2pt);
\fill[black] (oz) circle (2pt);
\fill[black] (one) circle (1pt);
\fill[black] (zero) circle (1pt);
\draw (z) -- (oz);
\end{tikzpicture} — Figure 1.5 Construction of $z.re$

Lemma 1.38 Construction of imaginary part

For $z \in M_{\infty }$ it follows that $z.im \in M_{\infty }$.

To get the point $z.im$ we draw a line through $z$ and $z-1$. Now we get $\imath\cdot z.im$ by taking the intersection with the imaginary line, defined by $0$ and . To get z.im draw a circle trough $\imath\cdot z.im$ and take the intersection with the real line.1.6

Proof ▶

Define the lines $l = \{ z, z-1\} $ and $l_{\Im } = \{ \imath, 0\} $.
Now it is analog to the proof of lemma 1.37, that $z.im \cdot \imath\in l \cap l_{\Im }$.

Now we can project $z.im \cdot $

 on the real axis by drawing a circle with center 0 and radius $\| z.im\| $ and taking the intersection with the real axis.

Proof ▶

\begin{tikzpicture}
\draw[->] (-1,0) -- (4,0) node[right] {$\Re$};
\draw[->] (0,-1) -- (0,4) node[above] {$\Im$};
\coordinate[label=90:$z$] (z) at (2,3);
\coordinate[label=-45:$z.im$] (zim) at (3,0);
\coordinate[label=90:$z-1$] (z1) at (1,3);
\coordinate[label=-135:$\imath\cdot z.im$] (izim) at (0,3);
\coordinate[label=-135:$0$] (zero) at (0,0);
\coordinate[label=180:$\imath$] (i) at (0,1);
\coordinate[label=-90:$1$] (one) at (1,0);
\fill[black] (z) circle (2pt);
\fill[black] (izim) circle (2pt);
\fill[black] (zim) circle (2pt);
\fill[black] (z1) circle (2pt);
\fill[black] (i) circle (1pt);
\fill[black] (zero) circle (1pt);
\fill[black] (one) circle (1pt);
\draw (-0.5,3) -- (3.5,3);
\draw (0,0) [carc=-30:120:3];
\end{tikzpicture} — Figure 1.6 Construction of $z.im$

Corollary 1.39 $z \in M_{\infty } \Rightarrow z.re, z.im \in M_{\infty }$

✓

For $z \in \mathbb {C}$. $z$ is in $M_{\infty }$ if and only if $z.re, z.im \in M_{\infty }$.

Proof ▶

"$\Rightarrow $:" If $z \in M_{\infty }$ then $z.re, z.im \in M_{\infty }$ after lemma 1.37 and 1.38.
"$\Leftarrow $:" If $z.re, z.im \in M_{\infty }$ then $z.re + \imath z.im \in M_{\infty }$ after lemma 1.31 and lemma 1.35.

Lemma 1.40 Multiplication of positve real numbers

✓

For $a, b \in M_{\infty }\cap \mathbb {R}$ it follows that $a \cdot b \in M_{\infty }$.

This construction is taken from [ 4 ] .
To get the point $a\cdot b$ we draw a line trough $a$ and  and a parallel line through b. The intersection of the second line with the real axis is $a\cdot b$.1.7

Proof ▶

Define the three lines $l = \{ a+\imath b - \imath, \imath b\} $ and $l_{\Re } = \{ 1,0\} $.
Claim 1: $l \in \mathcal{L(M_{\infty })}$

Proof ▶

By assumption $b \in M_{\infty }$ so after Lemma 1.35 $\imath b \in M_{\infty }$. Futhermore $l_2 \in \mathcal{L(M_{\infty })}$ after Claim 1 and Lemma 1.33.

Claim 2: $l_{\Re } \in \mathcal{L(M_{\infty })}$

Proof ▶

By assumption $0, 1 \in M_{\infty }$, so $l_{\Re } \in \mathcal{L(M_{\infty })}$.

To show that $a\cdot b \in M_{\infty }$ we need to show that $l \cap l_{\Re } \in M_{\infty }$1.26. That $ab \in l_{\Re } \cap l$ is clear after definition $t=ab$. For $ab \in l$ we use $t=b$ and get $t(a+\imath b - \imath) + (1-t)\imath b \stackrel{t:=b}{=}ba + \imath b^2 -\imath b + \imath b -\imath b^2 = a\cdot b$.

Remark 1.41

This construction uses parallel lines, but it is not needed for the proof of the lemma.

\begin{tikzpicture}
\draw[->] (-0.5,0) -- (5,0) node[right] {$\Re$};
\draw[->] (0,-0.5) -- (0,3) node[above] {$\Im$};
\coordinate[label=135:$\imath$] (i) at (0,1);
\coordinate[label=-90:$a$] (a) at (2,0);
\coordinate[label=135:$\imath b$] (ib) at (0,2);
\coordinate[label=-90:$ab$] (ab) at (4,0);
\fill[black] (i) circle (2pt);
\fill[black] (a) circle (2pt);
\fill[black] (ib) circle (2pt);
\fill[black] (ab) circle (2pt);
\draw (a) -- (i);
\draw (ib) -- (ab);
\end{tikzpicture} — Figure 1.7 Construction of $z_1 \cdot z_2$

Corollary 1.42 Multiplication of complex numbers

✓

For $z_1, z_2 \in M_{\infty }$ it follows that $z_1 \cdot z_2$ in $M_{\infty }$.

Proof ▶

Let $z_1 = a + \imath b$ and $z_2 = c + \imath d$. Then

\[ z_1 \cdot z_2 = (a + \imath b) \cdot (c + \imath d) = (a \cdot c - b \cdot d) + \imath(a \cdot d + b \cdot c). \]

By combining the Lemmas 1.40, 1.31, 1.32, 1.37 and 1.38 we get that $z_1 \cdot z_2 \in M_{\infty }$.

Lemma 1.43 Invers of a pos real number

✓

If $a \in M_{\infty }\cap \mathbb {R}$, then $a^{-1}$ is in $M_{\infty }$.

This can be constructed analog to the multiplication of positve real numbers. Using the fact that $a\cdot a^{-1} = 1$. Draw a line through $1$ and $\imath a$ and a parallel line through . The intersection of the second line with the real axis is a^-1. (Fig. 1.8)

Proof ▶

The proof is analogous to that of Lemma 1.40. It requires only two lines: $l = \{ 1 - \imath z + \imath, \imath\} $ and $l_{\Re } = \{ 1,0\} $.
With out loss of generality we can assume that $a \ne 0$.
The fact that they are in $\mathcal{L(M_{\infty })}$ follows analog to the proof of Lemma 1.40.
Thus we have just to show that $z^{-1} \in l$, i.e. $\exists t: t (1 - \imath a + \imath) + (1 - t) I = a^{-1}$

\[ t (1 - \imath a + \imath) + (1 - t) \imath\stackrel {t:=a^{-1}}{=} a^{-1} - a^{-1} \imath a + a^{-1}\imath+ \imath- a^{-1}\imath= a^{-1}. \]

The rest follows analog.

\begin{tikzpicture}
\draw[->] (-1,0) -- (2,0) node[right] {$\Re$};
\draw[->] (0,-1) -- (0,3) node[above] {$\Im$};
\coordinate[label=135:$\imath$] (i) at (0,1);
\coordinate[label=-90:$1$] (1) at (1,0);
\coordinate[label=135:$\imath a$] (ia) at (0,2);
\coordinate[label=-90:$a^{-1}$] (ainv) at (0.5,0);
\fill[black] (i) circle (2pt);
\fill[black] (1) circle (2pt);
\fill[black] (ia) circle (2pt);
\fill[black] (ainv) circle (2pt);
\draw (1) -- (ia);
\draw (i) -- (ainv);
\end{tikzpicture} — Figure 1.8 Construction of $z^{-1}$

Corollary 1.44 Inverse of a complex number

✓

If $z \in M_{\infty }$, then $z^{-1}$ is in $M_{\infty }$.

Proof ▶

For $z \in M_{\infty }$ we can write $z = a + \imath b$ with $a, b \in \mathbb {R}$. Then

\[ z^{-1} = \frac{1}{z} = \frac{\overline{z}}{z\overline{z}} = \frac{a - \imath b}{a^2+b^2}= (a - \imath b) \cdot (aa+bb)^{-1}. \]

It is now possible to combine the lemmas for addition 1.31, subtraction 1.32, multiplication 1.42 and the corollary for the inverse of a positive real number 1.43 with the part concerning the existence of real and imaginary components 1.39 in order to conclude that $z^{-1} \in M_{\infty }$.

Lemma 1.45 Angle in $M_{\infty }$

✓

If $0 \ne z = r\cdot e^{\imath\alpha } \in M_{\infty }$, then $e^{\imath\alpha } \in M_{\infty }$.

For the construction we draw a line through $0$ and $z$ and take the intersection with the unit circle. 1.9

Proof ▶

Let $l$ be a line through $0$ and $z$ and $c$ be the unit circle. Then $l \cap c = \{ e^{\imath\alpha }\} $. The rest follows from the construction of the intersection of a line and a circle1.29.

\begin{tikzpicture}
\draw[->] (-0.5,0) -- (4,0) node[right] {$\Re$};
\draw[->] (0,-0.5) -- (0,3) node[above] {$\Im$};
\coordinate[label=-135:$0$] (zero) at (0,0);
\coordinate[label=-135:$1$] (one) at (1,0);
\coordinate[label=135:$z$] (z) at (3,2);
\coordinate[label=90:$e^{\imath\alpha}$] (ea) at (0.8321,0.5547);
\fill[black] (zero) circle (1pt);
\fill[black] (one) circle (2pt);
\fill[black] (z) circle (2pt);
\fill[black] (ea) circle (2pt);
\draw (zero) -- (z);
\draw (zero) [carc=-20:110:1];
\end{tikzpicture} — Figure 1.9 Construction of $e^{\imath\alpha }$

Corollary 1.46 Midpoint in $M_{\infty }$

✓

If $z_1, z_2 \in M_{\infty }$, then $\frac{z_1 + z_2}{2} \in M_{\infty }$.

Proof ▶

Combining the lemmas for addition1.31, multiplication1.42 and the invers of a complex number1.44 we get that $\frac{z_1 + z_2}{1+1} \in M_{\infty }$.

Lemma 1.47 Halving of an angle

✓

For $\alpha \in [0,2\pi )$, if $e^{\imath\alpha } \in M_{\infty }$, then $e^{\imath\frac {\alpha }{2}} \in M_{\infty }$.

Proof ▶

For $\alpha \ne 0 \ne \pi $ we take the intersection of the unit circle with the line through $0$ and and the mipiont of $e^{\imath\alpha }$ and $1$.

For $\alpha = 0$ we get $e^{\imath\frac {\alpha }{2}} = 1$ and for $\alpha = \pi $ we get $e^{\imath\frac {\alpha }{2}} = $

.

Proof ▶

Lemma 1.48 Construction of radius

✓

If 

z = r·e^α M_∞, then $r \in M_{\infty }$.

Lemma

Remark 1.49

The radius is the distance from $0$ to $z$, which is the same as $\| z\| $.

We get the radius by taking the intersection of the real axis with a circle in zero with radius $\text{ dist }(0,z)$. 1.10

Proof ▶

We use the fact that $r = \| z\| = \sqrt{\Re (z)^2 + \Im (z)^2}$. Since we have spilt $r$ in already constructed parts, we get that $r \in M_{\infty }$.

\begin{tikzpicture}
\draw[->] (-0.5,0) -- (4,0) node[right] {$\Re$};
\draw[->] (0,-0.5) -- (0,4) node[above] {$\Im$};
\coordinate[label=-135:$0$] (zero) at (0,0);
\coordinate[label=-135:$1$] (one) at (1,0);
\coordinate[label=90:$z$] (z) at (3,2);
\coordinate[label=-135:$r$] (r) at (3.6056,0);
\fill[black] (zero) circle (2pt);
\fill[black] (one) circle (1pt);
\fill[black] (z) circle (2pt);
\fill[black] (r) circle (2pt);
\draw (zero) -- (z);
\draw (zero) [carc=-10:100:3.6056];
\end{tikzpicture} — Figure 1.10 Construction of $r = \| z\| $

Lemma 1.50 Root of pos real number

✓

If $r \in M_{\infty }\cap \mathbb {R}_{\ge 0}$, then $\sqrt{r}$ is in $M_{\infty }$.

This construction is taken from [ 6 ] .
Draw a circle trough $0$ and $r$ and a line through $1$ parallel to the imaginary axis. Project the intersection to the real axis, using a circle with center $0$ and you get $\sqrt{r}$. (Fig. 1.11)

Proof ▶

Without loss of generality we can assume that $r \ge 1$. Otherwise we can use the fact that $\sqrt{r} = \frac{1}{\sqrt{r^{-1}}}$. The initial step is to define the following lines and circles:

$:= \{ z_1 :=1; z_2 := \imath+ 1\} $
$:= \{ z_1:=0; z_2:= 1\} $
$:= \{ \text{center}:= \frac{r}{2}; \text{radius} := \text{ dist }(0,\frac{r}{2})\} $
$:= \{ \text{center}:= 0; \text{radius} := \text{ dist }(0,\sqrt{r})\} $

It can be observed that both $l_1$ and $l_{\Re }$ are elements of $L(M)$, and that $c_1$ is an element of $C(M)$. Furthermore, it can be demonstrated that the $\sqrt{r}$ is an element of $l_{\Re } \cap c_2$. Consequently, the only remaining step is to show that $c_2$ is an element of $C(M)$, which is equivalent to proving that there exists a $z$ in $M_{\infty }$ that is also an element of $c_2$. This is possible since $0$ is an element of $M_{\infty }$.
Claim: There exists a $z \in l_1 \cap c_1$, such that $z \in c_2$.

Proof ▶

In accordance with the theorem of Pythagoras, it can be demonstrated that$z= 1 \pm \imath\sqrt {r-1}$. A further application of the Pythagorean theorem yields the following result:

\[ \text{ dist }(0,z) \overset {z= 1 + \imath\sqrt {r-1}}{=} \sqrt{1^2 + (\sqrt{r-1})^2} = \sqrt{1 + r - 1} = \sqrt{r} = \text{ dist }(0,\sqrt{r}). \]

Therefore, it can be concluded that $\sqrt{r}$ is also constructible.

\begin{tikzpicture}
\draw[->] (-1,0) -- (7,0) node[right] {$\Re$};
\draw[->] (0,-1) -- (0,4) node[above] {$\Im$};
\coordinate[label=-135:$0$] (zero) at (0,0);
\coordinate[label=-90:$1$] (one) at (1,0);
\coordinate[label=-45:$r$] (r) at (6,0);
\coordinate[label=-90:$\frac{r}{2}$] (r2) at (3,0);
\coordinate[label=135:] (sqrt1) at (1,2.2360679775);
\coordinate[label=135:$\sqrt{r}$] (sqrt) at (2.4494897428,0);
\fill[black] (zero) circle (1pt);
\fill[black] (one) circle (2pt);
\fill[black] (r) circle (2pt);
\fill[black] (r2) circle (2pt);
\fill[black] (sqrt1) circle (2pt);
\draw (r2) [carc=-10:190:3];
\draw (zero) [carc=-10:80:2.4494897428];
\draw (one) -- (sqrt1);
\fill[red] (sqrt) circle (3pt);
\end{tikzpicture} — Figure 1.11 Construction of $\sqrt{r}$

Corollary 1.51 Square root of a complexnumber

✓

If $z \in M_{\infty }$, then $\sqrt{z}$ is in $M_{\infty }$.

Proof ▶

$z = r \cdot e^{\imath\alpha }$ with $r \in \mathbb {R}_{\ge 0}$ and $\alpha \in \mathbb {R}$. Then $\sqrt{z} = \sqrt{r} \cdot e^{\imath\frac {\alpha }{2}}$. Now we can use Lemma 1.48 and Lemma 1.50 to get that $\sqrt{z} \in M_{\infty }$. For $e^{\imath\frac {\alpha }{2}}$ we can combine Lemma 1.45 and Lemma 1.47. Now we get that $\sqrt{z} \in M_{\infty }$, after Lemma 1.40.

Formalisation-of-constructable-numbers

1 Basic Constructions with Ruler and Compass

1.1 Defining lines, circles and the set of constructable points

1.2 Properties of Lines

1.3 The Set \(M_{\infty }\)

1.4 Basic constructions