AownChains

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

theorem ConwaySoifer.Simplified.aown_absent {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) (j : Fin 3) (hj : j ≠ 0) (p : Point) (hp : p ∈ hexagon) : p ∉ (T (cornerIndex j)).carrier

theorem ConwaySoifer.Simplified.aown_double_next {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) (i : Fin 6) (d : Bool) (hi : i ≠ 0) (hA : ∀ (j : Fin 3), sideAllowed (sideOf i d) (cornerIndex j) = true → j ≠ 0) (hprev : 2 * s ≤ rayLen (T (sideIndex i)) (vertex i) (sideDirection i !d)) : 2 * s ≤ rayLen (T (sideIndex (neighbor i d))) (vertex (neighbor i d)) (sideDirection (neighbor i d) !d)

theorem ConwaySoifer.Simplified.aown_seed1 {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : 2 * s ≤ rayLen (T (sideIndex 1)) (vertex 1) (sideDirection 1 false)

theorem ConwaySoifer.Simplified.aown_seed5 {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : 2 * s ≤ rayLen (T (sideIndex 5)) (vertex 5) (sideDirection 5 true)

theorem ConwaySoifer.Simplified.aown_double {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) (i : Fin 6) (hi : i ≠ 0) (d : Bool) : 2 * s ≤ rayLen (T (sideIndex i)) (vertex i) (sideDirection i d)