CornerAbsent

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

def ConwaySoifer.Simplified.cornerAt (j : Fin 3) : Point →ᵃ[ℝ] Point

Local coordinates at each of the three outer corners.

Equations

• ConwaySoifer.Simplified.cornerAt j = ConwaySoifer.Simplified.cornerCoordinates.comp (ConwaySoifer.Simplified.hexToZero ⟨2 * ↑j, ⋯⟩).toAffineMap

theorem ConwaySoifer.Simplified.cornerAt_isometry (j : Fin 3) (p q : Point) : sqDist ((cornerAt j) p) ((cornerAt j) q) = sqDist p q

theorem ConwaySoifer.Simplified.cornerAt_corner (j : Fin 3) : (cornerAt j) (corner j) = (0, 0)

theorem ConwaySoifer.Simplified.cornerAt_mid0 (j : Fin 3) : (cornerAt j) (cornerMid j 0) = (1 / 2, 0)

theorem ConwaySoifer.Simplified.cornerAt_mid1 (j : Fin 3) : (cornerAt j) (cornerMid j 1) = (0, 1 / 2)

theorem ConwaySoifer.Simplified.cornerAt_base (j : Fin 3) (u : ℝ) : (cornerAt j) (linePoint (vertex ⟨2 * ↑j, ⋯⟩) (sideDirection ⟨2 * ↑j, ⋯⟩ true) u) = (1 - u, u)

theorem ConwaySoifer.Simplified.corner_base_exclusion (j : Fin 3) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) {Q : EquilateralTriangle} (hQ : 0 < Q.side) (hQ1 : Q.side < 1) (hw : corner j ∈ Q.carrier) (hm0 : cornerMid j 0 ∈ Q.carrier) (hm1 : cornerMid j 1 ∈ Q.carrier) (hp : linePoint (vertex ⟨2 * ↑j, ⋯⟩) (sideDirection ⟨2 * ↑j, ⋯⟩ true) u ∈ Q.carrier) : False

theorem ConwaySoifer.Canonical.corner_absent_simplified {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (j : Fin 3) (hm : ∀ (m : Fin 2), cornerMid j m ∈ (T (cornerIndex j)).carrier) {p : Point} (hp : p ∈ hexagon) : p ∉ (T (cornerIndex j)).carrier