Rational coordinates for the covering problem

(x, z) represents the Euclidean point (x, sqrt(3)/2 * z). The product norm on ℝ × ℝ is NOT the metric used for lengths below. All metric statements use sqDist; convexity is unchanged by this invertible linear change of coordinates. No geometric theorem is assumed as an axiom.

@[reducible, inline]

abbrev ConwaySoifer.SevenTriangles.Point : Type

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

Equations

• ConwaySoifer.SevenTriangles.Point = (ℝ × ℝ)

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

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

Equations

• ConwaySoifer.SevenTriangles.sqDist p q = (p.1 - q.1) ^ 2 + 3 / 4 * (p.2 - q.2) ^ 2

noncomputable def ConwaySoifer.SevenTriangles.rotate60 (p : Point) : Point

Rotation through 60 degrees in oblique coordinates.

Equations

• ConwaySoifer.SevenTriangles.rotate60 p = (p.1 / 2 - 3 * p.2 / 4, p.1 + p.2 / 2)

noncomputable def ConwaySoifer.SevenTriangles.vertex (i : Fin 6) : Point

The six cyclic vertices of the unit hexagon.

Equations

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

def ConwaySoifer.SevenTriangles.unitHexagon : Set Point

The closed regular unit hexagon in oblique coordinates.

Equations

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

def ConwaySoifer.SevenTriangles.previous (i : Fin 6) : Fin 6

The preceding vertex index in the cyclic hexagon order.

Equations

• ConwaySoifer.SevenTriangles.previous i = i + 5

def ConwaySoifer.SevenTriangles.next (i : Fin 6) : Fin 6

The following vertex index in the cyclic hexagon order.

Equations

• ConwaySoifer.SevenTriangles.next i = i + 1

noncomputable def ConwaySoifer.SevenTriangles.boundaryPoint (i : Fin 6) (t : ℝ) : Point

The affine interpolation along a unit-hexagon edge.

Equations

• ConwaySoifer.SevenTriangles.boundaryPoint i t = (1 - t) • ConwaySoifer.SevenTriangles.vertex i + t • ConwaySoifer.SevenTriangles.vertex (ConwaySoifer.SevenTriangles.next i)

structure ConwaySoifer.SevenTriangles.EquilateralTriangle : Type

A nondegenerate filled equilateral triangle, with an explicit side length.

• vertices : Fin 3 → Point

  The three triangle vertices.

• side : ℝ

  The common side length.

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

def ConwaySoifer.SevenTriangles.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.SevenTriangles.Configuration : Type

The finite family of covering triangles used by this module.

Equations

• ConwaySoifer.SevenTriangles.Configuration = (Fin 7 → ConwaySoifer.SevenTriangles.EquilateralTriangle)

def ConwaySoifer.SevenTriangles.CoversUnitHexagon (T : Configuration) : Prop

Every point of the closed unit hexagon belongs to one of the seven triangles.

Equations

• ConwaySoifer.SevenTriangles.CoversUnitHexagon T = ∀ p ∈ ConwaySoifer.SevenTriangles.unitHexagon, ∃ (i : Fin 7), p ∈ (T i).carrier

def ConwaySoifer.SevenTriangles.UnitHexagonLowerBound : Prop

The actual geometric goal. This is a proposition, not a proved theorem.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

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

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

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

theorem ConwaySoifer.SevenTriangles.rotate60_preserves_sqDist (p q : Point) : sqDist (rotate60 p) (rotate60 q) = sqDist p q

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

theorem ConwaySoifer.SevenTriangles.vertex_mem_hexagon (i : Fin 6) : vertex i ∈ unitHexagon

noncomputable def ConwaySoifer.SevenTriangles.standardSector : EquilateralTriangle

Sanity check: the geometric datatype is inhabited by a standard unit sector.

Equations

• One or more equations did not get rendered due to their size.