The Multicoloured Graph of an Independent Set Instance

Lax496464.WH_F2_MccConstruction · concepts/Lax496464/WH_F2_MccConstruction.lean · lax-496464

definition

Loading review…

Natural Language Statement

Definition

Let $G$ be a graph on $n$ vertices and $k \in \mathbb N$ . The multicoloured graph of $(G, k)$ has the $kn$ vertices $(c, v)$ for $c < k$ and $v$ a vertex of $G$ , the vertex $(c, v)$ coloured $c$ . Two vertices $(c, u)$ and $(c', v)$ are adjacent when

$c \ne c'$ ,
$u \ne v$ , and
$uv$ is not an edge of $G$ .

A multicoloured clique chooses one vertex $(c, v_c)$ of each colour, pairwise adjacent; the vertices $v_0, \dots, v_{k-1}$ are then $k$ distinct pairwise non-adjacent vertices of $G$ . This is the construction of [FHRV09, Lemma 1] applied to the complement of $G$ (see also [CFK+15, Theorem 13.7]).

The reduction $reduce$ maps the word of an instance $(G, k)$ of $WH_F1_IndependentSetMatrix$ to the word of its multicoloured graph, and every other word to the empty word.

Concept map

13 concepts; 2 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax496464.WH_F1_IndependentSetMatrix
2	import Lax762056.GraphEncoding
3	import Lax888481.MulticolouredClique
4	import Mathlib.Logic.Equiv.Fin.Basic
5
6	/-!
7	---
8	title: The Multicoloured Graph of an Independent Set Instance
9	type: definition
10	---
11	Let $G$ be a graph on $n$ vertices and $k \in \mathbb N$ . The multicoloured graph of $(G, k)$
12	has the $kn$ vertices $(c, v)$ for $c < k$ and $v$ a vertex of $G$ , the vertex $(c, v)$ coloured
13	$c$ . Two vertices $(c, u)$ and $(c', v)$ are adjacent when
14
15	* $c \ne c'$ ,
16	* $u \ne v$ , and
17	* $uv$ is not an edge of $G$ .
18
19	A multicoloured clique chooses one vertex $(c, v_c)$ of each colour, pairwise adjacent; the
20	vertices $v_0, \dots, v_{k-1}$ are then $k$ distinct pairwise non-adjacent vertices of $G$ . This is
21	the construction of [FHRV09, Lemma 1] applied to the complement of $G$ (see also
22	[CFK+15, Theorem 13.7]).
23
24	The reduction `reduce` maps the word of an instance $(G, k)$ of `WH_F1_IndependentSetMatrix` to
25	the word of its multicoloured graph, and every other word to the empty word.
26
27	# Formalization Notes
28
29	Vertex numbering. The vertex $(c, v)$ is numbered $v + nc$ (`finProdFinEquiv`), so the
30	vertices are listed colour by colour, and the vertex $s$ is $(\lfloor s/n \rfloor, s \bmod n)$ .
31
32	The word is in the format of `Lax888481.MulticolouredClique`: a compressed sparse row block,
33	one colour per vertex, and the number of colours. The block lists the number $N = kn$ of vertices,
34	the number of edges, the $N + 1$ offsets, and the targets, which are the neighbours of each vertex
35	in increasing order. The colours follow, and the word ends with $k$ . The word is given explicitly,
36	as the unique word of this form, so that the running time of the reduction is a statement about a
37	single output.
38
39	The map on words. `reduce` is a function on all words. On the word of an instance it takes the
40	instance chosen by `Classical.choose`; this instance is unique, since the encoding is injective.
41	The empty word is a no-instance of Multicoloured Clique.
42	-/
43
44	namespace Lax496464.WH_F2_MccConstruction
45
46	open Lax762056.GraphEncoding (Instance)
47
48	-- The multicoloured graph
49
50	/-- The copies `(c, u)` and `(c', v)` are adjacent. -/
51	def Adj (I : Instance) (a b : Fin I.threshold × Fin I.order) : Prop :=
52	a.1 ≠ b.1 ∧ a.2 ≠ b.2 ∧ ¬ I.graph.Adj a.2 b.2
53
54	/-- The graph on the `k · n` copies, the copy `(c, v)` being the vertex `v + n c`. -/
55	def graph (I : Instance) : SimpleGraph (Fin (I.threshold * I.order)) where
56	Adj s t := Adj I (finProdFinEquiv.symm s) (finProdFinEquiv.symm t)
57	symm := ⟨fun _ _ ⟨h1, h2, h3⟩ => ⟨h1.symm, h2.symm, fun h => h3 h.symm⟩⟩
58	loopless := ⟨fun _ ⟨h1, _, _⟩ => h1 rfl⟩
59
60	/-- The Multicoloured Clique instance: `k` colours, `k · n` vertices, the copy `(c, v)`
61	coloured `c`. -/
62	def construct (I : Instance) : Lax888481.MulticolouredClique.Instance where
63	colours := I.threshold
64	vertices := I.threshold * I.order
65	graph := graph I
66	colour s := (finProdFinEquiv.symm s).1
67	adj_colour_ne _ _ h := h.1
68
69	-- The word of the multicoloured graph
70
71	open Classical in
72	/-- Adjacency in `G` of the numbers `u` and `v`; false unless both are vertices. -/
73	noncomputable def adjG (I : Instance) (u v : ℕ) : Bool :=
74	decide (∃ (hu : u < I.order) (hv : v < I.order), I.graph.Adj ⟨u, hu⟩ ⟨v, hv⟩)
75
76	/-- The number `k · n` of vertices of the multicoloured graph. -/
77	def size (I : Instance) : ℕ := I.threshold * I.order
78
79	/-- Adjacency in the multicoloured graph of the numbers `s` and `t`; false unless both are
80	vertices. -/
81	noncomputable def adjB (I : Instance) (s t : ℕ) : Bool :=
82	decide (s < size I ∧ t < size I ∧ s / I.order ≠ t / I.order ∧ s % I.order ≠ t % I.order ∧
83	adjG I (s % I.order) (t % I.order) = false)
84
85	/-- The neighbours of the vertex `s`, in increasing order. -/
86	noncomputable def neighbours (I : Instance) (s : ℕ) : List ℕ :=
87	(List.range (size I)).filter (adjB I s)
88
89	/-- The target array: the neighbours of each vertex in turn. -/
90	noncomputable def targets (I : Instance) : List ℕ :=
91	(List.range (size I)).flatMap (neighbours I)
92
93	/-- The offsets: `0`, then the running sums of the degrees. -/
94	noncomputable def offsets (I : Instance) : List ℕ :=
95	(List.range (size I + 1)).map fun s => ((List.range s).map fun r => (neighbours I r).length).sum
96
97	/-- The colour of each vertex. -/
98	def colours (I : Instance) : List ℕ := (List.range (size I)).map fun s => s / I.order
99
100	/-- The word of the multicoloured graph: the number of vertices, the number of edges, the
101	offsets, the targets, the colours, and the number of colours. -/
102	noncomputable def word (I : Instance) : List ℕ :=
103	[size I, (targets I).length / 2] ++ offsets I ++ targets I ++ colours I ++ [I.threshold]
104
105	-- The reduction on words
106
107	open Classical in
108	/-- The reduction: the word of the multicoloured graph on the word of an instance, and the
109	empty word elsewhere. -/
110	noncomputable def reduce (x : List ℕ) : List ℕ :=
111	if h : x ∈ WH_F1_IndependentSetMatrix.Instances then word (Classical.choose h) else []
112
113	end Lax496464.WH_F2_MccConstruction
114

Formalization Notes

Vertex numbering. The vertex $(c, v)$ is numbered $v + nc$ ( $finProdFinEquiv$ ), so the vertices are listed colour by colour, and the vertex $s$ is $(\lfloor s/n \rfloor, s \bmod n)$ .

The word is in the format of $Lax888481.MulticolouredClique$ : a compressed sparse row block, one colour per vertex, and the number of colours. The block lists the number $N = kn$ of vertices, the number of edges, the $N + 1$ offsets, and the targets, which are the neighbours of each vertex in increasing order. The colours follow, and the word ends with $k$ . The word is given explicitly, as the unique word of this form, so that the running time of the reduction is a statement about a single output.

The map on words. $reduce$ is a function on all words. On the word of an instance it takes the instance chosen by $Classical.choose$ ; this instance is unique, since the encoding is injective. The empty word is a no-instance of Multicoloured Clique.

Builds on

Used by

Lax496464.WH_F4_IndependentSetToMcc

From Mathlib

Mathlib.Logic.Equiv.Fin.Basic

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The Multicoloured Graph of an Independent Set Instance

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments