Locality: which owners can meet a boundary segment

Every anchor other than the listed ones is at squared distance at least 1 from every point of the segment, so its owner (a closed triangle of side < 1) cannot contain any point of the segment. Hexagon side i runs from vertex i to vertex (i+1); its admissible owners are the centre, S_i, S_{i+1} and, for even i, the corner owner A_{i/2}. The corner segment from corner j to vertex (2j+m) admits A_j, S_{2j}, S_{2j+1}. This is the content of proof/verify_locality.py.

def ConwaySoifer.sideAllowed (i : Fin 6) (k : Fin 10) : Bool

Admissible owners of hexagon side i.

Equations

• ConwaySoifer.sideAllowed i k = (decide (k = 0) || decide (k = ConwaySoifer.sideIndex i) || decide (k = ConwaySoifer.sideIndex (i + 1)) || decide (↑i % 2 = 0) && decide (↑k = 7 + ↑i / 2))

def ConwaySoifer.cornerAllowed (j : Fin 3) (k : Fin 10) : Bool

Admissible owners of the corner segments of cell j.

Equations

• ConwaySoifer.cornerAllowed j k = (decide (k = ConwaySoifer.cornerIndex j) || decide (↑k = 2 * ↑j + 1) || decide (↑k = 2 * ↑j + 2))

theorem ConwaySoifer.anchor_far_from_side (i : Fin 6) (k : Fin 10) (hk : sideAllowed i k = false) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 1 ≤ sqDist (anchor k) (linePoint (vertex i) (sideDirection i true) t)

theorem ConwaySoifer.anchor_far_from_cornerSeg (j : Fin 3) (m : Fin 2) (k : Fin 10) (hk : cornerAllowed j k = false) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 1 ≤ sqDist (anchor k) (linePoint (corner j) (cornerDirection j m) t)

theorem ConwaySoifer.side_owner_allowed {T : Configuration} {r : ℝ} (hcommon : CommonSide T r) (hr : r < 1) (hanch : ∀ (i : Fin 10), anchor i ∈ (T i).carrier) (i : Fin 6) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) {k : Fin 10} (hk : linePoint (vertex i) (sideDirection i true) t ∈ (T k).carrier) : sideAllowed i k = true

A point of hexagon side i can only belong to an admissible owner.

theorem ConwaySoifer.cornerSeg_owner_allowed {T : Configuration} {r : ℝ} (hcommon : CommonSide T r) (hr : r < 1) (hanch : ∀ (i : Fin 10), anchor i ∈ (T i).carrier) (j : Fin 3) (m : Fin 2) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) {k : Fin 10} (hk : linePoint (corner j) (cornerDirection j m) t ∈ (T k).carrier) : cornerAllowed j k = true

A point of a corner segment of cell j can only belong to an admissible owner.

theorem ConwaySoifer.cornerSeg_mem_target (j : Fin 3) (m : Fin 2) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : linePoint (corner j) (cornerDirection j m) t ∈ target

Points of the corner segments lie in the target triangle.