The four normalized contact cases

After the geometric normalization (owner relabelling, symmetries of T₃, choice of the minimal full section) a hypothetical cover is described by Canonical c T r s: ten anchored owners of common side r < 1, the parameter s bounding all twelve full side sections from below and attained by the section of S₀ towards v_jj (jj = 5 for Sext, 1 otherwise), the corner sections of length at least s, the adaptive core K_s ⊆ C, and the case-specific contact. SmallStrengthening records the additional necessary conditions proved for s ≤ 1/14.

Owner indices: 0 = centre C, sideIndex i = i+1 = S_i, cornerIndex j = j+7 = A_j.

def ConwaySoifer.coreDir : Fin 6 → Point

The six directions of the central hexagon 𝒦.

Equations

• ConwaySoifer.coreDir = ![(1, 1), (-1, 2), (-2, 1), (-1, -1), (1, -2), (2, -1)]

noncomputable def ConwaySoifer.coreVertex (u : ℝ) (j : Fin 6) : Point

The vertices of K_u = (u(1-u)/3) 𝒦.

Equations

• ConwaySoifer.coreVertex u j = (u * (1 - u) / 3) • ConwaySoifer.coreDir j

def ConwaySoifer.cornerDirection (j : Fin 3) (k : Fin 2) : Point

Unit direction from corner j towards vertex (2j + k).

Equations

• ConwaySoifer.cornerDirection j k = ConwaySoifer.vertex ⟨2 * ↑j + ↑k, ⋯⟩ - ConwaySoifer.corner j

theorem ConwaySoifer.cornerDirection_unit (j : Fin 3) (k : Fin 2) : sqDist (cornerDirection j k) (0, 0) = 1

noncomputable def ConwaySoifer.cornerMid (j : Fin 3) (k : Fin 2) : Point

The external midpoint (w_j + v_{2j+k}) / 2 of corner cell j.

Equations

• ConwaySoifer.cornerMid j k = ConwaySoifer.corner j + (1 / 2) • ConwaySoifer.cornerDirection j k

noncomputable def ConwaySoifer.extMid0 : Point

M₀ = (1, 1/2), the midpoint of [w₀, v₀].

Equations

• ConwaySoifer.extMid0 = (1, 1 / 2)

theorem ConwaySoifer.extMid0_eq : extMid0 = cornerMid 0 0

inductive ConwaySoifer.ContactCase : Type

The receiving vertex index of the minimal section.

• Sext : ContactCase
• Sint : ContactCase
• Aown : ContactCase
• Across : ContactCase

@[instance_reducible]

instance ConwaySoifer.instDecidableEqContactCase : DecidableEq ContactCase

Equations

• ConwaySoifer.instDecidableEqContactCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConwaySoifer.instReprContactCase.repr : ContactCase → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ConwaySoifer.instReprContactCase : Repr ContactCase

Equations

• ConwaySoifer.instReprContactCase = { reprPrec := ConwaySoifer.instReprContactCase.repr }

def ConwaySoifer.ContactCase.right : ContactCase → Bool

The neighbor direction of the attained minimal section in this contact case.

Equations

• ConwaySoifer.ContactCase.Sext.right = false
• x✝.right = true

def ConwaySoifer.ContactCase.isS : ContactCase → Prop

Whether the minimal endpoint is received by a side owner.

Equations

• ConwaySoifer.ContactCase.Sext.isS = True
• ConwaySoifer.ContactCase.Sint.isS = True
• x✝.isS = False

def ConwaySoifer.minEndpoint (c : ContactCase) (s : ℝ) : Point

The minimal endpoint v₀ + s (v_jj - v₀).

Equations

• ConwaySoifer.minEndpoint c s = ConwaySoifer.linePoint (ConwaySoifer.vertex 0) (ConwaySoifer.sideDirection 0 c.right) s

def ConwaySoifer.BranchHolds : ContactCase → Configuration → ℝ → Prop

The case-specific contact conditions.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.BranchHolds ConwaySoifer.ContactCase.Sext x✝¹ x✝ = (ConwaySoifer.minEndpoint ConwaySoifer.ContactCase.Sext x✝ ∈ (x✝¹ 6).carrier)
• ConwaySoifer.BranchHolds ConwaySoifer.ContactCase.Sint x✝¹ x✝ = (ConwaySoifer.minEndpoint ConwaySoifer.ContactCase.Sint x✝ ∈ (x✝¹ 2).carrier)

structure ConwaySoifer.Canonical (c : ContactCase) (T : Configuration) (r s : ℝ) : Prop

A normalized hypothetical cover in contact case c with parameter s.

• common : CommonSide T r
• covers : Covers T
• r_pos : 0 < r
• r_lt : r < 1
• anchored (i : Fin 10) : anchor i ∈ (T i).carrier
• s_pos : 0 < s
• s_lt : s < 11 / 25
• side_min (i : Fin 6) (right : Bool) : s ≤ rayLen (T (sideIndex i)) (vertex i) (sideDirection i right)
• corner_min (j : Fin 3) (k : Fin 2) : s ≤ rayLen (T (cornerIndex j)) (corner j) (cornerDirection j k)
• core (j : Fin 6) : coreVertex s j ∈ (T 0).carrier
• endpoint : rayLen (T 1) (vertex 0) (sideDirection 0 c.right) = s
• contact : BranchHolds c T s

structure ConwaySoifer.SmallStrengthening (c : ContactCase) (T : Configuration) (r : ℝ) : Prop

The strengthenings available for s ≤ 1/14: non-overfull side owners and corner owners containing both external midpoints (outside the cell of the receiver).

• nonOverfull (i : Fin 6) : (c = ContactCase.Sext → i ≠ 5) → (c = ContactCase.Sint → i ≠ 1) → (c = ContactCase.Aown → i ≠ 0) → c ≠ ContactCase.Across → rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true) ≤ r
• mids (j : Fin 3) (k : Fin 2) : (c = ContactCase.Sext → j ≠ 2) → (c = ContactCase.Sint → j ≠ 0) → (c = ContactCase.Aown → j ≠ 0) → c ≠ ContactCase.Across → cornerMid j k ∈ (T (cornerIndex j)).carrier