Soundness of degree reduction

Completeness was proved in DegreeReduction; this is the other half. An assignment A of the reduced system is decoded to a vertex assignment by plurality, and the unsatisfied darts of A are charged against the edges that decoding fails:

• cloud-links pay for every half-edge that disagrees with its vertex's plurality label (CloudDisagreement.total_cloud_charge), and
• edge-links pay for every original edge that the decoded assignment fails and whose two half-edges both agree — for such an edge the edge-link carries exactly the failed original constraint.

An edge escapes the second bill only by having a disagreeing half-edge, and those are already billed by the first. Trading the two off gives a bound of min 1 c times the original unsatisfied fraction, with c = (1 - lam) · degree / card α.

Main definitions

• ConstraintGraph.cloudDarts, edgeDarts — the unsatisfied darts split by which kind of link they are
• ConstraintGraph.goodEdges — the failed original edges whose halves agree

Main results

• ConstraintGraph.card_unsatEdges_le_charge — an edge failed by decoding is either billed to an edge-link or has a disagreeing half-edge
• ConstraintGraph.card_unsatDarts_ge — the combined charge
• ConstraintGraph.unsatFrac_reduce_ge, ConstraintGraph.le_unsatVal_reduce — soundness: the reduced system's unsatisfied fraction, and its value, are at least reduceConst times G's value

noncomputable def Complexity.ConstraintGraph.reduceConst (E : ExpanderFamily) (α : Type) [Fintype α] : ℝ

The constant factor degree reduction costs: the trade-off between the cloud charge (1 - lam) · degree / card α and the edge charge 1, diluted by the (1 + degree)-fold increase in darts.

Equations

• Complexity.ConstraintGraph.reduceConst E α = min 1 ((1 - E.lam) * ↑E.degree / ↑(Fintype.card α)) / (2 * (1 + ↑E.degree))

Splitting the unsatisfied darts

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

The unsatisfied cloud-links.

Equations

• G.cloudDarts E A = {x ∈ (G.reduce E).unsatDarts A | x.2 ≠ none}

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

The unsatisfied edge-links.

Equations

• G.edgeDarts E A = {x ∈ (G.reduce E).unsatDarts A | x.2 = none}

theorem Complexity.ConstraintGraph.card_cloudDarts_add_card_edgeDarts {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) : (G.cloudDarts E A).card + (G.edgeDarts E A).card = ((G.reduce E).unsatDarts A).card

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

theorem Complexity.ConstraintGraph.cloud_charge_le_card_cloudDarts {α : 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.cloudDarts E A).card

The cloud charge lands entirely among the unsatisfied cloud-links.

The edge-link charge

noncomputable def Complexity.ConstraintGraph.goodEdges {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) : Finset (Fin G.numEdges)

The original edges that decoding fails and whose two half-edges both agree with their vertices' labels.

Equations

• G.goodEdges E A = {e ∈ G.unsatEdges (G.decode A) | (e, false) ∉ G.devSet A ∧ (e, true) ∉ G.devSet A}

theorem Complexity.ConstraintGraph.card_goodEdges_le {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) : (G.goodEdges E A).card ≤ (G.edgeDarts E A).card

Each such edge contributes an unsatisfied edge-link: the link carries exactly the original constraint, evaluated at the decoded labels.

theorem Complexity.ConstraintGraph.card_unsatEdges_le_charge {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) : (G.unsatEdges (G.decode A)).card ≤ (G.goodEdges E A).card + (G.devSet A).card

An edge that decoding fails is either billed to an edge-link or has a disagreeing half-edge.

Soundness

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

The combined charge. With c = (1 - lam) · degree / card α, the unsatisfied darts number at least min 1 c times the edges that decoding fails.

theorem Complexity.ConstraintGraph.unsatFrac_reduce_ge {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) (A : (G.reduce E).Assignment) : min 1 ((1 - E.lam) * ↑E.degree / ↑(Fintype.card α)) / (2 * (1 + ↑E.degree)) * ↑G.unsatVal ≤ ↑((G.reduce E).unsatFrac A)

Soundness of degree reduction. The reduced system's unsatisfied fraction is at least a constant times the original's unsatisfiability value, the constant depending only on the alphabet size and the cloud expander.

theorem Complexity.ConstraintGraph.le_unsatVal_reduce {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (G : ConstraintGraph α) (E : ExpanderFamily) : reduceConst E α * ↑G.unsatVal ≤ ↑(G.reduce E).unsatVal

Soundness of degree reduction, on values.