Multiprover interactive proofs (MIP₂ and MIP)

This umbrella module re-exports the multiprover interactive proof development:

• Complexity.Computability.Complexity.Classes.MIP.Defs: non-communicating prover families (Prover.independent, Prover.independent_state_eq_of_ne), IsMultiproverProof, the classes MIP₂ and MIP, closure under polynomial-time many-one reductions (PolyTimeReducible.mem_MIP₂, PolyTimeReducible.mem_MIP), and the embeddings IP ⊆ MIP₂ ⊆ MIP. The number of provers is constant for each language.
• Complexity.Computability.Complexity.Classes.MIP.OptimalProver: coin-fixing for multi-channel oracle machines (MIP.acceptProb_eq_sum), coordinatewise presampling and deterministic prover optimality (MIP.exists_deterministic_prover_family), and pairwise history consistency (MIP.consistentHist, MIP.DetProver.ValidFrom.consistentHist, MIP.validFrom_candidateProver).
• Complexity.Computability.Complexity.Classes.MIP.NEXP: polynomial-time multi-channel transcript verification, the exponential-padding translation in Classes.Padding, and the unconditional upper bounds MIP_subset_NEXP : MIP enc ⊆ NEXP enc and MIP₂_subset_NEXP : MIP₂ enc ⊆ NEXP enc.

The converse inclusion NEXP ⊆ MIP₂ (Babai–Fortnow–Lund multilinearity testing and arithmetization of NEXP verification tableaux) remains open.

References

• M. Ben-Or, S. Goldwasser, J. Kilian, A. Wigderson, Multi-prover interactive proofs: How to remove intractability assumptions
• L. Babai, L. Fortnow, C. Lund, Non-deterministic exponential time has two-prover interactive protocols
• S. Arora, B. Barak, Computational Complexity: A Modern Approach