PSPACE ⊆ IP

⚠️ Unreviewed by Bolton

Shamir's theorem, the hard half of IP = PSPACE.

Take a PSPACE-complete problem — validity of a quantified Boolean formula — and arithmetize it: replace the Boolean connectives by polynomial operations over a finite field, so that the formula's truth value becomes the value of an iterated sum and product. The prover then convinces the verifier of that value by the sum-check protocol, one variable at a time, with a degree-reduction step interleaved to keep the intermediate polynomials small.

What the proof needs

• A PSPACE-complete problem and the reduction to it — Complexitylib.SAT.QBF has the syntax.
• Arithmetization over a finite field, and the sum-check protocol with its soundness bound.
• The interactive machinery of Complexitylib.Classes.Interactive to package the protocol.

TODO

• Prove it. This is the deepest single theorem on the roadmap's long-term track.

def Complexity.PSPACESubsetIP : Prop

PSPACE ⊆ IP (Shamir): arithmetize a quantified Boolean formula and run sum-check.

Equations

• Complexity.PSPACESubsetIP = (Complexity.PSPACE ⊆ Complexity.IP)

theorem Complexity.IP_eq_PSPACE_of (h' : PSPACESubsetIP) : IP = PSPACE

The two halves together are Shamir's theorem; the first is IP_subset_PSPACE.