The symmetry group of the target triangle

rot (rotation by 120 degrees) and refl (a, b) = (b, a) preserve sqDist, the target triangle, the hexagon, permute the ten anchors and transport full ray lengths. A configuration is relabelled along the induced anchor permutation, so that the minimal full side section can be moved to vertex 0, towards vertex 5 (external side) or towards vertex 1 (internal side).

def ConwaySoifer.refl (p : Point) : Point

Reflection that exchanges the two triangular coordinates.

Equations

• ConwaySoifer.refl p = (p.2, p.1)

theorem ConwaySoifer.refl_refl (p : Point) : refl (refl p) = p

theorem ConwaySoifer.refl_add (p q : Point) : refl (p + q) = refl p + refl q

theorem ConwaySoifer.refl_smul (t : ℝ) (p : Point) : refl (t • p) = t • refl p

theorem ConwaySoifer.refl_sub (p q : Point) : refl (p - q) = refl p - refl q

theorem ConwaySoifer.sqDist_rot' (p q : Point) : sqDist (rot p) (rot q) = sqDist p q

theorem ConwaySoifer.sqDist_refl (p q : Point) : sqDist (refl p) (refl q) = sqDist p q

def ConwaySoifer.rotL : Point →ₗ[ℝ] Point

Rotation through 120 degrees as a real linear map.

Equations

• ConwaySoifer.rotL = { toFun := ConwaySoifer.rot, map_add' := ConwaySoifer.rot_add, map_smul' := ConwaySoifer.rot_smul }

def ConwaySoifer.reflL : Point →ₗ[ℝ] Point

Coordinate reflection as a real linear map.

Equations

• ConwaySoifer.reflL = { toFun := ConwaySoifer.refl, map_add' := ConwaySoifer.refl_add, map_smul' := ConwaySoifer.refl_smul }

theorem ConwaySoifer.rot_bijective : Function.Bijective rot

theorem ConwaySoifer.refl_bijective : Function.Bijective refl

theorem ConwaySoifer.rot_mem_target (p : Point) : rot p ∈ target ↔ p ∈ target

theorem ConwaySoifer.refl_mem_target (p : Point) : refl p ∈ target ↔ p ∈ target

theorem ConwaySoifer.rot_mem_hexagon (p : Point) : rot p ∈ hexagon ↔ p ∈ hexagon

theorem ConwaySoifer.refl_mem_hexagon (p : Point) : refl p ∈ hexagon ↔ p ∈ hexagon

Anchor permutations

def ConwaySoifer.rotIdx : Fin 10 → Fin 10

rot sends anchor i to anchor (rotIdx i): centre fixed, v_i ↦ v_{i+2}, w_j ↦ w_{j+1}.

Equations

• ConwaySoifer.rotIdx = ![0, 3, 4, 5, 6, 1, 2, 8, 9, 7]

def ConwaySoifer.rotIdxInv : Fin 10 → Fin 10

The inverse owner permutation induced by rotation of the target.

Equations

• ConwaySoifer.rotIdxInv = ![0, 5, 6, 1, 2, 3, 4, 9, 7, 8]

def ConwaySoifer.reflIdx : Fin 10 → Fin 10

refl sends v_i ↦ v_{1-i}, w_0 ↦ w_0, w_1 ↔ w_2.

Equations

• ConwaySoifer.reflIdx = ![0, 2, 1, 6, 5, 4, 3, 7, 9, 8]

def ConwaySoifer.reflCorner : Fin 3 → Fin 3

The corner permutation of refl.

Equations

• ConwaySoifer.reflCorner = ![0, 2, 1]

theorem ConwaySoifer.rotIdxInv_rotIdx (i : Fin 10) : rotIdxInv (rotIdx i) = i

theorem ConwaySoifer.rotIdx_rotIdxInv (i : Fin 10) : rotIdx (rotIdxInv i) = i

theorem ConwaySoifer.reflIdx_reflIdx (i : Fin 10) : reflIdx (reflIdx i) = i

theorem ConwaySoifer.rot_anchor (i : Fin 10) : rot (anchor i) = anchor (rotIdx i)

theorem ConwaySoifer.refl_anchor (i : Fin 10) : refl (anchor i) = anchor (reflIdx i)

theorem ConwaySoifer.rotIdx_sideIndex (i : Fin 6) : rotIdx (sideIndex i) = sideIndex (i + 2)

theorem ConwaySoifer.reflIdx_sideIndex (i : Fin 6) : reflIdx (sideIndex i) = sideIndex (1 - i)

theorem ConwaySoifer.rotIdx_cornerIndex (j : Fin 3) : rotIdx (cornerIndex j) = cornerIndex (j + 1)

theorem ConwaySoifer.reflIdx_cornerIndex (j : Fin 3) : reflIdx (cornerIndex j) = cornerIndex (reflCorner j)

theorem ConwaySoifer.rotIdx_zero : rotIdx 0 = 0

theorem ConwaySoifer.reflIdx_zero : reflIdx 0 = 0

theorem ConwaySoifer.rot_vertex (i : Fin 6) : rot (vertex i) = vertex (i + 2)

theorem ConwaySoifer.refl_vertex (i : Fin 6) : refl (vertex i) = vertex (1 - i)

theorem ConwaySoifer.rot_corner (j : Fin 3) : rot (corner j) = corner (j + 1)

theorem ConwaySoifer.refl_corner (j : Fin 3) : refl (corner j) = corner (reflCorner j)

theorem ConwaySoifer.rot_sideDirection (i : Fin 6) (right : Bool) : rot (sideDirection i right) = sideDirection (i + 2) right

theorem ConwaySoifer.refl_sideDirection (i : Fin 6) (right : Bool) : refl (sideDirection i right) = sideDirection (1 - i) !right

theorem ConwaySoifer.rot_cornerDirection (j : Fin 3) (m : Fin 2) : rot (cornerDirection j m) = cornerDirection (j + 1) m

theorem ConwaySoifer.refl_cornerDirection (j : Fin 3) (m : Fin 2) : refl (cornerDirection j m) = cornerDirection (reflCorner j) (1 - m)

theorem ConwaySoifer.rot_coreDir (j : Fin 6) : rot (coreDir j) = coreDir (j + 2)

theorem ConwaySoifer.refl_coreDir (j : Fin 6) : refl (coreDir j) = coreDir (-j)

theorem ConwaySoifer.rot_coreVertex (u : ℝ) (j : Fin 6) : rot (coreVertex u j) = coreVertex u (j + 2)

theorem ConwaySoifer.refl_coreVertex (u : ℝ) (j : Fin 6) : refl (coreVertex u j) = coreVertex u (-j)

theorem ConwaySoifer.rot_cornerMid (j : Fin 3) (m : Fin 2) : rot (cornerMid j m) = cornerMid (j + 1) m

theorem ConwaySoifer.refl_cornerMid (j : Fin 3) (m : Fin 2) : refl (cornerMid j m) = cornerMid (reflCorner j) (1 - m)

Transformed triangles and configurations

def ConwaySoifer.EquilateralTriangle.mapIso (T : EquilateralTriangle) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) : EquilateralTriangle

The image of a triangle under an isometry given as a linear map.

Equations

• T.mapIso f hf = { vertices := fun (i : Fin 3) => f (T.vertices i), side := T.side, side_nonneg := ⋯, equilateral := ⋯ }

theorem ConwaySoifer.EquilateralTriangle.carrier_mapIso (T : EquilateralTriangle) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) : (T.mapIso f hf).carrier = ⇑f '' T.carrier

theorem ConwaySoifer.EquilateralTriangle.mem_mapIso (T : EquilateralTriangle) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) (hinj : Function.Injective ⇑f) (p : Point) : f p ∈ (T.mapIso f hf).carrier ↔ p ∈ T.carrier

theorem ConwaySoifer.rayLen_mapIso (T : EquilateralTriangle) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) (hinj : Function.Injective ⇑f) (v d : Point) : rayLen (T.mapIso f hf) (f v) (f d) = rayLen T v d

def ConwaySoifer.Configuration.transform (T : Configuration) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) (σinv : Fin 10 → Fin 10) : Configuration

Relabelled and transformed configuration: owner i of the new configuration is the image of the owner of the anchor sent to anchor i.

Equations

• T.transform f hf σinv i = (T (σinv i)).mapIso f hf

theorem ConwaySoifer.Configuration.transform_common {T : Configuration} {r : ℝ} (h : CommonSide T r) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) (σinv : Fin 10 → Fin 10) : CommonSide (T.transform f hf σinv) r

theorem ConwaySoifer.Configuration.transform_covers {T : Configuration} (h : Covers T) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) (hbij : Function.Bijective ⇑f) (htarget : ∀ (p : Point), f p ∈ target ↔ p ∈ target) (σinv : Fin 10 → Fin 10) (hσ : Function.Surjective σinv) : Covers (T.transform f hf σinv)

theorem ConwaySoifer.Configuration.transform_anchored {T : Configuration} (h : ∀ (i : Fin 10), anchor i ∈ (T i).carrier) (f : Point →ₗ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) (hinj : Function.Injective ⇑f) (σ σinv : Fin 10 → Fin 10) (hσ : ∀ (i : Fin 10), σ (σinv i) = i) (hanchor : ∀ (i : Fin 10), f (anchor i) = anchor (σ i)) (i : Fin 10) : anchor i ∈ (T.transform f hf σinv i).carrier

def ConwaySoifer.Configuration.rotate (T : Configuration) : Configuration

The rotated configuration.

Equations

• T.rotate = T.transform ConwaySoifer.rotL ConwaySoifer.sqDist_rot' ConwaySoifer.rotIdxInv

def ConwaySoifer.Configuration.reflect (T : Configuration) : Configuration

The reflected configuration.

Equations

• T.reflect = T.transform ConwaySoifer.reflL ConwaySoifer.sqDist_refl ConwaySoifer.reflIdx

theorem ConwaySoifer.rotate_common {T : Configuration} {r : ℝ} (h : CommonSide T r) : CommonSide T.rotate r

theorem ConwaySoifer.reflect_common {T : Configuration} {r : ℝ} (h : CommonSide T r) : CommonSide T.reflect r

theorem ConwaySoifer.rotate_covers {T : Configuration} (h : Covers T) : Covers T.rotate

theorem ConwaySoifer.reflect_covers {T : Configuration} (h : Covers T) : Covers T.reflect

theorem ConwaySoifer.rotate_anchored {T : Configuration} (h : ∀ (i : Fin 10), anchor i ∈ (T i).carrier) (i : Fin 10) : anchor i ∈ (T.rotate i).carrier

theorem ConwaySoifer.reflect_anchored {T : Configuration} (h : ∀ (i : Fin 10), anchor i ∈ (T i).carrier) (i : Fin 10) : anchor i ∈ (T.reflect i).carrier

theorem ConwaySoifer.mem_rotate (T : Configuration) (i : Fin 10) (p : Point) : rot p ∈ (T.rotate (rotIdx i)).carrier ↔ p ∈ (T i).carrier

Membership transport for the rotated owners.

theorem ConwaySoifer.mem_reflect (T : Configuration) (i : Fin 10) (p : Point) : refl p ∈ (T.reflect (reflIdx i)).carrier ↔ p ∈ (T i).carrier

theorem ConwaySoifer.rayLen_rotate (T : Configuration) (i : Fin 10) (v d : Point) : rayLen (T.rotate (rotIdx i)) (rot v) (rot d) = rayLen (T i) v d

theorem ConwaySoifer.rayLen_reflect (T : Configuration) (i : Fin 10) (v d : Point) : rayLen (T.reflect (reflIdx i)) (refl v) (refl d) = rayLen (T i) v d

theorem ConwaySoifer.sideLen_rotate (T : Configuration) (i : Fin 6) (right : Bool) : rayLen (T.rotate (sideIndex (i + 2))) (vertex (i + 2)) (sideDirection (i + 2) right) = rayLen (T (sideIndex i)) (vertex i) (sideDirection i right)

Side sections of the rotated configuration.

theorem ConwaySoifer.sideLen_reflect (T : Configuration) (i : Fin 6) (right : Bool) : rayLen (T.reflect (sideIndex (1 - i))) (vertex (1 - i)) (sideDirection (1 - i) !right) = rayLen (T (sideIndex i)) (vertex i) (sideDirection i right)

theorem ConwaySoifer.cornerLen_rotate (T : Configuration) (j : Fin 3) (m : Fin 2) : rayLen (T.rotate (cornerIndex (j + 1))) (corner (j + 1)) (cornerDirection (j + 1) m) = rayLen (T (cornerIndex j)) (corner j) (cornerDirection j m)

theorem ConwaySoifer.cornerLen_reflect (T : Configuration) (j : Fin 3) (m : Fin 2) : rayLen (T.reflect (cornerIndex (reflCorner j))) (corner (reflCorner j)) (cornerDirection (reflCorner j) (1 - m)) = rayLen (T (cornerIndex j)) (corner j) (cornerDirection j m)