Moving the minimal side section to vertex 0

MinAt T r s i₀ r₀ records an anchored full cover of common side r < 1 whose twelve full side sections are all at least s > 0, with equality at the section of S_{i₀} towards its neighbour selected by r₀. Rotations shift i₀ by two and reflections send (i₀, r₀) to (1 - i₀, ¬r₀), so every such cover can be moved to one with the minimum at vertex 0.

noncomputable def ConwaySoifer.sideLenC (T : Configuration) (i : Fin 6) (right : Bool) : ℝ

Full length of the section of side owner i towards its neighbour.

Equations

• ConwaySoifer.sideLenC T i right = ConwaySoifer.rayLen (T (ConwaySoifer.sideIndex i)) (ConwaySoifer.vertex i) (ConwaySoifer.sideDirection i right)

structure ConwaySoifer.MinAt (T : Configuration) (r s : ℝ) (i₀ : Fin 6) (r₀ : Bool) : Prop

An anchored subunit cover with a positive minimal side section attained at one selected ray.

• common : CommonSide T r
• covers : Covers T
• r_lt : r < 1
• anchored (i : Fin 10) : anchor i ∈ (T i).carrier
• s_pos : 0 < s
• side_min (i : Fin 6) (right : Bool) : s ≤ sideLenC T i right
• attained : sideLenC T i₀ r₀ = s

theorem ConwaySoifer.MinAt.rotate {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) : MinAt T.rotate r s (i₀ + 2) r₀

theorem ConwaySoifer.MinAt.reflect {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) : MinAt T.reflect r s (1 - i₀) !r₀

theorem ConwaySoifer.MinAt.toZero {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) : ∃ (T' : Configuration) (right : Bool), MinAt T' r s 0 right

Every minimal section can be moved to vertex 0.

theorem ConwaySoifer.AnchoredCover.minAt {r : ℝ} (C : AnchoredCover r) : MinAt C.triangles r C.minimum C.minRay.1 C.minRay.2

The minimum of the twelve full sections of an anchored cover.

theorem ConwaySoifer.exists_minAt_zero (r : ℝ) (T : Configuration) (hside : CommonSide T r) (hcover : Covers T) (hr : r < 1) : ∃ (T' : Configuration) (s : ℝ) (right : Bool), MinAt T' r s 0 right

From any full cover of common side r < 1 to a cover with its minimal section at vertex 0.