The gap graph, as an algorithm

The verifier does not read a graph; it reads an algorithm that answers three questions about one — how many edges, where an edge's ends are, and whether a pair of symbols satisfies it. This module packages the gap graph that way, by reading the string the reduction writes.

The constraint is a bounded-key decision: an edge's record names its constraint by a code, and the code, together with the two symbol blocks, is all the constraint depends on. Both are clamped to constant width, so the key is constant-size even on strings that are not graphs at all.

Main definitions

• Complexity.gapAlg — the gap graph as an AlgCSP

Main results

• Complexity.gapAlg_models — it agrees with the gap graph

Reading the graph

noncomputable def Complexity.gapStr (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (z : List Bool) : List Bool

The graph string a verifier argument names.

Equations

• Complexity.gapStr F hd E padU z = Complexity.gapAll F hd E padU (Complexity.pairFst (Complexity.pairFst z))

theorem Complexity.gapStr_mem_FP (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) : gapStr F hd E padU ∈ FP

noncomputable def Complexity.gapCodeBlk (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (z : List Bool) : List Bool

The code of the constraint the argument names, clamped to the number of constraints there are.

Equations

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

theorem Complexity.gapCodeBlk_mem_FP (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) : gapCodeBlk F hd E padU ∈ FP

noncomputable def Complexity.gapOkKey (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (z : List Bool) : List Bool

Everything the constraint depends on: the code and the two symbol blocks.

Equations

• Complexity.gapOkKey F hd E padU z = Complexity.pair (Complexity.gapCodeBlk F hd E padU z) (List.take 46 (Complexity.pairSnd z))

theorem Complexity.gapOkKey_mem_FP (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) : gapOkKey F hd E padU ∈ FP

theorem Complexity.gapOkKey_length_le (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (z : List Bool) : (gapOkKey F hd E padU z).length ≤ 2 * cRel + 48

def Complexity.gapOkPred (k : List Bool) : Prop

What the constraint says, of the key alone.

Equations

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

noncomputable def Complexity.gapOk (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) : Language

The constraint, as a language on the verifier's verdict argument.

Equations

• Complexity.gapOk F hd E padU = {z : List Bool | Complexity.gapOkPred (Complexity.gapOkKey F hd E padU z)}

theorem Complexity.gapOk_mem_P (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) : gapOk F hd E padU ∈ P

The record

noncomputable def Complexity.gapAlg (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) : AlgCSP

The gap graph as an algorithm.

Equations

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

@[simp]

theorem Complexity.numEdges_gapAlg (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) (x : List Bool) : (gapAlg F hd E padU hgap).numEdges x = gEdges (gapAll F hd E padU x)

@[simp]

theorem Complexity.width_gapAlg (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) : (gapAlg F hd E padU hgap).width = 23

theorem Complexity.vert_gapAlg_false (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) (x : List Bool) (e : ℕ) : (gapAlg F hd E padU hgap).vert false x e = gTail (gapAll F hd E padU x) e

theorem Complexity.vert_gapAlg_true (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) (x : List Bool) (e : ℕ) : (gapAlg F hd E padU hgap).vert true x e = gHead (gapAll F hd E padU x) e

@[simp]

theorem Complexity.ok_gapAlg (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) (hgap : gapAll F hd E padU ∈ FP) : (gapAlg F hd E padU hgap).ok = gapOk F hd E padU

It models the gap graph

theorem Complexity.gapCodeBlk_length (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (hmark : ∀ (x : List Bool), padU x = List.replicate (padU x).length true) (hle : ∀ (x : List Bool), 3 * List.length (Φ x) ≤ (padU x).length) (x : List Bool) (e : ℕ) (he : e < (gapAllG F hd padU x).numEdges) (a : List Bool) : (gapCodeBlk F hd E padU (pair (pair x (List.replicate e true)) a)).length = codeOfRel ((gapAllG F hd padU x).rel ⟨e, he⟩)

theorem Complexity.gapAlg_models (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hgap : gapAll F hd E padU ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (hmark : ∀ (x : List Bool), padU x = List.replicate (padU x).length true) (hle : ∀ (x : List Bool), 3 * List.length (Φ x) ≤ (padU x).length) : (gapAlg F hd E padU hgap).Models (fun (x : List Bool) => gapAllG F hd padU x) (symEnc DinurAlpha 23) (symDec DinurAlpha)

The algorithm models the gap graph.