The convexification argument is adapted from SevenTriangles.Geometry.Diameter, commit b17ca52a395519f43fc15f83fb49a5dd69996225, to triangular coordinates, ten anchors, and possibly degenerate triangles.

theorem ConwaySoifer.convex_sqDist_sublevel (q : Point) (s : ℝ) : Convex ℝ {p : Point | sqDist p q ≤ s}

theorem ConwaySoifer.sqDist_convexHull_le (S : Set Point) (s : ℝ) (h : ∀ p ∈ S, ∀ q ∈ S, sqDist p q ≤ s) {p q : Point} (hp : p ∈ (convexHull ℝ) S) (hq : q ∈ (convexHull ℝ) S) : sqDist p q ≤ s

theorem ConwaySoifer.EquilateralTriangle.sqDist_le (T : EquilateralTriangle) {p q : Point} (hp : p ∈ T.carrier) (hq : q ∈ T.carrier) : sqDist p q ≤ T.side ^ 2

theorem ConwaySoifer.EquilateralTriangle.cannot_contain_unit_chord (T : EquilateralTriangle) (hs : T.side < 1) {p q : Point} (hpq : 1 ≤ sqDist p q) (hp : p ∈ T.carrier) (hq : q ∈ T.carrier) : False

theorem ConwaySoifer.exists_anchor_owners (r : ℝ) (T : Configuration) (hs : ∀ (i : Fin 10), (T i).side ≤ r) (hr : r < 1) (hc : Covers T) : ∃ (owner : Fin 10 → Fin 10), Function.Bijective owner ∧ ∀ (i : Fin 10), anchor i ∈ (T (owner i)).carrier

theorem ConwaySoifer.anchor_owner_unique (r : ℝ) (T : Configuration) (hs : ∀ (i : Fin 10), (T i).side ≤ r) (hr : r < 1) (owner : Fin 10 → Fin 10) (hbij : Function.Bijective owner) (howner : ∀ (i : Fin 10), anchor i ∈ (T (owner i)).carrier) (i j : Fin 10) (hmem : anchor i ∈ (T j).carrier) : j = owner i