Library mathcomp.solvable.burnside_app
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 HB Require Import structures.
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]|.
Arguments burnside_formula {gT}.
Section colouring.
Variable n : nat.
Definition colors := 'I_n.
Section square_colouring.
Definition square := 'I_4.
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.
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.
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.