One round of Dinur's amplification

Preprocess, power, compose: the three steps assembled into a single transformation of constraint graphs over a fixed alphabet, packaged as an Amplifier. Given an expander family, the round

• preserves satisfiability,
• multiplies the number of edges by a constant, and
• at least doubles the unsatisfiability value until it reaches a universal threshold.

The alphabet is the one the composition produces, Alpha ReadIdx. Powering blows it up to KOpinion, whose size is a fixed function of the powering length and the preprocessed degree; composition brings it back.

The only free parameter is the killing rate q. The powering bound's slope grows linearly in q while every other loss — preprocessing, composition — is a constant, so a large enough q makes the round double the value. q is chosen by an Archimedean argument, and the threshold is any rational below the powering bound's floor.

Main definitions

• Complexity.DinurAlpha — the fixed alphabet
• Complexity.Dinur.step — one round
• Complexity.Dinur.amplifier — the round as an Amplifier

Main results

• Complexity.Dinur.numEdges_step — the edge count grows by a constant factor
• Complexity.Dinur.satisfiable_step — completeness
• Complexity.Dinur.min_le_unsatVal_step — the value at least doubles, up to the threshold

@[reducible, inline]

abbrev Complexity.DinurAlpha : Type

The fixed alphabet of the amplification: the composition's alphabet.

Equations

• Complexity.DinurAlpha = Complexity.MultiTest.Alpha Complexity.ReadIdx

The powered alphabet's size

def Complexity.Dinur.powDeg (E : ExpanderFamily) : ℕ

The degree after preprocessing.

Equations

• Complexity.Dinur.powDeg E = 2 + 2 * E.degree

def Complexity.Dinur.walkCount (E : ExpanderFamily) (T : ℕ) : ℕ

The number of walks of length at most T out of a vertex.

Equations

• Complexity.Dinur.walkCount E T = ∑ ℓ ∈ Finset.range (T + 1), Complexity.Dinur.powDeg E ^ ℓ

def Complexity.Dinur.bits (E : ExpanderFamily) (T : ℕ) : ℕ

The number of powered labels, as bits of a one-hot encoding.

Equations

• Complexity.Dinur.bits E T = Fintype.card Complexity.DinurAlpha ^ Complexity.Dinur.walkCount E T

theorem Complexity.Dinur.card_varWalk (E : ExpanderFamily) (G : ConstraintGraph DinurAlpha) (T : ℕ) : Fintype.card (VarWalk (G.preprocess E).graph T) = walkCount E T

theorem Complexity.Dinur.card_kOpinion (E : ExpanderFamily) (G : ConstraintGraph DinurAlpha) (T : ℕ) : Fintype.card (KOpinion (G.preprocess E).graph T DinurAlpha) = bits E T

The encoding

theorem Complexity.Dinur.basisVec_injective (n : ℕ) : Function.Injective basisVec

noncomputable def Complexity.Dinur.enc (E : ExpanderFamily) (G : ConstraintGraph DinurAlpha) (T : ℕ) (σ : KOpinion (G.preprocess E).graph T DinurAlpha) : BooleanAnalysis.Cube (bits E T)

The encoding of a powered label: the basis vector at its index.

Equations

• Complexity.Dinur.enc E G T σ = Complexity.basisVec (Fin.cast ⋯ ((Fintype.equivFin (Complexity.KOpinion (G.preprocess E).graph T Complexity.DinurAlpha)) σ))

theorem Complexity.Dinur.enc_injective (E : ExpanderFamily) (G : ConstraintGraph DinurAlpha) (T : ℕ) : Function.Injective (enc E G T)

One round

def Complexity.Dinur.K : ℕ

The alphabet's size, the K of the powering parameters.

Deliberately a def and not an abbrev. The alphabet has 2^23 symbols, and K occurs inside powT K q, which is itself an exponent; letting a tactic unfold K to a numeral there produces terms far too large to elaborate.

Equations

• Complexity.Dinur.K = Fintype.card Complexity.DinurAlpha

theorem Complexity.Dinur.one_le_K : 1 ≤ K

theorem Complexity.Dinur.card_dinurAlpha_eq : Fintype.card DinurAlpha = K

noncomputable def Complexity.Dinur.step (E : ExpanderFamily) (q : ℕ) (hq : 0 < q) (G : ConstraintGraph DinurAlpha) : ConstraintGraph DinurAlpha

One round of amplification with killing rate q.

Equations

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

def Complexity.Dinur.edgeFactor (E : ExpanderFamily) (q : ℕ) : ℕ

The constant factor by which a round multiplies the edge count.

Equations

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

theorem Complexity.Dinur.numEdges_step (E : ExpanderFamily) (q : ℕ) (hq : 0 < q) (G : ConstraintGraph DinurAlpha) : (step E q hq G).numEdges = edgeFactor E q * G.numEdges

theorem Complexity.Dinur.satisfiable_step (E : ExpanderFamily) (q : ℕ) (hq : 0 < q) (G : ConstraintGraph DinurAlpha) (h : G.Satisfiable) : (step E q hq G).Satisfiable

The value

theorem Complexity.Dinur.preprocessLam_nonneg (E : ExpanderFamily) : 0 ≤ ConstraintGraph.preprocessLam E

theorem Complexity.Dinur.preprocessConst_pos (E : ExpanderFamily) : 0 < ConstraintGraph.preprocessConst E DinurAlpha

theorem Complexity.Dinur.le_unsatVal_step (E : ExpanderFamily) (q : ℕ) (hq2 : 2 ≤ q) (G : ConstraintGraph DinurAlpha) (hG : 0 < G.numEdges) : min (RegCSP.powSlope (RegCSP.powConst q DinurAlpha) (↑(powT K q)) (ConstraintGraph.preprocessLam E) * ConstraintGraph.preprocessConst E DinurAlpha * ↑G.unsatVal) (RegCSP.powFloor (RegCSP.powConst q DinurAlpha) (↑(powT K q)) (ConstraintGraph.preprocessLam E)) / 704 ≤ ↑(step E q ⋯ G).unsatVal

The value of one round, for a fixed q ≥ 2 and any graph with an edge: at least the min of the powering slope (times the preprocessing constant) times the value, and the powering floor, all divided by the composition's loss.

Choosing the killing rate

theorem Complexity.Dinur.exists_q (E : ExpanderFamily) : ∃ (q : ℕ), 2 ≤ q ∧ 1408 ≤ RegCSP.powSlope (RegCSP.powConst q DinurAlpha) (↑(powT K q)) (ConstraintGraph.preprocessLam E) * ConstraintGraph.preprocessConst E DinurAlpha

A killing rate that doubles the value.

noncomputable def Complexity.Dinur.q₀ (E : ExpanderFamily) : ℕ

The chosen killing rate.

Equations

• Complexity.Dinur.q₀ E = Classical.choose ⋯

theorem Complexity.Dinur.two_le_q₀ (E : ExpanderFamily) : 2 ≤ q₀ E

theorem Complexity.Dinur.q₀_spec (E : ExpanderFamily) : 1408 ≤ RegCSP.powSlope (RegCSP.powConst (q₀ E) DinurAlpha) (↑(powT K (q₀ E))) (ConstraintGraph.preprocessLam E) * ConstraintGraph.preprocessConst E DinurAlpha

noncomputable def Complexity.Dinur.floor₀ (E : ExpanderFamily) : ℝ

The powering floor at the chosen rate.

Equations

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

theorem Complexity.Dinur.floor₀_pos (E : ExpanderFamily) : 0 < floor₀ E

theorem Complexity.Dinur.exists_gap (E : ExpanderFamily) : ∃ (g : ℚ), 0 < g ∧ g ≤ 1 ∧ ↑g ≤ floor₀ E / 704

A rational threshold below the floor (after the composition's loss) and below one.

noncomputable def Complexity.Dinur.gap₀ (E : ExpanderFamily) : ℚ

The chosen threshold.

Equations

• Complexity.Dinur.gap₀ E = Classical.choose ⋯

theorem Complexity.Dinur.gap₀_pos (E : ExpanderFamily) : 0 < gap₀ E

theorem Complexity.Dinur.gap₀_le_one (E : ExpanderFamily) : gap₀ E ≤ 1

theorem Complexity.Dinur.gap₀_le (E : ExpanderFamily) : ↑(gap₀ E) ≤ floor₀ E / 704

theorem Complexity.Dinur.unsatVal_eq_zero_of_numEdges_eq_zero (G : ConstraintGraph DinurAlpha) (h : G.numEdges = 0) : G.unsatVal = 0

An edgeless graph has value zero.

theorem Complexity.Dinur.min_le_unsatVal_step (E : ExpanderFamily) (G : ConstraintGraph DinurAlpha) : min (gap₀ E) (2 * G.unsatVal) ≤ (step E (q₀ E) ⋯ G).unsatVal

The value at least doubles, up to the threshold.

The amplifier

noncomputable def Complexity.Dinur.amplifier (E : ExpanderFamily) : Amplifier DinurAlpha

Dinur's round as an Amplifier.

Equations

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