The amplified Lautemann characterization

Combining majority amplification with the covering lemma of Complexitylib.Classes.PH.SipserLautemann.Covering, this file proves the ∃∀ characterization at the heart of the Sipser–Lautemann theorem.

def Complexity.Lautemann.ampExp (f : ℕ → ℕ) (n : ℕ) : ℕ

Amplification exponent for inputs of length n: the amplified error is 2 ^ (-ampExp f n). It is taken large enough to dominate the amplified seed length, which is what the covering lemma's soundness direction needs.

Equations

• Complexity.Lautemann.ampExp f n = f n + 11

def Complexity.Lautemann.ampRuns (f : ℕ → ℕ) (n : ℕ) : ℕ

Number of independent trials of the source machine, an odd count so that majority votes cannot tie.

Equations

• Complexity.Lautemann.ampRuns f n = 12 * Complexity.Lautemann.ampExp f n + 1

def Complexity.Lautemann.ampShifts (f : ℕ → ℕ) (n : ℕ) : ℕ

Number of shifts used to cover the seed space: one more than the seed length, so that the degenerate zero-length seed space is still covered.

Equations

• Complexity.Lautemann.ampShifts f n = Complexity.Lautemann.ampRuns f n * f n + 1

def Complexity.Lautemann.ampEvent {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (x : List Bool) : Finset (Fin (ampRuns f x.length * f x.length) → Bool)

The amplified accepting event: the long seeds on which a strict majority of the ampRuns f n independent trials accepts.

Equations

• Complexity.Lautemann.ampEvent tm f x = {w : Fin (Complexity.Lautemann.ampRuns f x.length * f x.length) → Bool | Complexity.blockMajority (tm.repeatAcceptEvent x (f x.length)) w = true}

@[simp]

theorem Complexity.Lautemann.mem_ampEvent {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (x : List Bool) (w : Fin (ampRuns f x.length * f x.length) → Bool) : w ∈ ampEvent tm f x ↔ blockMajority (tm.repeatAcceptEvent x (f x.length)) w = true

Membership in the amplified event is the majority verdict.

theorem Complexity.Lautemann.compl_ampEvent {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (x : List Bool) : (ampEvent tm f x)ᶜ = {w : Fin (ampRuns f x.length * f x.length) → Bool | blockMajority (tm.repeatAcceptEvent x (f x.length)) w = false}

The complement of the amplified event is the majority-rejecting event.

theorem Complexity.Lautemann.mem_compl_ampEvent {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (x : List Bool) (w : Fin (ampRuns f x.length * f x.length) → Bool) : w ∈ (ampEvent tm f x)ᶜ ↔ blockMajority (tm.repeatAcceptEvent x (f x.length)) w = false

Membership in the complement of the amplified event is the rejecting majority verdict. Not a simp lemma: simp reaches the same normal form through Finset.mem_compl and mem_ampEvent.

theorem Complexity.Lautemann.ampShifts_lt_two_pow_ampExp (f : ℕ → ℕ) (n : ℕ) : ampShifts f n < 2 ^ ampExp f n

The number of shifts is below the amplified error denominator.

theorem Complexity.Lautemann.exists_covers_of_mem {k : ℕ} {tm : NTM k} {L : Language} {f : ℕ → ℕ} (haccept : tm.AcceptsWithProb L f (2 / 3)) {x : List Bool} (hx : x ∈ L) : ∃ (u : Fin (ampShifts f x.length) → Fin (ampRuns f x.length * f x.length) → Bool), Covers (ampEvent tm f x) u

Completeness. On an accepted input the amplified event fails with probability at most 2 ^ (-ampExp f n), so the covering lemma supplies ampShifts f n shifts covering the whole seed space.

theorem Complexity.Lautemann.not_covers_of_notMem {k : ℕ} {tm : NTM k} {L : Language} {f : ℕ → ℕ} (hreject : tm.RejectsWithProb L f (1 / 3)) {x : List Bool} (hx : x ∉ L) (u : Fin (ampShifts f x.length) → Fin (ampRuns f x.length * f x.length) → Bool) : ¬Covers (ampEvent tm f x) u

Soundness. On a rejected input the amplified event holds with probability at most 2 ^ (-ampExp f n), which is too small for ampShifts f n shifts of it to cover the seed space.

theorem Complexity.Lautemann.mem_iff_exists_covers {k : ℕ} {tm : NTM k} {L : Language} {f : ℕ → ℕ} (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) (x : List Bool) : x ∈ L ↔ ∃ (u : Fin (ampShifts f x.length) → Fin (ampRuns f x.length * f x.length) → Bool), Covers (ampEvent tm f x) u

The Lautemann characterization. For a bounded-error machine deciding L, membership is equivalent to the existence of a tuple of shifts whose translates of the amplified accepting event cover the seed space — an ∃∀ form with a deterministic, polynomially-checkable matrix.

theorem Complexity.Lautemann.notMem_iff_exists_covers_compl {k : ℕ} {tm : NTM k} {L : Language} {f : ℕ → ℕ} (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) (x : List Bool) : x ∉ L ↔ ∃ (u : Fin (ampShifts f x.length) → Fin (ampRuns f x.length * f x.length) → Bool), Covers (ampEvent tm f x)ᶜ u

The complementary Lautemann characterization. Non-membership is equivalent to the existence of shifts covering the seed space with translates of the majority-rejecting event. Together with mem_iff_exists_covers this puts both L and its complement in the same ∃∀ form, which is what places BPP in Σ₂ᵖ ∩ Π₂ᵖ rather than only in Σ₂ᵖ.