feat(Classes/Hierarchy): nondeterministic exponential time hierarchy by lazy diagonalization (#1539 M2)

Complexity.lean

@@ -1207,6 +1207,7 @@ public import Complexity.Computability.Complexity.Classes.FunctionTime.WordRAM
 public import Complexity.Computability.Complexity.Classes.Hierarchy
 public import Complexity.Computability.Complexity.Classes.Hierarchy.LogClock
 public import Complexity.Computability.Complexity.Classes.Hierarchy.Nondeterministic
+public import Complexity.Computability.Complexity.Classes.Hierarchy.NondeterministicExponentialTime
 public import Complexity.Computability.Complexity.Classes.Hierarchy.NondeterministicPolynomial
 public import Complexity.Computability.Complexity.Classes.Hierarchy.NondeterministicTime
 public import Complexity.Computability.Complexity.Classes.Hierarchy.Polynomial
@@ -1753,6 +1754,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.PolyTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.PolynomialPadding
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Sum
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.TwoPow
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigOLe
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds
@@ -2088,6 +2090,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.T
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Tidy.Redirect
 public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
 public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Degree
+public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Exponential
 public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynomial
 public import Complexity.Computability.Machines.Turing.MultiTape.Run
 public import Complexity.Computability.Machines.Turing.MultiTape.SingleTape

Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean

@@ -12,6 +12,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bi
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Exponential
 import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
 import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 
@@ -86,14 +87,6 @@ theorem savitch_boundedExistsEdge {β : Type} (f : β × List Bool → Bool) (x
     · simp [boundedExistsEdge, List.replicate_succ, hf]
     · simp [boundedExistsEdge, List.replicate_succ]
 
-/-- A polynomially bounded resource function is within a constant multiple of `2 ^ size`. -/
-private theorem PolyBounded.exists_le_mul_two_pow {α : Type*} {size u : α → ℕ}
-    (h : PolyBounded size u) : ∃ C, ∀ a, u a ≤ C * 2 ^ size a := by
-  obtain ⟨c, d, hcd⟩ := h.exists_le
-  obtain ⟨C, hC⟩ := PolynomiallyBounded.exists_le_mul_two_pow
-    (p := fun n => c * (n + 1) ^ d) (by fun_prop)
-  exact ⟨C, fun a => (hcd a).trans (hC _)⟩
-
 attribute [local fun_prop] ComputableInPolyTime.fst' ComputableInPolyTime.snd'
     ComputableInPolyTime.bool_and' in
 /-- **Bounded existential quantification in exponential time.** If a test `f` is computable within

Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/TwoPow.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.PolyTime
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
+import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Exponential
+
+/-!
+# Exponentials of polynomial-time exponents
+
+For an exponent `L x` computable in unary in polynomial time, `2 ^ L x` is computable in unary
+within time `O(2 ^ |x| + 4 ^ L x)` and space `O(2 ^ |x| + 2 ^ L x)`
+(`Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_unary_two_pow`): compute `L x`,
+then double `L x` times (`Turing.MultiTapeTM.ComputableInO.unary_two_pow`). The polynomial cost
+of computing the exponent is absorbed by `2 ^ |x|`
+(`Turing.MultiTapeTM.PolyBounded.exists_le_mul_two_pow`).
+
+## Main results
+
+* `Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_unary_two_pow`: `2 ^ L x` in
+  unary within exponential time and space.
+-/
+
+public section
+
+namespace Turing.MultiTapeTM
+
+/-- **`2 ^ L x` in unary**, for an exponent `L x` computable in unary in polynomial time, within
+time `O(2 ^ |x| + 4 ^ L x)` and space `O(2 ^ |x| + 2 ^ L x)`. -/
+theorem ComputableInPolyTime.exists_computableInO_unary_two_pow {α : Type} {enc : α ↪ List Bool}
+    {L : α → ℕ} (hL : ComputableInPolyTime L enc encUnary) :
+    ∃ C, ComputableInO (fun x => 2 ^ L x) enc encUnary
+      (fun x => C * 2 ^ (enc x).length + 4 ^ L x) (fun x => C * 2 ^ (enc x).length + 2 ^ L x) := by
+  obtain ⟨T, S, hT, hS, h⟩ := hL.exists_computableInO
+  obtain ⟨C₁, hC₁⟩ := hT.exists_le_mul_two_pow
+  obtain ⟨C₂, hC₂⟩ := hS.exists_le_mul_two_pow
+  refine ⟨C₁ + C₂, (ComputableInO.unary_two_pow.comp h).mono_le (fun x => ?_) fun x => ?_⟩
+  · have h₁ := hC₁ x
+    have h₂ : (L x + 1) * 2 ^ L x ≤ 4 ^ L x := by
+      rw [show (4 : ℕ) = 2 * 2 by rfl, mul_pow]
+      exact Nat.mul_le_mul_right _ Nat.lt_two_pow_self
+    have h₃ : C₁ * 2 ^ (enc x).length ≤ (C₁ + C₂) * 2 ^ (enc x).length :=
+      Nat.mul_le_mul_right _ (by omega)
+    omega
+  · have h₁ := hC₂ x
+    have h₃ : C₂ * 2 ^ (enc x).length ≤ (C₁ + C₂) * 2 ^ (enc x).length :=
+      Nat.mul_le_mul_right _ (by omega)
+    omega
+
+end Turing.MultiTapeTM

Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds/Exponential.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynomial
+import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
+
+/-!
+# Polynomial bounds below exponentials
+
+A resource function polynomially bounded in an input size `size` is within a constant multiple of
+`2 ^ size` (`Turing.MultiTapeTM.PolyBounded.exists_le_mul_two_pow`), the form of
+`Cslib.PolynomiallyBounded.exists_le_mul_two_pow` for arbitrary inputs. Exponential resource
+bounds absorb the polynomial costs of their subroutines this way.
+
+## Main results
+
+* `Turing.MultiTapeTM.PolyBounded.exists_le_mul_two_pow`: a polynomially bounded resource
+  function is `O(2 ^ size)`.
+-/
+
+public section
+
+namespace Turing.MultiTapeTM.PolyBounded
+
+/-- A polynomially bounded resource function is within a constant multiple of `2 ^ size`. -/
+theorem exists_le_mul_two_pow {α : Type*} {size u : α → ℕ} (h : PolyBounded size u) :
+    ∃ C, ∀ a, u a ≤ C * 2 ^ size a := by
+  obtain ⟨c, d, hcd⟩ := h.exists_le
+  obtain ⟨C, hC⟩ := Cslib.PolynomiallyBounded.exists_le_mul_two_pow
+    (p := fun n => c * (n + 1) ^ d) (by fun_prop)
+  exact ⟨C, fun a => (hcd a).trans (hC _)⟩
+
+end Turing.MultiTapeTM.PolyBounded

ComplexityTests/NondeterministicExponentialTimeHierarchy.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Complexity.Computability.Complexity.Classes.Hierarchy.NondeterministicExponentialTime
+
+/-! The coarse nondeterministic exponential time hierarchy on concrete exponents. The exponential
+lazy diagonal for `k = 2` is in nondeterministic time `O(2 ^ (32 * n))` and not in nondeterministic
+time `O(2 ^ (2 * n))`, the separation that Williams's witness-circuit argument for `E^NP` lower
+bounds consumes (#1539); `k = 0` separates constant from `O(2 ^ (16 * n))` nondeterministic time.
+The verifier rejects inputs without a short description, such as the empty input. -/
+
+public section
+
+namespace ComplexityTests.NondeterministicExponentialTimeHierarchy
+
+open Cslib Cslib.Complexity Turing Turing.MultiTapeTM
+
+/-- The exponential lazy diagonal for `k = 2` separates nondeterministic time `O(2 ^ (2 * n))` from
+nondeterministic time `O(2 ^ (32 * n))`, at the separating problem itself. -/
+example : expLazyDiagonal 2 ∈ NTIME encBits (fun n => 2 ^ (32 * n)) ∧
+    expLazyDiagonal 2 ∉ NTIME encBits (fun n => 2 ^ (2 * n)) :=
+  ⟨expLazyDiagonal_mem_NTIME 2, expLazyDiagonal_notMem_NTIME 2⟩
+
+/-- Nondeterministic time `O(2 ^ (2 * n))` is strictly inside nondeterministic time
+`O(2 ^ (32 * n))`. -/
+example : NTIME encBits (fun n => 2 ^ (2 * n)) ⊂ NTIME encBits fun n => 2 ^ (32 * n) :=
+  NTIME_two_pow_ssubset_NTIME_two_pow_of_le le_rfl
+
+/-- Nondeterministic constant time is strictly inside nondeterministic time `O(2 ^ (16 * n))`. -/
+example : NTIME encBits (fun _ => 1) ⊂ NTIME encBits fun n => 2 ^ (16 * n) := by
+  simpa using NTIME_two_pow_ssubset_NTIME_two_pow_of_le (k := 0) (e := 16) le_rfl
+
+/-- `NE` is not contained in nondeterministic time `O(2 ^ (2 * n))`. -/
+example : ¬NE encBits ⊆ NTIME encBits fun n => 2 ^ (2 * n) := fun h =>
+  let ⟨_, hH, hH'⟩ := exists_mem_NE_notMem_NTIME_two_pow 2
+  hH' (h hH)
+
+/-- The empty input carries no short description, so the verifier rejects it with every
+certificate, and the empty input is not in the exponential lazy diagonal. -/
+example (k : ℕ) (v : List Bool) : ExpLazyDiagonal.verifier k ([], v) = false := by
+  simp [ExpLazyDiagonal.verifier, Diagonal.shortDesc, unframe]
+
+example (k : ℕ) : [] ∉ expLazyDiagonal k := by
+  simp [expLazyDiagonal, ExpLazyDiagonal.verifier, Diagonal.shortDesc, unframe]
+
+end ComplexityTests.NondeterministicExponentialTimeHierarchy

ROADMAP.md

@@ -183,7 +183,9 @@ index links to canonical definitions rather than keeping a second set.
   `(f + 1) * polylog f ≤ g`, with an absolute exponent (`Hierarchy/TimePolylog`). Composing it
   with the word-RAM simulations gives `RAMTIME T ⊂ RAMTIME T⁵` over `Basis.additive` for
   polynomial `T` (`Hierarchy/WordRAM`). For nondeterministic time, padding amplifies the coarse
-  lazy-diagonal hierarchy, which separates degree `d` from degree `6 * d + 14`. Remaining targets
+  lazy-diagonal hierarchy, which separates degree `d` from degree `6 * d + 14`; lazy
+  diagonalization also separates `NTIME (2 ^ (k * n))` from `NTIME (2 ^ ((8 * k + 16) * n))`, so
+  `NE ⊄ NTIME (2 ^ (k * n))`. Remaining targets
   include the textbook `f log f = o(g)` hierarchy, which needs the diagonal to clock the universal
   machine's own steps, noninteger polynomial degrees, a word-RAM hierarchy by direct
   diagonalization with a smaller gap, and sharp nondeterministic and alternating time