SideChains

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

theorem ConwaySoifer.Canonical.s_nonOverfull_simplified {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) (hs : s ≤ 1 / 10) (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_simplified {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) (hs : s ≤ 1 / 10) (i : Fin 6) (hi : i ≠ recvOf c) (j : Fin 3) (m : Fin 2) : cornerMid j m ∉ (T (sideIndex i)).carrier

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

theorem ConwaySoifer.Canonical.centre_far_simplified {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hs : s ≤ 1 / 3) (i : Fin 6) (dir : Bool) {t : ℝ} (ht0 : 0 < t) (ht : t ≤ 2 * s) : linePoint (vertex i) (sideDirection i dir) t ∉ (T 0).carrier

theorem ConwaySoifer.Canonical.chain_step_simplified {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hs : s ≤ 1 / 3) (i : Fin 6) (dir : Bool) (hM : rayLen (T (sideIndex i)) (vertex i) (sideDirection i dir) < 2 * s) (hA : ∀ (j : Fin 3), sideAllowed (sideOf i dir) (cornerIndex j) = true → ∀ p ∈ hexagon, p ∉ (T (cornerIndex j)).carrier) : 1 - rayLen (T (sideIndex i)) (vertex i) (sideDirection i dir) ≤ rayLen (T (sideIndex (neighbor i dir))) (vertex (neighbor i dir)) (sideDirection (neighbor i dir) !dir)

theorem ConwaySoifer.Canonical.chain_next_simplified {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hs : s ≤ 1 / 3) (i : Fin 6) (dir : Bool) (nb : Fin 6) (hnb : neighbor i dir = nb) (hM : rayLen (T (sideIndex i)) (vertex i) (sideDirection i dir) < 2 * s) (hA : ∀ (j : Fin 3), sideAllowed (sideOf i dir) (cornerIndex j) = true → ∀ p ∈ hexagon, p ∉ (T (cornerIndex j)).carrier) (hno : rayLen (T (sideIndex nb)) (vertex nb) (sideDirection nb false) + rayLen (T (sideIndex nb)) (vertex nb) (sideDirection nb true) ≤ r) : 1 - rayLen (T (sideIndex i)) (vertex i) (sideDirection i dir) ≤ rayLen (T (sideIndex nb)) (vertex nb) (sideDirection nb !dir) ∧ rayLen (T (sideIndex nb)) (vertex nb) (sideDirection nb dir) < rayLen (T (sideIndex i)) (vertex i) (sideDirection i dir)

One step of the chain: the next owner receives at least 1 - M and its own short section is below M.

theorem ConwaySoifer.Canonical.sint_chain_simplified {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sint T r s) (hs : s ≤ 1 / 10) (hno : ∀ (i : Fin 6), i ≠ 1 → rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true) ≤ r) (hA1 : ∀ p ∈ hexagon, p ∉ (T (cornerIndex 1)).carrier) (hA2 : ∀ p ∈ hexagon, p ∉ (T (cornerIndex 2)).carrier) : (∀ (i : Fin 6), i ≠ 1 → 1 - 2 * s < rayLen (T (sideIndex i)) (vertex i) (sideDirection i false)) ∧ 1 - rayLen (T (sideIndex 1)) (vertex 1) (sideDirection 1 true) < rayLen (T (sideIndex 0)) (vertex 0) (sideDirection 0 false)

theorem ConwaySoifer.Canonical.sext_chain_simplified {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) (hs : s ≤ 1 / 10) (hno : ∀ (i : Fin 6), i ≠ 5 → rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true) ≤ r) (hA0 : ∀ p ∈ hexagon, p ∉ (T (cornerIndex 0)).carrier) (hA1 : ∀ p ∈ hexagon, p ∉ (T (cornerIndex 1)).carrier) (hA2 : ∀ p ∈ hexagon, p ∉ (T (cornerIndex 2)).carrier) (i : Fin 6) : i ≠ 5 → 1 - 2 * s < rayLen (T (sideIndex i)) (vertex i) (sideDirection i true)