Diameter bounds for the filled convex hull, in the project's Euclidean coordinates.

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

theorem ConwaySoifer.SevenTriangles.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

Convexification does not increase a bound on squared pairwise distances.

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

theorem ConwaySoifer.SevenTriangles.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

noncomputable def ConwaySoifer.SevenTriangles.anchor : Fin 7 → Point

The centre and boundary vertices used to assign distinct covering owners.

Equations

• ConwaySoifer.SevenTriangles.anchor = ![(0, 0), (1, 0), (1 / 2, 1), (-1 / 2, 1), (-1, 0), (-1 / 2, -1), (1 / 2, -1)]

theorem ConwaySoifer.SevenTriangles.anchor_mem_hexagon (i : Fin 7) : anchor i ∈ unitHexagon

theorem ConwaySoifer.SevenTriangles.anchors_separated (i j : Fin 7) (h : i ≠ j) : 1 ≤ sqDist (anchor i) (anchor j)

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

Seven anchors have seven distinct owners in every hypothetical subunit cover.