
92 Ruler-and-Compass Constructions
Proof. The inclusions are clear. Let p
n
be the number of points in P
n
, l
n
the number
of lines in L
n
, and c
n
the number of circles in C
n
. Then
|L
n+1
| ≤
1
2
p
n
(p
n
+ 1)
|C
n+1
| ≤ p
n
1
2
p
n
(p
n
+ 1)
|P
n+1
| ≤
1
2
l
n+1
(l
n+1
+ 1) + 2l
n
c
n
+ c
n+1
(c
n+1
+ 1)
bearing in mind that a line or circle meets a distinct circle in ≤2 points. By induction,
all three sets are finite for all n.
We formalise a Euclidean ruler-and-compass construction using these sets. The
intuitive idea is that starting from 0 and 1, such a construction generates a finite
sequence of points by drawing a line through two previously constructed points, or
a circle whose centre is ...