Platonic solids and regular polytopes

TheoremClassification of the Platonic solids#✓fully proved

Let \(V, E, F, p, q\) be natural numbers with \(V, E, F > 0\) and \(p, q \ge 3\), and let \(l > 0\) and \(d > 0\) be real numbers. Let \(x_0, \dots, x_{V-1}\) be points of the Euclidean space \(\mathbb{R}^3\), let \(K\) be their convex hull and let \(\partial K\) be its topological boundary. Let each edge \(e < E\) be an ordered pair \((a_e, b_e)\) of point indices, with segment \([x_{a_e}, x_{b_e}]\), and let each face \(f < F\) be a list \(\phi_f(0), \dots, \phi_f(p-1)\) of point indices, read cyclically: positions are taken modulo \(p\), the sides of \(f\) are the pairs \((\phi_f(i), \phi_f(i+1))\), and the filled face is the convex hull of \(x_{\phi_f(0)}, \dots, x_{\phi_f(p-1)}\). An edge \(e\) lies on side \(i\) of \(f\) when \((a_e, b_e)\) equals \((\phi_f(i), \phi_f(i+1))\) or \((\phi_f(i+1), \phi_f(i))\). Assume: \(K\) is convex and contains every \(x_i\); no \(x_i\) lies in the convex hull of the \(x_j\) with \(j \ne i\); the differences \(x_i - x_j\) span a space of dimension \(3\); every edge segment has length \(l\); for every face \(f\) and position \(i\), \(\operatorname{dist}(x_{\phi_f(i)}, x_{\phi_f(i+1)}) = l\) and \(\operatorname{dist}(x_{\phi_f(i-1)}, x_{\phi_f(i+1)}) = d\); the indices \(\phi_f(0), \dots, \phi_f(p-1)\) of each face are distinct; no vertex \(x_{\phi_f(k)}\) of a face lies in the convex hull of the other vertices of that face; two sides \((i_1, i_1+1)\) and \((i_2, i_2+1)\) of a face whose four endpoint positions are all different have disjoint segments; some edge lies on each side of every face, and every edge lies on a side of some face; every edge lies on a side of exactly two faces; every edge segment and every filled face is contained in \(K\); the differences of the vertices of each face span a space of dimension at most \(2\); for every face \(f\) there are a nonzero vector \(n\) and a real \(c\) with \(\langle n, x \rangle \le c\) for all \(x \in K\) and \(\langle n, x_{\phi_f(i)} \rangle = c\) for every position \(i\); two edges \(e_1, e_2\) with \((a_{e_1}, b_{e_1})\) equal to \((a_{e_2}, b_{e_2})\) or \((b_{e_2}, a_{e_2})\) are equal; two faces with the same set of indices are equal; every \(x_i\), every edge segment and every filled face is contained in \(\partial K\); every point of \(\partial K\) lies in some filled face; every point index occurs in exactly \(q\) faces; and \(2E = pF\), \(2E = qV\) and \(V - E + F = 2\). Then \((p, q, V, E, F)\) is one of \((3, 3, 4, 6, 4)\) (tetrahedron), \((4, 3, 8, 12, 6)\) (cube), \((3, 4, 6, 12, 8)\) (octahedron), \((5, 3, 20, 30, 12)\) (dodecahedron) or \((3, 5, 12, 30, 20)\) (icosahedron).

Conversely, each of these five tuples \((p, q, V, E, F)\) is realized: there are points, edges, faces and reals \(l, d > 0\) satisfying all the conditions above, except that the points, edge segments and filled faces are required to lie in \(\partial K\) but not separately in \(K\).

Euler's relation \(V - E + F = 2\) and the incidence counts \(2E = pF\), \(2E = qV\) are hypotheses, and the classification is up to the tuple \((p, q, V, E, F)\), not up to congruence. Together they give \(1/p + 1/q > 1/2\), which leaves the five tuples; explicit coordinates realize each one.

MetaMathlibExt.platonic_solids_classification · 287 lines

theorem platonic_solids_classification :
    ((∀ (V E F p q : ℕ) (verts : Fin V → EuclideanSpace ℝ (Fin 3))
      (edgeEnds : Fin E → Fin V × Fin V) (faceVerts : Fin F → Fin p → Fin V)
      (body : Set (EuclideanSpace ℝ (Fin 3))) (l angleDiag : ℝ),
      0 < V → 0 < E → 0 < F → 3 ≤ p → 3 ≤ q → 0 < l → 0 < angleDiag →
      body = convexHull ℝ (Set.range verts) →
      Convex ℝ body →
      (∀ v : Fin V, verts v ∈ body) →
      (∀ v : Fin V, verts v ∉ convexHull ℝ (verts '' {w : Fin V | w ≠ v})) →
      (Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin V, d = verts i - verts j}) = 3) →
      (∀ e : Fin E, dist (verts (edgeEnds e).1) (verts (edgeEnds e).2) = l) →
      (∀ f : Fin F, ∀ i j : Fin p,
        j.val = (i.val + 1) % p →
        dist (verts (faceVerts f i)) (verts (faceVerts f j)) = l) →
      (∀ f : Fin F, ∀ h i j : Fin p,
        h.val = (i.val + p - 1) % p → j.val = (i.val + 1) % p →
        dist (verts (faceVerts f h)) (verts (faceVerts f j)) = angleDiag) →
      (∀ f : Fin F, Function.Injective (faceVerts f)) →
      (∀ f : Fin F, ∀ k : Fin p,
        verts (faceVerts f k) ∉ convexHull ℝ
          (verts '' (Set.range (faceVerts f) \ {faceVerts f k}))) →
      (∀ f : Fin F, ∀ i₁ j₁ i₂ j₂ : Fin p,
        j₁.val = (i₁.val + 1) % p → j₂.val = (i₂.val + 1) % p →
        i₁ ≠ i₂ → i₁ ≠ j₂ → j₁ ≠ i₂ → j₁ ≠ j₂ →
        Disjoint (convexHull ℝ {verts (faceVerts f i₁), verts (faceVerts f j₁)})
          (convexHull ℝ {verts (faceVerts f i₂), verts (faceVerts f j₂)})) →
      (∀ f : Fin F, ∀ i j : Fin p,
        j.val = (i.val + 1) % p →
        ∃ e : Fin E, edgeEnds e = (faceVerts f i, faceVerts f j) ∨
          edgeEnds e = (faceVerts f j, faceVerts f i)) →
      (∀ e : Fin E, ∃ f : Fin F, ∃ i j : Fin p,
        j.val = (i.val + 1) % p ∧
        (edgeEnds e = (faceVerts f i, faceVerts f j) ∨
          edgeEnds e = (faceVerts f j, faceVerts f i))) →
      (∀ e : Fin E, Set.ncard {f : Fin F | ∃ i j : Fin p,
        j.val = (i.val + 1) % p ∧
        (edgeEnds e = (faceVerts f i, faceVerts f j) ∨
          edgeEnds e = (faceVerts f j, faceVerts f i))} = 2) →
      (∀ e : Fin E, convexHull ℝ {verts (edgeEnds e).1, verts (edgeEnds e).2} ⊆ body) →
      (∀ f : Fin F, convexHull ℝ (verts '' Set.range (faceVerts f)) ⊆ body) →
      (∀ f : Fin F, Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin p, d = verts (faceVerts f i) - verts (faceVerts f j)}) ≤ 2) →
      (∀ f : Fin F, ∃ n : EuclideanSpace ℝ (Fin 3), ∃ c : ℝ,
        n ≠ 0 ∧ (∀ x ∈ body, inner (𝕜 := ℝ) n x ≤ c) ∧
        (∀ i : Fin p, inner (𝕜 := ℝ) n (verts (faceVerts f i)) = c)) →
      (∀ e₁ e₂ : Fin E,
        (edgeEnds e₁ = edgeEnds e₂ ∨ edgeEnds e₁ = (edgeEnds e₂).swap) → e₁ = e₂) →
      (∀ f₁ f₂ : Fin F, Set.range (faceVerts f₁) = Set.range (faceVerts f₂) → f₁ = f₂) →
      (∀ v : Fin V, verts v ∈ frontier body) →
      (∀ e : Fin E, convexHull ℝ {verts (edgeEnds e).1, verts (edgeEnds e).2} ⊆ frontier body) →
      (∀ f : Fin F, convexHull ℝ (verts '' Set.range (faceVerts f)) ⊆ frontier body) →
      (∀ x ∈ frontier body, ∃ f : Fin F,
        x ∈ convexHull ℝ (verts '' Set.range (faceVerts f))) →
      (∀ v : Fin V, Set.ncard {f : Fin F | ∃ i, faceVerts f i = v} = q) →
      2 * E = p * F → 2 * E = q * V →
      (V : ℤ) - (E : ℤ) + (F : ℤ) = 2 →
      ((p = 3 ∧ q = 3 ∧ V = 4 ∧ E = 6 ∧ F = 4) ∨
      (p = 4 ∧ q = 3 ∧ V = 8 ∧ E = 12 ∧ F = 6) ∨
      (p = 3 ∧ q = 4 ∧ V = 6 ∧ E = 12 ∧ F = 8) ∨
      (p = 5 ∧ q = 3 ∧ V = 20 ∧ E = 30 ∧ F = 12) ∨
      (p = 3 ∧ q = 5 ∧ V = 12 ∧ E = 30 ∧ F = 20))) ∧
    ((∃ (w : Fin 4 → EuclideanSpace ℝ (Fin 3)) (ee : Fin 6 → Fin 4 × Fin 4)
      (fv : Fin 4 → Fin 3 → Fin 4) (b : Set (EuclideanSpace ℝ (Fin 3)))
      (ll dd : ℝ),
      0 < ll ∧ 0 < dd ∧
      b = convexHull ℝ (Set.range w) ∧
      Convex ℝ b ∧
      (∀ v : Fin 4, w v ∈ frontier b) ∧
      (∀ v : Fin 4, w v ∉ convexHull ℝ (w '' {u : Fin 4 | u ≠ v})) ∧
      (Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 4, d = w i - w j}) = 3) ∧
      (∀ e : Fin 6, dist (w (ee e).1) (w (ee e).2) = ll) ∧
      (∀ (f : Fin 4) (i j : Fin 3), j.val = (i.val + 1) % 3 →
        dist (w (fv f i)) (w (fv f j)) = ll) ∧
      (∀ (f : Fin 4) (h i j : Fin 3), h.val = (i.val + 3 - 1) % 3 →
        j.val = (i.val + 1) % 3 → dist (w (fv f h)) (w (fv f j)) = dd) ∧
      (∀ f : Fin 4, Function.Injective (fv f)) ∧
      (∀ (f : Fin 4) (k : Fin 3), w (fv f k) ∉ convexHull ℝ
        (w '' (Set.range (fv f) \ {fv f k}))) ∧
      (∀ (f : Fin 4) (i₁ j₁ i₂ j₂ : Fin 3),
        j₁.val = (i₁.val + 1) % 3 →
        j₂.val = (i₂.val + 1) % 3 →
        i₁ ≠ i₂ → i₁ ≠ j₂ → j₁ ≠ i₂ → j₁ ≠ j₂ →
        Disjoint (convexHull ℝ {w (fv f i₁), w (fv f j₁)})
          (convexHull ℝ {w (fv f i₂), w (fv f j₂)})) ∧
      (∀ (f : Fin 4) (i j : Fin 3), j.val = (i.val + 1) % 3 →
        ∃ e : Fin 6, ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i)) ∧
      (∀ e : Fin 6, ∃ f : Fin 4, ∃ i j : Fin 3,
        j.val = (i.val + 1) % 3 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))) ∧
      (∀ e : Fin 6, Set.ncard {f : Fin 4 | ∃ i j : Fin 3,
        j.val = (i.val + 1) % 3 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))} = 2) ∧
      (∀ f : Fin 4, Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 3, d = w (fv f i) - w (fv f j)}) ≤ 2) ∧
      (∀ f : Fin 4, ∃ n : EuclideanSpace ℝ (Fin 3), ∃ c : ℝ,
        n ≠ 0 ∧ (∀ x ∈ b, inner (𝕜 := ℝ) n x ≤ c) ∧
        (∀ i : Fin 3, inner (𝕜 := ℝ) n (w (fv f i)) = c)) ∧
      (∀ e₁ e₂ : Fin 6, (ee e₁ = ee e₂ ∨ ee e₁ = (ee e₂).swap) → e₁ = e₂) ∧
      (∀ f₁ f₂ : Fin 4, Set.range (fv f₁) = Set.range (fv f₂) → f₁ = f₂) ∧
      (∀ e : Fin 6, convexHull ℝ {w (ee e).1, w (ee e).2} ⊆ frontier b) ∧
      (∀ f : Fin 4, convexHull ℝ (w '' Set.range (fv f)) ⊆ frontier b) ∧
      (∀ x ∈ frontier b, ∃ f : Fin 4,
        x ∈ convexHull ℝ (w '' Set.range (fv f))) ∧
      (∀ v : Fin 4, Set.ncard {f : Fin 4 | ∃ i : Fin 3, fv f i = v} = 3) ∧
      2 * 6 = 3 * 4 ∧ 2 * 6 = 3 * 4 ∧ (4 : ℤ) - (6 : ℤ) + (4 : ℤ) = 2) ∧
    (∃ (w : Fin 8 → EuclideanSpace ℝ (Fin 3)) (ee : Fin 12 → Fin 8 × Fin 8)
      (fv : Fin 6 → Fin 4 → Fin 8) (b : Set (EuclideanSpace ℝ (Fin 3)))
      (ll dd : ℝ),
      0 < ll ∧ 0 < dd ∧
      b = convexHull ℝ (Set.range w) ∧
      Convex ℝ b ∧
      (∀ v : Fin 8, w v ∈ frontier b) ∧
      (∀ v : Fin 8, w v ∉ convexHull ℝ (w '' {u : Fin 8 | u ≠ v})) ∧
      (Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 8, d = w i - w j}) = 3) ∧
      (∀ e : Fin 12, dist (w (ee e).1) (w (ee e).2) = ll) ∧
      (∀ (f : Fin 6) (i j : Fin 4), j.val = (i.val + 1) % 4 →
        dist (w (fv f i)) (w (fv f j)) = ll) ∧
      (∀ (f : Fin 6) (h i j : Fin 4), h.val = (i.val + 4 - 1) % 4 →
        j.val = (i.val + 1) % 4 → dist (w (fv f h)) (w (fv f j)) = dd) ∧
      (∀ f : Fin 6, Function.Injective (fv f)) ∧
      (∀ (f : Fin 6) (k : Fin 4), w (fv f k) ∉ convexHull ℝ
        (w '' (Set.range (fv f) \ {fv f k}))) ∧
      (∀ (f : Fin 6) (i₁ j₁ i₂ j₂ : Fin 4),
        j₁.val = (i₁.val + 1) % 4 →
        j₂.val = (i₂.val + 1) % 4 →
        i₁ ≠ i₂ → i₁ ≠ j₂ → j₁ ≠ i₂ → j₁ ≠ j₂ →
        Disjoint (convexHull ℝ {w (fv f i₁), w (fv f j₁)})
          (convexHull ℝ {w (fv f i₂), w (fv f j₂)})) ∧
      (∀ (f : Fin 6) (i j : Fin 4), j.val = (i.val + 1) % 4 →
        ∃ e : Fin 12, ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i)) ∧
      (∀ e : Fin 12, ∃ f : Fin 6, ∃ i j : Fin 4,
        j.val = (i.val + 1) % 4 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))) ∧
      (∀ e : Fin 12, Set.ncard {f : Fin 6 | ∃ i j : Fin 4,
        j.val = (i.val + 1) % 4 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))} = 2) ∧
      (∀ f : Fin 6, Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 4, d = w (fv f i) - w (fv f j)}) ≤ 2) ∧
      (∀ f : Fin 6, ∃ n : EuclideanSpace ℝ (Fin 3), ∃ c : ℝ,
        n ≠ 0 ∧ (∀ x ∈ b, inner (𝕜 := ℝ) n x ≤ c) ∧
        (∀ i : Fin 4, inner (𝕜 := ℝ) n (w (fv f i)) = c)) ∧
      (∀ e₁ e₂ : Fin 12, (ee e₁ = ee e₂ ∨ ee e₁ = (ee e₂).swap) → e₁ = e₂) ∧
      (∀ f₁ f₂ : Fin 6, Set.range (fv f₁) = Set.range (fv f₂) → f₁ = f₂) ∧
      (∀ e : Fin 12, convexHull ℝ {w (ee e).1, w (ee e).2} ⊆ frontier b) ∧
      (∀ f : Fin 6, convexHull ℝ (w '' Set.range (fv f)) ⊆ frontier b) ∧
      (∀ x ∈ frontier b, ∃ f : Fin 6,
        x ∈ convexHull ℝ (w '' Set.range (fv f))) ∧
      (∀ v : Fin 8, Set.ncard {f : Fin 6 | ∃ i : Fin 4, fv f i = v} = 3) ∧
      2 * 12 = 4 * 6 ∧ 2 * 12 = 3 * 8 ∧ (8 : ℤ) - (12 : ℤ) + (6 : ℤ) = 2) ∧
    (∃ (w : Fin 6 → EuclideanSpace ℝ (Fin 3)) (ee : Fin 12 → Fin 6 × Fin 6)
      (fv : Fin 8 → Fin 3 → Fin 6) (b : Set (EuclideanSpace ℝ (Fin 3)))
      (ll dd : ℝ),
      0 < ll ∧ 0 < dd ∧
      b = convexHull ℝ (Set.range w) ∧
      Convex ℝ b ∧
      (∀ v : Fin 6, w v ∈ frontier b) ∧
      (∀ v : Fin 6, w v ∉ convexHull ℝ (w '' {u : Fin 6 | u ≠ v})) ∧
      (Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 6, d = w i - w j}) = 3) ∧
      (∀ e : Fin 12, dist (w (ee e).1) (w (ee e).2) = ll) ∧
      (∀ (f : Fin 8) (i j : Fin 3), j.val = (i.val + 1) % 3 →
        dist (w (fv f i)) (w (fv f j)) = ll) ∧
      (∀ (f : Fin 8) (h i j : Fin 3), h.val = (i.val + 3 - 1) % 3 →
        j.val = (i.val + 1) % 3 → dist (w (fv f h)) (w (fv f j)) = dd) ∧
      (∀ f : Fin 8, Function.Injective (fv f)) ∧
      (∀ (f : Fin 8) (k : Fin 3), w (fv f k) ∉ convexHull ℝ
        (w '' (Set.range (fv f) \ {fv f k}))) ∧
      (∀ (f : Fin 8) (i₁ j₁ i₂ j₂ : Fin 3),
        j₁.val = (i₁.val + 1) % 3 →
        j₂.val = (i₂.val + 1) % 3 →
        i₁ ≠ i₂ → i₁ ≠ j₂ → j₁ ≠ i₂ → j₁ ≠ j₂ →
        Disjoint (convexHull ℝ {w (fv f i₁), w (fv f j₁)})
          (convexHull ℝ {w (fv f i₂), w (fv f j₂)})) ∧
      (∀ (f : Fin 8) (i j : Fin 3), j.val = (i.val + 1) % 3 →
        ∃ e : Fin 12, ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i)) ∧
      (∀ e : Fin 12, ∃ f : Fin 8, ∃ i j : Fin 3,
        j.val = (i.val + 1) % 3 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))) ∧
      (∀ e : Fin 12, Set.ncard {f : Fin 8 | ∃ i j : Fin 3,
        j.val = (i.val + 1) % 3 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))} = 2) ∧
      (∀ f : Fin 8, Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 3, d = w (fv f i) - w (fv f j)}) ≤ 2) ∧
      (∀ f : Fin 8, ∃ n : EuclideanSpace ℝ (Fin 3), ∃ c : ℝ,
        n ≠ 0 ∧ (∀ x ∈ b, inner (𝕜 := ℝ) n x ≤ c) ∧
        (∀ i : Fin 3, inner (𝕜 := ℝ) n (w (fv f i)) = c)) ∧
      (∀ e₁ e₂ : Fin 12, (ee e₁ = ee e₂ ∨ ee e₁ = (ee e₂).swap) → e₁ = e₂) ∧
      (∀ f₁ f₂ : Fin 8, Set.range (fv f₁) = Set.range (fv f₂) → f₁ = f₂) ∧
      (∀ e : Fin 12, convexHull ℝ {w (ee e).1, w (ee e).2} ⊆ frontier b) ∧
      (∀ f : Fin 8, convexHull ℝ (w '' Set.range (fv f)) ⊆ frontier b) ∧
      (∀ x ∈ frontier b, ∃ f : Fin 8,
        x ∈ convexHull ℝ (w '' Set.range (fv f))) ∧
      (∀ v : Fin 6, Set.ncard {f : Fin 8 | ∃ i : Fin 3, fv f i = v} = 4) ∧
      2 * 12 = 3 * 8 ∧ 2 * 12 = 4 * 6 ∧ (6 : ℤ) - (12 : ℤ) + (8 : ℤ) = 2) ∧
    (∃ (w : Fin 20 → EuclideanSpace ℝ (Fin 3)) (ee : Fin 30 → Fin 20 × Fin 20)
      (fv : Fin 12 → Fin 5 → Fin 20) (b : Set (EuclideanSpace ℝ (Fin 3)))
      (ll dd : ℝ),
      0 < ll ∧ 0 < dd ∧
      b = convexHull ℝ (Set.range w) ∧
      Convex ℝ b ∧
      (∀ v : Fin 20, w v ∈ frontier b) ∧
      (∀ v : Fin 20, w v ∉ convexHull ℝ (w '' {u : Fin 20 | u ≠ v})) ∧
      (Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 20, d = w i - w j}) = 3) ∧
      (∀ e : Fin 30, dist (w (ee e).1) (w (ee e).2) = ll) ∧
      (∀ (f : Fin 12) (i j : Fin 5), j.val = (i.val + 1) % 5 →
        dist (w (fv f i)) (w (fv f j)) = ll) ∧
      (∀ (f : Fin 12) (h i j : Fin 5), h.val = (i.val + 5 - 1) % 5 →
        j.val = (i.val + 1) % 5 → dist (w (fv f h)) (w (fv f j)) = dd) ∧
      (∀ f : Fin 12, Function.Injective (fv f)) ∧
      (∀ (f : Fin 12) (k : Fin 5), w (fv f k) ∉ convexHull ℝ
        (w '' (Set.range (fv f) \ {fv f k}))) ∧
      (∀ (f : Fin 12) (i₁ j₁ i₂ j₂ : Fin 5),
        j₁.val = (i₁.val + 1) % 5 →
        j₂.val = (i₂.val + 1) % 5 →
        i₁ ≠ i₂ → i₁ ≠ j₂ → j₁ ≠ i₂ → j₁ ≠ j₂ →
        Disjoint (convexHull ℝ {w (fv f i₁), w (fv f j₁)})
          (convexHull ℝ {w (fv f i₂), w (fv f j₂)})) ∧
      (∀ (f : Fin 12) (i j : Fin 5), j.val = (i.val + 1) % 5 →
        ∃ e : Fin 30, ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i)) ∧
      (∀ e : Fin 30, ∃ f : Fin 12, ∃ i j : Fin 5,
        j.val = (i.val + 1) % 5 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))) ∧
      (∀ e : Fin 30, Set.ncard {f : Fin 12 | ∃ i j : Fin 5,
        j.val = (i.val + 1) % 5 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))} = 2) ∧
      (∀ f : Fin 12, Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 5, d = w (fv f i) - w (fv f j)}) ≤ 2) ∧
      (∀ f : Fin 12, ∃ n : EuclideanSpace ℝ (Fin 3), ∃ c : ℝ,
        n ≠ 0 ∧ (∀ x ∈ b, inner (𝕜 := ℝ) n x ≤ c) ∧
        (∀ i : Fin 5, inner (𝕜 := ℝ) n (w (fv f i)) = c)) ∧
      (∀ e₁ e₂ : Fin 30, (ee e₁ = ee e₂ ∨ ee e₁ = (ee e₂).swap) → e₁ = e₂) ∧
      (∀ f₁ f₂ : Fin 12, Set.range (fv f₁) = Set.range (fv f₂) → f₁ = f₂) ∧
      (∀ e : Fin 30, convexHull ℝ {w (ee e).1, w (ee e).2} ⊆ frontier b) ∧
      (∀ f : Fin 12, convexHull ℝ (w '' Set.range (fv f)) ⊆ frontier b) ∧
      (∀ x ∈ frontier b, ∃ f : Fin 12,
        x ∈ convexHull ℝ (w '' Set.range (fv f))) ∧
      (∀ v : Fin 20, Set.ncard {f : Fin 12 | ∃ i : Fin 5, fv f i = v} = 3) ∧
      2 * 30 = 5 * 12 ∧ 2 * 30 = 3 * 20 ∧ (20 : ℤ) - (30 : ℤ) + (12 : ℤ) = 2) ∧
    (∃ (w : Fin 12 → EuclideanSpace ℝ (Fin 3)) (ee : Fin 30 → Fin 12 × Fin 12)
      (fv : Fin 20 → Fin 3 → Fin 12) (b : Set (EuclideanSpace ℝ (Fin 3)))
      (ll dd : ℝ),
      0 < ll ∧ 0 < dd ∧
      b = convexHull ℝ (Set.range w) ∧
      Convex ℝ b ∧
      (∀ v : Fin 12, w v ∈ frontier b) ∧
      (∀ v : Fin 12, w v ∉ convexHull ℝ (w '' {u : Fin 12 | u ≠ v})) ∧
      (Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 12, d = w i - w j}) = 3) ∧
      (∀ e : Fin 30, dist (w (ee e).1) (w (ee e).2) = ll) ∧
      (∀ (f : Fin 20) (i j : Fin 3), j.val = (i.val + 1) % 3 →
        dist (w (fv f i)) (w (fv f j)) = ll) ∧
      (∀ (f : Fin 20) (h i j : Fin 3), h.val = (i.val + 3 - 1) % 3 →
        j.val = (i.val + 1) % 3 → dist (w (fv f h)) (w (fv f j)) = dd) ∧
      (∀ f : Fin 20, Function.Injective (fv f)) ∧
      (∀ (f : Fin 20) (k : Fin 3), w (fv f k) ∉ convexHull ℝ
        (w '' (Set.range (fv f) \ {fv f k}))) ∧
      (∀ (f : Fin 20) (i₁ j₁ i₂ j₂ : Fin 3),
        j₁.val = (i₁.val + 1) % 3 →
        j₂.val = (i₂.val + 1) % 3 →
        i₁ ≠ i₂ → i₁ ≠ j₂ → j₁ ≠ i₂ → j₁ ≠ j₂ →
        Disjoint (convexHull ℝ {w (fv f i₁), w (fv f j₁)})
          (convexHull ℝ {w (fv f i₂), w (fv f j₂)})) ∧
      (∀ (f : Fin 20) (i j : Fin 3), j.val = (i.val + 1) % 3 →
        ∃ e : Fin 30, ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i)) ∧
      (∀ e : Fin 30, ∃ f : Fin 20, ∃ i j : Fin 3,
        j.val = (i.val + 1) % 3 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))) ∧
      (∀ e : Fin 30, Set.ncard {f : Fin 20 | ∃ i j : Fin 3,
        j.val = (i.val + 1) % 3 ∧
        (ee e = (fv f i, fv f j) ∨ ee e = (fv f j, fv f i))} = 2) ∧
      (∀ f : Fin 20, Module.finrank ℝ (Submodule.span ℝ {d : EuclideanSpace ℝ (Fin 3) |
        ∃ i j : Fin 3, d = w (fv f i) - w (fv f j)}) ≤ 2) ∧
      (∀ f : Fin 20, ∃ n : EuclideanSpace ℝ (Fin 3), ∃ c : ℝ,
        n ≠ 0 ∧ (∀ x ∈ b, inner (𝕜 := ℝ) n x ≤ c) ∧
        (∀ i : Fin 3, inner (𝕜 := ℝ) n (w (fv f i)) = c)) ∧
      (∀ e₁ e₂ : Fin 30, (ee e₁ = ee e₂ ∨ ee e₁ = (ee e₂).swap) → e₁ = e₂) ∧
      (∀ f₁ f₂ : Fin 20, Set.range (fv f₁) = Set.range (fv f₂) → f₁ = f₂) ∧
      (∀ e : Fin 30, convexHull ℝ {w (ee e).1, w (ee e).2} ⊆ frontier b) ∧
      (∀ f : Fin 20, convexHull ℝ (w '' Set.range (fv f)) ⊆ frontier b) ∧
      (∀ x ∈ frontier b, ∃ f : Fin 20,
        x ∈ convexHull ℝ (w '' Set.range (fv f))) ∧
      (∀ v : Fin 12, Set.ncard {f : Fin 20 | ∃ i : Fin 3, fv f i = v} = 5) ∧
      2 * 30 = 3 * 20 ∧ 2 * 30 = 5 * 12 ∧ (12 : ℤ) - (30 : ℤ) + (20 : ℤ) = 2)))

Sources

• https://en.wikipedia.org/wiki/Platonic_solid.

AbbreviationAmbient Euclidean space of the Platonic classification#✓fully proved

For a natural number \(n\), the real Euclidean space \(\mathbb{R}^n\): \(n\)-tuples of reals with the standard inner product and norm.

abbrev E (n : ℕ) := EuclideanSpace ℝ (Fin n)

Used by 10

Used byConvex polytope · Dimension of a convex polytope · Affine dimension of a set · Flag of a convex polytope · Face of a convex polytope · Regular convex polytope · Symmetry of a convex polytope · Rigid motions · Similar polytopes · Underlying set of a convex polytope

StructureConvex polytope#✓fully proved

A convex polytope in \(\mathbb{R}^n\) is given by its vertex set: a finite nonempty set \(V \subseteq \mathbb{R}^n\) that equals the set of extreme points of its convex hull \(\operatorname{conv}(V)\). The polytope itself is the convex set \(\operatorname{conv}(V)\).

structure ConvexPolytope (n : ℕ) where
  vertices : Finset (E n)
  vertices_nonempty : vertices.Nonempty
  vertices_eq_extremePoints :
    (vertices : Set (E n)) =
      Set.extremePoints ℝ (convexHull ℝ ((vertices : Set (E n))))

Uses 1 · Used by 11

Statement usesAmbient Euclidean space of the Platonic classification

Used byDimension of a convex polytope · Flag of a convex polytope · Face of a convex polytope · Full-dimensional convex polytope · Regular convex polytope · Symmetry of a convex polytope · Number of Platonic polytopes · Regular polytopes · Similarity of regular polytopes · Similar polytopes · Underlying set of a convex polytope

DefinitionUnderlying set of a convex polytope#✓fully proved

The underlying set of a convex polytope \(P\) in \(\mathbb{R}^n\) is the convex hull of its vertex set.

def toSet {n : ℕ} (P : ConvexPolytope n) : Set (E n) :=
  convexHull ℝ ((P.vertices : Set (E n)))

Uses 2 · Used by 4

Statement usesConvex polytope · Ambient Euclidean space of the Platonic classification

Used byDimension of a convex polytope · Face of a convex polytope · Symmetry of a convex polytope · Similar polytopes

DefinitionDimension of a convex polytope#✓fully proved

The dimension of a convex polytope \(P \subseteq \mathbb{R}^n\) is its affine dimension: the dimension of the real vector space spanned by the differences \(x - y\) of points \(x, y \in P\).

noncomputable def dim {n : ℕ} (P : ConvexPolytope n) : ℕ :=
  Module.finrank ℝ (vectorSpan ℝ P.toSet)

Uses 3 · Used by 1

Statement usesConvex polytope · Underlying set of a convex polytope · Ambient Euclidean space of the Platonic classification

Used byFull-dimensional convex polytope

DefinitionFull-dimensional convex polytope#✓fully proved

A convex polytope \(P \subseteq \mathbb{R}^n\) is full-dimensional if its dimension equals \(n\).

def IsFullDim {n : ℕ} (P : ConvexPolytope n) : Prop := P.dim = n

Uses 2 · Used by 1

Statement usesConvex polytope · Dimension of a convex polytope

Used byRegular convex polytope

DefinitionFace of a convex polytope#✓fully proved

A face of a convex polytope \(P \subseteq \mathbb{R}^n\) is a nonempty set of the form \(\{x \in P : \ell(y) \le \ell(x) \text{ for all } y \in P\}\) for some linear functional \(\ell\) on \(\mathbb{R}^n\), that is, the set of points where \(\ell\) attains its maximum over \(P\). Taking \(\ell = 0\) shows that \(P\) itself is a face.

def IsFace {n : ℕ} (P : ConvexPolytope n) (F : Set (E n)) : Prop :=
  IsExposed ℝ P.toSet F ∧ F.Nonempty

Uses 3 · Used by 1

Statement usesConvex polytope · Underlying set of a convex polytope · Ambient Euclidean space of the Platonic classification

Used byFlag of a convex polytope

DefinitionAffine dimension of a set#✓fully proved

For a subset \(F \subseteq \mathbb{R}^n\), its affine dimension is the dimension of the real vector space spanned by the differences \(x - y\) with \(x, y \in F\). The empty set and every single point get dimension \(0\).

noncomputable def faceDim {n : ℕ} (F : Set (E n)) : ℕ :=
  Module.finrank ℝ (vectorSpan ℝ F)

Uses 1 · Used by 1

Statement usesAmbient Euclidean space of the Platonic classification

Used byFlag of a convex polytope

StructureFlag of a convex polytope#✓fully proved

A flag of a convex polytope \(P \subseteq \mathbb{R}^n\) is a sequence \(F_0, F_1, \dots, F_{n-1}\) of faces of \(P\) such that each \(F_k\) has affine dimension \(k\) and \(F_i \subsetneq F_j\) whenever \(i < j\).

The definition applies to every \(P\); it is used for full-dimensional \(P\).

structure Flag {n : ℕ} (P : ConvexPolytope n) where
  face : Fin n → Set (E n)
  isFace : ∀ k, P.IsFace (face k)
  dim_eq : ∀ k : Fin n, faceDim (face k) = k.val
  strict_mono : ∀ i j : Fin n, i < j → face i ⊂ face j

Uses 4 · Used by 1

Statement usesConvex polytope · Face of a convex polytope · Affine dimension of a set · Ambient Euclidean space of the Platonic classification

Used byRegular convex polytope

AbbreviationRigid motions#✓fully proved

The rigid motions of \(\mathbb{R}^n\) are the affine isometric bijections \(\mathbb{R}^n \to \mathbb{R}^n\).

abbrev Isom (n : ℕ) := E n ≃ᵃⁱ[ℝ] E n

Uses 1 · Used by 3

Statement usesAmbient Euclidean space of the Platonic classification

Used byRegular convex polytope · Symmetry of a convex polytope · Similar polytopes

DefinitionSymmetry of a convex polytope#✓fully proved

An affine isometry \(\varphi\) of \(\mathbb{R}^n\) is a symmetry of a convex polytope \(P \subseteq \mathbb{R}^n\) if \(\varphi(P) = P\).

def isSymmetry {n : ℕ} (P : ConvexPolytope n) (φ : Isom n) : Prop :=
  ((φ : E n → E n)) '' P.toSet = P.toSet

Uses 4 · Used by 1

Statement usesConvex polytope · Rigid motions · Underlying set of a convex polytope · Ambient Euclidean space of the Platonic classification

Used byRegular convex polytope

DefinitionRegular convex polytope#✓fully proved

A convex polytope \(P \subseteq \mathbb{R}^n\) is regular (Platonic) if it is full-dimensional and for any two flags \((F_0, \dots, F_{n-1})\) and \((G_0, \dots, G_{n-1})\) of \(P\) there is an affine isometry \(\varphi\) of \(\mathbb{R}^n\) with \(\varphi(P) = P\) and \(\varphi(F_k) = G_k\) for every \(k < n\).

def IsRegular {n : ℕ} (P : ConvexPolytope n) : Prop :=
  P.IsFullDim ∧
    ∀ F G : P.Flag, ∃ φ : Isom n,
      P.isSymmetry φ ∧
        ∀ k : Fin n, ((φ : E n → E n)) '' F.face k = G.face k

Uses 6 · Used by 1

Statement usesConvex polytope · Flag of a convex polytope · Full-dimensional convex polytope · Rigid motions · Symmetry of a convex polytope · Ambient Euclidean space of the Platonic classification

Used byRegular polytopes

DefinitionSimilar polytopes#✓fully proved

Two convex polytopes \(P\) and \(Q\) in \(\mathbb{R}^n\) are similar when there are a real number \(a > 0\) and an affine isometry \(\varphi\) of \(\mathbb{R}^n\) such that the underlying set of \(Q\) is \(\{a\,\varphi(x) : x \in P\}\).

def Similar {n : ℕ} (P Q : ConvexPolytope n) : Prop :=
  ∃ a : ℝ, 0 < a ∧ ∃ φ : Isom n,
    Q.toSet = (fun x : E n => a • x) '' ((φ : E n → E n) '' P.toSet)

Uses 4 · Used by 1

Statement usesConvex polytope · Rigid motions · Underlying set of a convex polytope · Ambient Euclidean space of the Platonic classification

Used bySimilarity of regular polytopes

DefinitionRegular polytopes#✓fully proved

For \(d \in \mathbb{N}\), this is the set of regular (Platonic) convex polytopes in \(\mathbb{R}^d\): the convex polytopes in \(\mathbb{R}^d\) that are full-dimensional and whose symmetry group acts transitively on their flags.

def regularPolytopes (d : ℕ) : Set (ConvexPolytope d) :=
  {P | P.IsRegular}

Uses 2 · Used by 2

Statement usesConvex polytope · Regular convex polytope

Used byNumber of Platonic polytopes · Similarity of regular polytopes

DefinitionSimilarity of regular polytopes#✓fully proved

For regular convex polytopes \(P\) and \(Q\) in \(\mathbb{R}^d\), \(P\) is related to \(Q\) when they are similar as convex polytopes, that is, when there are a real number \(a > 0\) and an affine isometry \(\varphi\) of \(\mathbb{R}^d\) such that the underlying set of \(Q\) is \(\{a\,\varphi(x) : x \in P\}\).

def regularSimilar (d : ℕ) (P Q : regularPolytopes d) : Prop :=
  ConvexPolytope.Similar (P : ConvexPolytope d) (Q : ConvexPolytope d)

Uses 3 · Used by 1

Statement usesConvex polytope · Similar polytopes · Regular polytopes

Used byNumber of Platonic polytopes

DefinitionNumber of Platonic polytopes#✓fully proved

For \(d \in \mathbb{N}\), \(p_d \in \mathbb{N} \cup \{\infty\}\) is the number of similarity classes of regular convex polytopes in \(\mathbb{R}^d\), with \(p_d = \infty\) when there are infinitely many classes.

noncomputable def platonicCount (d : ℕ) : ℕ∞ :=
  Set.encard {S : Set (regularPolytopes d) |
    ∃ P, S = {Q : regularPolytopes d | regularSimilar d P Q}}

Uses 3 · Used by 1

Statement usesConvex polytope · Regular polytopes · Similarity of regular polytopes

Used byClassification of the Platonic polytopes

TheoremClassification of the Platonic polytopes#●ready to prove

For \(d \in \mathbb{N}\) let \(p_d \in \mathbb{N} \cup \{\infty\}\) be the number of regular convex polytopes in \(\mathbb{R}^d\) up to similarity. Then \(p_2 = \infty\), \(p_3 = 5\), \(p_4 = 6\), and \(p_d = 3\) for every \(d \ge 5\).

public theorem_wanted platonic_classification :
    platonicCount 2 = ⊤ ∧
      platonicCount 3 = 5 ∧
        platonicCount 4 = 6 ∧
          ∀ d, 5 ≤ d → platonicCount d = 3

Sources

• Euclid, Elements, Book XIII (~300 BC, p_3 = 5); L. Schläfli, Theorie der vielfachen Kontinuität (1852, posthumous publication; p_4 = 6, p_d = 3 for d ≥ 5). Listed as §42 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem platonic_classification of the lean-eval benchmark.

Uses 1

Statement usesNumber of Platonic polytopes

16 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.