Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `PSPACE equals NPSPACE`

groundedproofs/Lax307052Proofs/Savitch.lean · lax-307052

What this proof establishes

thm✓Lax307052.PolynomialSpace

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Enlarge the original polynomial bound to p(n)+n+2p(n)+n+2 and square it.