def SpaceComplexity.IsAsympBoundedBy (g f : ℕ → ℕ) : Prop

Asymptotic upper bound: g is O(f) in the sense that there exist constants c > 0 and n₀ such that g n ≤ c * f n for all n ≥ n₀.

noncomputable def SpaceComplexity.TMSpaceUsed {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (w : List Γ) (n : ℕ) : ℕ

Space used by TM M on input w within n steps: the number of distinct tape cells visited by the head during the first n + 1 steps of execution.

def SpaceComplexity.TMRunsInSpace {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (f : ℕ → ℕ) : Prop

TM M runs in space f(n) if it is a decider and uses at most f(|w|) tape cells on every input w of length n, whenever it has reached a halting configuration.

def SpaceComplexity.InSPACE {Γ : Type} (f : ℕ → ℕ) (A : Set (List Γ)) : Prop

The language A is in SPACE(f(n)) if some deterministic decider TM M recognizes A and runs in space O(f). Corresponds to Sipser's SPACE(f(n)).

structure SpaceComplexity.NTM (Q Γ : Type) : Type

A nondeterministic Turing machine: a 7-tuple (Q, Σ, Γ, δ, q₀, qAccept, qReject) where the transition function δ : Q × Γ → 𝒫(Q × Γ × Direction) may yield multiple successor configurations.

• blank : Γ
• inputAlpha : Set Γ
• blank_not_in_inputAlpha : self.blank ∉ self.inputAlpha
• δ : Q → Γ → Set (Q × Γ × TuringMachine.Direction)
• q₀ : Q
• qAccept : Q
• qReject : Q
• qReject_ne_qAccept : self.qReject ≠ self.qAccept

def SpaceComplexity.NTM.initConfig {Q Γ : Type} (M : NTM Q Γ) (w : List Γ) : TuringMachine.Config Q Γ

Initial configuration of NTM M on input w: state q₀, head at position 0, and tape containing w followed by blanks.

def SpaceComplexity.NTM.isAcceptConfig {Q Γ : Type} (M : NTM Q Γ) (c : TuringMachine.Config Q Γ) : Prop

A configuration is accepting if its state equals qAccept.

def SpaceComplexity.NTM.isRejectConfig {Q Γ : Type} (M : NTM Q Γ) (c : TuringMachine.Config Q Γ) : Prop

A configuration is rejecting if its state equals qReject.

def SpaceComplexity.NTM.isHaltConfig {Q Γ : Type} (M : NTM Q Γ) (c : TuringMachine.Config Q Γ) : Prop

A configuration is halting if it is either accepting or rejecting.

def SpaceComplexity.NTM.step {Q Γ : Type} (M : NTM Q Γ) (c₁ c₂ : TuringMachine.Config Q Γ) : Prop

Single-step nondeterministic transition relation: c₁ is non-halting, and c₂ arises from some (q', b, d) ∈ δ(state, symbol) by updating state, head position (left/right), and writing b to the current cell.

def SpaceComplexity.NTM.IsValidBranch {Q Γ : Type} (M : NTM Q Γ) (w : List Γ) (branch : ℕ → TuringMachine.Config Q Γ) : Prop

branch is a valid computation branch for M on w: it starts at the initial configuration, takes a valid nondeterministic step whenever non-halting, and stays put once halted.

noncomputable def SpaceComplexity.NTMBranchSpaceUsed {Q Γ : Type} (branch : ℕ → TuringMachine.Config Q Γ) (n : ℕ) : ℕ

Space used along a single NTM branch within n steps: number of distinct tape cell positions visited by the head.

def SpaceComplexity.NTM.RunsInSpace {Q Γ : Type} (M : NTM Q Γ) (f : ℕ → ℕ) : Prop

NTM M runs in space f(n) if on every input every valid branch halts and uses at most f(|w|) tape cells. This is Sipser's definition for NSPACE complexity.

def SpaceComplexity.NTM.accepts {Q Γ : Type} (M : NTM Q Γ) (w : List Γ) : Prop

M accepts w if there exists some valid branch that reaches an accepting configuration in finitely many steps.

def SpaceComplexity.NTM.language {Q Γ : Type} (M : NTM Q Γ) : Set (List Γ)

The language of NTM M: all strings over inputAlpha that are accepted.

def SpaceComplexity.InNSPACE {Γ : Type} (f : ℕ → ℕ) (A : Set (List Γ)) : Prop

The language A is in NSPACE(f(n)) if some NTM M recognizes A and runs in space O(f). Corresponds to Sipser's NSPACE(f(n)).

theorem SpaceComplexity.nspace_of_infinite_state_ntm {Γ : Type} [DecidableEq Γ] {Q : Type} [DecidableEq Q] (M : NTM Q Γ) (A : Set (List Γ)) (f : ℕ → ℕ) (hA : M.language = A) (hSpace : ∃ (g : ℕ → ℕ), IsAsympBoundedBy g f ∧ M.RunsInSpace g) : InNSPACE f A

A technical lifting lemma: even if the NTM M does not a priori have a finite state type, we can still witness InNSPACE f A. (Placeholder; the proof is deferred.)

def SpaceComplexity.InPSPACE {Γ : Type} (A : Set (List Γ)) : Prop

A ∈ PSPACE iff A ∈ SPACE(n^k) for some k.

def SpaceComplexity.InNPSPACE {Γ : Type} (A : Set (List Γ)) : Prop

A ∈ NPSPACE iff A ∈ NSPACE(n^k) for some k. By Savitch's theorem NPSPACE = PSPACE.

def SpaceComplexity.IsPSPACEComplete {Γ : Type} (B : Set (List Γ)) : Prop

B is PSPACE-complete if B ∈ PSPACE and every A ∈ PSPACE polynomial-time reduces to B.

def SpaceComplexity.DifferInOneSymbol {α : Type u_1} (x y : List α) : Prop

Two equal-length strings x and y differ in exactly one symbol: there is a unique position i where they disagree, and they agree elsewhere.

def SpaceComplexity.IsLadder {α : Type u_1} (seq : List (List α)) : Prop

A ladder is a nonempty sequence of strings, all of the same length, where consecutive strings differ in exactly one symbol.

def SpaceComplexity.IsLadderIn {α : Type u_1} (L : Language α) (seq : List (List α)) : Prop

A ladder in language L is a ladder whose every entry belongs to L.

def SpaceComplexity.LADDER_DFA {α : Type u_1} {σ : Type u_2} [Fintype σ] [Fintype α] (B : DFA α σ) (u v : List α) : Prop

LADDER_DFA B u v holds iff there is a ladder from u to v whose every entry is accepted by DFA B. This is the language LADDER_DFA from Sipser, used as an example of a problem in NSPACE(n) hence in PSPACE.

theorem SpaceComplexity.step_halted {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) (hc : M.isHaltConfig c) : M.step c = c

A halting configuration is a fixed point of the TM step function.

theorem SpaceComplexity.run_halted {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) (k : ℕ) (hk : M.isHaltConfig (M.run c k)) (m : ℕ) : k ≤ m → M.run c m = M.run c k

Once a TM run reaches a halting configuration at step k, all subsequent steps remain in that same halting configuration.

theorem SpaceComplexity.tmSpaceUsed_le_steps {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (w : List Γ) (n : ℕ) : TMSpaceUsed M w n ≤ n + 1

A TM running for n steps cannot use more than n + 1 tape cells (it visits at most one new cell per step, plus the starting cell).

theorem SpaceComplexity.tmSpaceUsed_halted_eq {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (w : List Γ) (k n : ℕ) (hk : M.isHaltConfig (M.runOnInput w k)) (hkn : k ≤ n) : TMSpaceUsed M w n = TMSpaceUsed M w k

After the machine has halted at step k, the space used does not grow with additional steps n ≥ k.

theorem SpaceComplexity.TIME_subset_SPACE {Γ : Type} (t : ℕ → ℕ) (A : Set (List Γ)) (ht : ∀ (n : ℕ), n ≤ t n) : TuringMachine.InTIME t A → InSPACE t A

Time–Space relationship (1/2) (Sipser, Theorem 8.5): for t(n) ≥ n, TIME(t(n)) ⊆ SPACE(t(n)). A TM that runs in time t cannot use more than t + 1 cells of tape.

theorem SpaceComplexity.P_subset_PSPACE {Γ : Type} (A : Set (List Γ)) : TuringMachine.InP A → InPSPACE A

Corollary (Sipser): P ⊆ PSPACE. Any language decidable in polynomial time is decidable in polynomial space.

theorem SpaceComplexity.run_periodic_of_config_repeat {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c₀ : TuringMachine.Config Q Γ) (i j : ℕ) (_hij : i < j) (hrepeat : M.run c₀ i = M.run c₀ j) (k : ℕ) : M.run c₀ (i + k) = M.run c₀ (j + k)

If a TM returns to the same configuration at two distinct steps i < j, then its computation is periodic with period j - i from step i onward.

theorem SpaceComplexity.not_halts_of_config_repeat {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (w : List Γ) (i j : ℕ) (hij : i < j) (hrepeat : M.runOnInput w i = M.runOnInput w j) (hNotHalt : ¬M.isHaltConfig (M.runOnInput w i)) : ¬M.halts w

If a TM enters a non-halting configuration repetition (same config at distinct steps i < j), then it loops forever and never halts.

theorem SpaceComplexity.tape_unchanged_at_unvisited {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c₀ : TuringMachine.Config Q Γ) (n : ℕ) (p : ℤ) (hp : ∀ k ≤ n, (M.run c₀ k).headPos ≠ p) : (M.run c₀ n).tape p = c₀.tape p

A tape cell p that the head has never visited during the first n steps still contains its original symbol.

theorem SpaceComplexity.configs_eq_of_encode_eq {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c₀ : TuringMachine.Config Q Γ) (i j N : ℕ) (hiN : i ≤ N) (hjN : j ≤ N) (S : Finset ℤ) (hS : ∀ k ≤ N, (M.run c₀ k).headPos ∈ S) (hstate : (M.run c₀ i).state = (M.run c₀ j).state) (hhead : (M.run c₀ i).headPos = (M.run c₀ j).headPos) (htape : ∀ p ∈ S, (M.run c₀ i).tape p = (M.run c₀ j).tape p) : M.run c₀ i = M.run c₀ j

Two configurations at steps i and j are equal whenever they agree on state, head position, and tape contents at every cell in the visited region S. (Outside S the tape contents agree because no cell was ever visited.)

theorem SpaceComplexity.SPACE_subset_TIME_exp {Γ : Type} [Fintype Γ] (t : ℕ → ℕ) (A : Set (List Γ)) (ht : ∀ (n : ℕ), n ≤ t n) : InSPACE t A → ∃ (c : ℕ), TuringMachine.InTIME (fun (n : ℕ) => c ^ t n) A

Time–Space relationship (2/2) (Sipser, Theorem 8.5): for t(n) ≥ n, SPACE(t(n)) ⊆ ⋃_c TIME(c^{t(n)}) = TIME(2^{O(t(n))}). The bound comes from the fact that there are at most |Q| · t(n) · |Γ|^{t(n)} distinct configurations of a TM using t(n) cells, so any halting machine must halt within that many steps.

theorem SpaceComplexity.TIME_SPACE_relationship {Γ : Type} [Fintype Γ] (t : ℕ → ℕ) (A : Set (List Γ)) (ht : ∀ (n : ℕ), n ≤ t n) : (TuringMachine.InTIME t A → InSPACE t A) ∧ (InSPACE t A → ∃ (c : ℕ), TuringMachine.InTIME (fun (n : ℕ) => c ^ t n) A)

Theorem (Time–Space relationships, Sipser Theorem 8.5). For t(n) ≥ n:

1. TIME(t(n)) ⊆ SPACE(t(n)), and
2. SPACE(t(n)) ⊆ ⋃_c TIME(c^{t(n)}) = TIME(2^{O(t(n))}).

theorem SpaceComplexity.NTIME_subset_SPACE {Γ : Type} (t : ℕ → ℕ) (A : Set (List Γ)) (ht : ∀ (n : ℕ), n ≤ t n) : TuringMachine.InNTIME t A → InSPACE t A

NTIME(t(n)) ⊆ SPACE(t(n)) (Sipser): a nondeterministic machine running in time t can be simulated by a deterministic machine using space t. (Placeholder; proof deferred.)

inductive SpaceComplexity.QBF : Type

Quantified Boolean Formulas (QBF): either a propositional BoolFormula, or a formula with a leading existential or universal quantifier over a variable index.

• body : NPCompleteness.BoolFormula → QBF
• exists_ : ℕ → QBF → QBF
• forall_ : ℕ → QBF → QBF

def SpaceComplexity.QBF.freeVars : QBF → Finset ℕ

The free (unquantified) variables of a QBF: the variables of the body that are not captured by any enclosing ∃ or ∀.

def SpaceComplexity.QBF.IsFullyQuantified (ψ : QBF) : Prop

A QBF is fully quantified (a sentence) when it has no free variables.

def SpaceComplexity.QBF.eval (σ : NPCompleteness.BoolAssignment) : QBF → Bool

Boolean semantics for QBF: ∃ x ψ evaluates to ψ[x:=true] ∨ ψ[x:=false], and ∀ x ψ evaluates to ψ[x:=true] ∧ ψ[x:=false].

def SpaceComplexity.QBF.IsTrue (ψ : QBF) : Prop

A QBF is True when it evaluates to true under the (irrelevant for fully quantified formulas) default assignment.

def SpaceComplexity.TQBF : Set QBF

The language TQBF = {ψ | ψ is a fully-quantified Boolean formula that is true}. TQBF is the canonical PSPACE-complete problem.

theorem SpaceComplexity.IsBigO_of_le_eventually {f g₁ g₂ : ℕ → ℕ} (hf : TuringMachine.IsBigO f g₁) (hle : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → g₁ n ≤ g₂ n) : TuringMachine.IsBigO f g₂

Monotonicity of O(·): if f is O(g₁) and eventually g₁ ≤ g₂, then f is also O(g₂).

theorem SpaceComplexity.InNTIME_mono {Γ : Type} {t₁ t₂ : ℕ → ℕ} {A : Set (List Γ)} (hle : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → t₁ n ≤ t₂ n) (h : TuringMachine.InNTIME t₁ A) : TuringMachine.InNTIME t₂ A

Monotonicity of NTIME: enlarging the time bound (eventually) preserves membership.

theorem SpaceComplexity.le_pow_of_pos {k : ℕ} (hk : 1 ≤ k) (n : ℕ) : n ≤ n ^ k

For k ≥ 1, n ≤ n^k.

theorem SpaceComplexity.NP_subset_PSPACE {Γ : Type} (A : Set (List Γ)) : TuringMachine.InNP A → InPSPACE A

NP ⊆ PSPACE (Sipser, Lecture 17). Every NP language is in PSPACE: combine NP ⊆ NTIME(n^k) with NTIME ⊆ SPACE.

def SpaceComplexity.QBF.ExistsPlayerWins (σ : NPCompleteness.BoolAssignment) : QBF → Prop

The "formula game" semantics of a QBF: the existential player wins on ψ from assignment σ iff at each ∃ x she can pick a value of x, and at each ∀ x she wins for both values of x, ultimately making the body true.

theorem SpaceComplexity.QBF.existsPlayerWins_iff_eval (σ : NPCompleteness.BoolAssignment) (ψ : QBF) : ExistsPlayerWins σ ψ ↔ eval σ ψ = true

Formula Game ↔ QBF evaluation: the existential player wins on ψ from σ exactly when ψ.eval σ = true.

theorem SpaceComplexity.QBF.existsPlayerWins_iff_isTrue (ψ : QBF) : ExistsPlayerWins (fun (x : ℕ) => false) ψ ↔ ψ.IsTrue

Specialization of existsPlayerWins_iff_eval to the default assignment: the existential player wins on ψ iff ψ is true.

theorem SpaceComplexity.formulaGameLanguage_eq_TQBF : {ψ : QBF | ψ.IsFullyQuantified ∧ QBF.ExistsPlayerWins (fun (x : ℕ) => false) ψ} = TQBF

Claim (Sipser, Lecture 19): the language {⟨ψ⟩ | the ∃-player has a forced win on ψ} equals TQBF.

def SpaceComplexity.NTM.CanYield {Q Γ : Type} (M : NTM Q Γ) (c₁ c₂ : TuringMachine.Config Q Γ) : ℕ → Prop

Reachability in at most b steps (used in Savitch's theorem proof): c₁ can yield c₂ in at most b nondeterministic steps.

theorem SpaceComplexity.NTM.canYield_zero {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) (c₁ c₂ : TuringMachine.Config Q Γ) : M.CanYield c₁ c₂ 0 ↔ c₁ = c₂

CanYield c₁ c₂ 0 is exactly c₁ = c₂.

theorem SpaceComplexity.NTM.canYield_succ {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) (c₁ c₂ : TuringMachine.Config Q Γ) (b : ℕ) : M.CanYield c₁ c₂ b → M.CanYield c₁ c₂ (b + 1)

CanYield is monotone in the step budget: enlarging the budget by one preserves reachability.

theorem SpaceComplexity.NTM.canYield_of_le {Q Γ : Type} [DecidableEq Q] (M : NTM Q Γ) (c₁ c₂ : TuringMachine.Config Q Γ) (b b' : ℕ) (hle : b ≤ b') (h : M.CanYield c₁ c₂ b) : M.CanYield c₁ c₂ b'

General monotonicity: if b ≤ b', then CanYield … b implies CanYield … b'.

theorem SpaceComplexity.can_yield_dtm {Γ Q : Type} [Fintype Q] [DecidableEq Q] (N : NTM Q Γ) (g : ℕ → ℕ) (hSpace : N.RunsInSpace g) : ∃ (Q' : Type) (x : Fintype Q') (x : DecidableEq Q') (M : TuringMachine.TM Q' Γ), M.language = N.language ∧ M.isDecider ∧ ∀ (w : List Γ) (n : ℕ), M.isHaltConfig (M.runOnInput w n) → TMSpaceUsed M w n ≤ g w.length ^ 2

Core of Savitch's theorem (Sipser, Theorem 8.5): given an NTM N running in space g, construct a deterministic TM M recognizing the same language that decides membership using space O(g²) via the recursive CANYIELD procedure. (Placeholder.)

theorem SpaceComplexity.dtm_of_nspace_bounded {Γ Q : Type} [Fintype Q] [DecidableEq Q] (N : NTM Q Γ) (g : ℕ → ℕ) (hSpace : N.RunsInSpace g) (hLang : ∀ w ∈ N.language, ∀ s ∈ w, s ∈ N.inputAlpha) : ∃ (Q' : Type) (x : Fintype Q') (x : DecidableEq Q') (M : TuringMachine.TM Q' Γ), M.language = N.language ∧ ∃ (g' : ℕ → ℕ), (∀ (n : ℕ), g' n ≤ g n ^ 2) ∧ TMRunsInSpace M g'

Packaging of can_yield_dtm: from an NTM in space g we obtain a DTM in space g² that decides the same language.

theorem SpaceComplexity.savitch {Γ : Type} (f : ℕ → ℕ) (hf : ∀ (n : ℕ), n ≤ f n) (A : Set (List Γ)) (hA : InNSPACE f A) : InSPACE (fun (n : ℕ) => f n ^ 2) A

Savitch's Theorem (Sipser, Theorem 8.5): for f(n) ≥ n, NSPACE(f(n)) ⊆ SPACE(f(n)²). Every nondeterministic computation in space f can be simulated deterministically in space f².

theorem SpaceComplexity.npspace_subset_pspace {Γ : Type} (A : Set (List Γ)) : InNPSPACE A → InPSPACE A

Corollary of Savitch's Theorem: NPSPACE = PSPACE. Polynomial nondeterministic space coincides with polynomial deterministic space.

structure SpaceComplexity.QBFEncoding (Γ : Type) [Inhabited Γ] : Type

An encoding of QBFs as strings over alphabet Γ: an injective encoder/decoder pair that uses non-blank symbols, with the standard round-trip laws.

• encode : QBF → List Γ
• decode : List Γ → Option QBF
• encode_injective : Function.Injective self.encode
• decode_encode (ψ : QBF) : self.decode (self.encode ψ) = some ψ
• blank_free (ψ : QBF) : default ∉ self.encode ψ
• encode_decode (l : List Γ) (ψ : QBF) : self.decode l = some ψ → self.encode ψ = l

def SpaceComplexity.tqbfLanguage {Γ : Type} [Inhabited Γ] (enc : QBFEncoding Γ) : Set (List Γ)

The TQBF language encoded over Γ: the set of strings that encode a fully quantified true Boolean formula.

def SpaceComplexity.TQBFState (Γ : Type) : Type

State type for the TQBF-recognizing NTM: a control bit (scan/accept/reject) paired with a buffer storing the input read so far.

@[implicit_reducible]

instance SpaceComplexity.instDecidableEqTQBFState (Γ : Type) [DecidableEq Γ] : DecidableEq (TQBFState Γ)

Decidable equality on TQBFState Γ, inherited from Fin 3 × List Γ.

noncomputable def SpaceComplexity.tqbfNTM {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) : NTM (TQBFState Γ) Γ

A (degenerate) NTM that reads its input into a buffer, decodes it as a QBF, and accepts iff the QBF is fully quantified and true. Used as a witness that tqbfLanguage ∈ NSPACE(n).

theorem SpaceComplexity.tqbfNTM_language {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) : (tqbfNTM enc).language = tqbfLanguage enc

The NTM tqbfNTM enc recognizes exactly the encoded TQBF language.

theorem SpaceComplexity.tqbfNTM_runs_in_linear_space {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) : ∃ (g : ℕ → ℕ), IsAsympBoundedBy g id ∧ (tqbfNTM enc).RunsInSpace g

The TQBF-recognizing NTM runs in linear space O(n): it only sweeps over the input once. Combined with tqbfNTM_language this places TQBF in NSPACE(n).

theorem SpaceComplexity.tqbf_in_pspace {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) : InPSPACE (tqbfLanguage enc)

TQBF ∈ PSPACE (Sipser, Lecture 17). Since TQBF is in NSPACE(n) and NPSPACE = PSPACE by Savitch, TQBF lies in PSPACE.

def SpaceComplexity.tqbfConfigSize {Q Γ : Type} (_M : TuringMachine.TM Q Γ) (w : List Γ) (spacebound : ℕ) : ℕ

Number of bits needed to encode a configuration of a spacebound-space TM running on input w: state + tape contents + head position.

def SpaceComplexity.tqbfNumLevels (spacebound : ℕ) : ℕ

Number of recursion levels in the TQBF reduction: one level per bit of space.

def SpaceComplexity.tqbfBaseBody : ℕ → NPCompleteness.BoolFormula

A trivial conjunction x_{n-1} ∧ x_{n-2} ∧ … ∧ x_0 ∧ True used as a placeholder body when building the TQBF formula.

theorem SpaceComplexity.tqbfBaseBody_vars (n : ℕ) : (tqbfBaseBody n).vars = Finset.range n

The variables of tqbfBaseBody n are exactly {0, 1, …, n-1}.

def SpaceComplexity.quantifyHalving (q : QBF) (configSize : ℕ) : ℕ → QBF

Wraps q with n alternating quantifiers ∃ k. … ∀ k. … according to the divisibility pattern used in the halving construction for the PSPACE-completeness proof of TQBF.

theorem SpaceComplexity.freeVars_quantifyHalving (q : QBF) (configSize n : ℕ) : (quantifyHalving q configSize n).freeVars = q.freeVars \ Finset.range n

Quantifying q with quantifyHalving … n removes the variables 0, …, n-1 from the free-variable set.

noncomputable def SpaceComplexity.buildTQBFFormula {Q : Type} [DecidableEq Q] {Γ : Type} (M : TuringMachine.TM Q Γ) (w : List Γ) (spacebound : ℕ) : QBF

Given a TM M, input w, and a space bound, construct a QBF whose truth is equivalent to M accepting w in space spacebound. This is the Sipser construction underlying the reduction A ≤ₚ TQBF for the PSPACE-hardness of TQBF.

theorem SpaceComplexity.buildTQBFFormula_isFullyQuantified {Q : Type} [DecidableEq Q] {Γ : Type} (M : TuringMachine.TM Q Γ) (w : List Γ) (spacebound : ℕ) : (buildTQBFFormula M w spacebound).IsFullyQuantified

The constructed QBF buildTQBFFormula M w spacebound is a sentence: every variable is quantified.

theorem SpaceComplexity.buildTQBFFormula_correct {Q : Type} [DecidableEq Q] {Γ : Type} (M : TuringMachine.TM Q Γ) (w : List Γ) (spacebound : ℕ) (hSpace : ∀ (n : ℕ), M.isHaltConfig (M.runOnInput w n) → TMSpaceUsed M w n ≤ spacebound) : (buildTQBFFormula M w spacebound).IsTrue ↔ M.accepts w

Correctness of the TQBF reduction: the QBF buildTQBFFormula M w spacebound is true iff M accepts w, under the assumption that M halts within spacebound tape cells. (Placeholder.)

noncomputable def SpaceComplexity.tqbfReductionFn {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (enc : QBFEncoding Γ) {Q : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (g : ℕ → ℕ) : List Γ → List Γ

The reduction function w ↦ ⟨φ_{M,w}⟩ mapping inputs of a PSPACE machine M to encoded QBFs.

theorem SpaceComplexity.buildTQBFFormula_computableInPolyTime {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) {Q : Type} [Fintype Q] [DecidableEq Q] (M : TuringMachine.TM Q Γ) (k : ℕ) (g : ℕ → ℕ) (hAsymp : IsAsympBoundedBy g fun (n : ℕ) => n ^ k) (hSpace : TMRunsInSpace M g) : TuringMachine.IsPolyTimeComputableFunction fun (w : List Γ) => enc.encode (buildTQBFFormula M w (g w.length))

The TQBF reduction function is polynomial-time computable when M runs in polynomial space. This is the key efficiency lemma for PSPACE-hardness of TQBF.

theorem SpaceComplexity.tqbfReductionFn_polyTime {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) {Q : Type} [Fintype Q] [DecidableEq Q] (M : TuringMachine.TM Q Γ) (k : ℕ) (g : ℕ → ℕ) (hAsymp : IsAsympBoundedBy g fun (n : ℕ) => n ^ k) (hSpace : TMRunsInSpace M g) : TuringMachine.IsPolyTimeComputableFunction (tqbfReductionFn enc M g)

Restatement: tqbfReductionFn enc M g is polynomial-time computable.

theorem SpaceComplexity.tqbf_pspace_hard {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) (A : Set (List Γ)) (hA : InPSPACE A) : TuringMachine.PolyReducible A (tqbfLanguage enc)

TQBF is PSPACE-hard (Sipser, Theorem 8.9): every PSPACE language polynomial-time reduces to TQBF via the construction w ↦ ⟨φ_{M,w}⟩.

theorem SpaceComplexity.tqbf_pspace_complete {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : QBFEncoding Γ) : IsPSPACEComplete (tqbfLanguage enc)

Theorem (TQBF is PSPACE-complete) (Sipser, Theorem 8.9). TQBF is in PSPACE and every PSPACE language reduces to it in polynomial time.

structure SpaceComplexity.GGEncoding (Γ : Type) [Inhabited Γ] : Type 1

An encoding of Generalized Geography instances (G, a) (a digraph with a starting node) as strings over alphabet Γ.

• V : Type
• decEqV : DecidableEq self.V
• encode : Digraph self.V × self.V → List Γ
• decode : List Γ → Option (Digraph self.V × self.V)
• encode_injective : Function.Injective self.encode
• decode_encode (p : Digraph self.V × self.V) : self.decode (self.encode p) = some p
• blank_free (p : Digraph self.V × self.V) : default ∉ self.encode p
• encode_decode (l : List Γ) (p : Digraph self.V × self.V) : self.decode l = some p → self.encode p = l
• fintypeV : Fintype self.V
• nonemptyV : Nonempty self.V

def SpaceComplexity.ggLanguage {Γ : Type} [Inhabited Γ] (enc : GGEncoding Γ) : Set (List Γ)

The Generalized Geography language GG = {⟨G, a⟩ | Player I has a forced win on G starting at a}, encoded over Γ.

def SpaceComplexity.GGState (Γ : Type) : Type

State type for the GG-recognizing NTM: a control bit plus a buffer holding the input read so far.

@[implicit_reducible]

instance SpaceComplexity.ggStateDecEq (Γ : Type) [DecidableEq Γ] : DecidableEq (GGState Γ)

Decidable equality on GGState Γ, inherited from Fin 3 × List Γ.

noncomputable def SpaceComplexity.ggNTM {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : GGEncoding Γ) : NTM (GGState Γ) Γ

The GG-recognizing NTM: scans the input, decodes it as a digraph (G, a), and accepts iff Player I has a forced win in Generalized Geography on G from a.

theorem SpaceComplexity.ggNTM_language {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : GGEncoding Γ) : (ggNTM enc).language = ggLanguage enc

The NTM ggNTM enc recognizes exactly the encoded GG language.

theorem SpaceComplexity.ggNTM_runs_in_linear_space {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : GGEncoding Γ) : ∃ (g : ℕ → ℕ), IsAsympBoundedBy g id ∧ (ggNTM enc).RunsInSpace g

The GG-recognizing NTM runs in linear space (just stores its input). (Placeholder.)

theorem SpaceComplexity.gg_in_pspace {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : GGEncoding Γ) : InPSPACE (ggLanguage enc)

GG ∈ PSPACE (Sipser, Lecture 19). Generalized Geography is in PSPACE, by the NSPACE(n) recognizer combined with Savitch.

noncomputable def SpaceComplexity.buildFormulaGameGraph {Γ : Type} [Inhabited Γ] (genc : GGEncoding Γ) (ψ : QBF) : Digraph genc.V × genc.V

The Sipser TQBF→GG reduction: build a Generalized Geography instance whose Player-I forced wins correspond exactly to truth of the QBF ψ. (Uses choice to witness the existence of an appropriate digraph.)

theorem SpaceComplexity.buildFormulaGameGraph_correct {Γ : Type} [Inhabited Γ] (genc : GGEncoding Γ) (ψ : QBF) : GeographyGame.GG (buildFormulaGameGraph genc ψ).1 (buildFormulaGameGraph genc ψ).2 ↔ ψ.IsFullyQuantified ∧ ψ.IsTrue

Correctness of the TQBF→GG reduction: Player I has a forced win on the constructed graph iff ψ is a true sentence. (Placeholder.)

noncomputable def SpaceComplexity.ggReductionFn {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (qenc : QBFEncoding Γ) (genc : GGEncoding Γ) : List Γ → List Γ

The string-level reduction from encoded QBFs to encoded GG instances.

theorem SpaceComplexity.ggReductionFn_polyTime {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (qenc : QBFEncoding Γ) (genc : GGEncoding Γ) : TuringMachine.IsPolyTimeComputableFunction (ggReductionFn qenc genc)

The TQBF→GG reduction function is polynomial-time computable. (Placeholder.)

theorem SpaceComplexity.ggEncoding_encode_nonempty {Γ : Type} [Inhabited Γ] (genc : GGEncoding Γ) (p : Digraph genc.V × genc.V) : genc.encode p ≠ []

A GG encoding always produces a nonempty string. (Placeholder.)

theorem SpaceComplexity.ggReductionFn_correct {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (qenc : QBFEncoding Γ) (genc : GGEncoding Γ) (w : List Γ) : w ∈ tqbfLanguage qenc ↔ ggReductionFn qenc genc w ∈ ggLanguage genc

The TQBF→GG reduction is correct on the language level: w ∈ TQBF ↔ f(w) ∈ GG.

theorem SpaceComplexity.tqbf_reduces_to_gg {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (qenc : QBFEncoding Γ) (genc : GGEncoding Γ) : TuringMachine.PolyReducible (tqbfLanguage qenc) (ggLanguage genc)

TQBF ≤ₚ GG: TQBF polynomial-time reduces to Generalized Geography.

theorem SpaceComplexity.gg_pspace_hard {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (qenc : QBFEncoding Γ) (genc : GGEncoding Γ) (A : Set (List Γ)) (hA : InPSPACE A) : TuringMachine.PolyReducible A (ggLanguage genc)

GG is PSPACE-hard (Sipser, Lecture 19). Every PSPACE language reduces to GG via TQBF.

theorem SpaceComplexity.gg_pspace_complete {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (qenc : QBFEncoding Γ) (genc : GGEncoding Γ) : IsPSPACEComplete (ggLanguage genc)

Theorem (GG is PSPACE-complete) (Sipser, Lecture 19). Generalized Geography is in PSPACE and is PSPACE-hard.