Charging disagreement inside a cloud

The soundness half of Dinur's degree reduction, one cloud at a time.

An assignment of the reduced system labels half-edges, not vertices. It is decoded back to a vertex assignment by plurality: decode A v is a label that at least a 1 / card α fraction of v's cloud agrees with. The half-edges of the cloud that disagree form a set the cloud's expander must charge for: by edge expansion, the disagreeing set sends out many cloud-links, and every one of them joins two half-edges with different labels, so every one of them is an unsatisfied constraint.

Everything is phrased at the level of a cloud's enumeration cloudList v, so that the expander family — which lives on Fin n — applies directly, with cloudRot_getElem as the only bridge back to half-edges.

Main definitions

• ConstraintGraph.decode — the plurality label of a cloud
• ConstraintGraph.devIdx — the indices of a cloud that disagree with it
• ConstraintGraph.cloudUnsat — the unsatisfied cloud-links sitting at a vertex

Main results

• ConstraintGraph.length_le_card_agree — plurality: the agreeing part of a cloud is at least a 1 / card α fraction of it
• ConstraintGraph.card_dartsBetween_le_card_cloudUnsat — every expander boundary dart of the disagreeing set is an unsatisfied cloud-link
• ConstraintGraph.cloud_disagreement_bound — the resulting charge: (1 - lam) · degree · |dev| / card α unsatisfied links at v
• ConstraintGraph.total_cloud_charge — summed over the vertices, since the clouds' bills never overlap

Plurality decoding

noncomputable def Complexity.ConstraintGraph.decode {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (A : G.HalfEdge → α) (v : Fin G.numVerts) : α

The plurality label of v's cloud: a label at least a 1 / card α fraction of the cloud agrees with.

Equations

• G.decode A v = Classical.choose ⋯

noncomputable def Complexity.ConstraintGraph.devIdx {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (A : G.HalfEdge → α) (v : Fin G.numVerts) : Finset (Fin (G.cloudList v).length)

The indices of v's cloud whose labels disagree with the plurality.

Equations

• G.devIdx A v = {i : Fin (G.cloudList v).length | A (G.cloudList v)[↑i] ≠ G.decode A v}

theorem Complexity.ConstraintGraph.mem_devIdx {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) {A : G.HalfEdge → α} {v : Fin G.numVerts} {i : Fin (G.cloudList v).length} : i ∈ G.devIdx A v ↔ A (G.cloudList v)[↑i] ≠ G.decode A v

theorem Complexity.ConstraintGraph.mem_compl_devIdx {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) {A : G.HalfEdge → α} {v : Fin G.numVerts} {i : Fin (G.cloudList v).length} : i ∈ (G.devIdx A v)ᶜ ↔ A (G.cloudList v)[↑i] = G.decode A v

theorem Complexity.ConstraintGraph.length_le_card_agree {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (A : G.HalfEdge → α) (v : Fin G.numVerts) : (G.cloudList v).length ≤ Fintype.card α * (G.devIdx A v)ᶜ.card

Plurality. The part of a cloud agreeing with its decoded label is at least a 1 / card α fraction of the cloud.

From cloud indices to half-edges

theorem Complexity.ConstraintGraph.cloud_filter_eq_image {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) (P : G.HalfEdge → Prop) [DecidablePred P] : Finset.filter P (G.cloud v) = Finset.image (fun (i : Fin (G.cloudList v).length) => (G.cloudList v)[↑i]) {i : Fin (G.cloudList v).length | P (G.cloudList v)[↑i]}

A cloud's filtered subset is the image of the corresponding index set.

theorem Complexity.ConstraintGraph.card_filter_cloud {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) (P : G.HalfEdge → Prop) [DecidablePred P] : {i : Fin (G.cloudList v).length | P (G.cloudList v)[↑i]}.card = (Finset.filter P (G.cloud v)).card

Counting inside a cloud is the same through its enumeration.

noncomputable def Complexity.ConstraintGraph.devSet {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (A : G.HalfEdge → α) : Finset G.HalfEdge

The half-edges whose label disagrees with their vertex's decoded label.

Equations

• G.devSet A = {p : G.HalfEdge | A p ≠ G.decode A (G.owner p)}

theorem Complexity.ConstraintGraph.mem_devSet {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) {A : G.HalfEdge → α} {p : G.HalfEdge} : p ∈ G.devSet A ↔ A p ≠ G.decode A (G.owner p)

theorem Complexity.ConstraintGraph.card_devIdx_eq {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (A : G.HalfEdge → α) (v : Fin G.numVerts) : (G.devIdx A v).card = {p ∈ G.devSet A | G.owner p = v}.card

A cloud's disagreeing indices count the same as its disagreeing half-edges.

theorem Complexity.ConstraintGraph.sum_card_devIdx {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (A : G.HalfEdge → α) : ∑ v : Fin G.numVerts, (G.devIdx A v).card = (G.devSet A).card

Summed over the vertices, the cloud charges account for every disagreeing half-edge exactly once.

Unsatisfied cloud-links

noncomputable def Complexity.ConstraintGraph.cloudUnsat {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) (v : Fin G.numVerts) : Finset (G.reduce E).Dart

The unsatisfied cloud-links of the reduced system sitting at v.

Equations

• G.cloudUnsat E A v = {x ∈ (G.reduce E).unsatDarts A | G.owner x.1 = v ∧ x.2 ≠ none}

theorem Complexity.ConstraintGraph.cloudUnsat_subset {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) (v : Fin G.numVerts) : G.cloudUnsat E A v ⊆ (G.reduce E).unsatDarts A

theorem Complexity.ConstraintGraph.cloudUnsat_disjoint {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) {u v : Fin G.numVerts} (huv : u ≠ v) : Disjoint (G.cloudUnsat E A u) (G.cloudUnsat E A v)

The clouds' unsatisfied links are disjoint: a dart's tail determines the vertex it sits at.

theorem Complexity.ConstraintGraph.card_dartsBetween_le_card_cloudUnsat {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) (v : Fin G.numVerts) : ((E.graph (G.cloudList v).length).dartsBetween (G.devIdx A v) (G.devIdx A v)ᶜ).card ≤ (G.cloudUnsat E A v).card

Every boundary dart of the disagreeing set is an unsatisfied cloud-link: its two ends carry different labels, one being the plurality and one not.

The charge

theorem Complexity.ConstraintGraph.cloud_disagreement_bound {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) (v : Fin G.numVerts) : (1 - E.lam) * ↑E.degree * ↑(G.devIdx A v).card / ↑(Fintype.card α) ≤ ↑(G.cloudUnsat E A v).card

The cloud charge. The disagreeing part of v's cloud is billed (1 - lam) · degree / card α unsatisfied cloud-links per disagreeing half-edge.

The total charge

theorem Complexity.ConstraintGraph.sum_card_cloudUnsat_le {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) : ∑ v : Fin G.numVerts, (G.cloudUnsat E A v).card ≤ ((G.reduce E).unsatDarts A).card

The clouds' unsatisfied links are disjoint subsets of all the unsatisfied darts, so their counts add up to at most the whole.

theorem Complexity.ConstraintGraph.total_cloud_charge {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) : (1 - E.lam) * ↑E.degree * ↑(G.devSet A).card / ↑(Fintype.card α) ≤ ↑((G.reduce E).unsatDarts A).card

The total cloud charge. Every disagreeing half-edge is billed (1 - lam) · degree / card α unsatisfied cloud-links, and the bills for different vertices never overlap.