Geometric normalization: every subunit cover is a canonical contact case

From a cover with the minimal full side section at vertex 0 (MinAt T r s 0 right):

• the adaptive core K_s lies in the centre owner (Lemma A and the distance of the core vertices from the corner anchors);
• the bridge (Lemma B at u = s/2) keeps the minimal endpoint p out of the centre owner;
• p is reached by another owner (closedness), which by locality is the neighbouring side owner (external side) or the neighbouring side owner or corner owner (internal side);
• every corner section is at least s (the neighbouring side owners cannot continue the cover immediately after a shorter corner section);
• in the corner branch the external midpoint M₀ is not in A₀ (Lemma 4.2), so it belongs to S₀ (Aown) or S₁ (Across).

def ConwaySoifer.CoreObstruction : Prop

Geometric interface for the adaptive-core obstruction.

Equations

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

def ConwaySoifer.BridgeObstruction : Prop

Geometric interface for the bridge at the minimum endpoint.

Equations

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

def ConwaySoifer.MidpointObstruction : Prop

Geometric interface for the forbidden own midpoint in a corner branch.

Equations

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

Index bookkeeping

theorem ConwaySoifer.owner_cases (k : Fin 10) : k = 0 ∨ (∃ (i : Fin 6), k = sideIndex i) ∨ ∃ (j : Fin 3), k = cornerIndex j

theorem ConwaySoifer.MinAt.side_pos' {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (k : Fin 10) : 0 < (T k).side

theorem ConwaySoifer.MinAt.side_lt' {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (k : Fin 10) : (T k).side < 1

theorem ConwaySoifer.MinAt.vertex_mem {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (i : Fin 6) : vertex i ∈ (T (sideIndex i)).carrier

theorem ConwaySoifer.MinAt.corner_mem {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (j : Fin 3) : corner j ∈ (T (cornerIndex j)).carrier

theorem ConwaySoifer.MinAt.zero_mem {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) : 0 ∈ (T 0).carrier

theorem ConwaySoifer.MinAt.s_half {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) : s ≤ 1 / 2

The adaptive core

theorem ConwaySoifer.coreVertex_mem_hexagon {u : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ 1 / 2) (j : Fin 6) : coreVertex u j ∈ hexagon

theorem ConwaySoifer.sqDist_corner_coreVertex {u : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ 1 / 2) (k : Fin 3) (j : Fin 6) : 1 ≤ sqDist (corner k) (coreVertex u j)

theorem ConwaySoifer.MinAt.core_of_geometry {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (hcore : CoreObstruction) (j : Fin 6) : coreVertex s j ∈ (T 0).carrier

theorem ConwaySoifer.coreVertex_half_mem {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) (j : Fin 6) : coreVertex (s / 2) j ∈ C

theorem ConwaySoifer.MinAt.endpoint_not_centre_of_geometry {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (hcore : CoreObstruction) (hbridge : BridgeObstruction) : linePoint (vertex 0) (sideDirection 0 right) s ∉ (T 0).carrier

Transfer of the minimal endpoint

theorem ConwaySoifer.MinAt.endpoint_owner {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) : ∃ (k : Fin 10), k ≠ 1 ∧ linePoint (vertex 0) (sideDirection 0 right) s ∈ (T k).carrier

theorem ConwaySoifer.endpoint_ext_eq (s : ℝ) : linePoint (vertex 0) (sideDirection 0 false) s = linePoint (vertex 5) (sideDirection 5 true) (1 - s)

theorem ConwaySoifer.MinAt.ext_contact_of_geometry {T : Configuration} {r s : ℝ} (h : MinAt T r s 0 false) (hcore : CoreObstruction) (hbridge : BridgeObstruction) : linePoint (vertex 0) (sideDirection 0 false) s ∈ (T 6).carrier

External side: the endpoint belongs to S₅.

theorem ConwaySoifer.MinAt.int_contact_of_geometry {T : Configuration} {r s : ℝ} (h : MinAt T r s 0 true) (hcore : CoreObstruction) (hbridge : BridgeObstruction) : linePoint (vertex 0) (sideDirection 0 true) s ∈ (T 2).carrier ∨ linePoint (vertex 0) (sideDirection 0 true) s ∈ (T 7).carrier

Internal side: the endpoint belongs to S₁ or to A₀.

Corner sections are at least s

theorem ConwaySoifer.cornerCont_eq (j : Fin 3) (m : Fin 2) (t : ℝ) : linePoint (corner j) (cornerDirection j m) (1 + t) = linePoint (vertex ⟨2 * ↑j + ↑m, ⋯⟩) (sideDirection ⟨2 * ↑j + ↑m, ⋯⟩ (decide (m = 1))) t

The continuation of the corner ray beyond vertex (2j+m) is a side point of S_{2j+m}.

theorem ConwaySoifer.sqDist_cornerRay_same (j : Fin 3) (m : Fin 2) (x t : ℝ) : sqDist (linePoint (corner j) (cornerDirection j m) x) (linePoint (corner j) (cornerDirection j m) t) = (x - t) ^ 2

theorem ConwaySoifer.sqDist_cornerRay_other (j : Fin 3) (m : Fin 2) (x t : ℝ) : sqDist (linePoint (corner j) (cornerDirection j m) x) (linePoint (corner j) (cornerDirection j (1 - m)) t) = x ^ 2 - x * t + t ^ 2

theorem ConwaySoifer.MinAt.contPt_mem {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (j : Fin 3) (m : Fin 2) : linePoint (corner j) (cornerDirection j m) (1 + s) ∈ (T (sideIndex ⟨2 * ↑j + ↑m, ⋯⟩)).carrier

theorem ConwaySoifer.cornerAllowed_cases (j : Fin 3) (k : Fin 10) (hk : cornerAllowed j k = true) : k = cornerIndex j ∨ k = sideIndex ⟨2 * ↑j, ⋯⟩ ∨ k = sideIndex ⟨2 * ↑j + 1, ⋯⟩

theorem ConwaySoifer.MinAt.corner_min {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (j : Fin 3) (m : Fin 2) : s ≤ rayLen (T (cornerIndex j)) (corner j) (cornerDirection j m)

The corner branch

theorem ConwaySoifer.extMid0_eq_linePoint : extMid0 = linePoint (corner 0) (cornerDirection 0 0) (1 / 2)

theorem ConwaySoifer.MinAt.mid_owner {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) : extMid0 ∈ (T 7).carrier ∨ extMid0 ∈ (T 1).carrier ∨ extMid0 ∈ (T 2).carrier

theorem ConwaySoifer.MinAt.mid_not_corner_of_geometry {T : Configuration} {r s : ℝ} (h : MinAt T r s 0 true) (hmid : MidpointObstruction) (hp : linePoint (vertex 0) (sideDirection 0 true) s ∈ (T 7).carrier) : extMid0 ∉ (T 7).carrier

Assembly

theorem ConwaySoifer.MinAt.endpoint_eq {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) : rayLen (T 1) (vertex 0) (sideDirection 0 right) = s

theorem ConwaySoifer.MinAt.canonical_of_geometry {T : Configuration} {r s : ℝ} {right : Bool} (h : MinAt T r s 0 right) (hcore : CoreObstruction) (c : ContactCase) (hc : c.right = right) (hcontact : BranchHolds c T s) : Canonical c T r s

The normalized cover in case c (with c.right = right).

theorem ConwaySoifer.exists_canonical_of_geometry (hcore : CoreObstruction) (hbridge : BridgeObstruction) (hmid : MidpointObstruction) (r : ℝ) (T : Configuration) (hside : CommonSide T r) (hcover : Covers T) (hr : r < 1) : ∃ (c : ContactCase) (U : Configuration) (s : ℝ), Canonical c U r s

Every subunit full cover is a canonical contact case.