-
Definition Sh (
sc :
square) :
square :=
tnth [tuple c1; c0; c3; c2] sc.
+
Definition Sh (
sc :
square) :
square :=
tnth [tuple c1; c0; c3; c2] sc.
-
Lemma Sh_inj :
injective Sh.
+
Lemma Sh_inj :
injective Sh.
Definition sh := (
perm Sh_inj).
-
Lemma sh_inv :
sh^-1 = sh.
+
Lemma sh_inv :
sh^-1 = sh.
-
Definition Sv (
sc :
square) :
square :=
tnth [tuple c3; c2; c1; c0] sc.
+
Definition Sv (
sc :
square) :
square :=
tnth [tuple c3; c2; c1; c0] sc.
-
Lemma Sv_inj :
injective Sv.
+
Lemma Sv_inj :
injective Sv.
Definition sv := (
perm Sv_inj).
-
Lemma sv_inv :
sv^-1 = sv.
+
Lemma sv_inv :
sv^-1 = sv.
-
Definition Sd1 (
sc :
square) :
square :=
tnth [tuple c0; c3; c2; c1] sc.
+
Definition Sd1 (
sc :
square) :
square :=
tnth [tuple c0; c3; c2; c1] sc.
-
Lemma Sd1_inj :
injective Sd1.
+
Lemma Sd1_inj :
injective Sd1.
Definition sd1 := (
perm Sd1_inj).
-
Lemma sd1_inv :
sd1^-1 = sd1.
+
Lemma sd1_inv :
sd1^-1 = sd1.
-
Definition Sd2 (
sc :
square) :
square :=
tnth [tuple c2; c1; c0; c3] sc.
+
Definition Sd2 (
sc :
square) :
square :=
tnth [tuple c2; c1; c0; c3] sc.
-
Lemma Sd2_inj :
injective Sd2.
+
Lemma Sd2_inj :
injective Sd2.
Definition sd2 := (
perm Sd2_inj).
-
Lemma sd2_inv :
sd2^-1 = sd2.
+
Lemma sd2_inv :
sd2^-1 = sd2.
-
Lemma ord_enum4 :
enum 'I_4 = [:: c0; c1; c2; c3].
+
Lemma ord_enum4 :
enum 'I_4 = [:: c0; c1; c2; c3].
-
Lemma diff_id_sh : 1
!= sh.
+
Lemma diff_id_sh : 1
!= sh.
-
Definition isometries2 :=
[set 1
; sh].
+
Definition isometries2 :=
[set 1
; sh].
-
Lemma card_iso2 :
#|isometries2| = 2.
+
Lemma card_iso2 :
#|isometries2| = 2.
Lemma group_set_iso2 :
group_set isometries2.
@@ -225,33 +224,33 @@ symmetries
Definition isometries :=
-
[set p | [|| p == 1
, p == r1, p == r2, p == r3,
-
p == sh, p == sv, p == sd1 | p == sd2 ]].
+
[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 opp (
sc :
square) :=
tnth [tuple c2; c3; c0; c1] sc.
-
Definition is_iso (
p :
{perm square}) :=
∀ ci,
p (
opp ci)
= opp (
p ci).
+
Definition is_iso (
p :
{perm square}) :=
∀ ci,
p (
opp ci)
= opp (
p ci).
-
Lemma isometries_iso :
∀ p,
p \in isometries → is_iso p.
+
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));
+(
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];
+
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.
+
apply:
etrans (
congr1 p _) (
etrans e _);
apply/
eqP;
rewrite //
permE.
-
Lemma is_isoP :
∀ p,
reflect (
is_iso p) (
p \in isometries).
+
Lemma is_isoP :
∀ p,
reflect (
is_iso p) (
p \in isometries).
Lemma group_set_iso :
group_set isometries.
@@ -260,7 +259,7 @@ symmetries
Canonical iso_group :=
Group group_set_iso.
-
Lemma card_rot :
#|rot| = 4.
+
Lemma card_rot :
#|rot| = 4.
Lemma group_set_rotations :
group_set rotations.
@@ -269,31 +268,31 @@ symmetries
Canonical rotations_group :=
Group group_set_rotations.
-
Notation col_squares :=
{ffun square → colors}.
+
Notation col_squares :=
{ffun square → colors}.
-
Definition act_f (
sc :
col_squares) (
p :
{perm square}) :
col_squares :=
-
[ffun z ⇒ sc (
p^-1 z)
].
+
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_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.
+
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|.
+
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 Fid :
'Fix_to(1
) = setT.
-
Lemma card_Fid :
#|'Fix_to(1
)| = (
n ^ 4)%
N.
+
Lemma card_Fid :
#|'Fix_to(1
)| = (
n ^ 4)%
N.
Definition coin0 (
sc :
col_squares) :
colors :=
sc c0.
@@ -303,72 +302,72 @@ symmetries
Lemma eqperm_map :
∀ p1 p2 :
col_squares,
-
(p1 == p2) = all (
fun s ⇒
p1 s == p2 s)
[:: c0; c1; c2; c3].
+
(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)].
+
'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)].
+
'Fix_to[sv] = [set x | (coin0 x == coin3 x) && (coin2 x == coin1 x)].
Ltac inv_tac :=
-
apply:
esym (
etrans _ (
mul1g _));
apply:
canRL (
mulgK _)
_;
+
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 r1_inv :
r1^-1 = r3.
-
Lemma r2_inv :
r2^-1 = r2.
+
Lemma r2_inv :
r2^-1 = r2.
-
Lemma r3_inv :
r3^-1 = r1.
+
Lemma r3_inv :
r3^-1 = r1.
Lemma F_r2 :
-
'Fix_to[r2] = [set x | (coin0 x == coin2 x) && (coin1 x == coin3 x)].
+
'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_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 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_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.
+
#|[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_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.
+ (
square_coloring_number4 × 4
= n ^ 4
+ n ^ 2
+ 2
× n)%
N.
-
Lemma F_Sd1 :
'Fix_to[sd1] = [set x | coin1 x == coin3 x].
+
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 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 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.
+ (
square_coloring_number8 × 8
= n ^ 4
+ 2
× n ^ 3
+ 3
× n ^ 2
+ 2
× n)%
N.
End square_colouring.
@@ -377,17 +376,17 @@ symmetries
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 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 mkFcube i :
cube :=
Sub (
i %% 6) (
ltn_mod i 6).
Definition F0 :=
mkFcube 0.
Definition F1 :=
mkFcube 1.
Definition F2 :=
mkFcube 2.
@@ -402,16 +401,16 @@ symmetries
axial symetries
-
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.
+
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 S1_inv :
involutive S1f.
-
Lemma S2_inv :
involutive S2f.
+
Lemma S2_inv :
involutive S2f.
-
Lemma S3_inv :
involutive S3f.
+
Lemma S3_inv :
involutive S3f.
-
Lemma S4_inv :
involutive S4f.
+
Lemma S4_inv :
involutive S4f.
-
Lemma S5_inv :
involutive S5f.
+
Lemma S5_inv :
involutive S5f.
-
Lemma S6_inv :
involutive S6f.
+
Lemma S6_inv :
involutive S6f.
-
Lemma S05_inj :
injective S05f.
+
Lemma S05_inj :
injective S05f.
-
Lemma S14_inj :
injective S14f.
+
Lemma S14_inj :
injective S14f.
-
Lemma S23_inv :
involutive S23f.
+
Lemma S23_inv :
involutive S23f.
-
Lemma R05_inj :
injective R05f.
+
Lemma R05_inj :
injective R05f.
-
Lemma R14_inj :
injective R14f.
+
Lemma R14_inj :
injective R14f.
-
Lemma R23_inj :
injective R23f.
+
Lemma R23_inj :
injective R23f.
-
Lemma R50_inj :
injective R50f.
+
Lemma R50_inj :
injective R50f.
-
Lemma R41_inj :
injective R41f.
+
Lemma R41_inj :
injective R41f.
-
Lemma R32_inj :
injective R32f.
+
Lemma R32_inj :
injective R32f.
-
Lemma R024_inj :
injective R024f.
+
Lemma R024_inj :
injective R024f.
-
Lemma R042_inj :
injective R042f.
+
Lemma R042_inj :
injective R042f.
-
Lemma R012_inj :
injective R012f.
+
Lemma R012_inj :
injective R012f.
-
Lemma R021_inj :
injective R021f.
+
Lemma R021_inj :
injective R021f.
-
Lemma R031_inj :
injective R031f.
+
Lemma R031_inj :
injective R031f.
-
Lemma R013_inj :
injective R013f.
+
Lemma R013_inj :
injective R013f.
-
Lemma R043_inj :
injective R043f.
+
Lemma R043_inj :
injective R043f.
-
Lemma R034_inj :
injective R034f.
+
Lemma R034_inj :
injective R034f.
-
Definition id3 := 1
: {perm cube}.
+
Definition id3 := 1
: {perm cube}.
Definition s05 := (
perm S05_inj).
-
Definition s14 :
{perm cube}.
+
Definition s14 :
{perm cube}.
-
Definition s23 := (
perm (
inv_inj S23_inv)).
+
Definition s23 := (
perm (
inv_inj S23_inv)).
Definition r05 := (
perm R05_inj).
Definition r14 := (
perm R14_inj).
Definition r23 := (
perm R23_inj).
@@ -569,118 +568,118 @@ symmetries
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 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_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 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.
+
Definition S0 :=
[:: F5; F4; F3; F2; F1; F0].
+
Definition S0f (
sc :
cube) :
cube :=
tnth [tuple of S0] sc.
-
Lemma S0_inv :
involutive S0f.
+
Lemma S0_inv :
involutive S0f.
-
Definition s0 := (
perm (
inv_inj S0_inv)).
+
Definition s0 := (
perm (
inv_inj S0_inv)).
-
Definition is_iso3 (
p :
{perm cube}) :=
∀ fi,
p (
s0 fi)
= s0 (
p fi).
+
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 dir_iso_iso3 :
∀ p,
p \in dir_iso3 → is_iso3 p.
-
Lemma iso3_ndir :
∀ p,
p \in dir_iso3 → is_iso3 (
s0 × p).
+
Lemma iso3_ndir :
∀ p,
p \in dir_iso3 → is_iso3 (
s0 × p).
-
Definition sop (
p :
{perm cube}) :
seq cube :=
val (
val (
val p)).
+
Definition sop (
p :
{perm cube}) :
seq cube :=
fgraph (
val p).
-
Lemma sop_inj :
injective sop.
+
Lemma sop_inj :
injective sop.
Definition prod_tuple (
t1 t2 :
seq cube) :=
-
map (
fun n :
'I_6 ⇒
nth F0 t2 n)
t1.
+
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 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 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}.
+
Lemma sop_morph :
{morph sop : x y / x × y >-> prod_tuple x y}.
-
Definition ecubes :
seq cube :=
[:: F0; F1; F2; F3; F4; F5].
+
Definition ecubes :
seq cube :=
[:: F0; F1; F2; F3; F4; F5].
-
Lemma ecubes_def :
ecubes = enum (@
predT cube).
+
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].
+
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 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 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 iso0_1 :
dir_iso3 =i dir_iso3l.
-
Lemma L_iso :
∀ p,
(p \in dir_iso3) = (sop p \in seq_iso_L).
+
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.
+
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 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.
+
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 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 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.
+
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 :=
@@ -689,17 +688,17 @@ symmetries
Ltac inv_tac :=
-
apply:
esym (
etrans _ (
mul1g _));
apply:
canRL (
mulgK _)
_;
iso_tac.
+
apply:
esym (
etrans _ (
mul1g _));
apply:
canRL (
mulgK _)
_;
iso_tac.
-
Lemma dir_s0p :
∀ p,
(s0 × p) \in dir_iso3 → p \notin dir_iso3.
+
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].
+
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 is_iso3P :
∀ p,
reflect (
is_iso3 p) (
p \in iso3).
Lemma group_set_iso3 :
group_set iso3.
@@ -712,32 +711,32 @@ symmetries
Canonical diso_group3 :=
Group group_set_diso3.
-
Lemma gen_diso3 :
dir_iso3 = <<[set r05; r14]>>.
+
Lemma gen_diso3 :
dir_iso3 = <<[set r05; r14]>>.
-
Notation col_cubes :=
{ffun cube → colors}.
+
Notation col_cubes :=
{ffun cube → colors}.
-
Definition act_g (
sc :
col_cubes) (
p :
{perm cube}) :
col_cubes :=
-
[ffun z ⇒ sc (
p^-1 z)
].
+
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_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.
+
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|.
+
Definition cube_coloring_number24 :=
#|orbit to_g diso_group3 @: setT|.
-
Lemma Fid3 :
'Fix_to_g[1
] = setT.
+
Lemma Fid3 :
'Fix_to_g[1
] = setT.
-
Lemma card_Fid3 :
#|'Fix_to_g[1
]| = (
n ^ 6)%
N.
+
Lemma card_Fid3 :
#|'Fix_to_g[1
]| = (
n ^ 6)%
N.
Definition col0 (
sc :
col_cubes) :
colors :=
sc F0.
@@ -749,157 +748,157 @@ symmetries
Lemma eqperm_map2 :
∀ p1 p2 :
col_cubes,
-
(p1 == p2) = all (
fun s ⇒
p1 s == p2 s)
[:: F0; F1; F2; F3; F4; F5].
+
(p1 == p2) = all (
fun s ⇒
p1 s == p2 s)
[:: F0; F1; F2; F3; F4; F5].
-
Notation infE := (
sameP afix1P eqP).
+
Notation infE := (
sameP afix1P eqP).
Lemma F_s05 :
-
'Fix_to_g[s05] = [set x | (col1 x == col4 x) && (col2 x == col3 x)].
+
'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)].
+
'Fix_to_g[s14]= [set x | (col0 x == col5 x) && (col2 x == col3 x)].
-
Lemma r05_inv :
r05^-1 = r50.
+
Lemma r05_inv :
r05^-1 = r50.
-
Lemma r50_inv :
r50^-1 = r05.
+
Lemma r50_inv :
r50^-1 = r05.
-
Lemma r14_inv :
r14^-1 = r41.
+
Lemma r14_inv :
r14^-1 = r41.
-
Lemma r41_inv :
r41^-1 = r14.
+
Lemma r41_inv :
r41^-1 = r14.
-
Lemma s23_inv :
s23^-1 = s23.
+
Lemma s23_inv :
s23^-1 = s23.
Lemma F_s23 :
-
'Fix_to_g[s23] = [set x | (col0 x == col5 x) && (col1 x == col4 x)].
+
'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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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 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].
+
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_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_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_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 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.
+ (
cube_coloring_number24 × 24
=
+
n ^ 6
+ 6
× n ^ 3
+ 3
× n ^ 4
+ 8
× (n ^ 2
) + 6
× n ^ 3)%
N.
End cube_colouring.
@@ -908,10 +907,10 @@ symmetries
End colouring.
-
Corollary burnside_app_iso_3_3col:
cube_coloring_number24 3
= 57.
+
Corollary burnside_app_iso_3_3col:
cube_coloring_number24 3
= 57.
-
Corollary burnside_app_iso_2_4col:
square_coloring_number8 4
= 55.
+
Corollary burnside_app_iso_2_4col:
square_coloring_number8 4
= 55.