Foundations and constructions

Axiom systems for plane geometry and the limits of compass-and-straightedge constructions.

TheoremImpossibility of angle trisection#✓fully proved

Let "constructible" be any property of real numbers such that a real number \(x\) is constructible exactly when there are \(n \ge 0\) and subfields \(K_0 \subseteq K_1 \subseteq \dots \subseteq K_n\) of \(\mathbb{R}\) with \(K_0 = \mathbb{Q}\) (the smallest subfield of \(\mathbb{R}\)), \(x \in K_n\), and, for each \(i < n\), some \(b \in K_{i+1}\) with \(b^2 \in K_i\) such that every element of \(K_{i+1}\) equals \(u + bv\) for some \(u, v \in K_i\). Let an angle \(\theta\) be constructible exactly when \(\cos \theta\) is constructible. Then the polynomial \(8X^3 - 6X - 1\) is irreducible over \(\mathbb{Q}\), \(\cos(\pi/9)\) is a root of it, \(\cos(\pi/9)\) is not constructible, and it is not true that \(\theta / 3\) is a constructible angle for every constructible angle \(\theta\).

In particular the \(60^\circ\) angle, whose cosine \(1/2\) is constructible, cannot be trisected: by the triple-angle formula, \(\cos 20^\circ = \cos(\pi/9)\) is a root of \(8X^3 - 6X - 1\).

MetaMathlibExt.angle_trisection_impossible · 18 lines 
theorem angle_trisection_impossible :
    ∀ (IsConstructible : ℝ → Prop) (IsConstructibleAngle : ℝ → Prop),
      (∀ x : ℝ, IsConstructible x ↔
        ∃ (n : ℕ) (K : Fin (n + 1) → Subfield ℝ),
          K 0 = ⊥ ∧
          x ∈ K (Fin.last n) ∧
          ∀ i : Fin n, K i.castSucc ≤ K i.succ ∧
            ∃ b : ℝ, b ∈ K i.succ ∧ b ^ 2 ∈ K i.castSucc ∧
            ∀ y : ℝ, y ∈ K i.succ →
              ∃ u v : ℝ, u ∈ K i.castSucc ∧ v ∈ K i.castSucc ∧ y = u + b * v) →
      (∀ θ : ℝ, IsConstructibleAngle θ ↔ IsConstructible (Real.cos θ)) →
      Irreducible (8 * (Polynomial.X : Polynomial ℚ) ^ 3 -
        6 * (Polynomial.X : Polynomial ℚ) - 1) ∧
      Polynomial.aeval (Real.cos (Real.pi / 9))
        (8 * (Polynomial.X : Polynomial ℚ) ^ 3 -
          6 * (Polynomial.X : Polynomial ℚ) - 1) = 0 ∧
      ¬ IsConstructible (Real.cos (Real.pi / 9)) ∧
      ¬ ∀ θ : ℝ, IsConstructibleAngle θ → IsConstructibleAngle (θ / 3)
Sources
  • https://en.wikipedia.org/wiki/Angle_trisection.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.