A constraint graph as a string

An algorithm that runs Dinur's amplification has to hold a constraint graph in its hand. Over a fixed finite alphabet a graph is a small amount of data: how many vertices, and for each edge its two endpoints and its constraint. The endpoints are numbers below the vertex count, and the constraint — a predicate on two symbols — is itself one of finitely many, so it too is a number.

That is the encoding used here: the vertex count in unary, followed by a list of records, each three unary numbers. Numbering the constraints rather than tabulating them keeps every record a triple of numbers, so the whole toolkit of UnaryList applies; and because the number of constraints is a constant, reading one back is a lookup on a bounded key.

Main definitions

• Complexity.relOfCode, Complexity.codeOfRel — numbering the constraints
• Complexity.encGraph — the graph as a string
• Complexity.gVerts, gEdges, gTail, gHead, gCode — reading it back

Main results

• Complexity.gVerts_encGraph, gEdges_encGraph, gTail_encGraph, gHead_encGraph, gRel_encGraph — the reading inverts the writing
• Complexity.buildGraph_eq, Complexity.buildGraph_mem_FP — a rule for each edge writes the graph, in polynomial time

Numbering the constraints

noncomputable def Complexity.relOfCode (α : Type) [Fintype α] [DecidableEq α] (r : ℕ) : α → α → Bool

The constraint a code stands for; the always-false constraint for a code that is out of range.

Equations

• Complexity.relOfCode α r = if h : r < Fintype.card (α → α → Bool) then (Fintype.equivFin (α → α → Bool)).symm ⟨r, h⟩ else fun (x x_1 : α) => false

noncomputable def Complexity.codeOfRel {α : Type} [Fintype α] [DecidableEq α] (f : α → α → Bool) : ℕ

The code of a constraint.

Equations

• Complexity.codeOfRel f = ↑((Fintype.equivFin (α → α → Bool)) f)

theorem Complexity.codeOfRel_lt {α : Type} [Fintype α] [DecidableEq α] (f : α → α → Bool) : codeOfRel f < Fintype.card (α → α → Bool)

@[simp]

theorem Complexity.relOfCode_codeOfRel {α : Type} [Fintype α] [DecidableEq α] (f : α → α → Bool) : relOfCode α (codeOfRel f) = f

The encoding

noncomputable def Complexity.edgeRecs {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) : List (List Bool × List Bool × List Bool)

One record for each edge: its two endpoints and the code of its constraint.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.length_edgeRecs {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) : (edgeRecs G).length = G.numEdges

noncomputable def Complexity.encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) : List Bool

A constraint graph, as a string.

Equations

• Complexity.encGraph G = Complexity.pair (List.replicate G.numVerts true) (Complexity.DataEncode.bitstringEncode (Complexity.edgeRecs G))

Reading it back

def Complexity.gVerts (z : List Bool) : ℕ

How many vertices an encoded graph has.

Equations

• Complexity.gVerts z = (Complexity.pairFst z).length

noncomputable def Complexity.gEdges (z : List Bool) : ℕ

How many edges.

Equations

• Complexity.gEdges z = (Complexity.posCount (Complexity.pairSnd z)).length

noncomputable def Complexity.gTail (z : List Bool) (e : ℕ) : ℕ

The first endpoint of an edge.

Equations

• Complexity.gTail z e = (Complexity.recFst (Complexity.pairSnd z) e).length

noncomputable def Complexity.gHead (z : List Bool) (e : ℕ) : ℕ

The second endpoint.

Equations

• Complexity.gHead z e = (Complexity.recSnd (Complexity.pairSnd z) e).length

noncomputable def Complexity.gCode (z : List Bool) (e : ℕ) : ℕ

The code of the constraint.

Equations

• Complexity.gCode z e = (Complexity.recThd (Complexity.pairSnd z) e).length

@[simp]

theorem Complexity.gVerts_encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) : gVerts (encGraph G) = G.numVerts

@[simp]

theorem Complexity.gEdges_encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) : gEdges (encGraph G) = G.numEdges

theorem Complexity.getElem_edgeRecs {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (e : ℕ) (he : e < G.numEdges) : (edgeRecs G)[e] = (List.replicate (↑(G.tail ⟨e, he⟩)) true, List.replicate (↑(G.head ⟨e, he⟩)) true, List.replicate (codeOfRel (G.rel ⟨e, he⟩)) true)

@[simp]

theorem Complexity.gTail_encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (e : ℕ) (he : e < G.numEdges) : gTail (encGraph G) e = ↑(G.tail ⟨e, he⟩)

@[simp]

theorem Complexity.gHead_encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (e : ℕ) (he : e < G.numEdges) : gHead (encGraph G) e = ↑(G.head ⟨e, he⟩)

theorem Complexity.gCode_encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (e : ℕ) (he : e < G.numEdges) : gCode (encGraph G) e = codeOfRel (G.rel ⟨e, he⟩)

theorem Complexity.gRel_encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (e : ℕ) (he : e < G.numEdges) : relOfCode α (gCode (encGraph G) e) = G.rel ⟨e, he⟩

The constraint of an edge survives the round trip.

theorem Complexity.length_encGraph_le {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) : (encGraph G).length ≤ 2 * G.numVerts + 4 + G.numEdges * (8 * G.numVerts + 4 * Fintype.card (α → α → Bool) + 10)

How long a graph's encoding is, in terms of its two counts.

Writing one out

noncomputable def Complexity.buildGraph (nv cnt E : List Bool → List Bool) (z : List Bool) : List Bool

A graph assembled from a vertex count, an edge count and a rule for each edge record.

Equations

• Complexity.buildGraph nv cnt E z = Complexity.pair (nv z) (Complexity.listEncFn E (Complexity.pair (cnt z) z))

theorem Complexity.buildGraph_mem_FP {nv cnt E : List Bool → List Bool} (hnv : nv ∈ FP) (hcnt : cnt ∈ FP) (hE : E ∈ FP) : buildGraph nv cnt E ∈ FP

theorem Complexity.buildGraph_eq {α : Type} [Fintype α] [DecidableEq α] {nv cnt E : List Bool → List Bool} {z : List Bool} {G : ConstraintGraph α} (hnv : nv z = List.replicate G.numVerts true) (hcnt : cnt z = List.replicate G.numEdges true) (hE : ∀ (e : ℕ) (he : e < G.numEdges), E (pair z (List.replicate e true)) = encTriple (List.replicate (↑(G.tail ⟨e, he⟩)) true) (List.replicate (↑(G.head ⟨e, he⟩)) true) (List.replicate (codeOfRel (G.rel ⟨e, he⟩)) true)) : buildGraph nv cnt E z = encGraph G

The rule writes the graph.

Reading one, in polynomial time

theorem Complexity.gVertsFn_mem_FP {g : List Bool → List Bool} (hg : g ∈ FP) : (fun (z : List Bool) => marks (pairFst (g z))) ∈ FP

theorem Complexity.gEdgesFn_mem_FP {g : List Bool → List Bool} (hg : g ∈ FP) : (fun (z : List Bool) => posCount (pairSnd (g z))) ∈ FP

theorem Complexity.gTailFn_mem_FP {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (z : List Bool) => recFst (pairSnd (g z)) (f z).length) ∈ FP

theorem Complexity.gHeadFn_mem_FP {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (z : List Bool) => recSnd (pairSnd (g z)) (f z).length) ∈ FP

theorem Complexity.gCodeFn_mem_FP {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (z : List Bool) => recThd (pairSnd (g z)) (f z).length) ∈ FP

theorem Complexity.length_marks_fstBlock (z : List Bool) : (marks (pairFst z)).length = gVerts z

theorem Complexity.length_posCount_sndBlock (z : List Bool) : (posCount (pairSnd z)).length = gEdges z

theorem Complexity.length_recFst_sndBlock (z : List Bool) (e : ℕ) : (recFst (pairSnd z) e).length = gTail z e

theorem Complexity.length_recSnd_sndBlock (z : List Bool) (e : ℕ) : (recSnd (pairSnd z) e).length = gHead z e

theorem Complexity.length_recThd_sndBlock (z : List Bool) (e : ℕ) : (recThd (pairSnd z) e).length = gCode z e