PH ⊆ PSPACE — the induction on the level

⚠️ Unreviewed by Bolton

The hierarchy is built one quantifier at a time: SigmaP 0 = P and SigmaP (n+1) = polyExistsClass (complClass (SigmaP n)). So an induction on the level reduces the containment to two closure properties of PSPACE, and nothing else: closure under complement, and closure under a polynomially bounded existential quantifier. The base case is already available as P_subset_PSPACE.

Closure under complement is now proved — see Complexitylib.Classes.Containments.Internal.ComplementSpace — so only the existential quantifier is left, and PH_subset_PSPACE_of_polyExists_internal states the containment with that as its single remaining hypothesis.

The intended construction

The machine that will discharge the remaining hypothesis enumerates witnesses in a loop. Its space accounting is supplied by Complexitylib.Models.TuringMachine.Combinators.Internal.Window: TM.KeepsWindow is a space discipline that survives re-entry, TM.loopTM_keepsWindow shows a loop inherits it from its body and test — so a loop may run as long as it likes without its bound growing — and TM.decidesInSpace_of_keepsWindow turns the result into a DSPACE membership.

The enumeration itself is a single loop. mem_polyExistsLang_iff_count replaces the two numeric quantifiers by one counter below 2 ^ (p |x| + 1), a value denoting the witness dropTop v — its canonical bits with the leading one removed. The machine never computes dropTop: it carries the witness on a tape of its own and advances it in step with the counter, which dropTop_succ says is the increment bumpLE — the ordinary binary increment, except that a carry off the end extends the witness by a zero rather than writing a one. So the loop control is exactly the one NTM.ppMachine already runs, and the witness tape is maintained by a variant of TM.binarySuccTM.

The body can be assembled from existing subroutines rather than built from scratch. The one apparent obstacle is that TM.pairInputWorkTM emits pair w x, taking its second component from the real input, whereas polyExistsLang needs pair x w. Retargeting resolves it: TM.retargetInputStarted makes a machine read its input off a work tape, so the emitter can be pointed at the witness tape as its "input" while the copy of x — produced by TM.copyInputToOutputTM under TM.retargetOutput — sits on the work tape it delimits. No new emitter is required. The space cost of that relocation is accounted for by TM.retargetInput_keepsWindow_of_reaches: what was the machine's free input tape becomes a charged work tape, so the window it needs is its own budget plus the virtual input's length. TM.resetTapesTM clears the scratch between iterations, which is what makes the body robust enough for TM.seqTM_keepsWindow_of_post.

Main results

• PH_subset_PSPACE_of_enumerator_internal — the containment, modulo one machine
• SigmaP_subset_PSPACE_of_internal — every level, modulo the two closure properties
• PH_subset_PSPACE_of_internal — the induction, modulo the two closure properties
• PH_subset_PSPACE_of_polyExists_internal — the containment, modulo the existential alone
• mem_polyExistsLang_iff_numeric — what the enumerating machine has to decide
• mem_polyExistsLang_iff_count — the same, as a single count over one counter
• PH_subset_PSPACE_of_polyExistsLang_internal — the containment, modulo one concrete language-level statement
• PH_enumerator_exists — the enumerating machine, with its window and its verdict
• PH_subset_PSPACE_internal — the containment

theorem Complexity.SigmaP_subset_PSPACE_of_internal (hcompl : ∀ L ∈ PSPACE, Lᶜ ∈ PSPACE) (hex : polyExistsClass PSPACE ⊆ PSPACE) (n : ℕ) : SigmaP n ⊆ PSPACE

Every level of the hierarchy is in PSPACE, granted the two closure properties.

theorem Complexity.PH_subset_PSPACE_of_internal (hcompl : ∀ L ∈ PSPACE, Lᶜ ∈ PSPACE) (hex : polyExistsClass PSPACE ⊆ PSPACE) : PH ⊆ PSPACE

PH ⊆ PSPACE, modulo two closure properties of PSPACE. The alternating prefix is consumed one quantifier at a time; a complement flips the verdict and an existential is evaluated by trying every witness in place.

theorem Complexity.PH_subset_PSPACE_of_polyExists_internal (hex : polyExistsClass PSPACE ⊆ PSPACE) : PH ⊆ PSPACE

PH ⊆ PSPACE, modulo a single closure property. Closure under complement is proved, so only the polynomially bounded existential quantifier remains.

theorem Complexity.mem_polyExistsLang_iff_numeric (p : Polynomial ℕ) (L' : Language) (x : List Bool) : x ∈ polyExistsLang p L' ↔ ∃ ℓ ≤ Polynomial.eval x.length p, ∃ v < 2 ^ ℓ, pair x (bitsOfLen ℓ v) ∈ L'

Membership in a bounded existential, as two numeric quantifiers. This is the condition the enumerating machine decides: iterate a witness length and a witness value, and test the pair.

theorem Complexity.mem_polyExistsLang_iff_count (p : Polynomial ℕ) (L' : Language) (x : List Bool) : x ∈ polyExistsLang p L' ↔ ∃ v < 2 ^ (Polynomial.eval x.length p + 1), pair x (dropTop v) ∈ L'

Membership in a bounded existential, as a single count. The two numeric quantifiers above collapse to one: a counter below 2 ^ (p |x| + 1) denotes a witness through dropTop, every witness of the admitted lengths being denoted. This is the form the enumerating machine runs — one loop over one register, the same shape as the path-counting machine of PP ⊆ PSPACE.

theorem Complexity.polyExistsClass_PSPACE_subset_PSPACE_of (h : ∀ (p : Polynomial ℕ), ∀ L' ∈ PSPACE, polyExistsLang p L' ∈ PSPACE) : polyExistsClass PSPACE ⊆ PSPACE

The class-level closure reduces to a statement about one language construction.

theorem Complexity.PH_subset_PSPACE_of_polyExistsLang_internal (h : ∀ (p : Polynomial ℕ), ∀ L' ∈ PSPACE, polyExistsLang p L' ∈ PSPACE) : PH ⊆ PSPACE

PH ⊆ PSPACE, reduced to a single concrete obligation. No class-level plumbing is left: what remains is to exhibit, for one polynomial and one polynomially space-bounded language, a machine deciding the bounded existential in polynomial space. Closure under complement is already proved, and mem_polyExistsLang_iff_numeric says exactly what that machine has to decide.

theorem Complexity.PH_subset_PSPACE_of_enumerator_internal (h : ∀ (p : Polynomial ℕ), ∀ L' ∈ PSPACE, ∃ (k : ℕ) (tm : TM k) (q : Polynomial ℕ), (∀ (x : List Bool) (c' : Cfg k tm.Q), tm.reaches (tm.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length q)) ∧ ∀ (x : List Bool), ∃ (c' : Cfg k tm.Q), tm.reaches (tm.initCfg x) c' ∧ tm.halted c' ∧ (x ∈ polyExistsLang p L' → c'.output.cells 1 = Γ.one) ∧ (x ∉ polyExistsLang p L' → c'.output.cells 1 = Γ.zero)) : PH ⊆ PSPACE

The last obligation, spelled out at the machine level. PH ⊆ PSPACE now follows from the existence of one machine: for each polynomial p and each polynomially space-bounded L', a machine that keeps a polynomial window and decides the bounded existential — whose membership condition is the two numeric quantifiers of mem_polyExistsLang_iff_numeric.

theorem Complexity.PH_enumerator_exists (p : Polynomial ℕ) (L' : Language) (hL' : L' ∈ PSPACE) : ∃ (k' : ℕ) (tm : TM k') (Q : Polynomial ℕ), (∀ (x : List Bool) (c' : Cfg k' tm.Q), tm.reaches (tm.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length Q)) ∧ ∀ (x : List Bool), ∃ (c' : Cfg k' tm.Q), tm.reaches (tm.initCfg x) c' ∧ tm.halted c' ∧ (x ∈ polyExistsLang p L' → c'.output.cells 1 = Γ.one) ∧ (x ∉ polyExistsLang p L' → c'.output.cells 1 = Γ.zero)

The enumerating machine exists. For every polynomial p and every polynomially space-bounded L', the witness enumerator PolyExists.enumTM decides the bounded existential polyExistsLang p L' and keeps a polynomial window while doing so. Its space bound is independent of the loop's running time: the counter and the witness are the only things that grow, and both stay below p |x| + 1 bits.

theorem Complexity.PH_subset_PSPACE_internal : PH ⊆ PSPACE

PH ⊆ PSPACE. The induction on the level leaves two closure properties of PSPACE; complement is PSPACE_compl, and the bounded existential is discharged by the witness enumerator of PH_enumerator_exists.