Polynomial-space Mathlib stack machines decide problems in PSPACE

The source certificate supplies termination and a Boolean answer. A polynomial bound on every reachable source stack gives a tidy polynomial-space computation, then membership in PSPACE. The source runtime need not be polynomially bounded. Input and output words use the bridge's standard finite-symbol encodings; the final Boolean answer is recoded to encBool.

Main results

• Cslib.Complexity.mem_PSPACE_of_tm2: a terminating Mathlib TM2 decider with polynomially bounded stacks decides a problem in PSPACE.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.1

theorem Cslib.Complexity.mem_PSPACE_of_tm2 {α αΓ βΓ : Type} [Finite αΓ] [Finite βΓ] {ea : α → List αΓ} {eb : Bool → List βΓ} {f : α → Bool} {A : Set α} (h : Turing.TM2Computable ea eb f) [∀ (k : h.tm.K), Finite (h.tm.Γ k)] (ha : Function.Injective ea) (hb : Function.Injective eb) {space : α → ℕ} (hspace : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ea a).length) space) (hstacks : ∀ (a : α) (i : ℕ) (k : h.tm.K), (((Turing.TM2.stepTotal h.tm.m)^[i] (Turing.initList h.tm (List.map (⇑h.inputAlphabet.symm) (ea a)))).stk k).length ≤ space a) (hA : ∀ (a : α), a ∈ A ↔ f a = true) : A ∈ PSPACE ({ toFun := ea, inj' := ha }.trans (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encFinite αΓ)))

A terminating finite-alphabet Mathlib stack-machine decider with polynomially bounded stacks decides a problem in PSPACE, under the standard binary input-word encoding.

The hypothesis hstacks uses Turing.TM2.stepTotal, which agrees with Mathlib's partial Turing.TM2.step whenever it returns a successor and fixes halted configurations (Turing.TM2.stepTotal_of_step). Thus it bounds the ordinary source run, including its initial and final configurations; padding beyond halting imposes no additional stack bound.