The point (a, b) represents (a+b/2, sqrt(3)*b/2) in the Euclidean plane. The product norm on Real × Real is deliberately NOT used for lengths. All triangles below include their boundary and interior. Degenerate triangles are allowed, so the eventual statement also includes common side zero.

@[reducible, inline]

abbrev ConwaySoifer.Point : Type

Planar coordinates; Euclidean lengths use the quadratic form described in this module.

Equations

• ConwaySoifer.Point = (ℝ × ℝ)

def ConwaySoifer.sqDist (p q : Point) : ℝ

Squared Euclidean distance in the coordinate system described in this module.

Equations

• ConwaySoifer.sqDist p q = (p.1 - q.1) ^ 2 + (p.1 - q.1) * (p.2 - q.2) + (p.2 - q.2) ^ 2

def ConwaySoifer.target : Set Point

The filled equilateral target of side three in triangular coordinates.

Equations

• ConwaySoifer.target = {p : ConwaySoifer.Point | p.1 ≤ 1 ∧ p.2 ≤ 1 ∧ -1 ≤ p.1 + p.2}

def ConwaySoifer.hexagon : Set Point

The closed central unit hexagon in triangular coordinates.

Equations

• ConwaySoifer.hexagon = {p : ConwaySoifer.Point | |p.1| ≤ 1 ∧ |p.2| ≤ 1 ∧ |p.1 + p.2| ≤ 1}

def ConwaySoifer.vertex : Fin 6 → Point

The six cyclic vertices of the unit hexagon.

Equations

• ConwaySoifer.vertex = ![(1, 0), (0, 1), (-1, 1), (-1, 0), (0, -1), (1, -1)]

def ConwaySoifer.corner : Fin 3 → Point

The three vertices of the side-three target.

Equations

• ConwaySoifer.corner = ![(1, 1), (-2, 1), (1, -2)]

def ConwaySoifer.anchor : Fin 10 → Point

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

Equations

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

structure ConwaySoifer.EquilateralTriangle : Type

Three equidistant vertices with a nonnegative side length; the carrier is their closed hull.

• vertices : Fin 3 → Point

  The three triangle vertices.

• side : ℝ

  The common side length.

• side_nonneg : 0 ≤ self.side
• equilateral (i j : Fin 3) : i ≠ j → sqDist (self.vertices i) (self.vertices j) = self.side ^ 2

def ConwaySoifer.EquilateralTriangle.carrier (T : EquilateralTriangle) : Set Point

The filled closed convex hull of the three triangle vertices.

Equations

• T.carrier = (convexHull ℝ) (Set.range T.vertices)

@[reducible, inline]

abbrev ConwaySoifer.Configuration : Type

The finite family of covering triangles used by this module.

Equations

• ConwaySoifer.Configuration = (Fin 10 → ConwaySoifer.EquilateralTriangle)

def ConwaySoifer.Covers (T : Configuration) : Prop

Every point of the side-three target lies in at least one covering triangle.

Equations

• ConwaySoifer.Covers T = ∀ p ∈ ConwaySoifer.target, ∃ (i : Fin 10), p ∈ (T i).carrier

def ConwaySoifer.CommonSide (T : Configuration) (r : ℝ) : Prop

Every covering triangle has the specified common side length.

Equations

• ConwaySoifer.CommonSide T r = ∀ (i : Fin 10), (T i).side = r

def ConwaySoifer.LowerBound : Prop

This is the actual target proposition, not a claim that it has been proved.

Equations

• ConwaySoifer.LowerBound = ∀ (r : ℝ) (T : ConwaySoifer.Configuration), ConwaySoifer.CommonSide T r → ConwaySoifer.Covers T → 1 ≤ r

def ConwaySoifer.ExcludesSubunit (S : Set Point) : Prop

No equilateral triangle of side below one contains the given set.

Equations

• ConwaySoifer.ExcludesSubunit S = ∀ (T : ConwaySoifer.EquilateralTriangle), T.side < 1 → ¬S ⊆ T.carrier

theorem ConwaySoifer.sqDist_nonneg (p q : Point) : 0 ≤ sqDist p q

theorem ConwaySoifer.sqDist_comm (p q : Point) : sqDist p q = sqDist q p

theorem ConwaySoifer.sqDist_smul (a : ℝ) (p q : Point) : sqDist (a • p) (a • q) = a ^ 2 * sqDist p q

noncomputable def ConwaySoifer.toOblique (p : Point) : Point

Conversion to the oblique coordinates of the upstream SevenTriangles library.

Equations

• ConwaySoifer.toOblique p = (p.1 + p.2 / 2, p.2)

theorem ConwaySoifer.sqDist_toOblique (p q : Point) : ((toOblique p).1 - (toOblique q).1) ^ 2 + 3 / 4 * ((toOblique p).2 - (toOblique q).2) ^ 2 = sqDist p q

theorem ConwaySoifer.hexagon_subset_target : hexagon ⊆ target

theorem ConwaySoifer.anchor_mem_target (i : Fin 10) : anchor i ∈ target

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

def ConwaySoifer.targetTriangle : EquilateralTriangle

Sanity check: the target is the filled equilateral triangle of side three.

Equations

• ConwaySoifer.targetTriangle = { vertices := ConwaySoifer.corner, side := 3, side_nonneg := ConwaySoifer.targetTriangle._proof_1, equilateral := ConwaySoifer.targetTriangle._proof_4 }