--- /dev/null
+++ b/Mathlib/Unsorry/PlatonicSchlafliCore.lean
@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2026 Chris Barlow. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Barlow
+-/
+
+
+theorem platonic_schlafli_pairs (p q : ℕ) (hp : 3 ≤ p) (hq : 3 ≤ q)
+    (h : (p : ℚ)⁻¹ + (q : ℚ)⁻¹ > 2⁻¹) :
+    (p, q) ∈ ({(3,3),(3,4),(4,3),(3,5),(5,3)} : Finset (ℕ × ℕ)) :=
+  platonic_schlafli_pairs_of_bounds p q hp hq
+    (platonic_schlafli_fst_lt_six p q hp hq h)
+    (platonic_schlafli_snd_lt_six p q hp hq h) h