Library mathcomp.solvable.burnside_app
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop finset fingroup.
From mathcomp Require Import action perm primitive_action.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop finset fingroup.
From mathcomp Require Import action perm primitive_action.
Application of the Burside formula to count the number of distinct
colorings of the vertices of a square and a cube.
Set Implicit Arguments.
Import GroupScope.
Lemma burnside_formula : ∀ (gT : finGroupType) s (G : {group gT}),
uniq s → s =i G →
∀ (sT : finType) (to : {action gT &-> sT}),
(#|orbit to G @: setT| × size s)%N = \sum_(p <- s) #|'Fix_to[p]|.
Section colouring.
Variable n : nat.
Definition colors := 'I_n.
Canonical colors_eqType := Eval hnf in [eqType of colors].
Canonical colors_choiceType := Eval hnf in [choiceType of colors].
Canonical colors_countType := Eval hnf in [countType of colors].
Canonical colors_finType := Eval hnf in [finType of colors].
Section square_colouring.
Definition square := 'I_4.
Canonical square_eqType := Eval hnf in [eqType of square].
Canonical square_choiceType := Eval hnf in [choiceType of square].
Canonical square_countType := Eval hnf in [countType of square].
Canonical square_finType := Eval hnf in [finType of square].
Canonical square_subType := Eval hnf in [subType of square].
Canonical square_subCountType :=
Eval hnf in [subCountType of square].
Canonical square_subFinType := Eval hnf in [subFinType of square].
Definition mksquare i : square := Sub (i %% _) (ltn_mod i 4).
Definition c0 := mksquare 0.
Definition c1 := mksquare 1.
Definition c2 := mksquare 2.
Definition c3 := mksquare 3.
rotations
Definition R1 (sc : square) : square := tnth [tuple c1; c2; c3; c0] sc.
Definition R2 (sc : square) : square := tnth [tuple c2; c3; c0; c1] sc.
Definition R3 (sc : square) : square := tnth [tuple c3; c0; c1; c2] sc.
Ltac get_inv elt l :=
match l with
| (_, (elt, ?x)) ⇒ x
| (elt, ?x) ⇒ x
| (?x, _) ⇒ get_inv elt x
end.
Definition rot_inv := ((R1, R3), (R2, R2), (R3, R1)).
Ltac inj_tac :=
move: (erefl rot_inv); unfold rot_inv;
match goal with |- ?X = _ → injective ?Y ⇒
move⇒ _; let x := get_inv Y X in
apply: (can_inj (g:=x)); move⇒ [val H1]
end.
Lemma R1_inj : injective R1.
Lemma R2_inj : injective R2.
Lemma R3_inj : injective R3.
Definition r1 := (perm R1_inj).
Definition r2 := (perm R2_inj).
Definition r3 := (perm R3_inj).
Definition id1 := (1 : {perm square}).
Definition is_rot (r : {perm _}) := (r × r1 == r1 × r).
Definition rot := [set r | is_rot r].
Lemma group_set_rot : group_set rot.
Canonical rot_group := Group group_set_rot.
Definition rotations := [set id1; r1; r2; r3].
Lemma rot_eq_c0 : ∀ r s : {perm square},
is_rot r → is_rot s → r c0 = s c0 → r = s.
Lemma rot_r1 : ∀ r, is_rot r → r = r1 ^+ (r c0).
Lemma rotations_is_rot : ∀ r, r \in rotations → is_rot r.
Lemma rot_is_rot : rot = rotations.
Definition R2 (sc : square) : square := tnth [tuple c2; c3; c0; c1] sc.
Definition R3 (sc : square) : square := tnth [tuple c3; c0; c1; c2] sc.
Ltac get_inv elt l :=
match l with
| (_, (elt, ?x)) ⇒ x
| (elt, ?x) ⇒ x
| (?x, _) ⇒ get_inv elt x
end.
Definition rot_inv := ((R1, R3), (R2, R2), (R3, R1)).
Ltac inj_tac :=
move: (erefl rot_inv); unfold rot_inv;
match goal with |- ?X = _ → injective ?Y ⇒
move⇒ _; let x := get_inv Y X in
apply: (can_inj (g:=x)); move⇒ [val H1]
end.
Lemma R1_inj : injective R1.
Lemma R2_inj : injective R2.
Lemma R3_inj : injective R3.
Definition r1 := (perm R1_inj).
Definition r2 := (perm R2_inj).
Definition r3 := (perm R3_inj).
Definition id1 := (1 : {perm square}).
Definition is_rot (r : {perm _}) := (r × r1 == r1 × r).
Definition rot := [set r | is_rot r].
Lemma group_set_rot : group_set rot.
Canonical rot_group := Group group_set_rot.
Definition rotations := [set id1; r1; r2; r3].
Lemma rot_eq_c0 : ∀ r s : {perm square},
is_rot r → is_rot s → r c0 = s c0 → r = s.
Lemma rot_r1 : ∀ r, is_rot r → r = r1 ^+ (r c0).
Lemma rotations_is_rot : ∀ r, r \in rotations → is_rot r.
Lemma rot_is_rot : rot = rotations.
symmetries
Definition Sh (sc : square) : square := tnth [tuple c1; c0; c3; c2] sc.
Lemma Sh_inj : injective Sh.
Definition sh := (perm Sh_inj).
Lemma sh_inv : sh^-1 = sh.
Definition Sv (sc : square) : square := tnth [tuple c3; c2; c1; c0] sc.
Lemma Sv_inj : injective Sv.
Definition sv := (perm Sv_inj).
Lemma sv_inv : sv^-1 = sv.
Definition Sd1 (sc : square) : square := tnth [tuple c0; c3; c2; c1] sc.
Lemma Sd1_inj : injective Sd1.
Definition sd1 := (perm Sd1_inj).
Lemma sd1_inv : sd1^-1 = sd1.
Definition Sd2 (sc : square) : square := tnth [tuple c2; c1; c0; c3] sc.
Lemma Sd2_inj : injective Sd2.
Definition sd2 := (perm Sd2_inj).
Lemma sd2_inv : sd2^-1 = sd2.
Lemma ord_enum4 : enum 'I_4 = [:: c0; c1; c2; c3].
Lemma diff_id_sh : 1 != sh.
Definition isometries2 := [set 1; sh].
Lemma card_iso2 : #|isometries2| = 2.
Lemma group_set_iso2 : group_set isometries2.
Canonical iso2_group := Group group_set_iso2.
Definition isometries :=
[set p | [|| p == 1, p == r1, p == r2, p == r3,
p == sh, p == sv, p == sd1 | p == sd2 ]].
Definition opp (sc : square) := tnth [tuple c2; c3; c0; c1] sc.
Definition is_iso (p : {perm square}) := ∀ ci, p (opp ci) = opp (p ci).
Lemma isometries_iso : ∀ p, p \in isometries → is_iso p.
Ltac non_inj p a1 a2 heq1 heq2 :=
let h1:= fresh "h1" in
(absurd (p a1 = p a2); first (by red ⇒ - h1; move: (perm_inj h1));
by rewrite heq1 heq2; apply/eqP).
Ltac is_isoPtac p f e0 e1 e2 e3 :=
suff ->: p = f by [rewrite inE eqxx ?orbT];
let e := fresh "e" in apply/permP;
do 5?[case] ⇒ // ?; [move: e0 | move: e1 | move: e2 | move: e3] ⇒ e;
apply: etrans (congr1 p _) (etrans e _); apply/eqP; rewrite // permE.
Lemma is_isoP : ∀ p, reflect (is_iso p) (p \in isometries).
Lemma group_set_iso : group_set isometries.
Canonical iso_group := Group group_set_iso.
Lemma card_rot : #|rot| = 4.
Lemma group_set_rotations : group_set rotations.
Canonical rotations_group := Group group_set_rotations.
Notation col_squares := {ffun square → colors}.
Definition act_f (sc : col_squares) (p : {perm square}) : col_squares :=
[ffun z ⇒ sc (p^-1 z)].
Lemma act_f_1 : ∀ k, act_f k 1 = k.
Lemma act_f_morph : ∀ k x y, act_f k (x × y) = act_f (act_f k x) y.
Definition to := TotalAction act_f_1 act_f_morph.
Definition square_coloring_number2 := #|orbit to isometries2 @: setT|.
Definition square_coloring_number4 := #|orbit to rotations @: setT|.
Definition square_coloring_number8 := #|orbit to isometries @: setT|.
Lemma Fid : 'Fix_to(1) = setT.
Lemma card_Fid : #|'Fix_to(1)| = (n ^ 4)%N.
Definition coin0 (sc : col_squares) : colors := sc c0.
Definition coin1 (sc : col_squares) : colors := sc c1.
Definition coin2 (sc : col_squares) : colors := sc c2.
Definition coin3 (sc : col_squares) : colors := sc c3.
Lemma eqperm_map : ∀ p1 p2 : col_squares,
(p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: c0; c1; c2; c3].
Lemma F_Sh :
'Fix_to[sh] = [set x | (coin0 x == coin1 x) && (coin2 x == coin3 x)].
Lemma F_Sv :
'Fix_to[sv] = [set x | (coin0 x == coin3 x) && (coin2 x == coin1 x)].
Ltac inv_tac :=
apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _;
let a := fresh "a" in apply/permP ⇒ a;
apply/eqP; rewrite permM !permE; case: a; do 4?case.
Lemma r1_inv : r1^-1 = r3.
Lemma r2_inv : r2^-1 = r2.
Lemma r3_inv : r3^-1 = r1.
Lemma F_r2 :
'Fix_to[r2] = [set x | (coin0 x == coin2 x) && (coin1 x == coin3 x)].
Lemma F_r1 : 'Fix_to[r1] =
[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
Lemma F_r3 : 'Fix_to[r3] =
[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
Lemma card_n2 : ∀ x y z t : square, uniq [:: x; y; z; t] →
#|[set p : col_squares | (p x == p y) && (p z == p t)]| = (n ^ 2)%N.
Lemma card_n :
#|[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&& (coin2 x == coin3 x)]|
= n.
Lemma burnside_app2 : (square_coloring_number2 × 2 = n ^ 4 + n ^ 2)%N.
Lemma burnside_app_rot :
(square_coloring_number4 × 4 = n ^ 4 + n ^ 2 + 2 × n)%N.
Lemma F_Sd1 : 'Fix_to[sd1] = [set x | coin1 x == coin3 x].
Lemma card_n3 : ∀ x y : square, x != y →
#|[set k : col_squares | k x == k y]| = (n ^ 3)%N.
Lemma F_Sd2 : 'Fix_to[sd2] = [set x | coin0 x == coin2 x].
Lemma burnside_app_iso :
(square_coloring_number8 × 8 = n ^ 4 + 2 × n ^ 3 + 3 × n ^ 2 + 2 × n)%N.
End square_colouring.
Section cube_colouring.
Definition cube := 'I_6.
Canonical cube_eqType := Eval hnf in [eqType of cube].
Canonical cube_choiceType := Eval hnf in [choiceType of cube].
Canonical cube_countType := Eval hnf in [countType of cube].
Canonical cube_finType := Eval hnf in [finType of cube].
Canonical cube_subType := Eval hnf in [subType of cube].
Canonical cube_subCountType := Eval hnf in [subCountType of cube].
Canonical cube_subFinType := Eval hnf in [subFinType of cube].
Definition mkFcube i : cube := Sub (i %% 6) (ltn_mod i 6).
Definition F0 := mkFcube 0.
Definition F1 := mkFcube 1.
Definition F2 := mkFcube 2.
Definition F3 := mkFcube 3.
Definition F4 := mkFcube 4.
Definition F5 := mkFcube 5.
Lemma Sh_inj : injective Sh.
Definition sh := (perm Sh_inj).
Lemma sh_inv : sh^-1 = sh.
Definition Sv (sc : square) : square := tnth [tuple c3; c2; c1; c0] sc.
Lemma Sv_inj : injective Sv.
Definition sv := (perm Sv_inj).
Lemma sv_inv : sv^-1 = sv.
Definition Sd1 (sc : square) : square := tnth [tuple c0; c3; c2; c1] sc.
Lemma Sd1_inj : injective Sd1.
Definition sd1 := (perm Sd1_inj).
Lemma sd1_inv : sd1^-1 = sd1.
Definition Sd2 (sc : square) : square := tnth [tuple c2; c1; c0; c3] sc.
Lemma Sd2_inj : injective Sd2.
Definition sd2 := (perm Sd2_inj).
Lemma sd2_inv : sd2^-1 = sd2.
Lemma ord_enum4 : enum 'I_4 = [:: c0; c1; c2; c3].
Lemma diff_id_sh : 1 != sh.
Definition isometries2 := [set 1; sh].
Lemma card_iso2 : #|isometries2| = 2.
Lemma group_set_iso2 : group_set isometries2.
Canonical iso2_group := Group group_set_iso2.
Definition isometries :=
[set p | [|| p == 1, p == r1, p == r2, p == r3,
p == sh, p == sv, p == sd1 | p == sd2 ]].
Definition opp (sc : square) := tnth [tuple c2; c3; c0; c1] sc.
Definition is_iso (p : {perm square}) := ∀ ci, p (opp ci) = opp (p ci).
Lemma isometries_iso : ∀ p, p \in isometries → is_iso p.
Ltac non_inj p a1 a2 heq1 heq2 :=
let h1:= fresh "h1" in
(absurd (p a1 = p a2); first (by red ⇒ - h1; move: (perm_inj h1));
by rewrite heq1 heq2; apply/eqP).
Ltac is_isoPtac p f e0 e1 e2 e3 :=
suff ->: p = f by [rewrite inE eqxx ?orbT];
let e := fresh "e" in apply/permP;
do 5?[case] ⇒ // ?; [move: e0 | move: e1 | move: e2 | move: e3] ⇒ e;
apply: etrans (congr1 p _) (etrans e _); apply/eqP; rewrite // permE.
Lemma is_isoP : ∀ p, reflect (is_iso p) (p \in isometries).
Lemma group_set_iso : group_set isometries.
Canonical iso_group := Group group_set_iso.
Lemma card_rot : #|rot| = 4.
Lemma group_set_rotations : group_set rotations.
Canonical rotations_group := Group group_set_rotations.
Notation col_squares := {ffun square → colors}.
Definition act_f (sc : col_squares) (p : {perm square}) : col_squares :=
[ffun z ⇒ sc (p^-1 z)].
Lemma act_f_1 : ∀ k, act_f k 1 = k.
Lemma act_f_morph : ∀ k x y, act_f k (x × y) = act_f (act_f k x) y.
Definition to := TotalAction act_f_1 act_f_morph.
Definition square_coloring_number2 := #|orbit to isometries2 @: setT|.
Definition square_coloring_number4 := #|orbit to rotations @: setT|.
Definition square_coloring_number8 := #|orbit to isometries @: setT|.
Lemma Fid : 'Fix_to(1) = setT.
Lemma card_Fid : #|'Fix_to(1)| = (n ^ 4)%N.
Definition coin0 (sc : col_squares) : colors := sc c0.
Definition coin1 (sc : col_squares) : colors := sc c1.
Definition coin2 (sc : col_squares) : colors := sc c2.
Definition coin3 (sc : col_squares) : colors := sc c3.
Lemma eqperm_map : ∀ p1 p2 : col_squares,
(p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: c0; c1; c2; c3].
Lemma F_Sh :
'Fix_to[sh] = [set x | (coin0 x == coin1 x) && (coin2 x == coin3 x)].
Lemma F_Sv :
'Fix_to[sv] = [set x | (coin0 x == coin3 x) && (coin2 x == coin1 x)].
Ltac inv_tac :=
apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _;
let a := fresh "a" in apply/permP ⇒ a;
apply/eqP; rewrite permM !permE; case: a; do 4?case.
Lemma r1_inv : r1^-1 = r3.
Lemma r2_inv : r2^-1 = r2.
Lemma r3_inv : r3^-1 = r1.
Lemma F_r2 :
'Fix_to[r2] = [set x | (coin0 x == coin2 x) && (coin1 x == coin3 x)].
Lemma F_r1 : 'Fix_to[r1] =
[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
Lemma F_r3 : 'Fix_to[r3] =
[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
Lemma card_n2 : ∀ x y z t : square, uniq [:: x; y; z; t] →
#|[set p : col_squares | (p x == p y) && (p z == p t)]| = (n ^ 2)%N.
Lemma card_n :
#|[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&& (coin2 x == coin3 x)]|
= n.
Lemma burnside_app2 : (square_coloring_number2 × 2 = n ^ 4 + n ^ 2)%N.
Lemma burnside_app_rot :
(square_coloring_number4 × 4 = n ^ 4 + n ^ 2 + 2 × n)%N.
Lemma F_Sd1 : 'Fix_to[sd1] = [set x | coin1 x == coin3 x].
Lemma card_n3 : ∀ x y : square, x != y →
#|[set k : col_squares | k x == k y]| = (n ^ 3)%N.
Lemma F_Sd2 : 'Fix_to[sd2] = [set x | coin0 x == coin2 x].
Lemma burnside_app_iso :
(square_coloring_number8 × 8 = n ^ 4 + 2 × n ^ 3 + 3 × n ^ 2 + 2 × n)%N.
End square_colouring.
Section cube_colouring.
Definition cube := 'I_6.
Canonical cube_eqType := Eval hnf in [eqType of cube].
Canonical cube_choiceType := Eval hnf in [choiceType of cube].
Canonical cube_countType := Eval hnf in [countType of cube].
Canonical cube_finType := Eval hnf in [finType of cube].
Canonical cube_subType := Eval hnf in [subType of cube].
Canonical cube_subCountType := Eval hnf in [subCountType of cube].
Canonical cube_subFinType := Eval hnf in [subFinType of cube].
Definition mkFcube i : cube := Sub (i %% 6) (ltn_mod i 6).
Definition F0 := mkFcube 0.
Definition F1 := mkFcube 1.
Definition F2 := mkFcube 2.
Definition F3 := mkFcube 3.
Definition F4 := mkFcube 4.
Definition F5 := mkFcube 5.
axial symetries
Definition S05 := [:: F0; F4; F3; F2; F1; F5].
Definition S05f (sc : cube) : cube := tnth [tuple of S05] sc.
Definition S14 := [:: F5; F1; F3; F2; F4; F0].
Definition S14f (sc : cube) : cube := tnth [tuple of S14] sc.
Definition S23 := [:: F5; F4; F2; F3; F1; F0].
Definition S23f (sc : cube) : cube := tnth [tuple of S23] sc.
Definition S05f (sc : cube) : cube := tnth [tuple of S05] sc.
Definition S14 := [:: F5; F1; F3; F2; F4; F0].
Definition S14f (sc : cube) : cube := tnth [tuple of S14] sc.
Definition S23 := [:: F5; F4; F2; F3; F1; F0].
Definition S23f (sc : cube) : cube := tnth [tuple of S23] sc.
rotations 90
Definition R05 := [:: F0; F2; F4; F1; F3; F5].
Definition R05f (sc : cube) : cube := tnth [tuple of R05] sc.
Definition R50 := [:: F0; F3; F1; F4; F2; F5].
Definition R50f (sc : cube) : cube := tnth [tuple of R50] sc.
Definition R14 := [:: F3; F1; F0; F5; F4; F2].
Definition R14f (sc : cube) : cube := tnth [tuple of R14] sc.
Definition R41 := [:: F2; F1; F5; F0; F4; F3].
Definition R41f (sc : cube) : cube := tnth [tuple of R41] sc.
Definition R23 := [:: F1; F5; F2; F3; F0; F4].
Definition R23f (sc : cube) : cube := tnth [tuple of R23] sc.
Definition R32 := [:: F4; F0; F2; F3; F5; F1].
Definition R32f (sc : cube) : cube := tnth [tuple of R32] sc.
Definition R05f (sc : cube) : cube := tnth [tuple of R05] sc.
Definition R50 := [:: F0; F3; F1; F4; F2; F5].
Definition R50f (sc : cube) : cube := tnth [tuple of R50] sc.
Definition R14 := [:: F3; F1; F0; F5; F4; F2].
Definition R14f (sc : cube) : cube := tnth [tuple of R14] sc.
Definition R41 := [:: F2; F1; F5; F0; F4; F3].
Definition R41f (sc : cube) : cube := tnth [tuple of R41] sc.
Definition R23 := [:: F1; F5; F2; F3; F0; F4].
Definition R23f (sc : cube) : cube := tnth [tuple of R23] sc.
Definition R32 := [:: F4; F0; F2; F3; F5; F1].
Definition R32f (sc : cube) : cube := tnth [tuple of R32] sc.
rotations 120
Definition R024 := [:: F2; F5; F4; F1; F0; F3].
Definition R024f (sc : cube) : cube := tnth [tuple of R024] sc.
Definition R042 := [:: F4; F3; F0; F5; F2; F1].
Definition R042f (sc : cube) : cube := tnth [tuple of R042] sc.
Definition R012 := [:: F1; F2; F0; F5; F3; F4].
Definition R012f (sc : cube) : cube := tnth [tuple of R012] sc.
Definition R021 := [:: F2; F0; F1; F4; F5; F3].
Definition R021f (sc : cube) : cube := tnth [tuple of R021] sc.
Definition R031 := [:: F3; F0; F4; F1; F5; F2].
Definition R031f (sc : cube) : cube := tnth [tuple of R031] sc.
Definition R013 := [:: F1; F3; F5; F0; F2; F4].
Definition R013f (sc : cube) : cube := tnth [tuple of R013] sc.
Definition R043 := [:: F4; F2; F5; F0; F3; F1].
Definition R043f (sc : cube) : cube := tnth [tuple of R043] sc.
Definition R034 := [:: F3; F5; F1; F4; F0; F2].
Definition R034f (sc : cube) : cube := tnth [tuple of R034] sc.
Definition R024f (sc : cube) : cube := tnth [tuple of R024] sc.
Definition R042 := [:: F4; F3; F0; F5; F2; F1].
Definition R042f (sc : cube) : cube := tnth [tuple of R042] sc.
Definition R012 := [:: F1; F2; F0; F5; F3; F4].
Definition R012f (sc : cube) : cube := tnth [tuple of R012] sc.
Definition R021 := [:: F2; F0; F1; F4; F5; F3].
Definition R021f (sc : cube) : cube := tnth [tuple of R021] sc.
Definition R031 := [:: F3; F0; F4; F1; F5; F2].
Definition R031f (sc : cube) : cube := tnth [tuple of R031] sc.
Definition R013 := [:: F1; F3; F5; F0; F2; F4].
Definition R013f (sc : cube) : cube := tnth [tuple of R013] sc.
Definition R043 := [:: F4; F2; F5; F0; F3; F1].
Definition R043f (sc : cube) : cube := tnth [tuple of R043] sc.
Definition R034 := [:: F3; F5; F1; F4; F0; F2].
Definition R034f (sc : cube) : cube := tnth [tuple of R034] sc.
last symmetries
Definition S1 := [:: F5; F2; F1; F4; F3; F0].
Definition S1f (sc : cube) : cube := tnth [tuple of S1] sc.
Definition S2 := [:: F5; F3; F4; F1; F2; F0].
Definition S2f (sc : cube) : cube := tnth [tuple of S2] sc.
Definition S3 := [:: F1; F0; F3; F2; F5; F4].
Definition S3f (sc : cube) : cube := tnth [tuple of S3] sc.
Definition S4 := [:: F4; F5; F3; F2; F0; F1].
Definition S4f (sc : cube) : cube := tnth [tuple of S4] sc.
Definition S5 := [:: F2; F4; F0; F5; F1; F3].
Definition S5f (sc : cube) : cube := tnth [tuple of S5] sc.
Definition S6 := [::F3; F4; F5; F0; F1; F2].
Definition S6f (sc : cube) : cube := tnth [tuple of S6] sc.
Lemma S1_inv : involutive S1f.
Lemma S2_inv : involutive S2f.
Lemma S3_inv : involutive S3f.
Lemma S4_inv : involutive S4f.
Lemma S5_inv : involutive S5f.
Lemma S6_inv : involutive S6f.
Lemma S05_inj : injective S05f.
Lemma S14_inj : injective S14f.
Lemma S23_inv : involutive S23f.
Lemma R05_inj : injective R05f.
Lemma R14_inj : injective R14f.
Lemma R23_inj : injective R23f.
Lemma R50_inj : injective R50f.
Lemma R41_inj : injective R41f.
Lemma R32_inj : injective R32f.
Lemma R024_inj : injective R024f.
Lemma R042_inj : injective R042f.
Lemma R012_inj : injective R012f.
Lemma R021_inj : injective R021f.
Lemma R031_inj : injective R031f.
Lemma R013_inj : injective R013f.
Lemma R043_inj : injective R043f.
Lemma R034_inj : injective R034f.
Definition id3 := 1 : {perm cube}.
Definition s05 := (perm S05_inj).
Definition s14 : {perm cube}.
Definition s23 := (perm (inv_inj S23_inv)).
Definition r05 := (perm R05_inj).
Definition r14 := (perm R14_inj).
Definition r23 := (perm R23_inj).
Definition r50 := (perm R50_inj).
Definition r41 := (perm R41_inj).
Definition r32 := (perm R32_inj).
Definition r024 := (perm R024_inj).
Definition r042 := (perm R042_inj).
Definition r012 := (perm R012_inj).
Definition r021 := (perm R021_inj).
Definition r031 := (perm R031_inj).
Definition r013 := (perm R013_inj).
Definition r043 := (perm R043_inj).
Definition r034 := (perm R034_inj).
Definition s1 := (perm (inv_inj S1_inv)).
Definition s2 := (perm (inv_inj S2_inv)).
Definition s3 := (perm (inv_inj S3_inv)).
Definition s4 := (perm (inv_inj S4_inv)).
Definition s5 := (perm (inv_inj S5_inv)).
Definition s6 := (perm (inv_inj S6_inv)).
Definition dir_iso3 := [set p |
[|| id3 == p, s05 == p, s14 == p, s23 == p, r05 == p, r14 == p, r23 == p,
r50 == p, r41 == p, r32 == p, r024 == p, r042 == p, r012 == p, r021 == p,
r031 == p, r013 == p, r043 == p, r034 == p,
s1 == p, s2 == p, s3 == p, s4 == p, s5 == p | s6 == p]].
Definition dir_iso3l := [:: id3; s05; s14; s23; r05; r14; r23; r50; r41;
r32; r024; r042; r012; r021; r031; r013; r043; r034;
s1; s2; s3; s4; s5; s6].
Definition S0 := [:: F5; F4; F3; F2; F1; F0].
Definition S0f (sc : cube) : cube := tnth [tuple of S0] sc.
Lemma S0_inv : involutive S0f.
Definition s0 := (perm (inv_inj S0_inv)).
Definition is_iso3 (p : {perm cube}) := ∀ fi, p (s0 fi) = s0 (p fi).
Lemma dir_iso_iso3 : ∀ p, p \in dir_iso3 → is_iso3 p.
Lemma iso3_ndir : ∀ p, p \in dir_iso3 → is_iso3 (s0 × p).
Definition sop (p : {perm cube}) : seq cube := fgraph (val p).
Lemma sop_inj : injective sop.
Definition prod_tuple (t1 t2 : seq cube) :=
map (fun n : 'I_6 ⇒ nth F0 t2 n) t1.
Lemma sop_spec x (n0 : 'I_6): nth F0 (sop x) n0 = x n0.
Lemma prod_t_correct : ∀ (x y : {perm cube}) (i : cube),
(x × y) i = nth F0 (prod_tuple (sop x) (sop y)) i.
Lemma sop_morph : {morph sop : x y / x × y >-> prod_tuple x y}.
Definition ecubes : seq cube := [:: F0; F1; F2; F3; F4; F5].
Lemma ecubes_def : ecubes = enum (@predT cube).
Definition seq_iso_L := [::
[:: F0; F1; F2; F3; F4; F5];
S05; S14; S23; R05; R14; R23; R50; R41; R32;
R024; R042; R012; R021; R031; R013; R043; R034;
S1; S2; S3; S4; S5; S6].
Lemma seqs1 : ∀ f injf, sop (@perm _ f injf) = map f ecubes.
Lemma Lcorrect : seq_iso_L == map sop [:: id3; s05; s14; s23; r05; r14; r23;
r50; r41; r32; r024; r042; r012; r021; r031; r013; r043; r034;
s1; s2; s3; s4; s5; s6].
Lemma iso0_1 : dir_iso3 =i dir_iso3l.
Lemma L_iso : ∀ p, (p \in dir_iso3) = (sop p \in seq_iso_L).
Lemma stable : ∀ x y,
x \in dir_iso3 → y \in dir_iso3 → x × y \in dir_iso3.
Lemma iso_eq_F0_F1 : ∀ r s : {perm cube}, r \in dir_iso3 →
s \in dir_iso3 → r F0 = s F0 → r F1 = s F1 → r = s.
Lemma ndir_s0p : ∀ p, p \in dir_iso3 → s0 × p \notin dir_iso3.
Definition indir_iso3l := map (mulg s0) dir_iso3l.
Definition iso3l := dir_iso3l ++ indir_iso3l.
Definition seq_iso3_L := map sop iso3l.
Lemma eqperm : ∀ p1 p2 : {perm cube},
(p1 == p2) = all (fun s ⇒ p1 s == p2 s) ecubes.
Lemma iso_eq_F0_F1_F2 : ∀ r s : {perm cube}, is_iso3 r →
is_iso3 s → r F0 = s F0 → r F1 = s F1 → r F2 = s F2 → r = s.
Ltac iso_tac :=
let a := fresh "a" in apply/permP ⇒ a;
apply/eqP; rewrite !permM !permE; case: a; do 6?case.
Ltac inv_tac :=
apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _; iso_tac.
Lemma dir_s0p : ∀ p, (s0 × p) \in dir_iso3 → p \notin dir_iso3.
Definition is_iso3b p := (p × s0 == s0 × p).
Definition iso3 := [set p | is_iso3b p].
Lemma is_iso3P : ∀ p, reflect (is_iso3 p) (p \in iso3).
Lemma group_set_iso3 : group_set iso3.
Canonical iso_group3 := Group group_set_iso3.
Lemma group_set_diso3 : group_set dir_iso3.
Canonical diso_group3 := Group group_set_diso3.
Lemma gen_diso3 : dir_iso3 = <<[set r05; r14]>>.
Notation col_cubes := {ffun cube → colors}.
Definition act_g (sc : col_cubes) (p : {perm cube}) : col_cubes :=
[ffun z ⇒ sc (p^-1 z)].
Lemma act_g_1 : ∀ k, act_g k 1 = k.
Lemma act_g_morph : ∀ k x y, act_g k (x × y) = act_g (act_g k x) y.
Definition to_g := TotalAction act_g_1 act_g_morph.
Definition cube_coloring_number24 := #|orbit to_g diso_group3 @: setT|.
Lemma Fid3 : 'Fix_to_g[1] = setT.
Lemma card_Fid3 : #|'Fix_to_g[1]| = (n ^ 6)%N.
Definition col0 (sc : col_cubes) : colors := sc F0.
Definition col1 (sc : col_cubes) : colors := sc F1.
Definition col2 (sc : col_cubes) : colors := sc F2.
Definition col3 (sc : col_cubes) : colors := sc F3.
Definition col4 (sc : col_cubes) : colors := sc F4.
Definition col5 (sc : col_cubes) : colors := sc F5.
Lemma eqperm_map2 : ∀ p1 p2 : col_cubes,
(p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: F0; F1; F2; F3; F4; F5].
Notation infE := (sameP afix1P eqP).
Lemma F_s05 :
'Fix_to_g[s05] = [set x | (col1 x == col4 x) && (col2 x == col3 x)].
Lemma F_s14 :
'Fix_to_g[s14]= [set x | (col0 x == col5 x) && (col2 x == col3 x)].
Lemma r05_inv : r05^-1 = r50.
Lemma r50_inv : r50^-1 = r05.
Lemma r14_inv : r14^-1 = r41.
Lemma r41_inv : r41^-1 = r14.
Lemma s23_inv : s23^-1 = s23.
Lemma F_s23 :
'Fix_to_g[s23] = [set x | (col0 x == col5 x) && (col1 x == col4 x)].
Lemma F_r05 : 'Fix_to_g[r05]=
[set x | (col1 x == col2 x) && (col2 x == col3 x)
&& (col3 x == col4 x)].
Lemma F_r50 : 'Fix_to_g[r50]=
[set x | (col1 x == col2 x) && (col2 x == col3 x)
&& (col3 x == col4 x)].
Lemma F_r23 : 'Fix_to_g[r23] =
[set x | (col0 x == col1 x) && (col1 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r32 : 'Fix_to_g[r32] =
[set x | (col0 x == col1 x) && (col1 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r14 : 'Fix_to_g[r14] =
[set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
Lemma F_r41 : 'Fix_to_g[r41] =
[set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
Lemma F_r024 : 'Fix_to_g[r024] =
[set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
&& (col3 x == col5 x) ].
Lemma F_r042 : 'Fix_to_g[r042] =
[set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
&& (col3 x == col5 x)].
Lemma F_r012 : 'Fix_to_g[r012] =
[set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r021 : 'Fix_to_g[r021] =
[set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r031 : 'Fix_to_g[r031] =
[set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r013 : 'Fix_to_g[r013] =
[set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r043 : 'Fix_to_g[r043] =
[set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
&& (col2 x == col5 x)].
Lemma F_r034 : 'Fix_to_g[r034] =
[set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
&& (col2 x == col5 x)].
Lemma F_s1 : 'Fix_to_g[s1] =
[set x | (col0 x == col5 x) && (col1 x == col2 x) && (col3 x == col4 x)].
Lemma F_s2 : 'Fix_to_g[s2] =
[set x | (col0 x == col5 x) && (col1 x == col3 x) && (col2 x == col4 x)].
Lemma F_s3 : 'Fix_to_g[s3] =
[set x | (col0 x == col1 x) && (col2 x == col3 x) && (col4 x == col5 x)].
Lemma F_s4 : 'Fix_to_g[s4] =
[set x | (col0 x == col4 x) && (col1 x == col5 x) && (col2 x == col3 x)].
Lemma F_s5 : 'Fix_to_g[s5] =
[set x | (col0 x == col2 x) && (col1 x == col4 x) && (col3 x == col5 x)].
Lemma F_s6 : 'Fix_to_g[s6] =
[set x | (col0 x == col3 x) && (col1 x == col4 x) && (col2 x == col5 x)].
Lemma uniq4_uniq6 : ∀ x y z t : cube,
uniq [:: x; y; z; t] → ∃ u, ∃ v, uniq [:: x; y; z; t; u; v].
Lemma card_n4 : ∀ x y z t : cube, uniq [:: x; y; z; t] →
#|[set p : col_cubes | (p x == p y) && (p z == p t)]| = (n ^ 4)%N.
Lemma card_n3_3 : ∀ x y z t: cube, uniq [:: x; y; z; t] →
#|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p z == p t)]|
= (n ^ 3)%N.
Lemma card_n2_3 : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
#|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p t == p u )
&& (p u== p v)]| = (n ^ 2)%N.
Lemma card_n3s : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
#|[set p : col_cubes | (p x == p y) && (p z == p t)&& (p u == p v )]|
= (n ^ 3)%N.
Lemma burnside_app_iso3 :
(cube_coloring_number24 × 24 =
n ^ 6 + 6 × n ^ 3 + 3 × n ^ 4 + 8 × (n ^ 2) + 6 × n ^ 3)%N.
End cube_colouring.
End colouring.
Corollary burnside_app_iso_3_3col: cube_coloring_number24 3 = 57.
Corollary burnside_app_iso_2_4col: square_coloring_number8 4 = 55.
Definition S1f (sc : cube) : cube := tnth [tuple of S1] sc.
Definition S2 := [:: F5; F3; F4; F1; F2; F0].
Definition S2f (sc : cube) : cube := tnth [tuple of S2] sc.
Definition S3 := [:: F1; F0; F3; F2; F5; F4].
Definition S3f (sc : cube) : cube := tnth [tuple of S3] sc.
Definition S4 := [:: F4; F5; F3; F2; F0; F1].
Definition S4f (sc : cube) : cube := tnth [tuple of S4] sc.
Definition S5 := [:: F2; F4; F0; F5; F1; F3].
Definition S5f (sc : cube) : cube := tnth [tuple of S5] sc.
Definition S6 := [::F3; F4; F5; F0; F1; F2].
Definition S6f (sc : cube) : cube := tnth [tuple of S6] sc.
Lemma S1_inv : involutive S1f.
Lemma S2_inv : involutive S2f.
Lemma S3_inv : involutive S3f.
Lemma S4_inv : involutive S4f.
Lemma S5_inv : involutive S5f.
Lemma S6_inv : involutive S6f.
Lemma S05_inj : injective S05f.
Lemma S14_inj : injective S14f.
Lemma S23_inv : involutive S23f.
Lemma R05_inj : injective R05f.
Lemma R14_inj : injective R14f.
Lemma R23_inj : injective R23f.
Lemma R50_inj : injective R50f.
Lemma R41_inj : injective R41f.
Lemma R32_inj : injective R32f.
Lemma R024_inj : injective R024f.
Lemma R042_inj : injective R042f.
Lemma R012_inj : injective R012f.
Lemma R021_inj : injective R021f.
Lemma R031_inj : injective R031f.
Lemma R013_inj : injective R013f.
Lemma R043_inj : injective R043f.
Lemma R034_inj : injective R034f.
Definition id3 := 1 : {perm cube}.
Definition s05 := (perm S05_inj).
Definition s14 : {perm cube}.
Definition s23 := (perm (inv_inj S23_inv)).
Definition r05 := (perm R05_inj).
Definition r14 := (perm R14_inj).
Definition r23 := (perm R23_inj).
Definition r50 := (perm R50_inj).
Definition r41 := (perm R41_inj).
Definition r32 := (perm R32_inj).
Definition r024 := (perm R024_inj).
Definition r042 := (perm R042_inj).
Definition r012 := (perm R012_inj).
Definition r021 := (perm R021_inj).
Definition r031 := (perm R031_inj).
Definition r013 := (perm R013_inj).
Definition r043 := (perm R043_inj).
Definition r034 := (perm R034_inj).
Definition s1 := (perm (inv_inj S1_inv)).
Definition s2 := (perm (inv_inj S2_inv)).
Definition s3 := (perm (inv_inj S3_inv)).
Definition s4 := (perm (inv_inj S4_inv)).
Definition s5 := (perm (inv_inj S5_inv)).
Definition s6 := (perm (inv_inj S6_inv)).
Definition dir_iso3 := [set p |
[|| id3 == p, s05 == p, s14 == p, s23 == p, r05 == p, r14 == p, r23 == p,
r50 == p, r41 == p, r32 == p, r024 == p, r042 == p, r012 == p, r021 == p,
r031 == p, r013 == p, r043 == p, r034 == p,
s1 == p, s2 == p, s3 == p, s4 == p, s5 == p | s6 == p]].
Definition dir_iso3l := [:: id3; s05; s14; s23; r05; r14; r23; r50; r41;
r32; r024; r042; r012; r021; r031; r013; r043; r034;
s1; s2; s3; s4; s5; s6].
Definition S0 := [:: F5; F4; F3; F2; F1; F0].
Definition S0f (sc : cube) : cube := tnth [tuple of S0] sc.
Lemma S0_inv : involutive S0f.
Definition s0 := (perm (inv_inj S0_inv)).
Definition is_iso3 (p : {perm cube}) := ∀ fi, p (s0 fi) = s0 (p fi).
Lemma dir_iso_iso3 : ∀ p, p \in dir_iso3 → is_iso3 p.
Lemma iso3_ndir : ∀ p, p \in dir_iso3 → is_iso3 (s0 × p).
Definition sop (p : {perm cube}) : seq cube := fgraph (val p).
Lemma sop_inj : injective sop.
Definition prod_tuple (t1 t2 : seq cube) :=
map (fun n : 'I_6 ⇒ nth F0 t2 n) t1.
Lemma sop_spec x (n0 : 'I_6): nth F0 (sop x) n0 = x n0.
Lemma prod_t_correct : ∀ (x y : {perm cube}) (i : cube),
(x × y) i = nth F0 (prod_tuple (sop x) (sop y)) i.
Lemma sop_morph : {morph sop : x y / x × y >-> prod_tuple x y}.
Definition ecubes : seq cube := [:: F0; F1; F2; F3; F4; F5].
Lemma ecubes_def : ecubes = enum (@predT cube).
Definition seq_iso_L := [::
[:: F0; F1; F2; F3; F4; F5];
S05; S14; S23; R05; R14; R23; R50; R41; R32;
R024; R042; R012; R021; R031; R013; R043; R034;
S1; S2; S3; S4; S5; S6].
Lemma seqs1 : ∀ f injf, sop (@perm _ f injf) = map f ecubes.
Lemma Lcorrect : seq_iso_L == map sop [:: id3; s05; s14; s23; r05; r14; r23;
r50; r41; r32; r024; r042; r012; r021; r031; r013; r043; r034;
s1; s2; s3; s4; s5; s6].
Lemma iso0_1 : dir_iso3 =i dir_iso3l.
Lemma L_iso : ∀ p, (p \in dir_iso3) = (sop p \in seq_iso_L).
Lemma stable : ∀ x y,
x \in dir_iso3 → y \in dir_iso3 → x × y \in dir_iso3.
Lemma iso_eq_F0_F1 : ∀ r s : {perm cube}, r \in dir_iso3 →
s \in dir_iso3 → r F0 = s F0 → r F1 = s F1 → r = s.
Lemma ndir_s0p : ∀ p, p \in dir_iso3 → s0 × p \notin dir_iso3.
Definition indir_iso3l := map (mulg s0) dir_iso3l.
Definition iso3l := dir_iso3l ++ indir_iso3l.
Definition seq_iso3_L := map sop iso3l.
Lemma eqperm : ∀ p1 p2 : {perm cube},
(p1 == p2) = all (fun s ⇒ p1 s == p2 s) ecubes.
Lemma iso_eq_F0_F1_F2 : ∀ r s : {perm cube}, is_iso3 r →
is_iso3 s → r F0 = s F0 → r F1 = s F1 → r F2 = s F2 → r = s.
Ltac iso_tac :=
let a := fresh "a" in apply/permP ⇒ a;
apply/eqP; rewrite !permM !permE; case: a; do 6?case.
Ltac inv_tac :=
apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _; iso_tac.
Lemma dir_s0p : ∀ p, (s0 × p) \in dir_iso3 → p \notin dir_iso3.
Definition is_iso3b p := (p × s0 == s0 × p).
Definition iso3 := [set p | is_iso3b p].
Lemma is_iso3P : ∀ p, reflect (is_iso3 p) (p \in iso3).
Lemma group_set_iso3 : group_set iso3.
Canonical iso_group3 := Group group_set_iso3.
Lemma group_set_diso3 : group_set dir_iso3.
Canonical diso_group3 := Group group_set_diso3.
Lemma gen_diso3 : dir_iso3 = <<[set r05; r14]>>.
Notation col_cubes := {ffun cube → colors}.
Definition act_g (sc : col_cubes) (p : {perm cube}) : col_cubes :=
[ffun z ⇒ sc (p^-1 z)].
Lemma act_g_1 : ∀ k, act_g k 1 = k.
Lemma act_g_morph : ∀ k x y, act_g k (x × y) = act_g (act_g k x) y.
Definition to_g := TotalAction act_g_1 act_g_morph.
Definition cube_coloring_number24 := #|orbit to_g diso_group3 @: setT|.
Lemma Fid3 : 'Fix_to_g[1] = setT.
Lemma card_Fid3 : #|'Fix_to_g[1]| = (n ^ 6)%N.
Definition col0 (sc : col_cubes) : colors := sc F0.
Definition col1 (sc : col_cubes) : colors := sc F1.
Definition col2 (sc : col_cubes) : colors := sc F2.
Definition col3 (sc : col_cubes) : colors := sc F3.
Definition col4 (sc : col_cubes) : colors := sc F4.
Definition col5 (sc : col_cubes) : colors := sc F5.
Lemma eqperm_map2 : ∀ p1 p2 : col_cubes,
(p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: F0; F1; F2; F3; F4; F5].
Notation infE := (sameP afix1P eqP).
Lemma F_s05 :
'Fix_to_g[s05] = [set x | (col1 x == col4 x) && (col2 x == col3 x)].
Lemma F_s14 :
'Fix_to_g[s14]= [set x | (col0 x == col5 x) && (col2 x == col3 x)].
Lemma r05_inv : r05^-1 = r50.
Lemma r50_inv : r50^-1 = r05.
Lemma r14_inv : r14^-1 = r41.
Lemma r41_inv : r41^-1 = r14.
Lemma s23_inv : s23^-1 = s23.
Lemma F_s23 :
'Fix_to_g[s23] = [set x | (col0 x == col5 x) && (col1 x == col4 x)].
Lemma F_r05 : 'Fix_to_g[r05]=
[set x | (col1 x == col2 x) && (col2 x == col3 x)
&& (col3 x == col4 x)].
Lemma F_r50 : 'Fix_to_g[r50]=
[set x | (col1 x == col2 x) && (col2 x == col3 x)
&& (col3 x == col4 x)].
Lemma F_r23 : 'Fix_to_g[r23] =
[set x | (col0 x == col1 x) && (col1 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r32 : 'Fix_to_g[r32] =
[set x | (col0 x == col1 x) && (col1 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r14 : 'Fix_to_g[r14] =
[set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
Lemma F_r41 : 'Fix_to_g[r41] =
[set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
Lemma F_r024 : 'Fix_to_g[r024] =
[set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
&& (col3 x == col5 x) ].
Lemma F_r042 : 'Fix_to_g[r042] =
[set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
&& (col3 x == col5 x)].
Lemma F_r012 : 'Fix_to_g[r012] =
[set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r021 : 'Fix_to_g[r021] =
[set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r031 : 'Fix_to_g[r031] =
[set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r013 : 'Fix_to_g[r013] =
[set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
&& (col4 x == col5 x)].
Lemma F_r043 : 'Fix_to_g[r043] =
[set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
&& (col2 x == col5 x)].
Lemma F_r034 : 'Fix_to_g[r034] =
[set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
&& (col2 x == col5 x)].
Lemma F_s1 : 'Fix_to_g[s1] =
[set x | (col0 x == col5 x) && (col1 x == col2 x) && (col3 x == col4 x)].
Lemma F_s2 : 'Fix_to_g[s2] =
[set x | (col0 x == col5 x) && (col1 x == col3 x) && (col2 x == col4 x)].
Lemma F_s3 : 'Fix_to_g[s3] =
[set x | (col0 x == col1 x) && (col2 x == col3 x) && (col4 x == col5 x)].
Lemma F_s4 : 'Fix_to_g[s4] =
[set x | (col0 x == col4 x) && (col1 x == col5 x) && (col2 x == col3 x)].
Lemma F_s5 : 'Fix_to_g[s5] =
[set x | (col0 x == col2 x) && (col1 x == col4 x) && (col3 x == col5 x)].
Lemma F_s6 : 'Fix_to_g[s6] =
[set x | (col0 x == col3 x) && (col1 x == col4 x) && (col2 x == col5 x)].
Lemma uniq4_uniq6 : ∀ x y z t : cube,
uniq [:: x; y; z; t] → ∃ u, ∃ v, uniq [:: x; y; z; t; u; v].
Lemma card_n4 : ∀ x y z t : cube, uniq [:: x; y; z; t] →
#|[set p : col_cubes | (p x == p y) && (p z == p t)]| = (n ^ 4)%N.
Lemma card_n3_3 : ∀ x y z t: cube, uniq [:: x; y; z; t] →
#|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p z == p t)]|
= (n ^ 3)%N.
Lemma card_n2_3 : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
#|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p t == p u )
&& (p u== p v)]| = (n ^ 2)%N.
Lemma card_n3s : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
#|[set p : col_cubes | (p x == p y) && (p z == p t)&& (p u == p v )]|
= (n ^ 3)%N.
Lemma burnside_app_iso3 :
(cube_coloring_number24 × 24 =
n ^ 6 + 6 × n ^ 3 + 3 × n ^ 4 + 8 × (n ^ 2) + 6 × n ^ 3)%N.
End cube_colouring.
End colouring.
Corollary burnside_app_iso_3_3col: cube_coloring_number24 3 = 57.
Corollary burnside_app_iso_2_4col: square_coloring_number8 4 = 55.