Gauss–Wantzel theorem on constructible polygons

InductiveConstructible real numbers#✓fully proved

The constructible real numbers form the smallest set of real numbers that contains every rational number and is closed under addition, negation, multiplication, inverses of nonzero elements and square roots of nonnegative elements; equivalently, the smallest subfield of \(\mathbb{R}\) closed under square roots.

These are the real values constructible from rational data by straightedge and compass.

inductive IsConstructible : ℝ → Prop
  | base (q : ℚ) : IsConstructible (q : ℝ)
  | add {x y : ℝ} : IsConstructible x → IsConstructible y → IsConstructible (x + y)
  | neg {x : ℝ} : IsConstructible x → IsConstructible (-x)
  | mul {x y : ℝ} : IsConstructible x → IsConstructible y → IsConstructible (x * y)
  | inv {x : ℝ} : IsConstructible x → IsConstructible x⁻¹
  | sqrt {x : ℝ} : IsConstructible x → IsConstructible (Real.sqrt x)

Used by 1

Used byGauss–Wantzel theorem

DefinitionGauss–Wantzel number#✓fully proved

A natural number \(n\) is a Gauss–Wantzel number if \(n > 0\), every prime factor of \(n\) is either \(2\) or a Fermat prime, and \(p^2\) does not divide \(n\) for every odd prime factor \(p\) of \(n\).

Equivalently, \(n\) is a power of \(2\) times a product of distinct Fermat primes.

def GaussWantzelNumber (n : ℕ) : Prop :=
  0 < n ∧
    ∀ p : ℕ, p.Prime → p ∣ n →
      (p = 2 ∨ MetaMathlibExt.IsFermatPrime p) ∧ (p ≠ 2 → ¬ p ^ 2 ∣ n)

Uses 1 · Used by 1

Statement usesFermat prime

Used byGauss–Wantzel theorem

TheoremGauss–Wantzel theorem#●ready to prove

For every natural number \(n \ge 3\), the real number \(\cos(2\pi/n)\) is constructible (it lies in the smallest subfield of \(\mathbb{R}\) closed under square roots) if and only if \(n\) is a Gauss–Wantzel number, that is, every prime factor of \(n\) is \(2\) or a Fermat prime and every odd prime factor of \(n\) divides \(n\) only once.

public theorem_wanted gauss_wantzel_constructible_polygon (n : ℕ) (hn : 3 ≤ n) :
    IsConstructible (Real.cos (2 * Real.pi / n)) ↔ GaussWantzelNumber n

Sources

• C. F. Gauss, Disquisitiones Arithmeticae (1801), §365-366; P. L. Wantzel, Recherches sur les moyens de reconnaître si un problème de géométrie peut se résoudre avec la règle et le compas, J. Math. Pures Appl. 1 (1837). Listed as §174 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §174. Problem gauss_wantzel_constructible_polygon of the lean-eval benchmark.

Uses 2

Statement usesGauss–Wantzel number · Constructible real numbers

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.