Angles

Why a triangle has 180 degrees, a polygon (n − 2) · 180 degrees and a star (n − 2k) · 180 degrees, why only triangle, square and hexagon fill the plane, and why ten is unique among the angle sums.

So far the subject was numbers. The page Angle sums and full circles links them with geometry: every figure $\{n/k\}$ has an angle sum, and ten stands out among them. This chapter proves the formulas for it, starting from Euclid’s geometry.

The parallel postulate

After the definitions, Euclid’s Elements set out five postulates about points, lines and circles. The fifth is the most famous, because it sounds less self-evident than the others. In the form usual today it reads:

Axiom

For a line $g$ and a point $P$ not on $g$ there is exactly one line through $P$ that does not meet $g$ , the parallel.

For two thousand years mathematicians tried to prove this axiom from the other four. In the nineteenth century Gauss, Bolyai and Lobachevsky developed a geometry without this axiom, and Beltrami, Klein and Poincaré showed with their models that it is consistent. So the proof is impossible: there are consistent geometries in which the axiom is false. There a triangle has less than 180 degrees. All theorems of this chapter therefore hold in the Euclidean plane, the geometry of a flat sheet of paper.

We measure angles in degrees, with the full circle as $360^\circ$ . The page on angle sums counts in full circles instead. Both are the same, only in different units: $180^\circ$ is half a full circle.

The triangle

Theorem 1

The angles of a triangle add up to $180^\circ$ .

Proof

Let $ABC$ be a triangle with angles $\alpha, \beta, \gamma$ at $A, B, C$ . Through $C$ draw the parallel to $AB$ . With $CA$ it forms an angle that, as an alternate angle at parallels, equals $\alpha$ , and with $CB$ one that equals $\beta$ . Together with $\gamma$ the three angles fill the straight line through $C$ , so $\alpha + \beta + \gamma = 180^\circ$ .

∎

This is how the Pythagoreans already proved it according to Eudemus, as Proclus reports in his commentary. Euclid proceeds a little differently in the Elements I 32 and extends one side.

Polygons and stars

Theorem 2

The interior angles of a convex $n$ -gon add up to $(n - 2) \cdot 180^\circ$ .

Proof

From one corner draw the diagonals to all non-adjacent corners. They divide the $n$ -gon into $n - 2$ triangles whose angles together make up exactly the interior angles of the polygon. By Theorem 1 this gives $(n-2) \cdot 180^\circ$ .

∎

Theorem 3

The angles at the points of the figure $\{n/k\}$ add up to

(n - 2k) \cdot 180^\circ,

counted in full circles $\tfrac{n - 2k}{2}$ .

Proof

Walk along the figure. At each corner you turn by the exterior angle $\varepsilon$ , and the interior angle at that corner is $180^\circ - \varepsilon$ . For a star drawn in a single stroke you go round the centre $k$ times, since each step skips $k$ of the $n$ pieces of the circle. So the turns add up to $k \cdot 360^\circ$ , and for the $n$ interior angles there remains

n \cdot 180^\circ - k \cdot 360^\circ = (n - 2k) \cdot 180^\circ.

If by Chapter 6 the figure falls into $g$ equal stars $\{\tfrac{n}{g}/\tfrac{k}{g}\}$ , these together give $g \cdot \bigl(\tfrac{n}{g} - 2\tfrac{k}{g}\bigr) \cdot 180^\circ$ , the same.

∎

For $k = 1$ this is Theorem 2. Every further step size takes away exactly one full circle.

Full circles of all figures in the simplexNumber of vertices

n	Figures	Full circles per figure	Sum
3	1	0.5	0.5
4	1	1	1
5	2	1.5 + 0.5	2
6	2	2 + 1	3
7	3	2.5 + 1.5 + 0.5	4.5
8	3	3 + 2 + 1	6
9	4	3.5 + 2.5 + 1.5 + 0.5	8
10	4	4 + 3 + 2 + 1	10
11	5	4.5 + 3.5 + 2.5 + 1.5 + 0.5	12.5
12	5	5 + 4 + 3 + 2 + 1	15

The angle sums of all figures up to the 16-gon, counted in full circles. Each row begins with the polygon and loses one full circle with every step size.

The special position of ten

Theorem 4

Adding up the angle sums of all figures $\{n/k\}$ with $1 \le k < n/2$ gives

W(n) = \begin{cases} T(m) & \text{for } n = 2m + 2, \\[2pt] \tfrac{m^2}{2} & \text{for } n = 2m + 1 \end{cases}

full circles. $W(n) = n$ only for $n = 10$ . For $n < 10$ , $W(n) < n$ , for $n > 10$ , $W(n) > n$ .

Proof

For $n = 2m + 2$ the step sizes run from 1 to $m$ , and by Theorem 3

\begin{aligned} W(n) &= \sum_{k=1}^{m} \frac{2m + 2 - 2k}{2} \\ &= \sum_{k=1}^{m} (m + 1 - k) \\ &= m + (m - 1) + \dots + 1 = T(m). \end{aligned}

From $T(m) = 2m + 2$ it follows that $m^2 - 3m - 4 = 0$ , so $(m - 4)(m + 1) = 0$ and $m = 4$ , $n = 10$ .

For $n = 2m + 1$ the step sizes also run from 1 to $m$ , and $W(n) = \sum_{k=1}^{m} \tfrac{2m + 1 - 2k}{2} = \tfrac{m^2}{2}$ . From $m^2 = 4m + 2$ it would follow that $m$ is even, but then $m^2$ would be divisible by 4 and $4m + 2$ would not. So a tie is impossible.

For the inequalities, write the differences as products: in the even case $W(n) - n = \tfrac{(m-4)(m+1)}{2}$ , negative for $m < 4$ and positive for $m > 4$ . In the odd case $W(n) - n = \tfrac{m^2 - 4m - 2}{2}$ , negative for $m \le 4$ , that is $n \le 9$ , and positive for $m \ge 5$ , that is $n \ge 11$ .

∎

For the decagon there are $4 + 3 + 2 + 1 = 10$ full circles: the tetractys appears here as a sum of angles. Remarkably, the proof shows why: the angle sums of an even simplex always form a triangular number, and only the fourth triangular number equals the corresponding number of corners.

n-gon

PolygonCompound polygonStar polygonCompound starLine star

The figures of the decagon with their angle sums in full circles: 4, 3, 2 and 1, together 10.

Theorem 5

Angle sum in full circles and quotient agree, $\tfrac{n - 2k}{2} = \tfrac{n}{k}$ , for exactly the four figures

\{16/4\},\;\; \{18/3\},\;\; \{18/6\},\;\; \{25/10\}.

Proof

The equation is $(n - 2k)\,k = 2n$ . Set $n = 2k + m$ with $m \ge 1$ and obtain $mk = 4k + 2m$ , rearranged

(m - 4)(k - 2) = 8.

For $k \le 2$ we would have $mk \le 2m < 4k + 2m$ , so $k \ge 3$ and hence also $m - 4 = \tfrac{8}{k-2} > 0$ . Both factors are positive, and $k - 2$ is a divisor of 8: $k - 2 \in \{1, 2, 4, 8\}$ , with $m - 4 \in \{8, 4, 2, 1\}$ . This gives $(k, n) = (3, 18), (4, 16), (6, 18), (10, 25)$ , and no others.

∎

Here the proof shows something no amount of calculating can: there are no further cases, not just up to 100 or up to a million but none at all, because 8 has only four divisors.

Checked by computer: the proof in Lean

four_solutions is Theorem 5 in the form $mk = 4k + 2m$ . Lean first shows bounds, $3 \le k \le 10$ and $5 \le m \le 12$ , each by a small estimate, and then with cases works through the finitely many remaining pairs. only_ten is the even case of Theorem 4: the triangular number $T(m)$ grows faster than $2m + 2$ from $m = 5$ on (induction), and below that Lean checks by calculation.

/-! Chapter 7: angle sums -/

/-- All cases with k ≤ 10 and m ≤ 12, checked one by one by Lean -/
theorem cases : ∀ k : Fin 11, ∀ m : Fin 13, 3 ≤ k.val → 5 ≤ m.val →
    m.val * k.val = 4 * k.val + 2 * m.val →
    (k.val = 3 ∧ m.val = 12) ∨ (k.val = 4 ∧ m.val = 8) ∨
    (k.val = 6 ∧ m.val = 6) ∨ (k.val = 10 ∧ m.val = 5) := by
  decide

/-- Theorem 5: Angle sum equals quotient, that is
    (n − 2k) · k = 2n, has exactly four solutions.
    With n = 2k + m this becomes m · k = 4k + 2m. -/
theorem four_solutions (k m : Nat) (hk : 1 ≤ k) (hm : 1 ≤ m)
    (h : m * k = 4 * k + 2 * m) :
    (k = 3 ∧ m = 12) ∨ (k = 4 ∧ m = 8) ∨
    (k = 6 ∧ m = 6) ∨ (k = 10 ∧ m = 5) := by
  -- k ≥ 3, otherwise m · k ≤ 2m < 4k + 2m
  have hk3 : 3 ≤ k := by
    rcases Nat.lt_or_ge k 3 with hlt | hge
    · have : m * k ≤ m * 2 := Nat.mul_le_mul_left m (by omega)
      omega
    · exact hge
  -- m ≥ 5, otherwise m · k ≤ 4k < 4k + 2m
  have hm5 : 5 ≤ m := by
    rcases Nat.lt_or_ge m 5 with hlt | hge
    · have : m * k ≤ 4 * k := Nat.mul_le_mul_right k (by omega)
      omega
    · exact hge
  -- m ≤ 12 and k ≤ 10, by similar estimates
  have hm12 : m ≤ 12 := by
    rcases Nat.lt_or_ge 12 m with hlt | hge
    · have : 13 * k ≤ m * k := Nat.mul_le_mul_right k (by omega)
      have : m * 3 ≤ m * k := Nat.mul_le_mul_left m hk3
      omega
    · exact hge
  have hk10 : k ≤ 10 := by
    rcases Nat.lt_or_ge 10 k with hlt | hge
    · have : m * 11 ≤ m * k := Nat.mul_le_mul_left m (by omega)
      have : 5 * k ≤ m * k := Nat.mul_le_mul_right k hm5
      omega
    · exact hge
  -- finitely many cases, Lean works through them
  exact cases ⟨k, by omega⟩ ⟨m, by omega⟩ hk3 hm5 h

/-- Theorem 4, even case: the angle sums of a simplex
    n = 2m + 2 give the triangular number T(m), and
    T(m) = 2m + 2 holds only for m = 4, that is n = 10. -/
def triangle : Nat → Nat
  | 0 => 0
  | m + 1 => triangle m + (m + 1)

theorem only_ten (m : Nat) (h : triangle m = 2 * m + 2) : m = 4 := by
  -- triangle m grows faster than 2m + 2: from m = 5 on it is too large
  have larger : ∀ j, triangle (j + 5) > 2 * (j + 5) + 2 := by
    intro j
    induction j with
    | zero => decide
    | succ j ih =>
      show triangle (j + 5) + (j + 5 + 1) > 2 * (j + 1 + 5) + 2
      omega
  rcases Nat.lt_or_ge m 5 with hlt | hge
  · have small : ∀ j : Fin 5, triangle j.val = 2 * j.val + 2 → j.val = 4 := by
      decide
    exact small ⟨m, hlt⟩ h
  · have := larger (m - 5)
    rw [show m - 5 + 5 = m by omega] at this
    omega

Try it in the browser at live.lean-lang.org ↗How to read Lean

Which polygons fill the plane

One last theorem links the angles with the page Circle, triangle and square.

Theorem 6

Using only one kind of regular polygon, the plane can be tiled without gaps and edge to edge only with equilateral triangles, squares or regular hexagons.

Proof

At each corner of the tiling $j$ polygons meet, whose interior angles add up to $360^\circ$ . By Theorem 2 the interior angle of the regular $n$ -gon is $\tfrac{(n-2) \cdot 180^\circ}{n}$ . So

\begin{aligned} j &= \frac{360^\circ \cdot n}{(n - 2) \cdot 180^\circ} \\ &= \frac{2n}{n - 2} = 2 + \frac{4}{n - 2}. \end{aligned}

For $j$ to be a whole number, $n - 2$ must divide 4: $n - 2 \in \{1, 2, 4\}$ , so $n \in \{3, 4, 6\}$ , with 6, 4 and 3 polygons at each corner.

∎

Once again a small divisor, this time of 4, limits an infinite question to three answers.

Sources and further reading

Sources

Euclid, Elements, around 300 BC, book I, postulate 5 and proposition 32
Proclus, Commentary on the First Book of Euclid’s Elements 379 (the proof of the Pythagoreans)