Owners

Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.

structure ConwaySoifer.AnchoredCover (r : ℝ) : Type

These are only the hypotheses of the proposed counterexample, with owners relabelled by their anchors. No area or certificate conclusion is a field.

• triangles : Configuration

  The ten triangles indexed by their distinguished anchors.

• common : CommonSide self.triangles r
• covers : Covers self.triangles
• subunit : r < 1
• anchored (i : Fin 10) : anchor i ∈ (self.triangles i).carrier

theorem ConwaySoifer.AnchoredCover.exists_of_cover {r : ℝ} (T : Configuration) (hside : CommonSide T r) (hcover : Covers T) (hr : r < 1) : Nonempty (AnchoredCover r)

theorem ConwaySoifer.AnchoredCover.side_eq {r : ℝ} (C : AnchoredCover r) (i : Fin 10) : (C.triangles i).side = r

theorem ConwaySoifer.AnchoredCover.nonneg {r : ℝ} (C : AnchoredCover r) : 0 ≤ r

theorem ConwaySoifer.AnchoredCover.unique_anchor {r : ℝ} (C : AnchoredCover r) (i j : Fin 10) (hi : anchor i ∈ (C.triangles j).carrier) : i = j

def ConwaySoifer.sideIndex (i : Fin 6) : Fin 10

The owner index assigned to a hexagon vertex.

Equations

• ConwaySoifer.sideIndex i = ⟨↑i + 1, ⋯⟩

def ConwaySoifer.cornerIndex (j : Fin 3) : Fin 10

The owner index assigned to a target corner.

Equations

• ConwaySoifer.cornerIndex j = ⟨↑j + 7, ⋯⟩

@[simp]

theorem ConwaySoifer.anchor_sideIndex (i : Fin 6) : anchor (sideIndex i) = vertex i

@[simp]

theorem ConwaySoifer.anchor_cornerIndex (j : Fin 3) : anchor (cornerIndex j) = corner j

def ConwaySoifer.neighbor (i : Fin 6) (right : Bool) : Fin 6

The next or previous cyclic hexagon vertex, selected by the direction flag.

Equations

• ConwaySoifer.neighbor i right = if right = true then i + 1 else i + 5

def ConwaySoifer.sideDirection (i : Fin 6) (right : Bool) : Point

The unit direction from a hexagon vertex to its selected neighbor.

Equations

• ConwaySoifer.sideDirection i right = ConwaySoifer.vertex (ConwaySoifer.neighbor i right) - ConwaySoifer.vertex i

theorem ConwaySoifer.sideDirection_unit (i : Fin 6) (right : Bool) : sqDist (sideDirection i right) (0, 0) = 1

theorem ConwaySoifer.vertex_mem_target (i : Fin 6) : vertex i ∈ target

theorem ConwaySoifer.target_convex : Convex ℝ target

theorem ConwaySoifer.sidePoint_mem_target (i : Fin 6) (right : Bool) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : linePoint (vertex i) (sideDirection i right) t ∈ target

def ConwaySoifer.AnchoredCover.sideOwner {r : ℝ} (C : AnchoredCover r) (i : Fin 6) : EquilateralTriangle

The covering triangle assigned to one hexagon vertex.

Equations

• C.sideOwner i = C.triangles (ConwaySoifer.sideIndex i)

def ConwaySoifer.AnchoredCover.cornerOwner {r : ℝ} (C : AnchoredCover r) (j : Fin 3) : EquilateralTriangle

The covering triangle assigned to one target corner.

Equations

• C.cornerOwner j = C.triangles (ConwaySoifer.cornerIndex j)

def ConwaySoifer.AnchoredCover.centre {r : ℝ} (C : AnchoredCover r) : EquilateralTriangle

The covering triangle assigned to the centre anchor.

Equations

• C.centre = C.triangles 0

theorem ConwaySoifer.AnchoredCover.side_anchor_mem {r : ℝ} (C : AnchoredCover r) (i : Fin 6) : vertex i ∈ (C.sideOwner i).carrier

theorem ConwaySoifer.AnchoredCover.corner_anchor_mem {r : ℝ} (C : AnchoredCover r) (j : Fin 3) : corner j ∈ (C.cornerOwner j).carrier

noncomputable def ConwaySoifer.AnchoredCover.sideLen {r : ℝ} (C : AnchoredCover r) (i : Fin 6) (right : Bool) : ℝ

The full contained ray section of a side owner towards a selected neighbor.

Equations

• C.sideLen i right = ConwaySoifer.rayLen (C.sideOwner i) (ConwaySoifer.vertex i) (ConwaySoifer.sideDirection i right)

theorem ConwaySoifer.AnchoredCover.sideLen_pos {r : ℝ} (C : AnchoredCover r) (i : Fin 6) (right : Bool) : 0 < C.sideLen i right

theorem ConwaySoifer.AnchoredCover.sideLen_le_side {r : ℝ} (C : AnchoredCover r) (i : Fin 6) (right : Bool) : C.sideLen i right ≤ r

theorem ConwaySoifer.AnchoredCover.pos {r : ℝ} (C : AnchoredCover r) : 0 < r

theorem ConwaySoifer.AnchoredCover.sideLen_lt_one {r : ℝ} (C : AnchoredCover r) (i : Fin 6) (right : Bool) : C.sideLen i right < 1

noncomputable def ConwaySoifer.AnchoredCover.minRay {r : ℝ} (C : AnchoredCover r) : Fin 6 × Bool

Choose an actual minimizer from the twelve full ray lengths.

Equations

• C.minRay = Classical.choose ⋯

noncomputable def ConwaySoifer.AnchoredCover.minimum {r : ℝ} (C : AnchoredCover r) : ℝ

The minimum of the twelve full side-owner ray sections.

Equations

• C.minimum = C.sideLen C.minRay.1 C.minRay.2

theorem ConwaySoifer.AnchoredCover.minimum_le {r : ℝ} (C : AnchoredCover r) (i : Fin 6) (right : Bool) : C.minimum ≤ C.sideLen i right

theorem ConwaySoifer.AnchoredCover.minimum_pos {r : ℝ} (C : AnchoredCover r) : 0 < C.minimum

theorem ConwaySoifer.AnchoredCover.minimum_lt_one {r : ℝ} (C : AnchoredCover r) : C.minimum < 1

theorem ConwaySoifer.AnchoredCover.mandatory_sidePoint {r : ℝ} (C : AnchoredCover r) (i : Fin 6) (right : Bool) : linePoint (vertex i) (sideDirection i right) C.minimum ∈ (C.sideOwner i).carrier

theorem ConwaySoifer.AnchoredCover.minRay_endpoint_mem {r : ℝ} (C : AnchoredCover r) : linePoint (vertex C.minRay.1) (sideDirection C.minRay.1 C.minRay.2) C.minimum ∈ (C.sideOwner C.minRay.1).carrier

theorem ConwaySoifer.AnchoredCover.minRay_endpoint_transfers {r : ℝ} (C : AnchoredCover r) : ∃ (j : Fin 10), j ≠ sideIndex C.minRay.1 ∧ linePoint (vertex C.minRay.1) (sideDirection C.minRay.1 C.minRay.2) C.minimum ∈ (C.triangles j).carrier