Shared geometric facts for both small-case proofs; no certificate evaluations.

The receiver

theorem ConwaySoifer.minEndpoint_eq_recv (c : ContactCase) (s : ℝ) : minEndpoint c s = linePoint (vertex (recvOf c)) (sideDirection (recvOf c) !c.right) (1 - s)

theorem ConwaySoifer.Canonical.recv_mem {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) : minEndpoint c s ∈ (T (sideIndex (recvOf c))).carrier

theorem ConwaySoifer.Canonical.recv_long {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) : 1 - s ≤ rayLen (T (sideIndex (recvOf c))) (vertex (recvOf c)) (sideDirection (recvOf c) !c.right)

theorem ConwaySoifer.sqDist_sidePts (i : Fin 6) (dir : Bool) (a b : ℝ) : sqDist (linePoint (vertex i) (sideDirection i dir) a) (linePoint (vertex i) (sideDirection i !dir) b) = a ^ 2 + a * b + b ^ 2

theorem ConwaySoifer.Canonical.recv_short_lt {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) : rayLen (T (sideIndex (recvOf c))) (vertex (recvOf c)) (sideDirection (recvOf c) c.right) < 2 * s

The short section of the receiver is below 2s.

The budget

theorem ConwaySoifer.Canonical.loss_recv {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) : (1 - s) ^ 2 ≤ sideLoss T (recvOf c)

theorem ConwaySoifer.Canonical.recv_cases {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) : recvOf c = 5 ∨ recvOf c = 1

theorem ConwaySoifer.Canonical.s_budget {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) (hs : s ≤ 1 / 14) (i : Fin 6) (hi : i ≠ recvOf c) (hD : r ^ 2 / 4 ≤ sideLoss T i) : False

The budget of an S cover with s ≤ 1/14: no other side owner can lose r²/4.

theorem ConwaySoifer.Canonical.s_nonOverfull {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) (hs : s ≤ 1 / 14) (i : Fin 6) (hi : i ≠ recvOf c) : rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true) ≤ r

theorem ConwaySoifer.Canonical.s_noMid {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) (hs : s ≤ 1 / 14) (i : Fin 6) (hi : i ≠ recvOf c) (j : Fin 3) (m : Fin 2) : cornerMid j m ∉ (T (sideIndex i)).carrier

Corner owners

theorem ConwaySoifer.Canonical.sext_recv_noMid {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) (m : Fin 2) : cornerMid 2 m ∉ (T 6).carrier

In Sext the receiver S₅ is far from the midpoints of its own cell.

theorem ConwaySoifer.Canonical.corner_mids {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (j : Fin 3) (m : Fin 2) (h0 : cornerMid j m ∉ (T (sideIndex ⟨2 * ↑j, ⋯⟩)).carrier) (h1 : cornerMid j m ∉ (T (sideIndex ⟨2 * ↑j + 1, ⋯⟩)).carrier) : cornerMid j m ∈ (T (cornerIndex j)).carrier

A corner midpoint not in either adjacent side owner belongs to the corner owner.

theorem ConwaySoifer.Canonical.s_corner_mids {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) (hs : s ≤ 1 / 14) (j : Fin 3) (hj : c = ContactCase.Sint → j ≠ 0) (m : Fin 2) : cornerMid j m ∈ (T (cornerIndex j)).carrier

Every corner owner except A₀ of Sint contains both its external midpoints.

theorem ConwaySoifer.hexagon_cross_base (j : Fin 3) {p : Point} (hp : p ∈ hexagon) : ∃ (u : ℝ) (lam : ℝ), 0 ≤ u ∧ u ≤ 1 ∧ 0 ≤ lam ∧ lam ≤ 1 ∧ corner j + lam • (p - corner j) = linePoint (vertex ⟨2 * ↑j, ⋯⟩) (sideDirection ⟨2 * ↑j, ⋯⟩ true) u

The segment from the corner to a hexagon point crosses the base of the cell.

theorem ConwaySoifer.coreVertex_mem_of_le {s : ℝ} {C : Set Point} (hC : Convex ℝ C) (h0 : 0 ∈ C) (hK : ∀ (j : Fin 6), coreVertex s j ∈ C) (hs0 : 0 < s) (hs : s ≤ 1 / 2) {u : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ s) (j : Fin 6) : coreVertex u j ∈ C

Every smaller central core vertex lies in a convex set containing the original core and zero.

theorem ConwaySoifer.sidePoint_flip (i : Fin 6) (dir : Bool) (t : ℝ) : linePoint (vertex i) (sideDirection i dir) t = linePoint (vertex (neighbor i dir)) (sideDirection (neighbor i dir) !dir) (1 - t)

theorem ConwaySoifer.sidePoint_mem_hexagon (i : Fin 6) (dir : Bool) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : linePoint (vertex i) (sideDirection i dir) t ∈ hexagon

def ConwaySoifer.sideOf (i : Fin 6) (dir : Bool) : Fin 6

The hexagon side containing the ray from vertex i in direction dir.

Equations

• ConwaySoifer.sideOf i dir = if dir = true then i else i + 5

theorem ConwaySoifer.Canonical.sidePoint_allowed {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (i : Fin 6) (dir : Bool) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) {k : Fin 10} (hk : linePoint (vertex i) (sideDirection i dir) t ∈ (T k).carrier) : sideAllowed (sideOf i dir) k = true

theorem ConwaySoifer.sideAllowed_cases (i : Fin 6) (dir : Bool) (k : Fin 10) (hk : sideAllowed (sideOf i dir) k = true) : k = 0 ∨ k = sideIndex i ∨ k = sideIndex (neighbor i dir) ∨ ∃ (j : Fin 3), k = cornerIndex j ∧ sideAllowed (sideOf i dir) (cornerIndex j) = true

The backward transfer