The Lautemann matrix language and the Σ₂ form

The ∃∀ characterization of Complexitylib.Classes.PH.SipserLautemann.Amplified quantifies over shift tuples and seeds; the polynomial hierarchy quantifies over bitstrings. This file bridges the two: matrixLang is the innermost, quantifier-free predicate as a language of encoded triples, and eq_polyExistsLang_polyForallLang says that a bounded-error language is literally a polynomially bounded ∃∀ over it.

Both the language and the identity are stated for a general time-bound function f, but the intended instance takes f to be the evaluation of a polynomial — see NTM.acceptsWithProb_of_le, which replaces a machine's arbitrary halting bound by a dominating polynomial. That is what makes the matrix predicate computable: a decider must recover the per-trial step count from the input length, which it can do when the count is a fixed polynomial in |x|, and cannot do for an arbitrary f.

Main definitions

• matrixLang tm f b — on pair (pair x w) r: the decoded shifts of the decoded seed contain one whose amplified majority verdict is b
• boundPoly — the polynomial bounding the amplified seed length

Main results

• mem_matrixLang_pair — membership on an encoded triple
• eq_polyExistsLang_polyForallLang — the Σ₂ form of a bounded-error language, and compl_eq_polyExistsLang_polyForallLang for its complement
• boundPoly_bounds — the amplified lengths are polynomially bounded

The matrix language

def Complexity.Lautemann.matrixPred {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) : Prop

The quantifier-free predicate of the Lautemann characterization, on the three decoded components.

Equations

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

noncomputable def Complexity.Lautemann.matrixVerdictOn {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) : Bool

The same predicate as a Bool-valued verdict.

Equations

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

theorem Complexity.Lautemann.matrixVerdictOn_eq_true_iff {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) : matrixVerdictOn tm f b x w r = true ↔ matrixPred tm f b x w r

The verdict decides the predicate.

def Complexity.Lautemann.matrixLang {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) : Language

The innermost predicate of the Lautemann characterization, as a language of encoded triples. The components are decoded with the polynomial-time payload scanners pairFst and pairSnd, which recover them from a canonical pair; on malformed input the decoders return their partial reads, and the language's contents there are irrelevant to the Σ₂ identity below.

Equations

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

theorem Complexity.Lautemann.mem_matrixLang_pair {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) : pair (pair x w) r ∈ matrixLang tm f b ↔ matrixPred tm f b x w r

Membership of an encoded triple in the matrix language.

noncomputable def Complexity.Lautemann.matrixVerdict {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (z : List Bool) : Bool

The matrix as a Bool-valued verdict function, so that the remaining polynomial-time obligation is about a function, which Complexitylib.Classes.P.Cobham can discharge inside Cobham's algebra without constructing a machine.

Equations

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

@[simp]

theorem Complexity.Lautemann.matrixVerdict_pair {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) : matrixVerdict tm f b (pair (pair x w) r) = matrixVerdictOn tm f b x w r

The verdict function on an encoded triple.

theorem Complexity.Lautemann.mem_matrixLang_iff_verdict {k : ℕ} (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (z : List Bool) : z ∈ matrixLang tm f b ↔ matrixVerdict tm f b z = true

The verdict function decides the matrix language.

The Σ₂ form

theorem Complexity.Lautemann.eq_polyExistsLang_polyForallLang {k : ℕ} {tm : NTM k} {f : ℕ → ℕ} {b : Bool} {A : Language} (E : (x : List Bool) → Finset (Fin (ampRuns f x.length * f x.length) → Bool)) (hmem : ∀ (x : List Bool) (w : Fin (ampRuns f x.length * f x.length) → Bool), w ∈ E x ↔ blockMajority (tm.repeatAcceptEvent x (f x.length)) w = b) (hA : ∀ (x : List Bool), x ∈ A ↔ ∃ (u : Fin (ampShifts f x.length) → Fin (ampRuns f x.length * f x.length) → Bool), Covers (E x) u) {p q : Polynomial ℕ} (hp : ∀ (n : ℕ), ampShifts f n * (ampRuns f n * f n) ≤ Polynomial.eval n p) (hq : ∀ (n : ℕ), ampRuns f n * f n ≤ Polynomial.eval n q) : A = polyExistsLang p (polyForallLang q (matrixLang tm f b))

The Σ₂ form of a covering characterization. Given a family of events whose covering-by-shifts characterizes a language A, that language is a polynomially bounded existential over a polynomially bounded universal over the matrix language. The existential witness encodes a covering tuple of shifts, and the universal variable ranges over seeds.

theorem Complexity.Lautemann.eq_polyExistsLang_of_boundedError {k : ℕ} {tm : NTM k} {L : Language} {f : ℕ → ℕ} (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) {p q : Polynomial ℕ} (hp : ∀ (n : ℕ), ampShifts f n * (ampRuns f n * f n) ≤ Polynomial.eval n p) (hq : ∀ (n : ℕ), ampRuns f n * f n ≤ Polynomial.eval n q) : L = polyExistsLang p (polyForallLang q (matrixLang tm f true))

The Σ₂ form of a bounded-error language: L itself.

theorem Complexity.Lautemann.compl_eq_polyExistsLang_of_boundedError {k : ℕ} {tm : NTM k} {L : Language} {f : ℕ → ℕ} (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3)) {p q : Polynomial ℕ} (hp : ∀ (n : ℕ), ampShifts f n * (ampRuns f n * f n) ≤ Polynomial.eval n p) (hq : ∀ (n : ℕ), ampRuns f n * f n ≤ Polynomial.eval n q) : Lᶜ = polyExistsLang p (polyForallLang q (matrixLang tm f false))

The Σ₂ form of a bounded-error language: its complement.

Polynomial bounds

noncomputable def Complexity.Lautemann.boundPoly (P : Polynomial ℕ) : Polynomial ℕ

The polynomial bounding the amplified seed length, given a polynomial P dominating the machine's time bound.

Equations

• Complexity.Lautemann.boundPoly P = (Polynomial.C 12 * P + Polynomial.C 133) * P

@[simp]

theorem Complexity.Lautemann.boundPoly_eval (P : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (boundPoly P) = (12 * Polynomial.eval n P + 133) * Polynomial.eval n P

theorem Complexity.Lautemann.boundPoly_bounds {f : ℕ → ℕ} {P : Polynomial ℕ} (hf : ∀ (n : ℕ), f n ≤ Polynomial.eval n P) : (∀ (n : ℕ), ampRuns f n * f n ≤ Polynomial.eval n (boundPoly P)) ∧ ∀ (n : ℕ), ampShifts f n * (ampRuns f n * f n) ≤ Polynomial.eval n ((boundPoly P + 1) * boundPoly P)

The amplified seed length is bounded by boundPoly P, and the amplified witness length by (boundPoly P + 1) * boundPoly P.