Proper rotations and cube varieties

theorem MacMahon.faceOne_bound : 1 < 6

Faces are +x, -x, +y, -y, +z, -z.

def MacMahon.opposite (f : Fin 6) : Fin 6

The face in the opposite coordinate direction.

Equations

• MacMahon.opposite f = if ↑f % 2 = 0 then f + ⟨1, MacMahon.faceOne_bound⟩ else f - ⟨1, MacMahon.faceOne_bound⟩

def MacMahon.fromAxes (a b c : Fin 6) : Fin 6 → Fin 6

The face map determined by the images of the three positive coordinate axes.

Equations

• MacMahon.fromAxes a b c = ![a, MacMahon.opposite a, b, MacMahon.opposite b, c, MacMahon.opposite c]

def MacMahon.ValidAxes (a b c : Fin 6) : Prop

Distinct coordinate axes and determinant +1.

Equations

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

@[instance_reducible]

instance MacMahon.instDecidableValidAxes (a b c : Fin 6) : Decidable (ValidAxes a b c)

Equations

• MacMahon.instDecidableValidAxes a b c = id inferInstance

def MacMahon.ProperRotation (r : Fin 6 → Fin 6) : Prop

A face map induced by a determinant-positive signed-axis permutation.

Equations

• MacMahon.ProperRotation r = ∃ (a : Fin 6) (b : Fin 6) (c : Fin 6), MacMahon.ValidAxes a b c ∧ r = MacMahon.fromAxes a b c

theorem MacMahon.rotation_table_valid (n : Fin 24) : ValidAxes (rotations n 0) (rotations n 2) (rotations n 4) ∧ rotations n = fromAxes (rotations n 0) (rotations n 2) (rotations n 4)

theorem MacMahon.rotation_table_complete (a b c : Fin 6) : ValidAxes a b c → ∃ (n : Fin 24), fromAxes a b c = rotations n

theorem MacMahon.proper_rotation_iff (r : Fin 6 → Fin 6) : ProperRotation r ↔ ∃ (n : Fin 24), r = rotations n

theorem MacMahon.rotations_bijective (n : Fin 24) : Function.Bijective (rotations n)

theorem MacMahon.rotations_distinct : Function.Injective rotations

theorem MacMahon.face_colours_valid (i j : Label) : i ≠ j → Function.Injective (faceColours i j) ∧ ∀ (f : Fin 6), faceColours i j f ≠ 0

theorem MacMahon.varieties_distinct (i j : Label) : i ≠ j → ∀ (u v : Label), u ≠ v → ∀ (r : Fin 24), (∀ (f : Fin 6), faceColours i j (rotations r f) = faceColours u v f) → i = u ∧ j = v

Different Conway labels represent different rotation classes.

theorem MacMahon.rotation_inverse (r : Fin 24) : ∃ (s : Fin 24), ∀ (f : Fin 6), rotations r (rotations s f) = f

theorem MacMahon.rotation_composition (r s : Fin 24) : ∃ (t : Fin 24), ∀ (f : Fin 6), rotations t f = rotations r (rotations s f)

theorem MacMahon.exposed_face_rule (k : Slot) (d : Fin 3) : ↑(exposedFaces k d) = 2 * ↑d + ↑k / 2 ^ (2 - ↑d) % 2

The three outward faces at each of the eight binary cube positions.