The Sipser–Lautemann theorem

The Sipser–Lautemann theorem (Arora–Barak Theorem 7.15) places bounded-error probabilistic polynomial time inside the second level of the polynomial hierarchy: BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ. This file states that containment against the library's concrete BPP (Complexitylib.Classes.Randomized) and the certificate-quantifier levels SigmaP / PiP (Complexitylib.Classes.PH), and proves it: sipserLautemann.

How it is proved

The development lives in the SipserLautemann subdirectory:

• Covering — Lautemann's covering lemma in both directions, by counting shifts of an event in the seed space;
• TimeBound — the acceptance probability is frozen past the halting time, so a machine's arbitrary time bound may be replaced by a dominating polynomial;
• Amplified — majority amplification plus the covering lemma give the ∃∀ characterization x ∈ L ↔ ∃ shifts, ∀ seeds, some shift accepts, and its complementary form for x ∉ L;
• Encode — bitstring codecs for seeds and shift tuples;
• Matrix — the quantifier-free matrix as a language of encoded triples, and the identity exhibiting L and Lᶜ as polynomially bounded ∃∀ forms over it;
• Verdict — the matrix verdict as a member of Cobham's algebra, hence in FP.

What remained was the polynomial-time decidability of the matrix, isolated as the interfaces MatrixInP and — as a statement about a function — MatrixVerdictInFP. It is discharged by matrixVerdictInFP with no machine construction at all: CobhamFP_eq_FP turns it into a programming task inside Cobham's algebra, and mem_P_of_decisionFn_bool converts the result back to P. The verdict is computed in SipserLautemann.Verdict — decode the triple with the payload scanners, build the trial count and seed length as smash lengths from the polynomial time bound, and take the disjunction over shift blocks of the majority vote over trial blocks — with each trial one run of the machine along the choice bits of its block, via NTM.choiceTM and its in-algebra simulation in Complexitylib.Classes.P.Cobham.Internal.ChoiceSim. The matrix is taken at a polynomial time bound, which is what makes the per-trial step count computable from the input; TimeBound supplies the normalization.

Main definitions

• SipserLautemann — the statement BPP ⊆ SigmaP 2 ∩ PiP 2
• MatrixInP — the polynomial-time decidability interface for the matrix
• MatrixVerdictInFP — the same interface as a statement about a function

Main results

• sipserLautemann — the theorem, BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ
• BPP_subset_SigmaP_two, BPP_subset_PiP_two, BPP_subset_PH — its halves and the corollary
• matrixVerdictInFP — the matrix interface, discharged
• sipserLautemann_of_matrixInP, sipserLautemann_of_verdictInFP — the theorem from either form of the interface
• matrixInP_of_verdictInFP — the function form implies the language form
• mem_SigmaP_two_of_matrixInP, mem_PiP_two_of_matrixInP — the two halves
• sipserLautemann_iff — the statement splits into its Σ₂ and Π₂ halves
• sipserLautemann_of_subset_SigmaP — the Σ₂ half suffices, given that BPP is closed under complement
• BPP_subset_SigmaP_two_of_sipserLautemann, BPP_subset_PiP_two_of_sipserLautemann — the two halves
• BPP_subset_PH_of_sipserLautemann — BPP ⊆ PH

def Complexity.SipserLautemann : Prop

Sipser–Lautemann: bounded-error probabilistic polynomial time lies in the second level of the polynomial hierarchy, BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ.

Stated as a Prop so that results can depend on it explicitly; it is proved from the MatrixInP interface by sipserLautemann_of_matrixInP.

Equations

• Complexity.SipserLautemann = (Complexity.BPP ⊆ Complexity.SigmaP 2 ∩ Complexity.PiP 2)

def Complexity.MatrixInP : Prop

The matrix-decidability interface. For every machine and every polynomial time bound, the quantifier-free matrix of the Lautemann characterization is decidable in deterministic polynomial time.

A decider parses pair (pair x w) r, computes the per-trial step count pt.eval |x| and the amplified seed length from it, decodes the shift tuple and the seed, and for each shift runs the fixed machine on the shifted seed, block by block, taking the majority verdict; all of this is polynomial in the input length. Isolating it here keeps the probabilistic and combinatorial content of the theorem free of machine engineering.

Equations

• Complexity.MatrixInP = ∀ (k : ℕ) (tm : Complexity.NTM k) (pt : Polynomial ℕ) (b : Bool), Complexity.Lautemann.matrixLang tm (fun (x : ℕ) => Polynomial.eval x pt) b ∈ Complexity.P

def Complexity.MatrixVerdictInFP : Prop

The matrix interface as a function statement. For every machine and every polynomial time bound, the matrix verdict is computable in deterministic polynomial time.

This is the form to discharge: by CobhamFP_eq_FP it suffices to build the verdict inside Cobham's algebra, with NTM.choiceTM_simulates supplying the semantics of running the machine along given choice bits.

Equations

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

theorem Complexity.matrixInP_of_verdictInFP (h : MatrixVerdictInFP) : MatrixInP

A polynomial-time verdict function gives the polynomial-time matrix language.

theorem Complexity.mem_SigmaP_two_of_matrixInP (hmatrix : MatrixInP) {L : Language} (hL : L ∈ BPP) : L ∈ SigmaP 2

Every BPP language is in Σ₂ᵖ, given the matrix interface.

theorem Complexity.mem_PiP_two_of_matrixInP (hmatrix : MatrixInP) {L : Language} (hL : L ∈ BPP) : L ∈ PiP 2

Every BPP language is in Π₂ᵖ, given the matrix interface: the complementary covering characterization puts the complement in Σ₂ᵖ.

theorem Complexity.sipserLautemann_of_matrixInP (hmatrix : MatrixInP) : SipserLautemann

The Sipser–Lautemann theorem, given the matrix-decidability interface: BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ.

theorem Complexity.sipserLautemann_of_verdictInFP (h : MatrixVerdictInFP) : SipserLautemann

The Sipser–Lautemann theorem, given the matrix interface in its function form.

theorem Complexity.sipserLautemann_iff : SipserLautemann ↔ BPP ⊆ SigmaP 2 ∧ BPP ⊆ PiP 2

The statement splits into its two halves: containment in Σ₂ᵖ and containment in Π₂ᵖ.

theorem Complexity.BPP_subset_SigmaP_two_of_sipserLautemann (h : SipserLautemann) : BPP ⊆ SigmaP 2

The Σ₂ᵖ half of the statement.

theorem Complexity.BPP_subset_PiP_two_of_sipserLautemann (h : SipserLautemann) : BPP ⊆ PiP 2

The Π₂ᵖ half of the statement.

theorem Complexity.sipserLautemann_of_subset_SigmaP (hcompl : ∀ L ∈ BPP, Lᶜ ∈ BPP) (h : BPP ⊆ SigmaP 2) : SipserLautemann

The Σ₂ᵖ half implies the full statement, given that BPP is closed under complement: a language of BPP lies in Π₂ᵖ exactly when its complement lies in Σ₂ᵖ, and the complement is again a BPP language.

theorem Complexity.BPP_subset_PH_of_sipserLautemann (h : SipserLautemann) : BPP ⊆ PH

Sipser–Lautemann puts BPP inside the polynomial hierarchy.

theorem Complexity.matrixVerdictInFP : MatrixVerdictInFP

The matrix interface holds. The verdict is computed inside Cobham's algebra — decode the triple with the payload scanners, build the trial count and seed length as smash lengths from the time bound, and take the disjunction over shift blocks of the majority vote over trial blocks, each trial being one run of the machine along the choice bits of its block — and CobhamFP_eq_FP makes that a polynomial-time function.

theorem Complexity.sipserLautemann : SipserLautemann

The Sipser–Lautemann theorem: bounded-error probabilistic polynomial time lies in the second level of the polynomial hierarchy, BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ (Arora–Barak Theorem 7.15).

theorem Complexity.BPP_subset_SigmaP_two : BPP ⊆ SigmaP 2

BPP ⊆ Σ₂ᵖ.

theorem Complexity.BPP_subset_PiP_two : BPP ⊆ PiP 2

BPP ⊆ Π₂ᵖ.

theorem Complexity.BPP_subset_PH : BPP ⊆ PH

BPP lies inside the polynomial hierarchy.