The Sipser–Lautemann theorem

Every problem in BPP lies in the second level Σ₂ ∩ Π₂ of the polynomial hierarchy, and hence in PH. This is the Sipser–Gács–Lautemann theorem: Sipser placed BPP in PH, Gács improved the placement to Σ₂ ∩ Π₂, and Lautemann gave the proof formalised here; see also Arora and Barak, Theorem 7.15.

Given a BPP verifier V using random strings of length m = p (enc a).length, repeating the test 2 R times (with R = 6 m + 48) and taking a strict majority (> R accepting runs) reduces the error fraction to at most (8 / 9) ^ R (Cslib.card_filter_card_filter_le_le). The amplified seeds Seed m = (Fin (2 R) → BitString m) form an additive group under bitwise xor, to which Lautemann's covering lemma applies:

• Completeness (a ∈ A): since 2 ^ (2 R m) * (8 ^ R) ^ (2 R) < (9 ^ R) ^ (2 R), the covering lemma (Cslib.exists_forall_exists_add_mem_of_card_mul_card_compl_pow_lt) yields T = 2 R shift vectors covering the entire space of amplified seeds.
• Soundness (a ∉ A): for any T = 2 R shift vectors, each shifted accepting set has size at most (8 / 9) ^ R of the seed space, and T * 8 ^ R < 9 ^ R, so their union cannot cover all amplified seeds (Cslib.exists_forall_add_notMem_of_mul_card_lt).

The resulting Σ₂ verifier SipserLautemann.verifier reads a concatenated certificate w = u ++ r with existential block length T * (2 R m) and universal block length 2 R m, reconstructs each shifted trial seed as the bitwise xor of two fixed-width rows of w (Cslib.BitString.listRow), and checks whether some shift yields more than R accepting trials. Seeds and shift tables are read from bit strings through the block views Cslib.BitString.ofList and Cslib.BitString.block. Closure of BPP under complement (Cslib.Complexity.compl_mem_BPP) and quantifier duality (Cslib.Complexity.compl_mem_PiP_of_mem_SigmaP) then give BPP enc ⊆ PiP 2 enc without repeating the construction.

Main definitions

• Cslib.Complexity.SipserLautemann.Seed, Cslib.Complexity.SipserLautemann.majorityAccepts: amplified seeds and strict majority acceptance. Seeds are shifted by pointwise bit-string addition (+).
• Cslib.Complexity.SipserLautemann.verifier: the Σ₂ matrix verifier for a BPP problem.
• Cslib.Complexity.SipserLautemann.witnessPoly, Cslib.Complexity.SipserLautemann.seedPoly: the polynomial block lengths of the existential shift table and universal seed.

Main results

• Cslib.Complexity.SipserLautemann.exists_shifts_majorityAccepts, Cslib.Complexity.SipserLautemann.exists_seed_not_majorityAccepts: combinatorial completeness and soundness of shifted majority votes.
• Cslib.Complexity.SipserLautemann.verifier_polyTime: the matrix verifier is computable in polynomial time.
• Cslib.Complexity.SipserLautemann.isAlternatingVerifier_verifier: the matrix verifier is a valid Σ₂ alternating verifier for any BPP problem.
• Cslib.Complexity.BPP_subset_SigmaP_two: BPP enc ⊆ SigmaP 2 enc.
• Cslib.Complexity.BPP_subset_PiP_two: BPP enc ⊆ PiP 2 enc.
• Cslib.Complexity.BPP_subset_SigmaP_two_inter_PiP_two: BPP enc ⊆ SigmaP 2 enc ∩ PiP 2 enc.
• Cslib.Complexity.BPP_subset_PH: BPP enc ⊆ PH enc.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Theorem 7.15
• M. Sipser, A complexity theoretic approach to randomness
• C. Lautemann, BPP and the polynomial hierarchy

Amplification and shift parameters

def Cslib.Complexity.SipserLautemann.halfRuns (m : ℕ) : ℕ

Half the number of majority-amplification trials for a single-trial seed of length m: 6 * m + 48 = 6 * (m + 7) + 6.

def Cslib.Complexity.SipserLautemann.runs (m : ℕ) : ℕ

Number of independent repetitions in majority amplification: 2 * halfRuns m = 12 * m + 96. A run accepts when strictly more than halfRuns m of the runs m trials accept.

def Cslib.Complexity.SipserLautemann.shifts (m : ℕ) : ℕ

Number of shift vectors in the Lautemann cover: shifts m = runs m = 12 * m + 96.

def Cslib.Complexity.SipserLautemann.seedLen (m : ℕ) : ℕ

Length of an amplified universal seed: runs m * m bits.

def Cslib.Complexity.SipserLautemann.witnessLen (m : ℕ) : ℕ

Length of the existential witness concatenating shifts m shift vectors: shifts m * seedLen m bits.

noncomputable def Cslib.Complexity.SipserLautemann.runsPoly (p : Polynomial ℕ) : Polynomial ℕ

Polynomial giving runs (p.eval n) at input length n.

noncomputable def Cslib.Complexity.SipserLautemann.seedPoly (p : Polynomial ℕ) : Polynomial ℕ

Polynomial giving seedLen (p.eval n) at input length n: the length of the universal quantifier block r.

noncomputable def Cslib.Complexity.SipserLautemann.witnessPoly (p : Polynomial ℕ) : Polynomial ℕ

Polynomial giving witnessLen (p.eval n) at input length n: the length of the existential quantifier block u.

@[simp]

theorem Cslib.Complexity.SipserLautemann.eval_runsPoly (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (runsPoly p) = runs (Polynomial.eval n p)

@[simp]

theorem Cslib.Complexity.SipserLautemann.eval_seedPoly (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (seedPoly p) = seedLen (Polynomial.eval n p)

@[simp]

theorem Cslib.Complexity.SipserLautemann.eval_witnessPoly (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (witnessPoly p) = witnessLen (Polynomial.eval n p)

Combinatorial shift-cover and soundness on amplified seeds

@[reducible, inline]

abbrev Cslib.Complexity.SipserLautemann.Seed (m : ℕ) : Type

An amplified seed for single-trial seed length m: runs m blocks of m bits each. Seeds form an additive group under pointwise bit-string addition (xor).

def Cslib.Complexity.SipserLautemann.majorityAccepts {m : ℕ} (P : (Fin m → Bool) → Bool) (ω : Seed m) : Prop

The amplified test accepts ω : Seed m when a strict majority (> halfRuns m) of the runs m = 2 * halfRuns m blocks satisfy the single-trial predicate P.

@[instance_reducible]

instance Cslib.Complexity.SipserLautemann.instDecidablePredSeedMajorityAccepts {m : ℕ} (P : (Fin m → Bool) → Bool) : DecidablePred (majorityAccepts P)

theorem Cslib.Complexity.SipserLautemann.exists_shifts_majorityAccepts {m : ℕ} {P : (Fin m → Bool) → Bool} (hP : 2 * 2 ^ m ≤ 3 * {s : Fin m → Bool | P s = true}.card) : ∃ (tests : Fin (shifts m) → Seed m), ∀ (r : Seed m), ∃ (i : Fin (shifts m)), majorityAccepts P (r + tests i)

Completeness on amplified seeds. If at least two thirds of the single-trial seeds satisfy P s = true, then there exist shifts m shift vectors covering every amplified seed r : Seed m under majorityAccepts P: Lautemann's covering lemma Cslib.exists_forall_exists_add_mem_of_card_mul_card_compl_pow_lt on the group Seed m.

theorem Cslib.Complexity.SipserLautemann.exists_seed_not_majorityAccepts {m : ℕ} {P : (Fin m → Bool) → Bool} (hP : 2 * 2 ^ m ≤ 3 * {s : Fin m → Bool | P s = false}.card) (tests : Fin (shifts m) → Seed m) : ∃ (r : Seed m), ∀ (i : Fin (shifts m)), ¬majorityAccepts P (r + tests i)

Soundness on amplified seeds. If at least two thirds of the single-trial seeds satisfy P s = false, then for every tuple tests : Fin (shifts m) → Seed m of shift vectors, some amplified seed r : Seed m fails majorityAccepts P (r + tests i) for all i: the converse Cslib.exists_forall_add_notMem_of_mul_card_lt of Lautemann's covering lemma on Seed m.

Bit-string encoding and decoding of seeds and shift tables

def Cslib.Complexity.SipserLautemann.listToSeed (m : ℕ) (r : List Bool) : Seed m

Decode a flat bit string r into an amplified seed, reading r as runs m consecutive blocks of m bits: bit k of block j is bit j * m + k of r, and bits missing from a short r read as false (Cslib.BitString.ofList, Cslib.BitString.block).

def Cslib.Complexity.SipserLautemann.listToShifts (m : ℕ) (u : List Bool) : Fin (shifts m) → Seed m

Decode a flat bit string u into a table of shifts m shift vectors, reading u as shifts m consecutive blocks of seedLen m bits, each an amplified seed as in listToSeed: bit k of block j of shift i is bit i * seedLen m + j * m + k of u, and bits missing from a short u read as false.

def Cslib.Complexity.SipserLautemann.seedToList {m : ℕ} (ω : Seed m) : List Bool

Encode an amplified seed ω : Seed m as a flat bit string of length seedLen m, inverting listToSeed.

def Cslib.Complexity.SipserLautemann.shiftsToList {m : ℕ} (tests : Fin (shifts m) → Seed m) : List Bool

Encode a table of shift vectors tests : Fin (shifts m) → Seed m as a flat bit string of length witnessLen m, inverting listToShifts.

@[simp]

theorem Cslib.Complexity.SipserLautemann.length_seedToList {m : ℕ} (ω : Seed m) : (seedToList ω).length = seedLen m

@[simp]

theorem Cslib.Complexity.SipserLautemann.length_shiftsToList {m : ℕ} (tests : Fin (shifts m) → Seed m) : (shiftsToList tests).length = witnessLen m

@[simp]

theorem Cslib.Complexity.SipserLautemann.listToSeed_seedToList {m : ℕ} (ω : Seed m) : listToSeed m (seedToList ω) = ω

@[simp]

theorem Cslib.Complexity.SipserLautemann.listToShifts_shiftsToList {m : ℕ} (tests : Fin (shifts m) → Seed m) : listToShifts m (shiftsToList tests) = tests

The functional matrix verifier and its polynomial-time certificate

def Cslib.Complexity.SipserLautemann.trialSeed (m : ℕ) (w : List Bool) (i j : ℕ) : List Bool

The j-th trial seed of length m under the i-th shift of a combined certificate w = u ++ r, where u lists shifts m shift vectors of seedLen m bits and r is the amplified seed: the bitwise xor of the rows of width m numbered shifts m * runs m + j (block j of r) and i * runs m + j (block j of the i-th shift) of w (Cslib.BitString.listRow). Bits missing from a short w read as false, and extra bits of w are ignored.

def Cslib.Complexity.SipserLautemann.shiftAccepts {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (a : α) (w : List Bool) (i : ℕ) : Bool

Whether the i-th shift vector causes a strict majority (> halfRuns m) of the runs m trials to be accepted by V.

def Cslib.Complexity.SipserLautemann.verifier {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (x : α × List Bool) : Bool

The Sipser–Lautemann Σ₂ matrix verifier: given (a, w) where w = u ++ r consists of an existential shift-table certificate u of length witnessLen m and a universal seed r of length seedLen m (for m = p.eval (enc a).length), test whether some shift i < shifts m makes a strict majority of the runs m shifted trials accept. The verifier is total: bits missing from a short w read as false and extra bits of w are ignored (trialSeed).

theorem Cslib.Complexity.SipserLautemann.verifier_polyTime {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (verifier enc p V) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

If V is computable in polynomial time, then so is the Sipser–Lautemann matrix verifier verifier enc p V.

Correctness of the matrix verifier

theorem Cslib.Complexity.SipserLautemann.shiftAccepts_append_iff {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {u r : List Bool} (hu : u.length = witnessLen (Polynomial.eval (enc a).length p)) (i : Fin (shifts (Polynomial.eval (enc a).length p))) : shiftAccepts enc p V a (u ++ r) ↑i = true ↔ majorityAccepts (fun (s : Fin (Polynomial.eval (enc a).length p) → Bool) => V (a, List.ofFn s)) (listToSeed (Polynomial.eval (enc a).length p) r + listToShifts (Polynomial.eval (enc a).length p) u i)

On a combined certificate u ++ r with u.length = witnessLen (p.eval (enc a).length), shiftAccepts agrees with majorityAccepts on the i-th shifted seed.

theorem Cslib.Complexity.SipserLautemann.verifier_append_iff {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {u r : List Bool} (hu : u.length = witnessLen (Polynomial.eval (enc a).length p)) : verifier enc p V (a, u ++ r) = true ↔ ∃ (i : Fin (shifts (Polynomial.eval (enc a).length p))), majorityAccepts (fun (s : Fin (Polynomial.eval (enc a).length p) → Bool) => V (a, List.ofFn s)) (listToSeed (Polynomial.eval (enc a).length p) r + listToShifts (Polynomial.eval (enc a).length p) u i)

On a combined certificate u ++ r with u.length = witnessLen (p.eval (enc a).length), verifier enc p V (a, u ++ r) accepts iff some shift i satisfies majorityAccepts.

theorem Cslib.Complexity.SipserLautemann.isAlternatingVerifier_verifier {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} (hA : DecidesWithBoundedError enc p V A) : IsAlternatingVerifier enc true [witnessPoly p, seedPoly p] (verifier enc p V) A

If V decides A with bounded error using seed polynomial p, then verifier enc p V is a valid Σ₂ alternating verifier for A with quantifier block lengths [witnessPoly p, seedPoly p].

Main class inclusions

theorem Cslib.Complexity.BPP_subset_SigmaP_two {α : Type} {enc : α ↪ List Bool} : BPP enc ⊆ SigmaP 2 enc

The Sipser–Gács–Lautemann theorem (Σ₂ form) Sipser, Lautemann, Arora and Barak, Theorem 7.15: every problem in BPP lies in Σ₂.

theorem Cslib.Complexity.BPP_subset_PiP_two {α : Type} {enc : α ↪ List Bool} : BPP enc ⊆ PiP 2 enc

The Sipser–Gács–Lautemann theorem (Π₂ form): every problem in BPP lies in Π₂, obtained from BPP_subset_SigmaP_two by complement closure of BPP and quantifier duality.

theorem Cslib.Complexity.BPP_subset_SigmaP_two_inter_PiP_two {α : Type} {enc : α ↪ List Bool} : BPP enc ⊆ SigmaP 2 enc ∩ PiP 2 enc

The Sipser–Gács–Lautemann theorem: BPP ⊆ Σ₂ ∩ Π₂ Sipser, Lautemann, Arora and Barak, Theorem 7.15.

theorem Cslib.Complexity.BPP_subset_PH {α : Type} {enc : α ↪ List Bool} : BPP enc ⊆ PH enc

Every problem in BPP lies in the polynomial hierarchy PH.