HexSymmetry

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

def ConwaySoifer.Simplified.hexToZeroFun (i : Fin 6) (p : Point) : Point

Rotation by -i * 60°. Only a local hexagon symmetry is asserted.

Equations

• ConwaySoifer.Simplified.hexToZeroFun i p = ![p, (p.1 + p.2, -p.1), (p.2, -p.1 - p.2), (-p.1, -p.2), (-p.1 - p.2, p.1), (-p.2, p.1 + p.2)] i

def ConwaySoifer.Simplified.hexToZero (i : Fin 6) : Point →ₗ[ℝ] Point

The linear hexagon symmetry moving a selected vertex to the first vertex.

Equations

• ConwaySoifer.Simplified.hexToZero i = { toFun := ConwaySoifer.Simplified.hexToZeroFun i, map_add' := ⋯, map_smul' := ⋯ }

theorem ConwaySoifer.Simplified.hexToZero_isometry (i : Fin 6) (p q : Point) : sqDist ((hexToZero i) p) ((hexToZero i) q) = sqDist p q

theorem ConwaySoifer.Simplified.hexToZero_vertex (i : Fin 6) : (hexToZero i) (vertex i) = vertex 0

theorem ConwaySoifer.Simplified.hexToZero_sidePoint (i : Fin 6) (right : Bool) (s : ℝ) : (hexToZero i) (linePoint (vertex i) (sideDirection i right) s) = linePoint (vertex 0) (sideDirection 0 right) s

theorem ConwaySoifer.Simplified.hexToZero_core (i j : Fin 6) (s : ℝ) : (hexToZero i) (coreVertex s j) = coreVertex s (j - i)

def ConwaySoifer.Simplified.horizontal : Point →ₗ[ℝ] Point

Reflection across the Euclidean horizontal axis, expressed in triangular coordinates.

Equations

• ConwaySoifer.Simplified.horizontal = { toFun := fun (p : ConwaySoifer.Point) => (p.1 + p.2, -p.2), map_add' := ⋯, map_smul' := ⋯ }

theorem ConwaySoifer.Simplified.horizontal_isometry (p q : Point) : sqDist (horizontal p) (horizontal q) = sqDist p q

theorem ConwaySoifer.Simplified.horizontal_core (j : Fin 6) (s : ℝ) : horizontal (coreVertex s j) = coreVertex s (5 - j)

theorem ConwaySoifer.Simplified.horizontal_sidePoint (right : Bool) (s : ℝ) : horizontal (linePoint (vertex 0) (sideDirection 0 right) s) = linePoint (vertex 0) (sideDirection 0 !right) s

theorem ConwaySoifer.Simplified.hexToZero_mem_hexagon (i : Fin 6) (p : Point) : (hexToZero i) p ∈ hexagon ↔ p ∈ hexagon

theorem ConwaySoifer.Simplified.sext_inverse (p : Point) : (hexToZero 5) ((hexToZero 1) p) = p

theorem ConwaySoifer.Simplified.sext_map_side (i : Fin 6) (d : Bool) (t : ℝ) : (hexToZero 5) (linePoint (vertex (i + 5)) (sideDirection (i + 5) d) t) = linePoint (vertex i) (sideDirection i d) t

theorem ConwaySoifer.Simplified.sint_map_side (i : Fin 6) (d : Bool) (t : ℝ) : reflL (linePoint (vertex (1 - i)) (sideDirection (1 - i) !d) t) = linePoint (vertex i) (sideDirection i d) t