Padding a constraint graph with isolated vertices

The expander family built by the zig-zag tower supplies graphs only at certain sizes, far apart from one another. Rather than fold a large expander onto an arbitrary vertex count — which costs a delicate spectral argument — one can enlarge the constraint graph instead, up to the next size the family offers.

Nothing is lost by doing so. The added vertices carry no edges, and every quantity the amplification tracks is counted over edges: the number of edges is unchanged, an assignment matters only through its values on the original vertices, and so both the unsatisfiability value and satisfiability are untouched.

Main definitions

• Complexity.ConstraintGraph.pad — the same graph on more vertices

Main results

• Complexity.ConstraintGraph.numEdges_pad, unsatVal_pad, satisfiable_pad_iff — padding changes nothing that matters

def Complexity.ConstraintGraph.pad {α : Type} (G : ConstraintGraph α) (N : ℕ) (h : G.numVerts ≤ N) : ConstraintGraph α

The same constraint graph, on N ≥ numVerts vertices; the extra ones carry no edges.

Equations

• G.pad N h = { numVerts := N, numEdges := G.numEdges, tail := fun (e : Fin G.numEdges) => Fin.castLE h (G.tail e), head := fun (e : Fin G.numEdges) => Fin.castLE h (G.head e), rel := G.rel }

@[simp]

theorem Complexity.ConstraintGraph.numEdges_pad {α : Type} (G : ConstraintGraph α) (N : ℕ) (h : G.numVerts ≤ N) : (G.pad N h).numEdges = G.numEdges

@[simp]

theorem Complexity.ConstraintGraph.numVerts_pad {α : Type} (G : ConstraintGraph α) (N : ℕ) (h : G.numVerts ≤ N) : (G.pad N h).numVerts = N

def Complexity.ConstraintGraph.restrict {α : Type} (G : ConstraintGraph α) {N : ℕ} (h : G.numVerts ≤ N) (a : (G.pad N h).Assignment) : G.Assignment

Restricting an assignment of the padded graph to the original vertices.

Equations

• G.restrict h a v = a (Fin.castLE h v)

noncomputable def Complexity.ConstraintGraph.extend {α : Type} [Nonempty α] (G : ConstraintGraph α) {N : ℕ} (h : G.numVerts ≤ N) (a : G.Assignment) : (G.pad N h).Assignment

Extending an assignment to the padded graph, arbitrarily on the new vertices.

Equations

• G.extend h a v = if hv : ↑v < G.numVerts then a ⟨↑v, hv⟩ else Classical.arbitrary α

theorem Complexity.ConstraintGraph.restrict_extend {α : Type} [Nonempty α] (G : ConstraintGraph α) {N : ℕ} (h : G.numVerts ≤ N) (a : G.Assignment) : G.restrict h (G.extend h a) = a

theorem Complexity.ConstraintGraph.satisfies_pad_iff {α : Type} (G : ConstraintGraph α) {N : ℕ} (h : G.numVerts ≤ N) (a : (G.pad N h).Assignment) (e : Fin (G.pad N h).numEdges) : (G.pad N h).Satisfies a e ↔ G.Satisfies (G.restrict h a) e

theorem Complexity.ConstraintGraph.unsatEdges_pad {α : Type} (G : ConstraintGraph α) {N : ℕ} (h : G.numVerts ≤ N) (a : (G.pad N h).Assignment) : (G.pad N h).unsatEdges a = G.unsatEdges (G.restrict h a)

theorem Complexity.ConstraintGraph.unsatFrac_pad {α : Type} (G : ConstraintGraph α) {N : ℕ} (h : G.numVerts ≤ N) (a : (G.pad N h).Assignment) : (G.pad N h).unsatFrac a = G.unsatFrac (G.restrict h a)

theorem Complexity.ConstraintGraph.unsatVal_pad {α : Type} [Fintype α] [Nonempty α] [DecidableEq α] (G : ConstraintGraph α) (N : ℕ) (h : G.numVerts ≤ N) : (G.pad N h).unsatVal = G.unsatVal

Padding does not change the value.

theorem Complexity.ConstraintGraph.satisfiable_pad_iff {α : Type} [Nonempty α] (G : ConstraintGraph α) (N : ℕ) (h : G.numVerts ≤ N) : (G.pad N h).Satisfiable ↔ G.Satisfiable

Padding does not change satisfiability.