Degree reduction

The first half of Dinur's preprocessing: an arbitrary constraint graph, whose vertices may have wildly different degrees, is replaced by a regular one over the same alphabet.

The vertices of the new graph are the half-edges of the old one — an edge together with one of its endpoints — so there are exactly 2 · numEdges of them, however lopsided the original degrees were. Each half-edge has

• one edge-link, to the other half of its own edge, carrying that edge's original constraint, and
• E.degree cloud-links, wiring together the half-edges that share an endpoint, by a member of an ExpanderFamily, carrying equality constraints.

So the result is (1 + E.degree)-regular by construction, with no padding, and its size is a constant multiple of the original's — which is what the amplification bookkeeping needs.

The cloud rotation, without dependent types

A cloud's expander lives on Fin (cloud size), and cloud sizes differ, so the naive rotation map forces a transport along owner p' = owner p that is not type-correct to rewrite. The fix is cloudRotAux, which takes the cloud's enumeration l as a parameter: within it the length is fixed, and involutivity is an ordinary argument about a Nodup list. At the top level the only rewriting needed is cloudList (owner p') = cloudList (owner p), an equation between plain lists with no dependent type in sight.

Main definitions

• ConstraintGraph.owner, flipHalf, cloud, cloudList — the cloud structure on half-edges
• ConstraintGraph.cloudRotAux, cloudRot — the cloud-link rotation
• ConstraintGraph.reduceGraph, reduce — the regular graph and system

Main results

• ConstraintGraph.cloudRotAux_involutive, cloudRot_involutive
• ConstraintGraph.cloudRot_getElem — a cloud, read through its enumeration, is a copy of the family's expander
• ConstraintGraph.order_reduceGraph, deg_reduceGraph — size 2 · numEdges, degree 1 + E.degree
• ConstraintGraph.satisfiable_reduce_of_satisfiable — completeness

Half-edges and clouds

@[reducible, inline]

abbrev Complexity.ConstraintGraph.HalfEdge {α : Type} (G : ConstraintGraph α) : Type

A half-edge: an edge together with one of its two endpoints (false is the tail, true the head). These are the vertices of the reduced graph.

Equations

• G.HalfEdge = (Fin G.numEdges × Bool)

def Complexity.ConstraintGraph.owner {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : Fin G.numVerts

The vertex a half-edge is attached to.

Equations

• G.owner p = if p.2 = true then G.head p.1 else G.tail p.1

def Complexity.ConstraintGraph.flipHalf {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : G.HalfEdge

The other half of the same edge.

Equations

• G.flipHalf p = (p.1, !p.2)

theorem Complexity.ConstraintGraph.flipHalf_involutive {α : Type} (G : ConstraintGraph α) : Function.Involutive G.flipHalf

def Complexity.ConstraintGraph.cloud {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : Finset G.HalfEdge

The half-edges attached to v.

Equations

• G.cloud v = {p : G.HalfEdge | G.owner p = v}

@[simp]

theorem Complexity.ConstraintGraph.mem_cloud {α : Type} (G : ConstraintGraph α) {v : Fin G.numVerts} {p : G.HalfEdge} : p ∈ G.cloud v ↔ G.owner p = v

def Complexity.ConstraintGraph.halfCode {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : ℕ

The number naming a half-edge. The head of an edge is numbered before its tail, which is the order Fintype enumerates Bool in.

Equations

• G.halfCode p = 2 * ↑p.1 + if p.2 = true then 0 else 1

theorem Complexity.ConstraintGraph.halfCode_injective {α : Type} (G : ConstraintGraph α) : Function.Injective G.halfCode

instance Complexity.ConstraintGraph.halfLE_trans {α : Type} (G : ConstraintGraph α) : IsTrans G.HalfEdge fun (p q : G.HalfEdge) => G.halfCode p ≤ G.halfCode q

instance Complexity.ConstraintGraph.halfLE_antisymm {α : Type} (G : ConstraintGraph α) : Std.Antisymm fun (p q : G.HalfEdge) => G.halfCode p ≤ G.halfCode q

instance Complexity.ConstraintGraph.halfLE_total {α : Type} (G : ConstraintGraph α) : Std.Total fun (p q : G.HalfEdge) => G.halfCode p ≤ G.halfCode q

noncomputable def Complexity.ConstraintGraph.cloudList {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : List G.HalfEdge

The half-edges of a cloud, listed without repetition, in order of their numbers — the order an algorithm can find them in.

Equations

• G.cloudList v = (G.cloud v).sort fun (p q : G.HalfEdge) => G.halfCode p ≤ G.halfCode q

theorem Complexity.ConstraintGraph.nodup_cloudList {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : (G.cloudList v).Nodup

theorem Complexity.ConstraintGraph.pairwise_cloudList {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : List.Pairwise (fun (p q : G.HalfEdge) => G.halfCode p ≤ G.halfCode q) (G.cloudList v)

@[simp]

theorem Complexity.ConstraintGraph.mem_cloudList {α : Type} (G : ConstraintGraph α) {v : Fin G.numVerts} {p : G.HalfEdge} : p ∈ G.cloudList v ↔ p ∈ G.cloud v

theorem Complexity.ConstraintGraph.mem_cloudList_self {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : p ∈ G.cloudList (G.owner p)

The cloud rotation

noncomputable def Complexity.ConstraintGraph.cloudRotAux {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (l : List G.HalfEdge) (p : G.HalfEdge) (j : Fin E.degree) : G.HalfEdge × Fin E.degree

The cloud-link rotation, with the cloud's enumeration passed in explicitly so that no dependent rewriting is ever needed.

Equations

• G.cloudRotAux E l p j = if h : List.idxOf p l < l.length then have q := E.rot l.length (⟨List.idxOf p l, h⟩, j); (l.getD (↑q.1) p, q.2) else (p, j)

theorem Complexity.ConstraintGraph.cloudRotAux_involutive {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) {l : List G.HalfEdge} (hnd : l.Nodup) {p : G.HalfEdge} (hp : p ∈ l) (j : Fin E.degree) : G.cloudRotAux E l (G.cloudRotAux E l p j).1 (G.cloudRotAux E l p j).2 = (p, j)

Inside one cloud, the rotation is an involution: this is the family's own involutivity, transported through the enumeration.

noncomputable def Complexity.ConstraintGraph.cloudRot {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (p : G.HalfEdge) (j : Fin E.degree) : G.HalfEdge × Fin E.degree

The cloud-link rotation at a half-edge, using its own cloud.

Equations

• G.cloudRot E p j = G.cloudRotAux E (G.cloudList (G.owner p)) p j

theorem Complexity.ConstraintGraph.cloudRotAux_mem {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) {l : List G.HalfEdge} {p : G.HalfEdge} (hp : p ∈ l) (j : Fin E.degree) : (G.cloudRotAux E l p j).1 ∈ l

A cloud-link lands inside the enumeration it started from.

theorem Complexity.ConstraintGraph.owner_cloudRot {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (p : G.HalfEdge) (j : Fin E.degree) : G.owner (G.cloudRot E p j).1 = G.owner p

A cloud-link stays inside the cloud.

theorem Complexity.ConstraintGraph.cloudRot_getElem {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (v : Fin G.numVerts) (i : Fin (G.cloudList v).length) (j : Fin E.degree) : (G.cloudRot E (G.cloudList v)[↑i] j).1 = (G.cloudList v)[↑(E.rot (G.cloudList v).length (i, j)).1]

The cloud is a copy of the expander. Reading the cloud through its enumeration, a cloud-link is exactly the family's rotation map. This is what lets the expander estimates of Disagreement be applied to a cloud.

theorem Complexity.ConstraintGraph.cloudRot_involutive {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (p : G.HalfEdge) (j : Fin E.degree) : G.cloudRot E (G.cloudRot E p j).1 (G.cloudRot E p j).2 = (p, j)

The reduced graph

noncomputable def Complexity.ConstraintGraph.reduceGraph {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) : RegGraph

The reduced graph: every half-edge has one edge-link to the other half of its edge, and E.degree cloud-links to the half-edges sharing its endpoint.

Equations

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

@[simp]

theorem Complexity.ConstraintGraph.V_reduceGraph {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) : (G.reduceGraph E).V = G.HalfEdge

@[simp]

theorem Complexity.ConstraintGraph.order_reduceGraph {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) : (G.reduceGraph E).order = 2 * G.numEdges

@[simp]

theorem Complexity.ConstraintGraph.deg_reduceGraph {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) : (G.reduceGraph E).deg = 1 + E.degree

The reduced graph is (1 + E.degree)-regular.

theorem Complexity.ConstraintGraph.nbr_reduceGraph_none {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (p : G.HalfEdge) : (G.reduceGraph E).nbr p none = G.flipHalf p

theorem Complexity.ConstraintGraph.nbr_reduceGraph_some {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (p : G.HalfEdge) (j : Fin E.degree) : (G.reduceGraph E).nbr p (some j) = (G.cloudRot E p j).1

The reduced constraint system

noncomputable def Complexity.ConstraintGraph.reduce {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : RegCSP α

The reduced constraint system: an edge-link carries the original constraint of its edge, oriented so that the tail's label comes first, and a cloud-link demands that the two half-edges agree.

Equations

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

@[simp]

theorem Complexity.ConstraintGraph.graph_reduce {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) [DecidableEq α] : (G.reduce E).graph = G.reduceGraph E

@[instance_reducible]

noncomputable instance Complexity.ConstraintGraph.instNumEncVGraphReduce {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) [DecidableEq α] : NumEnc (G.reduce E).graph.V

The reduced system's vertices are the half-edges, numbered by their edge and their side.

Equations

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

theorem Complexity.ConstraintGraph.satisfiable_reduce_of_satisfiable {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) [DecidableEq α] (h : G.Satisfiable) : (G.reduce E).Satisfiable

Completeness: labelling every half-edge by its endpoint's label carries a satisfying assignment of G to one of the reduced system.