Håstad's 3-bit linear test: soundness against Label Cover

Håstad [Has01] proved that, for every ε > 0, it is NP-hard to satisfy more than a 7 / 8 + ε fraction of the clauses of a satisfiable E3-CNF formula, matching the random-assignment bound Cslib.Logic.PL.CNF.IsExactThreeDistinct.unsatVal_le_one_eighth. Together with its submodule LinearTest, this module formalizes the analytic core of that proof, the completeness and soundness of Håstad's noisy 3-bit linear test on folded Long Code tables over a Label Cover projection π : β → γ. It does not prove the hardness result: no reduction to MAX-E3LIN or MAX-E3SAT is constructed, and NP-hardness of Label Cover (the PCP theorem with parallel repetition) is not formalized.

1. The Long Code of x : α (Cslib.BitString.longCode) evaluates each Boolean function g : α → Bool at x. A table B : (γ → Bool) → Bool is folded, that is, odd (Cslib.BitString.IsOdd), when B (f + fun _ => true) = !B f, which kills the empty Fourier coefficient fourierCoeff (signVal ∘ B) ∅ = 0 (Cslib.BitString.IsOdd.fourierCoeff_empty).
2. Given an edge projection π : β → γ, a right table B : (γ → Bool) → Bool, and a left table A : (β → Bool) → Bool, Håstad's 3-bit linear test samples uniform f : γ → Bool and g : β → Bool, a δ-biased noise function μ : β → Bool, and checks whether B f ^^ A g = A ((f ∘ π) + g + μ).
3. On valid Long Code tables B = longCode (π x) and A = longCode x, the linear test accepts with probability 1 - δ (Cslib.PCP.Hastad.hastadLinearProb_longCode).
4. By Walsh–Fourier inversion, the test correlation hastadLinearCorr π δ B A equals ∑ T : Finset β, (1 - 2 * δ) ^ #T * fourierCoeff (signVal ∘ B) (projectSet π T) * fourierCoeff (signVal ∘ A) T ^ 2 (Cslib.PCP.Hastad.hastadLinearCorr_eq_sum). Splitting at degree k and applying Cauchy–Schwarz and Parseval's identity bounds (hastadLinearCorr π δ B A) ^ 2 by (1 - 2 * δ) ^ (2 * k) + k ^ 2 * ∑ x, spectralWeight k A x * spectralWeight k B (π x) (Cslib.PCP.Hastad.hastadLinearCorr_sq_le), where spectralWeight k A is a sub-probability distribution on β.
5. Decoding the spectral weights into a labelling bounds the average correlation over a Label Cover instance by its value (Cslib.PCP.Hastad.hastadGraphLinearCorr_sq_le).

Main definitions

• Cslib.PCP.Hastad.hastadGraphLinearCorr, Cslib.PCP.Hastad.hastadGraphLinearProb: multi-edge test averages over a Label Cover instance.

Main results

• Cslib.PCP.Hastad.exists_labelling_of_spectralWeight: spectral decoding of Label Cover tables.
• Cslib.PCP.Hastad.hastadGraphLinearCorr_sq_le: multi-edge Cauchy–Schwarz + Parseval soundness bound.
• Cslib.PCP.Hastad.hastad_gapLabelCover_dichotomy_lt_one: for every ε and δ there is a threshold 0 < η < 1, independent of the label sets, such that on GapLabelCover yes-instances some folded tables pass the 3-bit test with probability 1 - δ, and on no-instances every folded table passes with probability at most 1 / 2 + 4 * ε.

References

• J. Håstad, Some optimal inapproximability results
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 22
• R. O'Donnell, Analysis of Boolean Functions, Chapter 7

Multi-edge Label Cover decoding and soundness

theorem Cslib.PCP.Hastad.exists_labelling_of_spectralWeight {β γ : Type} [Fintype β] [DecidableEq β] [Nonempty β] [Fintype γ] [DecidableEq γ] [Nonempty γ] (g : Encoded.Graph (β → γ)) (k : ℕ) (B : ℕ → (γ → Bool) → Bool) (A : ℕ → (β → Bool) → Bool) : ∃ (ℓ : ℕ → β) (r : ℕ → γ), ∑ i : Fin g.edges.length, ∑ x : β, spectralWeight k (A (g.edges.get i).src) x * spectralWeight k (B (g.edges.get i).dst) ((g.edges.get i).constraint x) ≤ ∑ i : Fin g.edges.length, if (g.edges.get i).constraint (ℓ (g.edges.get i).src) = r (g.edges.get i).dst then 1 else 0

Spectral decoding of Label Cover tables: for any Label Cover instance g : Graph (β → γ), degree cutoff k, left tables A, and right tables B, there exist deterministic labellings ℓ : ℕ → β and r : ℕ → γ whose number of satisfied edges is at least the total spectral weight agreement across all edges of g.

noncomputable def Cslib.PCP.Hastad.hastadGraphLinearCorr {β γ : Type} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (g : Encoded.Graph (β → γ)) (δ : ℝ) (B : ℕ → (γ → Bool) → Bool) (A : ℕ → (β → Bool) → Bool) : ℝ

Average correlation of Håstad's 3-bit linear test across the edges of a Label Cover instance g : Graph (β → γ).

noncomputable def Cslib.PCP.Hastad.hastadGraphLinearProb {β γ : Type} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (g : Encoded.Graph (β → γ)) (δ : ℝ) (B : ℕ → (γ → Bool) → Bool) (A : ℕ → (β → Bool) → Bool) : ℝ

Average acceptance probability of Håstad's 3-bit linear test across the edges of a Label Cover instance g : Graph (β → γ).

theorem Cslib.PCP.Hastad.hastadGraphProb_longCode_of_satisfies {β γ : Type} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] {g : Encoded.Graph (β → γ)} (hg : g.edges ≠ []) (δ : ℝ) {ℓ : ℕ → β} {r : ℕ → γ} (hℓr : ∀ d ∈ g.edges, d.constraint (ℓ d.src) = r d.dst) : (∀ (w : ℕ), BitString.IsOdd (BitString.longCode (r w))) ∧ (hastadGraphLinearProb g δ (fun (w : ℕ) => BitString.longCode (r w)) fun (u : ℕ) => BitString.longCode (ℓ u)) = 1 - δ

Multi-edge completeness of Håstad's tests: if (ℓ, r) satisfies every edge of a non-empty Label Cover instance g, then the Long Code tables B w = longCode (r w) and A u = longCode (ℓ u) are folded and achieve linear acceptance 1 - δ.

theorem Cslib.PCP.Hastad.hastadGraphLinearCorr_sq_le {β γ : Type} [Fintype β] [DecidableEq β] [Nonempty β] [Fintype γ] [DecidableEq γ] [Nonempty γ] (g : Encoded.Graph (β → γ)) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1 / 2) (k : ℕ) {B : ℕ → (γ → Bool) → Bool} (hB : ∀ (w : ℕ), BitString.IsOdd (B w)) (A : ℕ → (β → Bool) → Bool) : hastadGraphLinearCorr g δ B A ^ 2 ≤ (1 - 2 * δ) ^ (2 * k) + ↑k ^ 2 * (1 - (g.toGraph Complexity.projectionEval).unsatVal)

Multi-edge soundness bound for Håstad's 3-bit test over Label Cover Håstad, Theorem 5.6: for any Label Cover instance g : Graph (β → γ), noise rate 0 ≤ δ ≤ 1 / 2, degree cutoff k, folded right tables B, and left tables A, the squared average correlation hastadGraphLinearCorr g δ B A ^ 2 is at most (1 - 2 * δ) ^ (2 * k) + k ^ 2 * (1 - (g.toGraph projectionEval).unsatVal).

theorem Cslib.PCP.Hastad.hastad_gapLabelCover_dichotomy_lt_one {ε δ : ℝ} (hε : 0 < ε) (hδ0 : 0 < δ) (hδ1 : δ < 1 / 2) : ∃ (η : ℝ), 0 < η ∧ η < 1 ∧ ∀ {β γ : Type} [inst : Fintype β] [inst_1 : DecidableEq β] [Nonempty β] [inst_3 : Fintype γ] [inst_4 : DecidableEq γ] [Nonempty γ] {g : Encoded.Graph (β → γ)}, g.edges ≠ [] → (g ∈ (Complexity.GapLabelCover β γ 1 η).yes → ∃ (B : ℕ → (γ → Bool) → Bool) (A : ℕ → (β → Bool) → Bool), (∀ (w : ℕ), BitString.IsOdd (B w)) ∧ hastadGraphLinearProb g δ B A = 1 - δ) ∧ (g ∈ (Complexity.GapLabelCover β γ 1 η).no → ∀ (B : ℕ → (γ → Bool) → Bool) (A : ℕ → (β → Bool) → Bool), (∀ (w : ℕ), BitString.IsOdd (B w)) → hastadGraphLinearProb g δ B A ≤ 1 / 2 + 4 * ε)

Completeness and soundness of Håstad's 3-bit linear test against Label Cover Håstad, Theorem 5.6: for every ε > 0 and 0 < δ < 1 / 2, there exists a Label Cover soundness parameter 0 < η < 1, independent of the label sets β and γ, such that for every Label Cover instance g : Graph (β → γ) with g.edges ≠ []:

1. (Completeness) If g ∈ (GapLabelCover β γ 1 η).yes, there exist folded tables B and A achieving hastadGraphLinearProb g δ B A = 1 - δ.
2. (Soundness) If g ∈ (GapLabelCover β γ 1 η).no, then for all folded right tables B and all left tables A, hastadGraphLinearProb g δ B A ≤ 1 / 2 + 4 * ε.

This is the analytic core of Håstad's MAX-E3LIN hardness proof. It is not a reduction: no instance of MAX-E3LIN or MAX-E3SAT is constructed, and NP-hardness of GapLabelCover is not proved here. The threshold is strictly below the completeness value, as required by the no-instance promise. This does not assert that no-instances exist for every fixed pair of label sets; sufficiently large label sets can be required.

theorem Cslib.PCP.Hastad.hastad_gapLabelCover_dichotomy {ε δ : ℝ} (hε : 0 < ε) (hδ0 : 0 < δ) (hδ1 : δ < 1 / 2) : ∃ (η : ℝ), 0 < η ∧ ∀ {β γ : Type} [inst : Fintype β] [inst_1 : DecidableEq β] [Nonempty β] [inst_3 : Fintype γ] [inst_4 : DecidableEq γ] [Nonempty γ] {g : Encoded.Graph (β → γ)}, g.edges ≠ [] → (g ∈ (Complexity.GapLabelCover β γ 1 η).yes → ∃ (B : ℕ → (γ → Bool) → Bool) (A : ℕ → (β → Bool) → Bool), (∀ (w : ℕ), BitString.IsOdd (B w)) ∧ hastadGraphLinearProb g δ B A = 1 - δ) ∧ (g ∈ (Complexity.GapLabelCover β γ 1 η).no → ∀ (B : ℕ → (γ → Bool) → Bool) (A : ℕ → (β → Bool) → Bool), (∀ (w : ℕ), BitString.IsOdd (B w)) → hastadGraphLinearProb g δ B A ≤ 1 / 2 + 4 * ε)

Compatibility form of hastad_gapLabelCover_dichotomy_lt_one, retaining the original public statement. Use the stronger theorem when a nontrivial Label Cover gap is needed.