The unconditional upper bound MIP ⊆ NEXP

Every problem with a multiprover interactive proof (Cslib.Complexity.MIP or Cslib.Complexity.MIP₂) is decidable in nondeterministic exponential time (Cslib.Complexity.NEXP) Babai, Fortnow and Lund, Arora and Barak, Section 8.5:

$$\mathsf{MIP}_2 \subseteq \mathsf{MIP} \subseteq \mathsf{NEXP}.$$

Proof overview

1. Multi-channel live replay (Cslib.Complexity.MIP.aliveRun, Cslib.Complexity.MIP.accepts): A tagged history th : TaggedHistory is a list of (channel, (query, reply)) entries with channel index in ℕ (encoded in unary). Given input x and coin string r of length t, aliveRun M x r th specializes Cslib.Complexity.Interaction.aliveRun to execute M for t steps, consuming th from the front whenever M issues an oracle query (op, m) and checking that the entry matches (op.val, m). By Cslib.Complexity.Interaction.computableInPolyTime_accepts, accepts is computable tidily in polynomial time.
2. Correspondence with deterministic prover families (acceptFrom_eq_one_of_accepts, acceptFrom_eq_ite_accepts_canonicalTrace): Projecting a tagged history th onto prover i's channel (projHistory i th) commutes with non-communicating state updates (Function.update). Hence accepts M x r th = true under projected histories valid for D : Fin p → DetProver implies acceptFrom (Prover.independent fun i => (D i).toProver) ... (some (coinProgram M t x r)) = 1, and conversely every deterministic prover family D has a canonical tagged history canonicalTrace M t D ... r of length at most t with queries and replies of length at most t.
3. Certificate verification in polynomial time on exponentially padded instances (checkPaddedCert, paddedMIP_mem_NP): A certificate cert : Cert lists accepting pairs (r, th) of coin strings and tagged histories. The polynomial-time checker verifies that every (r, th) ∈ cert has r.length = t and accepts M x r th = true, that the coin strings r are pairwise distinct, that for every prover i < p the projected histories projHistory i th are pairwise consistentHist, and that 2 ^ t < 2 * cert.length. By DetProver.ValidFrom.consistentHist and validFrom_candidateProver, such a certificate exists if and only if some family of deterministic provers is accepted on more than half of the 2 ^ t coin strings.
4. Upward translation from NP to NEXP (preimage_mem_NTIME_of_mem_NP, preimage_pad_mem_NEXP, MIP_subset_NEXP): Composing the deterministic exponential-padding machine (ComputableInO.unary_two_pow) with the halting fair-coin certificate-verifier machine (IsPPTOn.exists_halting_machine) via MultiTapePTM.comp and converting to MultiTapeNTM via MultiTapePTM.toNTM places the unpadded language in NEXP.

The converse inclusion NEXP ⊆ MIP₂ (which requires the Babai–Fortnow–Lund multilinearity test and the arithmetization of NEXP verification tableaux) is not formalized here and remains open.

Main definitions

• Cslib.Complexity.MIP.TaggedHistory: multi-channel (prover, (query, reply)) transcripts.
• Cslib.Complexity.MIP.projHistory: projection of a tagged transcript onto one prover channel.
• Cslib.Complexity.MIP.aliveRun, Cslib.Complexity.MIP.accepts: polynomial-time multi-channel verifier replay.
• Cslib.Complexity.MIP.checkCert, Cslib.Complexity.MIP.paddedMIP: the certificate checker and exponentially padded NP language.

Main results

• Cslib.Complexity.MIP.exists_checkCert_of_detProver, Cslib.Complexity.MIP.exists_detProver_of_checkCert: completeness and soundness of checkCert against families of deterministic provers.
• Cslib.Complexity.MIP_subset_NEXP: MIP ⊆ NEXP.
• Cslib.Complexity.MIP₂_subset_NEXP: MIP₂ ⊆ NEXP.

References

• L. Babai, L. Fortnow, C. Lund, Non-deterministic exponential time has two-prover interactive protocols
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Tagged histories and per-prover projections

@[reducible, inline]

abbrev Cslib.Complexity.MIP.TaggedEntry : Type

A tagged query-reply entry (channel, (query, reply)) with channel index in ℕ.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.TaggedHistory : Type

A multi-channel transcript of (channel, (query, reply)) entries.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.encTaggedEntry : TaggedEntry ↪ List Bool

Encoding of a tagged transcript entry, with the channel index in unary.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.encTaggedHistory : TaggedHistory ↪ List Bool

Encoding of multi-channel tagged transcripts.

def Cslib.Complexity.MIP.projHistory (i : ℕ) (th : TaggedHistory) : Interaction.History

Project a multi-channel TaggedHistory onto the single-prover History seen by channel i.

@[simp]

theorem Cslib.Complexity.MIP.projHistory_nil (i : ℕ) : projHistory i [] = []

theorem Cslib.Complexity.MIP.projHistory_cons_self (i : ℕ) (my : List Bool × List Bool) (rest : TaggedHistory) : projHistory i ((i, my) :: rest) = my :: projHistory i rest

theorem Cslib.Complexity.MIP.projHistory_cons_of_ne {i j : ℕ} (hne : j ≠ i) (my : List Bool × List Bool) (rest : TaggedHistory) : projHistory i ((j, my) :: rest) = projHistory i rest

theorem Cslib.Complexity.MIP.computableInPolyTime_projHistory : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × TaggedHistory) => projHistory p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encTaggedHistory) Interaction.encHistory

Projecting a tagged history onto channel i is polynomial-time.

Pairwise history consistency in polynomial time

def Cslib.Complexity.MIP.consistentHistStep (s : Interaction.History × Bool × Bool) (e₁ : List Bool × List Bool) : Interaction.History × Bool × Bool

One step of the left-fold implementation of consistentHist: s = (rest₂, active, ok).

theorem Cslib.Complexity.MIP.foldl_consistentHistStep_false (h₁ h₂ : Interaction.History) (ok : Bool) : (List.foldl consistentHistStep (h₂, false, ok) h₁).2.2 = ok

theorem Cslib.Complexity.MIP.foldl_consistentHistStep_true (h₁ h₂ : Interaction.History) (ok : Bool) : (List.foldl consistentHistStep (h₂, true, ok) h₁).2.2 = (ok && consistentHist h₁ h₂)

theorem Cslib.Complexity.MIP.consistentHistStep_suffix {h₂ : Interaction.History} {s : Interaction.History × Bool × Bool} (hs : s.1 <:+ h₂) (e₁ : List Bool × List Bool) : (consistentHistStep s e₁).1 <:+ h₂

theorem Cslib.Complexity.MIP.computableInPolyTime_consistentHist : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Interaction.History × Interaction.History) => consistentHist p.1 p.2) (Turing.MultiTapeTM.encPair Interaction.encHistory Interaction.encHistory) Turing.MultiTapeTM.encBool

consistentHist is computable in polynomial time.

Multi-channel live replay in polynomial time

def Cslib.Complexity.MIP.matchTaggedOp {p : ℕ} (op : Fin p) (e : TaggedEntry) : Bool

Whether a tagged entry e belongs to prover channel op : Fin p.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.aliveStep {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (t : ℕ) (s : Interaction.AliveState k Control (Fin p) TaggedEntry) (b : Bool) : Interaction.AliveState k Control (Fin p) TaggedEntry

One step of the multi-channel live replay of M with truncation bound t and coin b.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.aliveRun {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (x r : List Bool) (th : TaggedHistory) : Interaction.AliveState k Control (Fin p) TaggedEntry

The multi-channel live replay of M on input x with coins r against tagged history th.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.accepts {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (x r : List Bool) (th : TaggedHistory) : Bool

Whether M on input x with coins r accepts along tagged history th: the replay stays live, consumes the entire tagged history, and has output [true] after the clocked run.

theorem Cslib.Complexity.MIP.computableInPolyTime_accepts {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) [Finite Control] : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : List Bool × List Bool × TaggedHistory) => accepts M q.1 q.2.1 q.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encTaggedHistory)) Turing.MultiTapeTM.encBool

Multi-channel replay acceptance is polynomial-time in the input, coins, and tagged history.

Correspondence between accepts and coinProgram against deterministic provers

theorem Cslib.Complexity.MIP.aliveStep_sound {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (t : ℕ) (D : Fin p → DetProver) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control (Fin p)) (th : TaggedHistory) (s : (i : Fin p) → (D i).State) (b : Bool) (hvalid : ∀ (i : Fin p), (D i).ValidFrom (s i) (projHistory (↑i) th)) (hlive : (aliveStep M t (cfg, th, true) b).2.2 = true) : ∃ (s' : (i : Fin p) → (D i).State), (∀ (i : Fin p), (D i).ValidFrom (s' i) (projHistory (↑i) (aliveStep M t (cfg, th, true) b).2.1)) ∧ (OracleComp.interpret (Prover.independent fun (i : Fin p) => (D i).toProver).respond (Interaction.coinStep M t cfg b)).run s = PMF.pure ((aliveStep M t (cfg, th, true) b).1, s')

Soundness of a single aliveStep: if aliveStep M t (cfg, th, true) b remains live and every prover channel's projection of th is valid for D i from s i, then coinStep M t cfg b against Prover.independent (fun i => (D i).toProver) transitions deterministically to the same configuration and an updated state vector s' for which the remaining tagged history is valid.

theorem Cslib.Complexity.MIP.foldl_aliveStep_sound {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (t : ℕ) (D : Fin p → DetProver) (l : List Bool) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control (Fin p)) (th : TaggedHistory) (s : (i : Fin p) → (D i).State) (hvalid : ∀ (i : Fin p), (D i).ValidFrom (s i) (projHistory (↑i) th)) (hlive : (List.foldl (aliveStep M t) (cfg, th, true) l).2.2 = true) : ∃ (s' : (i : Fin p) → (D i).State), (∀ (i : Fin p), (D i).ValidFrom (s' i) (projHistory (↑i) (List.foldl (aliveStep M t) (cfg, th, true) l).2.1)) ∧ (OracleComp.interpret (Prover.independent fun (i : Fin p) => (D i).toProver).respond (List.foldlM (Interaction.coinStep M t) cfg l)).run s = PMF.pure ((List.foldl (aliveStep M t) (cfg, th, true) l).1, s')

Soundness of foldl (aliveStep M t): if the multi-channel replay over l stays live and th has valid projections for D from s, then l.foldlM (coinStep M t) cfg transitions deterministically to the final configuration of the replay.

theorem Cslib.Complexity.MIP.acceptFrom_eq_one_of_accepts {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) {x r : List Bool} {t : ℕ} (hr : r.length = t) (D : Fin p → DetProver) (s : (i : Fin p) → (D i).State) (th : TaggedHistory) (hvalid : ∀ (i : Fin p), (D i).ValidFrom (s i) (projHistory (↑i) th)) (hacc : accepts M x r th = true) : Interaction.acceptFrom (Prover.independent fun (i : Fin p) => (D i).toProver) s (some (Interaction.coinProgram M t x r)) = 1

Soundness of accepts: if r.length = t, accepts M x r th = true, and every prover's projection of th is valid for D i from s i, then coinProgram M t x r accepts with probability 1 against D.

def Cslib.Complexity.MIP.canonicalTrace {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (t : ℕ) (D : Fin p → DetProver) : Turing.MultiTapeMachine.FiniteConfig k Bool Control (Fin p) → ((i : Fin p) → (D i).State) → List Bool → TaggedHistory

The canonical tagged history generated by running M with truncation t against deterministic provers D : Fin p → DetProver from configuration cfg and prover states s over coins l.

theorem Cslib.Complexity.MIP.validFrom_canonicalTrace {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (t : ℕ) (D : Fin p → DetProver) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control (Fin p)) (s : (i : Fin p) → (D i).State) (l : List Bool) (i : Fin p) : (DetProver.truncate t (D i)).ValidFrom (s i) (projHistory (↑i) (canonicalTrace M t D cfg s l))

Every prover's projection of canonicalTrace M t D cfg s l is a valid history for the t-truncated deterministic prover (D i).truncate t starting from s i.

theorem Cslib.Complexity.MIP.foldl_aliveStep_canonicalTrace {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (t : ℕ) (D : Fin p → DetProver) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control (Fin p)) (s : (i : Fin p) → (D i).State) (l : List Bool) : ∃ (cfg' : Turing.MultiTapeMachine.FiniteConfig k Bool Control (Fin p)) (s' : (i : Fin p) → (D i).State), List.foldl (aliveStep M t) (cfg, canonicalTrace M t D cfg s l, true) l = (cfg', [], true) ∧ (OracleComp.interpret (Prover.independent fun (i : Fin p) => (D i).toProver).respond (List.foldlM (Interaction.coinStep M t) cfg l)).run s = PMF.pure (cfg', s')

Running foldl (aliveStep M t) against canonicalTrace M t D cfg s l stays live, consumes the entire trace, and reaches the exact configuration produced by l.foldlM (coinStep M t) cfg against D.

theorem Cslib.Complexity.MIP.acceptFrom_eq_ite_accepts_canonicalTrace {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) {x r : List Bool} {t : ℕ} (hr : r.length = t) (D : Fin p → DetProver) : Interaction.acceptFrom (Prover.independent fun (i : Fin p) => (D i).toProver) (Prover.independent fun (i : Fin p) => (D i).toProver).init (some (Interaction.coinProgram M t x r)) = if accepts M x r (canonicalTrace M t D (Turing.MultiTapeMachine.FiniteConfig.init M.initial x) (fun (i : Fin p) => (D i).init) r) = true then 1 else 0

Completeness of accepts via canonicalTrace: for any r of length t, the acceptance probability of coinProgram M t x r against deterministic provers D is 1 if accepts holds on canonicalTrace, and 0 otherwise.

theorem Cslib.Complexity.MIP.bounds_canonicalTrace {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) {n i t : ℕ} (D : Fin p → DetProver) {cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control (Fin p)} (hspace : Turing.MultiTapeMachine.FiniteConfig.SpaceBound n i t cfg) (s : (j : Fin p) → (D j).State) (l : List Bool) : List.length (canonicalTrace M t D cfg s l) ≤ l.length ∧ ∀ e ∈ canonicalTrace M t D cfg s l, e.1 ≤ p ∧ e.2.1.length ≤ i + l.length ∧ e.2.2.length ≤ t

Size bounds on canonicalTrace M t D cfg s l: its length is at most l.length, every channel index is at most p, every query has length at most i + l.length, and every reply has length at most t.

Polynomial-time certificate checking and the padded NP language

@[reducible, inline]

abbrev Cslib.Complexity.MIP.Cert : Type

A multiprover certificate is a list of (coinString, taggedHistory) pairs.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.encCertEntry : List Bool × TaggedHistory ↪ List Bool

Encoding of a single (coinString, taggedHistory) certificate entry.

@[reducible, inline]

abbrev Cslib.Complexity.MIP.encCert : Cert ↪ List Bool

Encoding of multiprover certificates.

def Cslib.Complexity.MIP.certDecoder : Turing.MultiTapeTM.Decoder encCert

Total decoder for multiprover certificates.

def Cslib.Complexity.MIP.checkCert {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (c d : ℕ) (x : List Bool) (cert : Cert) : Bool

Check whether cert is a valid accepting multiprover transcript table for M on input x with clock t = c * (x.length + 1) ^ d:

1. every (r, th) ∈ cert has r.length = t and accepts M x r th = true,
2. every coin string r in cert appears once,
3. for every prover i < p, the projected histories projHistory i th are pairwise consistentHist,
4. 2 ^ t < 2 * cert.length.

def Cslib.Complexity.MIP.checkPaddedCert {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (c d : ℕ) (q : List Bool × Cert) : Bool

Check a certificate on a padded instance w: require (encCert cert).length ≤ w.length and run checkCert on the unframed prefix unframe w.

def Cslib.Complexity.MIP.paddedMIP {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) (c d : ℕ) : Set (List Bool)

The padded NP language associated to M and clock polynomial c * (n + 1) ^ d.

theorem Cslib.Complexity.MIP.computableInPolyTime_checkCert {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) [Finite Control] (c d : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : List Bool × Cert) => checkCert M c d q.1 q.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encCert) Turing.MultiTapeTM.encBool

checkCert is computable in polynomial time.

theorem Cslib.Complexity.MIP.computableInPolyTime_checkPaddedCert {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) [Finite Control] (c d : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (checkPaddedCert M c d) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encCert) Turing.MultiTapeTM.encBool

checkPaddedCert is computable in polynomial time.

theorem Cslib.Complexity.MIP.paddedMIP_mem_NP {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) [Finite Control] (c d : ℕ) : paddedMIP M c d ∈ NP Turing.MultiTapeTM.encBits

The padded multiprover language paddedMIP M c d belongs to NP encBits.

Soundness and completeness of checkCert

theorem Cslib.Complexity.MIP.exists_detProver_of_checkCert {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) {c d : ℕ} {x : List Bool} {cert : Cert} (hcheck : checkCert M c d x cert = true) : have t := c * (x.length + 1) ^ d; ∃ (D : Fin p → DetProver), ↑(List.length cert) ≤ ∑ f : Fin t → Bool, Interaction.acceptFrom (Prover.independent fun (i : Fin p) => (D i).toProver) (Prover.independent fun (i : Fin p) => (D i).toProver).init (some (Interaction.coinProgram M t x (List.ofFn f))) ∧ 2 ^ t < 2 * List.length cert

Soundness of checkCert: if checkCert M c d x cert = true, then there exists an independent family of deterministic provers D : Fin p → DetProver whose acceptance probability on the t = c * (x.length + 1) ^ d coin family exceeds 1 / 2.

theorem Cslib.Complexity.MIP.exists_checkCert_of_detProver {p k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control (Fin p)) {c d : ℕ} (x : List Bool) (D : Fin p → DetProver) (hlt : 2 ^ (c * (x.length + 1) ^ d) < 2 * {f : Fin (c * (x.length + 1) ^ d) → Bool | accepts M x (List.ofFn f) (canonicalTrace M (c * (x.length + 1) ^ d) D (Turing.MultiTapeMachine.FiniteConfig.init M.initial x) (fun (i : Fin p) => (D i).init) (List.ofFn f)) = true}.card) : have t := c * (x.length + 1) ^ d; ∃ (cert : Cert), checkCert M c d x cert = true ∧ (encCert cert).length ≤ 32 * (p + x.length + t + 1) ^ 2 * 2 ^ t

Completeness of checkCert: if a family D : Fin p → DetProver of deterministic provers makes M accept x on more than half of the t = c * (x.length + 1) ^ d coin strings, then the canonical certificate built from D passes checkCert, and its encoded length is at most 32 * (p + x.length + t + 1) ^ 2 * 2 ^ t.

The unconditional upper bounds MIP ⊆ NEXP and MIP₂ ⊆ NEXP

theorem Cslib.Complexity.MIP_subset_NEXP {α : Type} (enc : α ↪ List Bool) : MIP enc ⊆ NEXP enc

MIP ⊆ NEXP Babai, Fortnow and Lund, Arora and Barak, Section 8.5: every problem with a multiprover interactive proof is decidable in nondeterministic exponential time.

theorem Cslib.Complexity.MIP₂_subset_NEXP {α : Type} (enc : α ↪ List Bool) : MIP₂ enc ⊆ NEXP enc

MIP₂ ⊆ NEXP: every problem with a two-prover interactive proof is decidable in nondeterministic exponential time.