def HierarchyTheorems.IsTimeConstructible (f : ℕ → ℕ) : Prop

A function f : ℕ → ℕ is time constructible if there exists a Turing machine M which is a decider, runs in some time t', with t' = O(f). This is the standard hypothesis under which the Time Hierarchy Theorem is stated.

def HierarchyTheorems.IsLittleO (g f : ℕ → ℕ) : Prop

IsLittleO g f says g(n) = o(f(n)): for every positive constant c, there is some n₀ such that c · g(n) < f(n) for all n ≥ n₀.

theorem HierarchyTheorems.IsLittleO.isBigO {g f : ℕ → ℕ} (h : IsLittleO g f) : TuringMachine.IsBigO g f

Little-o implies big-O: if g = o(f) then g = O(f).

theorem TuringMachine.isBigO_div_log (f : ℕ → ℕ) : IsBigO (fun (n : ℕ) => f n / Nat.log 2 (f n)) f

For any f : ℕ → ℕ, the function n ↦ f(n) / log₂(f(n)) is O(f). This is the ratio that appears in the Time Hierarchy Theorem's lower bound TIME(o(f(n)/log(f(n)))) ⊊ TIME(f(n)).

theorem universal_simulation_overhead {Γ : Type} (f : ℕ → ℕ) (hf : HierarchyTheorems.IsTimeConstructible f) : ∃ (QS : Type) (x : Fintype QS) (x : DecidableEq QS) (enc : (Q' : Type) → [DecidableEq Q'] → TuringMachine.TM Q' Γ → List Γ) (sim : TuringMachine.TM QS Γ) (tSim : ℕ → ℕ), sim.isDecider ∧ sim.runsInTime tSim ∧ TuringMachine.IsBigO tSim f ∧ ∀ (Q' : Type) [inst : DecidableEq Q'] (M : TuringMachine.TM Q' Γ) (s : ℕ → ℕ), M.isDecider → M.runsInTime s → (TuringMachine.IsBigO s fun (n : ℕ) => f n / Nat.log 2 (f n)) → (enc Q' M ∈ sim.language ↔ enc Q' M ∈ M.language)

Universal simulation with logarithmic overhead. Given a time-constructible bound f, there is a single universal simulator TM sim that runs in time O(f) and correctly decides membership in M.language for every decider M whose running time s satisfies s = O(f(n)/log(f(n))). This is the key ingredient powering the Time Hierarchy Theorem: the log factor accounts for the overhead of simulating an arbitrary machine M on a fixed universal machine.

theorem TM.run_add {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) (n m : ℕ) : M.run c (n + m) = M.run (M.run c n) m

Running a deterministic TM for n + m steps is the same as running it for n steps and then m more steps from the resulting configuration.

theorem tm_swap_step_eq {Q Γ : Type} [DecidableEq Q] (sim : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) : have D := { blank := sim.blank, inputAlpha := sim.inputAlpha, blank_not_in_inputAlpha := ⋯, δ := sim.δ, q₀ := sim.q₀, qAccept := sim.qReject, qReject := sim.qAccept, qReject_ne_qAccept := ⋯ }; D.step c = sim.step c

Swapping the accept and reject states of a TM does not change how the next configuration is computed (the step function only consults δ, not the accept/reject labels). Used to build the diagonalizer machine which complements the language of the universal simulator.

theorem tm_swap_run_eq {Q Γ : Type} [DecidableEq Q] (sim : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) (n : ℕ) : have D := { blank := sim.blank, inputAlpha := sim.inputAlpha, blank_not_in_inputAlpha := ⋯, δ := sim.δ, q₀ := sim.q₀, qAccept := sim.qReject, qReject := sim.qAccept, qReject_ne_qAccept := ⋯ }; D.run c n = sim.run c n

Iterated version of tm_swap_step_eq: swapping the accept/reject states of a TM leaves every n-step run identical to that of the original machine.

theorem time_diagonalizer_exists {Γ : Type} (f : ℕ → ℕ) (hf : HierarchyTheorems.IsTimeConstructible f) : ∃ (Q : Type) (x : Fintype Q) (x : DecidableEq Q) (D : TuringMachine.TM Q Γ), (D.decides D.language ∧ ∃ (t' : ℕ → ℕ), D.runsInTime t' ∧ TuringMachine.IsBigO t' f) ∧ ∀ (Q' : Type) (x_1 : DecidableEq Q') (M : TuringMachine.TM Q' Γ) (t' : ℕ → ℕ), M.decides M.language → M.runsInTime t' → (TuringMachine.IsBigO t' fun (n : ℕ) => f n / Nat.log 2 (f n)) → D.language ≠ M.language

Existence of a time-diagonalizer. From a time-constructible bound f we construct a decider D running in time O(f) whose language differs from the language of every decider M running in time O(f(n)/log(f(n))). D is built by swapping accept/reject on the universal simulator from universal_simulation_overhead, so that it accepts exactly the encodings rejected by the simulator — a Cantor-style diagonalization within TIME(f).

theorem time_hierarchy_theorem (f : ℕ → ℕ) (hf : HierarchyTheorems.IsTimeConstructible f) : ∃ (Γ : Type) (A : Set (List Γ)), TuringMachine.InTIME f A ∧ ∀ (g : ℕ → ℕ), (HierarchyTheorems.IsLittleO g fun (n : ℕ) => f n / Nat.log 2 (f n)) → ¬TuringMachine.InTIME g A

Time Hierarchy Theorem. For any time-constructible f, there is a language A which is decidable in TIME(f(n)) but is not decidable in TIME(g(n)) for any g = o(f(n)/log(f(n))). Equivalently, TIME(o(f(n)/log(f(n)))) ⊊ TIME(f(n)). Proved by diagonalizing against all faster machines using time_diagonalizer_exists.

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

IsAsympDominated g f is the little-o relation on ℕ → ℕ: for every constant c > 0 there exists n₀ such that c · g(n) < f(n) for all n ≥ n₀. Used to express g = o(f) in the Space Hierarchy Theorem.

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

InSPACEo f A says the language A is decidable in space o(f(n)): some TM recognizes A and runs in space g with g = o(f). This is the class SPACE(o(f(n))) appearing in the Space Hierarchy Theorem.

def SpaceComplexity.SpaceConstructible (f : ℕ → ℕ) : Prop

A function f : ℕ → ℕ is space constructible if there is a TM decider M whose space usage on every input of length n equals f(n) exactly once it halts. This is the standard hypothesis for the Space Hierarchy Theorem.

structure SpaceComplexity.TMDesc (Γ : Type) : Type

A TM description packages a Turing machine over alphabet Γ together with its number of states. The state type Fin (numStates + 3) reserves three states (start, accept, reject) on top of the working states, providing a uniform shape for enumeration in the diagonalization construction.

• numStates : ℕ
• machine : TuringMachine.TM (Fin (self.numStates + 3)) Γ

def SpaceComplexity.diagLang {Γ : Type} (encode : TMDesc Γ → List Γ) : Set (List Γ)

The diagonal language with respect to an encoding encode : TMDesc Γ → List Γ: the set of strings w such that whenever w encodes some machine description d, d.machine does not accept w. By Cantor-style diagonalization, this language differs from every machine's language on at least one encoding.

theorem SpaceComplexity.diagLang_iff {Γ : Type} {encode : TMDesc Γ → List Γ} (h_inj : Function.Injective encode) (d : TMDesc Γ) : encode d ∈ diagLang encode ↔ ¬d.machine.accepts (encode d)

Under an injective encoding, membership of encode d in the diagonal language is equivalent to d.machine not accepting its own encoding encode d.

theorem SpaceComplexity.diagLang_ne {Γ : Type} {encode : TMDesc Γ → List Γ} (h_inj : Function.Injective encode) (d : TMDesc Γ) : diagLang encode ≠ d.machine.language

The diagonal language differs from the language of every machine d.machine. This is the diagonalization core: on its own encoding encode d, the two languages must disagree (whether or not d.machine accepts encode d).

theorem SpaceComplexity.sim_overhead {Γ : Type} (f : ℕ → ℕ) (hf : SpaceConstructible f) : ∃ (encode : TMDesc Γ → List Γ) (_ : Function.Injective encode) (Q : Type) (x : Fintype Q) (x : DecidableEq Q) (D : TuringMachine.TM Q Γ), D.language = diagLang encode ∧ (∃ (g : ℕ → ℕ), IsAsympBoundedBy g f ∧ TMRunsInSpace D g) ∧ ∀ (Q' : Type) (x : DecidableEq Q') (M : TuringMachine.TM Q' Γ) (g : ℕ → ℕ), IsAsympDominated g f → TMRunsInSpace M g → ∃ (d : TMDesc Γ), d.machine.language = M.language

Space-bounded universal simulation. Given a space-constructible bound f, there exists an injective encoding of TM descriptions and a single decider D whose language is the diagonal language diagLang encode, runs in space O(f), and such that every TM M running in space o(f) is represented (up to language) by some description d. This is the space analogue of universal_simulation_overhead and the engine of the Space Hierarchy Theorem.

theorem SpaceComplexity.diagonalizer_exists {Γ : Type} (f : ℕ → ℕ) (hf : SpaceConstructible f) : ∃ (Q : Type) (x : Fintype Q) (x : DecidableEq Q) (D : TuringMachine.TM Q Γ), (∃ (g : ℕ → ℕ), IsAsympBoundedBy g f ∧ TMRunsInSpace D g) ∧ ∀ (Q' : Type) (x_1 : DecidableEq Q') (M : TuringMachine.TM Q' Γ) (g : ℕ → ℕ), IsAsympDominated g f → TMRunsInSpace M g → D.language ≠ M.language

Existence of a space-diagonalizer. From a space-constructible bound f we build a TM D that runs in space O(f) and whose language differs from the language of every TM M running in space g = o(f). Combines sim_overhead with diagLang_ne to produce the witness used in the Space Hierarchy Theorem.

theorem SpaceComplexity.space_hierarchy_theorem {Γ : Type} (f : ℕ → ℕ) (hf : SpaceConstructible f) : ∃ (A : Set (List Γ)), InSPACE f A ∧ ¬InSPACEo f A

Space Hierarchy Theorem. For any space-constructible f, there exists a language A decidable in SPACE(f(n)) but not in SPACE(o(f(n))). In other words, SPACE(o(f(n))) ⊊ SPACE(f(n)). Proved by exhibiting the diagonalizer machine from diagonalizer_exists.

structure OracleComputation.OracleTM (Q Γ : Type) : Type

A deterministic oracle Turing machine over state set Q and tape alphabet Γ. Beyond the usual TM data (blank symbol, input alphabet, transition δ, start state, accept/reject states), the machine has a distinguished query state qQuery and an oracle oracle ⊆ List Γ. The transition function takes an extra Bool reading the oracle's answer to the current query tape, so the machine can consult oracle membership in a single step.

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

structure OracleComputation.OracleConfig (Q Γ : Type) : Type

A configuration of an oracle TM: the current state, head position on the two-way infinite tape, the tape contents, and the contents of the auxiliary query tape which holds the string to be tested against the oracle.

• state : Q
• headPos : ℤ
• tape : ℤ → Γ
• queryTape : List Γ

noncomputable def OracleComputation.OracleTM.step {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) (c : OracleConfig Q Γ) : OracleConfig Q Γ

One computation step of a deterministic oracle TM. If the current state is qAccept or qReject, the configuration is left unchanged (halted). Otherwise the oracle answer is computed (as queryTape ∈ oracle when in qQuery, else false), δ is consulted, and the head, state, and tape are updated.

noncomputable def OracleComputation.OracleTM.run {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) (c : OracleConfig Q Γ) : ℕ → OracleConfig Q Γ

M.run c n applies M.step exactly n times starting from configuration c.

def OracleComputation.OracleTM.initConfig {Q Γ : Type} (M : OracleTM Q Γ) (w : List Γ) : OracleConfig Q Γ

The initial oracle TM configuration on input w: state is q₀, head at position 0, tape contains w on cells 0, …, w.length - 1 and blank elsewhere, and the query tape is empty.

noncomputable def OracleComputation.OracleTM.runOnInput {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) (w : List Γ) (n : ℕ) : OracleConfig Q Γ

Run M for n steps starting from its initial configuration on input w.

noncomputable def OracleComputation.OracleTM.accepts {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) (w : List Γ) : Prop

M.accepts w if some finite-step run of M on input w ends in qAccept.

noncomputable def OracleComputation.OracleTM.halts {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) (w : List Γ) : Prop

M.halts w if some finite-step run of M on w reaches qAccept or qReject.

noncomputable def OracleComputation.OracleTM.language {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) : Set (List Γ)

The language of an oracle TM M is the set of strings it accepts.

noncomputable def OracleComputation.OracleTM.isDecider {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) : Prop

An oracle TM M is a decider if it halts on every input.

noncomputable def OracleComputation.OracleTM.decides {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) (B : Set (List Γ)) : Prop

M.decides B means M is a decider and L(M) = B.

noncomputable def OracleComputation.OracleTM.runsInTime {Q Γ : Type} [DecidableEq Q] (M : OracleTM Q Γ) (t : ℕ → ℕ) : Prop

M.runsInTime t if on every input w, M reaches an accept or reject state within t(|w|) steps.

structure OracleComputation.OracleNTM (Q Γ : Type) : Type

A nondeterministic oracle Turing machine: like OracleTM but the transition function δ returns a set of possible next moves at each step. Used to define NP-with-oracle complexity classes.

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

noncomputable def OracleComputation.OracleNTM.step {Q Γ : Type} [DecidableEq Q] (M : OracleNTM Q Γ) (c₁ c₂ : OracleConfig Q Γ) : Prop

Single-step relation for an oracle NTM: M.step c₁ c₂ holds when c₂ is one of the configurations reachable from c₁ in one step (or c₂ = c₁ if c₁ is a halt configuration). Membership of queryTape in oracle is consulted whenever the state is qQuery.

def OracleComputation.OracleNTM.initConfig {Q Γ : Type} (M : OracleNTM Q Γ) (w : List Γ) : OracleConfig Q Γ

Initial configuration of an oracle NTM on input w (analogous to OracleTM.initConfig).

def OracleComputation.OracleNTM.isHaltConfig {Q Γ : Type} (M : OracleNTM Q Γ) (c : OracleConfig Q Γ) : Prop

A configuration is a halt configuration if its state is qAccept or qReject.

def OracleComputation.OracleNTM.isAcceptConfig {Q Γ : Type} (M : OracleNTM Q Γ) (c : OracleConfig Q Γ) : Prop

A configuration is an accept configuration if its state equals qAccept.

noncomputable def OracleComputation.OracleNTM.accepts {Q Γ : Type} [DecidableEq Q] (M : OracleNTM Q Γ) (w : List Γ) : Prop

M.accepts w if there exists some nondeterministic computation branch of M on w (a finite sequence of valid step-related configurations starting from M.initConfig w) ending in an accept configuration.

noncomputable def OracleComputation.OracleNTM.language {Q Γ : Type} [DecidableEq Q] (M : OracleNTM Q Γ) : Set (List Γ)

The language of an oracle NTM M is the set of strings it accepts.

noncomputable def OracleComputation.OracleNTM.isDecider {Q Γ : Type} [DecidableEq Q] (M : OracleNTM Q Γ) : Prop

An oracle NTM M is a decider if every nondeterministic branch from the initial configuration eventually reaches a halt configuration.

noncomputable def OracleComputation.OracleNTM.decides {Q Γ : Type} [DecidableEq Q] (M : OracleNTM Q Γ) (B : Set (List Γ)) : Prop

M.decides B if M is a decider whose language is B.

noncomputable def OracleComputation.OracleNTM.runsInTime {Q Γ : Type} [DecidableEq Q] (M : OracleNTM Q Γ) (t : ℕ → ℕ) : Prop

M.runsInTime t if on every input w and every valid branch of length k ≤ t(|w|), the configuration at step k is a halt configuration.

def OracleComputation.InPWithOracle {Γ : Type} (A B : Set (List Γ)) : Prop

InPWithOracle A B says B ∈ P^A: some deterministic oracle TM with oracle A decides B in polynomial time n^k.

def OracleComputation.InNPWithOracle {Γ : Type} (A B : Set (List Γ)) : Prop

InNPWithOracle A B says B ∈ NP^A: some nondeterministic oracle TM with oracle A decides B in polynomial time n^k.

def OracleComputation.ClassPWithOracle {Γ : Type} (A : Set (List Γ)) : Set (Set (List Γ))

The complexity class P^A: all languages decidable in P with oracle A.

def OracleComputation.ClassNPWithOracle {Γ : Type} (A : Set (List Γ)) : Set (Set (List Γ))

The complexity class NP^A: all languages decidable in NP with oracle A.

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

InPSPACE A (in this namespace) reuses the definition SpaceComplexity.InPSPACE.

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

InNPSPACE A (in this namespace) reuses the definition SpaceComplexity.InNPSPACE.

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

TQBF is the language of true quantified Boolean formulae under encoding enc (a wrapper over SpaceComplexity.tqbfLanguage). TQBF is the canonical PSPACE-complete language used here as an oracle.

theorem pspace_subset_npspace_helper {Γ : Type} (A : Set (List Γ)) : OracleComputation.InPSPACE A → OracleComputation.InNPSPACE A

PSPACE ⊆ NPSPACE: any deterministic PSPACE machine is a (trivial) nondeterministic one.

theorem savitch_theorem_pspace {Γ : Type} (A : Set (List Γ)) : OracleComputation.InNPSPACE A ↔ OracleComputation.InPSPACE A

Savitch's Theorem at the PSPACE level: NPSPACE = PSPACE. Forward direction is the standard Savitch simulation NSPACE(s) ⊆ SPACE(s²); the reverse direction is trivial inclusion.

theorem np_tqbf_sub_npspace {Γ : Type} [Inhabited Γ] (enc : SpaceComplexity.QBFEncoding Γ) (B : Set (List Γ)) : OracleComputation.InNPWithOracle (OracleComputation.TQBF enc) B → OracleComputation.InNPSPACE B

NP^TQBF ⊆ NPSPACE: any nondeterministic polynomial-time machine using a TQBF oracle can be simulated in nondeterministic polynomial space, since each oracle query can be answered in PSPACE.

theorem poly_reducible_implies_in_P_oracle {Γ : Type} (A B : Set (List Γ)) : TuringMachine.PolyReducible B A → OracleComputation.InPWithOracle A B

If B ≤_P A then B ∈ P^A: a polynomial-time reduction can be carried out by a P machine that calls the oracle A once on the reduced input.

theorem pspace_sub_p_tqbf {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : SpaceComplexity.QBFEncoding Γ) (B : Set (List Γ)) : OracleComputation.InPSPACE B → OracleComputation.InPWithOracle (OracleComputation.TQBF enc) B

PSPACE ⊆ P^TQBF: every PSPACE language polynomial-time reduces to TQBF (since TQBF is PSPACE-complete), so it is in P with a TQBF oracle.

theorem p_oracle_sub_np_oracle {Γ : Type} (A B : Set (List Γ)) : OracleComputation.InPWithOracle A B → OracleComputation.InNPWithOracle A B

P^A ⊆ NP^A for every oracle A: a deterministic oracle machine is a (trivial) nondeterministic one.

theorem OracleComputation.exists_oracle_P_eq_NP {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (enc : SpaceComplexity.QBFEncoding Γ) : ∃ (A : Set (List Γ)), ClassPWithOracle A = ClassNPWithOracle A

There exists an oracle A such that P^A = NP^A. Take A = TQBF. Then both P^TQBF and NP^TQBF collapse to PSPACE: the containments P^TQBF ⊆ NP^TQBF ⊆ NPSPACE = PSPACE ⊆ P^TQBF together with Savitch's theorem give equality. This is the classic "relativization barrier" result for P vs NP.