Vertex colors given by a list

A coloring, or any other labeling of the vertices of a Cslib.Complexity.Graph by numbers, can be given as a list of numbers parallel to the vertex list: the label of a vertex is the entry at its first occurrence among the declared vertices (Cslib.Complexity.colorOf). The colored instances of color coding take colors in this form, and NP verifiers with colorings or vertex ranks as witnesses read them in this form (Cslib.Complexity.mem_NP_of_colorOf).

Main definitions

• Cslib.Complexity.colorOf: the color of a vertex in a list of colors.
• Cslib.Complexity.encColoredGraph: graphs with a list of vertex colors.

Main results

• Cslib.Complexity.colorOf_map: listing the colors of the declared vertices gives every declared vertex its color.
• Cslib.Complexity.computableInPolyTime_colorOf, Cslib.Complexity.computableInPolyTime_colorOf_comp: reading a color is polynomial-time.
• Cslib.Complexity.Graph.length_encList_map_le: quadratic encoded-length bound for a bounded vertex labeling listed along G.vertices.
• Cslib.Complexity.mem_NP_of_colorOf: NP membership for graph problems verified from a bounded vertex labeling.

def Cslib.Complexity.colorOf (G : Graph) (cs : List ℕ) (v : ℕ) : ℕ

The color of the vertex v under a list of colors cs parallel to the vertex list of G: the entry of cs at the first occurrence of v, and 0 when there is none.

@[reducible, inline]

abbrev Cslib.Complexity.encColoredGraph : Graph × List ℕ ↪ List Bool

Graphs with vertex colors: the graph (encGraph), framed, then the list of colors parallel to its vertex list (Cslib.Complexity.colorOf), each color framed and in binary.

@[simp]

theorem Cslib.Complexity.colorOf_map {G : Graph} {c : ℕ → ℕ} {v : ℕ} (hv : v ∈ G.vertices) : colorOf G (List.map c G.vertices) v = c v

The list of the colors of the declared vertices under c gives every declared vertex its color.

theorem Cslib.Complexity.computableInPolyTime_colorOf : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × List ℕ) × ℕ) => colorOf p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair encColoredGraph Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat

Reading a color from a list of colors is polynomial-time.

theorem Cslib.Complexity.computableInPolyTime_colorOf_comp {γ : Type} {enc : γ ↪ List Bool} {G : γ → Graph} {cs : γ → List ℕ} {v : γ → ℕ} (hG : Turing.MultiTapeTM.ComputableInPolyTime G enc encGraph) (hcs : Turing.MultiTapeTM.ComputableInPolyTime cs enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hv : Turing.MultiTapeTM.ComputableInPolyTime v enc Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => colorOf (G x) (cs x) (v x)) enc Turing.MultiTapeTM.encNat

Reading computed colors of computed vertices is polynomial-time; the compositional form of Cslib.Complexity.computableInPolyTime_colorOf used by fun_prop.

theorem Cslib.Complexity.Graph.length_encList_map_le {G : Graph} {f : ℕ → ℕ} {n : ℕ} (hG : G.vertices.length ≤ n) (hf : ∀ v ∈ G.vertices, f v ≤ n) : ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (List.map f G.vertices)).length ≤ 2 * n ^ 2 + n

A labeling listed along the vertex list of a graph with at most n listed vertices, whose values on the declared vertices are at most n, has an encoding of length at most 2 n ^ 2 + n.

theorem Cslib.Complexity.mem_NP_of_colorOf {α : Type} {enc : α ↪ List Bool} (graph : α → Graph) {S : Set α} {check : α × List ℕ → Bool} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBool) (hlen : ∀ (x : α), (graph x).vertices.length ≤ (enc x).length) (hsound : ∀ (x : α) (cs : List ℕ), check (x, cs) = true → x ∈ S) (hcomplete : ∀ x ∈ S, ∃ (g : ℕ → ℕ), (∀ v ∈ (graph x).vertices, g v ≤ (graph x).vertices.length) ∧ check (x, List.map g (graph x).vertices) = true) : S ∈ NP enc

NP membership from a bounded vertex labeling. Let check be polynomial-time on instances x paired with a list of vertex labels (Cslib.Complexity.colorOf). If every accepted list certifies membership in S, and every member x ∈ S has a labeling g of the declared vertices (graph x).vertices bounded by (graph x).vertices.length whose list (graph x).vertices.map g is accepted by check, then S ∈ NP enc.