From 415d328669b3160ba61fec83eb334ada48a05af9 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 07:56:51 -0400 Subject: [PATCH 1/9] feat(Classes/Time): explicit-time verifier characterization of NTIME (#1572) Guess and verify within explicit time (`setOf_exists_mem_NTIME`), through a closed fair-coin composition with the new framed sampler `pairSampler`, and a linear-time verifier for every problem in `NTIME` (`exists_verifier_of_mem_NTIME`). Infrastructure toward the nondeterministic time hierarchy. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/Time/Verifier.lean | 266 +++++++++++++++++ .../MultiTape/Probabilistic/PairSampler.lean | 268 ++++++++++++++++++ .../NondeterministicTimeVerifiers.lean | 85 ++++++ 4 files changed, 621 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/Time/Verifier.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean create mode 100644 ComplexityTests/NondeterministicTimeVerifiers.lean diff --git a/Complexity.lean b/Complexity.lean index d8146fc83f..7eddad2ea2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1327,6 +1327,7 @@ public import Complexity.Computability.Complexity.Classes.Tally public import Complexity.Computability.Complexity.Classes.Time public import Complexity.Computability.Complexity.Classes.Time.AcceptCount public import Complexity.Computability.Complexity.Classes.Time.Polynomial +public import Complexity.Computability.Complexity.Classes.Time.Verifier public import Complexity.Computability.Complexity.Classes.Toda public import Complexity.Computability.Complexity.Classes.Toda.Counting public import Complexity.Computability.Complexity.Classes.Toda.Hierarchy @@ -1990,6 +1991,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.O public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Oracle public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OutputPrefix public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OutputToTape +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PolynomialClock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.QueryBounds public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.QueryTake diff --git a/Complexity/Computability/Complexity/Classes/Time/Verifier.lean b/Complexity/Computability/Complexity/Classes/Time/Verifier.lean new file mode 100644 index 0000000000..89b4f594ab --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Time/Verifier.lean @@ -0,0 +1,266 @@ +/- +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.Complexity.Classes.Time +import Complexity.Computability.Complexity.Classes.NP.Nondeterministic +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Composition +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput +import Complexity.Computability.Machines.Turing.MultiTape.Run +import Complexity.Probability.BitString +import Complexity.Probability.PMF.Bind + +/-! +# Nondeterministic time through verifiers, with explicit bounds + +This module characterizes `Cslib.Complexity.NTIME enc t` by deterministic verifiers, keeping the +time bound up to constant factors. The polynomial characterization of `NP` +(`Cslib.Complexity.mem_NP_iff_decidableInPolyTime`) loses the degree in both directions. The +two directions here keep it. + +* **Guess and verify** (`Cslib.Complexity.setOf_exists_mem_NTIME`). Suppose a verifier `V` is + computable within time `T (a, w)` on encoded pairs, and a certificate length `ℓ a` is + computable in unary within time `Tℓ a`. Then the problem + `{a | ∃ w, w.length = ℓ a ∧ V (a, w) = true}` lies in `NTIME enc t` whenever + `(enc a).length + Tℓ a + T (a, w)` is within `O(t (enc a).length)` on certificates of that + length. The certificate length may depend on the instance, not only on its encoded length. + The machine is the nondeterministic reading of a closed fair-coin composition: + - a deterministic machine writes `frame (enc a)` followed by `ℓ` ones; + - the fixed sampler `Turing.MultiTapePTM.pairSampler` copies the framed instance and replaces + the ones by fair coins; + - a deterministic machine runs the verifier. + + Its computation paths are exactly the coin replays, so it accepts exactly when some + certificate is accepted, and every branch halts within the composed clock. +* **Verifiers from nondeterministic time** (`Cslib.Complexity.exists_verifier_of_mem_NTIME`). + A problem in `NTIME enc t` has a verifier that is computable in linear time on encoded pairs: + check that the certificate, read as coins of the choice table + (`Turing.MultiTapeNTM.checkChoices`), replays an accepting computation. Every certificate + length of at least `c * t (enc a).length + c` works, for a constant `c`. + +These are explicit-time forms of the guess-and-verify characterization of nondeterministic +polynomial time [Arora and Barak][AroraBarak09]: the choices of an accepting computation are a +certificate, and a certificate can be guessed and then checked. + +## Main results + +* `Cslib.Complexity.setOf_exists_mem_NTIME`: guess and verify within explicit time. +* `Cslib.Complexity.exists_verifier_of_mem_NTIME`: a linear-time verifier for a problem in + `NTIME`, with certificates of every sufficient length. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +public section + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} + +/-- **Guess and verify, within explicit time.** If a verifier `V` is computable within time +`T (a, w)` on encoded pairs, and the certificate length `ℓ a` is computable in unary within time +`Tℓ a`, then the problem of instances with an accepted certificate of that length is in +`NTIME enc t`, provided `(enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C` for every +certificate `w` of that length. -/ +theorem setOf_exists_mem_NTIME {V : α × List Bool → Bool} {ℓ : α → ℕ} {t : ℕ → ℕ} + {Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {C : ℕ} + (hℓ : ComputableInO ℓ enc encUnary Tℓ Sℓ) + (hV : ComputableInO V (encPair enc encBits) encBool T S) + (ht : ∀ a w, w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) : + {a | ∃ w : List Bool, w.length = ℓ a ∧ V (a, w) = true} ∈ NTIME enc t := by + -- the deterministic preparation and the verifier, as machines + obtain ⟨c₁, ⟨k₁, Q₁, _, tm₁, h₁⟩, -⟩ := + (ComputableInO.of_eq (f := fun a : α => a) (encIn := enc) (encMid := enc) fun _ => rfl).prod hℓ + obtain ⟨c₃, ⟨k₃, Q₃, _, tm₃, h₃⟩, -⟩ := hV + let L (a : α) : ℕ := ℓ a + let u (a : α) : List Bool := frame (enc a) ++ List.replicate (L a) true + let t₁ (a : α) : ℕ := c₁ * ((enc a).length + Tℓ a + 1) + let t₂ (a : α) : ℕ := (u a).length + 1 + let t₃ (a : α) : ℕ := c₃ * (C * t (enc a).length + C + 1) + have hrun₁ (a : α) := (h₁ a).runFrom_of_le (le_refl (t₁ a)) + have hlen₁ (a : α) : (u a).length ≤ t₁ a := (h₁ a).length_output_le + -- the first phase writes the framed instance and the unary certificate length + let M₁ : MultiTapePTM k₁ Bool Q₁ := MultiTapePTM.ofDeterministic tm₁ + have hfirst₁ (a : α) : ∀ final ∈ (ProbComp.eval + (M₁.runClosedConfigFrom (t₁ a) (M₁.initialConfig (enc a)))).support, + final.tapes.state = none := by + intro final hfinal + rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal + subst hfinal + exact (hrun₁ a).1 + have hout₁ (a : α) : ProbComp.eval (M₁.runClosed (t₁ a) (enc a)) = PMF.pure (u a) := by + rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₁ a).2] + rfl + -- the sampler copies the framed instance and guesses the certificate + have hsecond₁ (a : α) : ∀ word ∈ (ProbComp.eval (M₁.runClosed (t₁ a) (enc a))).support, + ∀ final ∈ (ProbComp.eval (MultiTapePTM.pairSampler.runClosedConfigFrom (t₂ a) + (MultiTapePTM.pairSampler.initialConfig word))).support, final.tapes.state = none := by + intro word hword + rw [hout₁ a, PMF.mem_support_pure_iff] at hword + subst hword + exact MultiTapePTM.pairSampler_halted (enc a) (List.replicate (L a) true) + let P₁₂ := MultiTapePTM.pairSampler.comp M₁ false + let t₁₂ (a : α) : ℕ := t₁ a + (t₁ a + 4 + t₂ a) + have heval₁₂ (a : α) : ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a)) = + (BitString.uniformList (L a)).map (frame (enc a) ++ ·) := by + rw [MultiTapePTM.eval_comp M₁ MultiTapePTM.pairSampler false (enc a) (t₁ a) (t₂ a) + (hfirst₁ a) (hsecond₁ a), hout₁ a, Probability.PMF.monad_bind_eq_bind, PMF.pure_bind] + simpa only [List.length_replicate, u] using + MultiTapePTM.eval_pairSampler (enc a) (List.replicate (L a) true) + have hhalt₁₂ (a : α) := MultiTapePTM.comp_halted M₁ MultiTapePTM.pairSampler false (enc a) + (t₁ a) (t₂ a) (hfirst₁ a) (hsecond₁ a) + -- the verifier runs on every guessed pair within the uniform clock `t₃` + let M₃ : MultiTapePTM k₃ Bool Q₃ := MultiTapePTM.ofDeterministic tm₃ + have hrun₃ (a : α) (w : List Bool) (hw : w.length = L a) := + (h₃ (a, w)).runFrom_of_le (J := t₃ a) (Nat.mul_le_mul_left c₃ (by + have := ht a w hw + omega)) + have hword (a : α) {word : List Bool} + (hword : word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support) : + ∃ w : List Bool, w.length = L a ∧ word = encPair enc encBits (a, w) := by + rw [heval₁₂ a] at hword + obtain ⟨w, hw, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hword + exact ⟨w, BitString.mem_support_uniformList_iff.mp hw, rfl⟩ + have hsecond₂ (a : α) : ∀ word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support, + ∀ final ∈ (ProbComp.eval (M₃.runClosedConfigFrom (t₃ a) (M₃.initialConfig word))).support, + final.tapes.state = none := by + intro word hw final hfinal + obtain ⟨w, hwlen, rfl⟩ := hword a hw + rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal + subst hfinal + exact (hrun₃ a w hwlen).1 + let P := M₃.comp P₁₂ false + let total (a : α) : ℕ := t₁₂ a + (t₁₂ a + 4 + t₃ a) + -- the nondeterministic reading decides the problem + have hdec : P.toNTM.DecidesInTime enc + {a | ∃ w : List Bool, w.length = ℓ a ∧ V (a, w) = true} total := by + intro a + have htime : P.toNTM.RunsInTime (enc a) (total a) := P.runsInTime_toNTM + (MultiTapePTM.comp_halted P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) (hsecond₂ a)) + refine ⟨htime, ?_⟩ + rw [MultiTapeNTM.accepts_iff_exists_time_eq htime, + P.exists_computationPath_toNTM_iff (P := fun cfg => cfg.output = [true])] + have hiff : (∃ final ∈ (ProbComp.eval (P.runClosedConfigFrom (total a) + (P.initialConfig (enc a)))).support, final.tapes.output = [true]) ↔ + [true] ∈ (ProbComp.eval (P.runClosed (total a) (enc a))).support := by + rw [MultiTapePTM.runClosed_eq_map, ProbComp.eval_map, PMF.mem_support_map_iff] + rw [hiff, MultiTapePTM.eval_comp P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) + (hsecond₂ a), Probability.PMF.monad_bind_eq_bind, PMF.mem_support_bind_iff] + constructor + · rintro ⟨w, hw, hV⟩ + refine ⟨encPair enc encBits (a, w), ?_, ?_⟩ + · rw [heval₁₂ a] + exact (PMF.mem_support_map_iff _ _ _).mpr + ⟨w, BitString.mem_support_uniformList_iff.mpr hw, rfl⟩ + · rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₃ a w hw).2, PMF.mem_support_pure_iff] + simp [hV] + · rintro ⟨word, hw, hacc⟩ + obtain ⟨w, hwlen, rfl⟩ := hword a hw + rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₃ a w hwlen).2, + PMF.mem_support_pure_iff] at hacc + exact ⟨w, hwlen, by simpa using hacc⟩ + -- the composed clock is within `O(t)` + refine ⟨(6 * c₁ + c₃) * C, (6 * c₁ + c₃) * (C + 1) + 14, _, _, inferInstance, P.toNTM, + hdec.mono fun a => ?_⟩ + set X := C * t (enc a).length + C + 1 + have hX₁ : t₁ a ≤ c₁ * X := Nat.mul_le_mul_left c₁ (by + have := ht a (List.replicate (L a) false) (List.length_replicate ..) + omega) + have htotal : total a ≤ 6 * t₁ a + 14 + t₃ a := by + have := hlen₁ a + simp only [total, t₁₂, t₂] + omega + have hX₃ : t₃ a = c₃ * X := rfl + calc total a ≤ 6 * (c₁ * X) + 14 + c₃ * X := by + have := Nat.mul_le_mul_left 6 hX₁ + rw [hX₃] at htotal + omega + _ = (6 * c₁ + c₃) * C * t (enc a).length + ((6 * c₁ + c₃) * (C + 1) + 14) := by + simp only [X] + ring + +/-- **A linear-time verifier for nondeterministic time.** A problem in `NTIME enc t` has a +verifier computable in linear time on encoded pairs. For a constant `c`, every certificate length +`L ≥ c * t (enc a).length + c` works: `a ∈ A` exactly when some certificate of length `L` is +accepted. The verifier checks that the certificate, read as coins of the choice table, replays an +accepting computation. -/ +theorem exists_verifier_of_mem_NTIME {A : Set α} {t : ℕ → ℕ} (hA : A ∈ NTIME enc t) : + ∃ (V : α × List Bool → Bool) (c : ℕ), + ComputableInO V (encPair enc encBits) encBool (fun p => (encPair enc encBits p).length) + (fun p => (encPair enc encBits p).length) ∧ + ∀ a L, c * t (enc a).length + c ≤ L → + (a ∈ A ↔ ∃ w : List Bool, w.length = L ∧ V (a, w) = true) := by + obtain ⟨c₁, c₂, k, State, hfinite, ntm, hdec⟩ := hA + set M := Nat.card (Turing.Action k Bool State) + refine ⟨ntm.checkChoices enc, M * (c₁ + c₂), ?_, fun a L hL => + hdec.mem_iff_exists_checkChoices ?_⟩ + · -- replay the certificate with the choice table, then compare the output with `[true]` + have hswap : ComputableInO (fun p : α × List Bool => (p.2, enc p.1)) (encPair enc encBits) + (encPair encBits encBits) + (fun p => (encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length)) + (fun p => (encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length)) := + (ComputableInO.snd enc encBits).prod + ((ComputableInO.of_eq (f := fun x : α => enc x) (encIn := enc) (encMid := encBits) + fun _ => rfl).comp (ComputableInO.fst enc encBits)) + have hrun := (ComputableInO.of_linear + (MultiTapePTM.computableInLinearTimeAndSpace_runClosedCoins ntm.choiceTable)).comp hswap + obtain ⟨cr, hcr⟩ := hrun.length_le_time + have heq := ComputableInO.eqWords.comp ((ComputableInO.const (encIn := encPair enc encBits) + (encMid := encBits) [true]).prod hrun) + have hfun : ((fun p : List Bool × List Bool => decide (p.1 = p.2)) ∘ + fun p : α × List Bool => ([true], ((fun q : List Bool × List Bool => + ntm.choiceTable.runClosedCoins q.1 q.2) ∘ fun p : α × List Bool => (p.2, enc p.1)) p)) = + ntm.checkChoices enc := by + funext p + simp [MultiTapeNTM.checkChoices, eq_comm] + rw [hfun] at heq + -- every part is linear in the encoded pair, including the replayed output + have hbound (p : α × List Bool) : + (encPair enc encBits p).length + ((encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length) + + (encPair encBits encBits (p.2, enc p.1)).length) + + 2 * ((ntm.choiceTable.runClosedCoins p.2 (enc p.1)).length + 2) ≤ + (9 + 10 * cr) * ((encPair enc encBits p).length + 1) := by + have hc := hcr p + simp only [Function.comp_apply, encBits_apply] at hc + have hle : (enc p.1).length ≤ (encPair enc encBits p).length := by + simp only [encPair_apply, List.length_append, length_frame, encBits_apply] + omega + have hsw : (encPair encBits encBits (p.2, enc p.1)).length ≤ + 2 * (encPair enc encBits p).length := by + simp only [encPair_apply, List.length_append, length_frame, encBits_apply] + omega + generalize (encPair enc encBits p).length = N at * + generalize (ntm.choiceTable.runClosedCoins p.2 (enc p.1)).length = R at * + generalize (encPair encBits encBits (p.2, enc p.1)).length = W at * + have hR : R ≤ cr * (5 * N + 1) := hc.trans (Nat.mul_le_mul_left cr (by omega)) + nlinarith + refine heq.mono (9 + 10 * cr) (fun p => ?_) fun p => ?_ + · have := hbound p + simp only [Function.comp_apply, List.length_singleton] at this ⊢ + nlinarith + · have := hbound p + simp only [Function.comp_apply, List.length_singleton] at this ⊢ + omega + · have hmul : M * (c₁ * t (enc a).length + c₂) ≤ + M * (c₁ + c₂) * t (enc a).length + M * (c₁ + c₂) := by + rw [Nat.mul_assoc, ← Nat.mul_add] + exact Nat.mul_le_mul_left M (by nlinarith) + exact hmul.trans hL + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean new file mode 100644 index 0000000000..7b6a8192b7 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean @@ -0,0 +1,268 @@ +/- +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.Probabilistic.Sampling +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame.Basic + +/-! +# Sampling a certificate beside a framed word + +`Turing.MultiTapePTM.pairSampler` is one fixed fair-coin machine with three control states and no +work tapes. On an input `frame y ++ r` it copies `frame y` to the output, then emits one fresh +fair bit for each symbol of `r`, and halts at the right boundary. So it outputs `frame y ++ w`, +the pair encoding of `(y, w)`, for a uniform word `w` of length `r.length`. It takes exactly +`(frame y ++ r).length + 1` transitions. Each copying transition also draws a coin, and ignores +it. Read nondeterministically, the machine guesses a certificate for the framed instance. + +## Main definitions + +* `Turing.MultiTapePTM.pairSampler`: the framed copier and certificate sampler. + +## Main results + +* `Turing.MultiTapePTM.eval_pairSampler`: the output is a uniform certificate after the framed + word. +* `Turing.MultiTapePTM.pairSampler_halted`: every run has halted at the linear clock. +-/ + +@[expose] public section + +namespace Turing.MultiTapePTM + +open Cslib MultiTapeMachine MultiTapeTM + +namespace PairSampler + +/-- The control phases: before a frame tag, before a framed data bit, and in the sampled tail. -/ +inductive Phase + | tag + | data + | tail + deriving DecidableEq + +instance : Fintype Phase := + ⟨{.tag, .data, .tail}, fun q => by cases q <;> simp⟩ + +/-- The control state after reading a symbol. The right boundary halts. -/ +def next : Phase → Option Bool → Option Phase + | _, none => none + | .tag, some true => some .data + | .tag, some false => some .tail + | .data, some _ => some .tag + | .tail, some _ => some .tail + +/-- The emitted symbol. Framed symbols are copied, and tail symbols are replaced by the coin. -/ +def emit : Phase → Option Bool → Bool → Option Bool + | _, none, _ => none + | .tail, some _, bit => some bit + | .tag, some b, _ => some b + | .data, some b, _ => some b + +end PairSampler + +open PairSampler in +/-- Copy a framed word, then emit one fair bit per remaining input symbol, and halt at the right +boundary, without work tapes. -/ +def pairSampler : MultiTapePTM 0 Bool Phase where + initial := .tag + tr q symbol _ _ bit := .step + { inputTape := if symbol.isSome then 1 else 0 + workTapes := Fin.elim0 + output := emit q symbol bit + state := next q symbol } + Empty.elim Empty.elim + +namespace PairSampler + +/-- The sampler at an input position, with the output written so far. -/ +def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : List Bool) + (h : index ≤ input.length) : Config 0 Bool Phase Empty input where + tapes := + { state := state + inputPos := ⟨index + 1, by lia⟩ + workTapes := Fin.elim0 + workTapePos := Fin.elim0 + output := output } + +/-- Reading a remaining symbol writes the emitted symbol and advances once. -/ +theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) + (q : Phase) (o : Option Bool) (s : Option Phase) : + (config input (some q) index output (by lia)).step + { inputTape := 1, workTapes := Fin.elim0, output := o, state := s } + Empty.elim Empty.elim = + config input s (index + 1) (output ++ o.toList) h := by + refine Config.ext ?_ (funext fun oracle => oracle.elim) + refine Cfg.ext_zero_tapes rfl ?_ rfl + apply Fin.ext + change (moveInputPos _ .pos).val = index + 1 + 1 + rw [moveInputPos_pos_of_ne_right _ (by simp only [config]; lia)] + rfl + +/-- One live transition at a remaining symbol: draw a coin and take the selected step. -/ +theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < input.length) + (q : Phase) (fuel : ℕ) : + ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) + (config input (some q) index output (by lia))) = + ProbComp.eval (ProbComp.uniform Bool >>= fun bit => + pairSampler.runClosedConfigFrom fuel + (config input (next q (some input[index])) (index + 1) + (output ++ (emit q (some input[index]) bit).toList) h)) := by + have hsym := inputSymbolInner (cfg := + (config input (some q) index output (by lia)).tapes) index (by simp [config]; lia) h + rw [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + simp only [show (config input (some q) index output (by lia)).tapes.state = some q from rfl, + hsym, pairSampler, Option.isSome_some, ↓reduceIte, bind_map_left, step h] + rfl + +/-- At the right boundary the sampler halts, drawing and discarding one coin. -/ +theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : + ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) + (config input (some q) input.length output le_rfl)) = + PMF.pure (config input none input.length output le_rfl) := by + have hsym := inputSymbol_eq_none_of_boundary (cfg := + (config input (some q) input.length output le_rfl).tapes) + (Or.inr (by simp [config])) + rw [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + simp only [show (config input (some q) input.length output le_rfl).tapes.state = some q from rfl, + pairSampler, hsym, Option.isSome_none, Bool.false_eq_true, ↓reduceIte, bind_map_left] + have hcfg : ∀ bit : Bool, (config input (some q) input.length output le_rfl).step + { inputTape := 0, workTapes := Fin.elim0, output := emit q none bit, + state := next q none } Empty.elim Empty.elim = + config input none input.length output le_rfl := by + intro bit + refine Config.ext ?_ (funext fun oracle => oracle.elim) + refine Cfg.ext_zero_tapes ?_ (by simp [Config.step, config, Turing.Action.apply]) ?_ + · cases q <;> rfl + · cases q <;> simp [Config.step, config, Turing.Action.apply, emit] + simp only [hcfg] + rcases fuel with _ | fuel + · simp only [MultiTapeMachine.runConfigFrom, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.bind_const] + · have hhalt : ∀ n, ProbComp.eval (pairSampler.runClosedConfigFrom n + (config input none input.length output le_rfl)) = + PMF.pure (config input none input.length output le_rfl) := by + intro n + cases n with + | zero => simp [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + | succ n => + rw [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + simp [config] + simp only [ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => ProbComp.eval + (pairSampler.runClosedConfigFrom (fuel + 1) + (config input none input.length output le_rfl))) = _ + rw [hhalt, PMF.bind_const] + +/-- The tail phase: one fresh fair bit per remaining symbol, then halting at the boundary. -/ +theorem eval_run_tail (input : List Bool) (remaining : ℕ) : + ∀ (index : ℕ) (output : List Bool) (h : index + remaining = input.length), + ProbComp.eval (pairSampler.runClosedConfigFrom (remaining + 1) + (config input (some .tail) index output (by lia))) = + (BitString.uniformList remaining).map + (fun tail => config input none input.length (output ++ tail) le_rfl) := by + induction remaining with + | zero => + intro index output h + have hi : index = input.length := by lia + subst index + rw [eval_run_boundary] + simp [BitString.uniformList_zero, PMF.pure_map] + | succ remaining ih => + intro index output h + have hi : index < input.length := by lia + rw [eval_run_succ hi] + simp only [next, emit, Option.toList_some] + simp only [ProbComp.eval_bind, ProbComp.eval_uniform, ih (index + 1) _ (by lia), + BitString.uniformList_succ, PMF.map_bind, PMF.map_comp, Function.comp_def, + List.append_assoc, List.singleton_append] + +/-- The copying phase: a framed word is copied verbatim, ignoring the coins drawn meanwhile. -/ +theorem eval_run_frame (input rest : List Bool) (fuel : ℕ) (y : List Bool) : + ∀ (pre output : List Bool) (hin : input = pre ++ frame y ++ rest), + ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y).length + fuel) + (config input (some .tag) pre.length output (by subst hin; simp))) = + ProbComp.eval (pairSampler.runClosedConfigFrom fuel + (config input (some .tail) (pre.length + (frame y).length) (output ++ frame y) + (by subst hin; simp))) := by + induction y with + | nil => + intro pre output hin + have hlt : pre.length < input.length := by subst hin; simp [frame] + have hget : input[pre.length] = false := by subst hin; simp [frame] + rw [show (frame []).length + fuel = fuel + 1 by simp [frame]; lia, eval_run_succ hlt] + simp only [hget, next, emit, Option.toList_some, ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => _) = _ + rw [PMF.bind_const] + rfl + | cons b y ih => + intro pre output hin + have hlt : pre.length < input.length := by subst hin; simp [frame] + have hlt' : pre.length + 1 < input.length := by subst hin; simp [frame] + have hget : input[pre.length] = true := by subst hin; simp [frame] + have hget' : input[pre.length + 1] = b := by + subst hin + simp only [frame, List.flatMap_cons, List.append_assoc] + rw [List.getElem_append_right (by simp)] + simp + have hlen : (frame (b :: y)).length + fuel = ((frame y).length + fuel + 1) + 1 := by + simp [frame]; lia + rw [hlen, eval_run_succ hlt] + simp only [hget, next, emit, Option.toList_some, ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => _) = _ + rw [PMF.bind_const, eval_run_succ hlt'] + simp only [hget', next, emit, Option.toList_some, ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => _) = _ + rw [PMF.bind_const] + have hpre : input = (pre ++ [true, b]) ++ frame y ++ rest := by + subst hin; simp [frame] + have := ih (pre ++ [true, b]) (output ++ [true] ++ [b]) hpre + simp only [List.length_append, List.length_cons, List.length_nil] at this + convert this using 3 + · congr 1 + · simp [frame]; lia + · simp + +end PairSampler + +open PairSampler + +/-- The final configuration retains the framed word and a uniform certificate, and has halted at +the right boundary. -/ +theorem eval_runClosedConfig_pairSampler (y r : List Bool) : + ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y ++ r).length + 1) + (pairSampler.initialConfig (frame y ++ r))) = + (BitString.uniformList r.length).map (fun w => + PairSampler.config (frame y ++ r) none (frame y ++ r).length (frame y ++ w) le_rfl) := by + have hcfg : pairSampler.initialConfig (frame y ++ r) = + PairSampler.config (frame y ++ r) (some .tag) ([] : List Bool).length [] (by simp) := by + refine Config.ext ?_ rfl + exact Cfg.ext_zero_tapes rfl rfl rfl + rw [hcfg, show (frame y ++ r).length + 1 = (frame y).length + (r.length + 1) by simp; lia, + eval_run_frame (frame y ++ r) r (r.length + 1) y [] [] (by simp)] + simpa only [List.length_nil, zero_add, List.nil_append] using + eval_run_tail (frame y ++ r) r.length (frame y).length (frame y) (by simp) + +/-- The sampler outputs a uniform certificate after the framed word, in a linear number of +transitions. -/ +theorem eval_pairSampler (y r : List Bool) : + ProbComp.eval (pairSampler.runClosed ((frame y ++ r).length + 1) (frame y ++ r)) = + (BitString.uniformList r.length).map (frame y ++ ·) := by + rw [runClosed_eq_map, ProbComp.eval_map, eval_runClosedConfig_pairSampler, PMF.map_comp] + rfl + +/-- Every supported configuration has actually halted by the linear clock. -/ +theorem pairSampler_halted (y r : List Bool) : + ∀ final ∈ (ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y ++ r).length + 1) + (pairSampler.initialConfig (frame y ++ r)))).support, final.tapes.state = none := by + intro final hfinal + rw [eval_runClosedConfig_pairSampler] at hfinal + obtain ⟨output, _, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hfinal + rfl + +end Turing.MultiTapePTM diff --git a/ComplexityTests/NondeterministicTimeVerifiers.lean b/ComplexityTests/NondeterministicTimeVerifiers.lean new file mode 100644 index 0000000000..995a36357f --- /dev/null +++ b/ComplexityTests/NondeterministicTimeVerifiers.lean @@ -0,0 +1,85 @@ +/- +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.Time.Verifier +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler + +/-! The explicit-time verifier characterization of `NTIME` on concrete bounds. A deterministic +linear-time decider is a verifier with empty certificates, and a linear-time nondeterministic +problem survives the round trip through its linear-time verifier and guess and verify, at the +same linear bound. The sampler's output distribution is checked on a small input. -/ + +public section + +namespace ComplexityTests.NondeterministicTimeVerifiers + +open Cslib Cslib.Complexity Turing Turing.MultiTapeTM + +/-- `c * n + c` in unary, within linear time and space. -/ +private theorem computableInO_linear_unary (c : ℕ) : + ComputableInO (fun x : List Bool => c * x.length + c) encBits encUnary + (fun x => x.length) (fun x => x.length) := by + induction c with + | zero => + simpa using ComputableInO.const (encIn := encBits) (encMid := encUnary) 0 + | succ c ih => + have hstep := ComputableInO.lengthUnary.append + (ComputableInO.const (encIn := encBits) (encMid := encUnary) 1) + (g := fun x : List Bool => x.length + 1) (encOut := encUnary) + fun x => by simp [encUnary_apply, List.replicate_add] + have h := ih.append hstep (g := fun x : List Bool => (c + 1) * x.length + (c + 1)) + (encOut := encUnary) fun x => by + simp only [encUnary_apply, ← List.replicate_add] + congr 1 + ring + exact h.mono 3 (fun x => by simp only [encBits_apply]; omega) + (fun x => by simp only [encBits_apply]; omega) + +/-- Guess and verify with empty certificates recovers deterministic linear time inside +nondeterministic linear time. -/ +example {A : Set (List Bool)} (hA : A ∈ DTIME encBits fun n => n) : + A ∈ NTIME encBits fun n => n := by + have hV := (computableInO_indicator_of_mem_DTIME hA).comp (ComputableInO.fst encBits encBits) + have h := setOf_exists_mem_NTIME (ℓ := fun _ => 0) (t := fun n => n) (C := 6) + (ComputableInO.const (encIn := encBits) (encMid := encUnary) 0) hV fun x w hw => by + simp only [List.length_eq_zero_iff] at hw + subst hw + simp only [encBits_apply, encPair_apply, List.length_append, length_frame, + List.length_nil] + omega + have hset : {x : List Bool | ∃ w : List Bool, w.length = 0 ∧ + (indicator A ∘ Prod.fst) (x, w) = true} = A := by + ext x + simp [indicator] + rwa [hset] at h + +/-- **Round trip at linear time.** A problem in nondeterministic linear time has a linear-time +verifier, and guessing certificates of length `c * n + c` for it decides the problem in +nondeterministic linear time again. Both explicit-time hypotheses are satisfiable together. -/ +theorem mem_NTIME_linear_of_verifier_roundTrip {A : Set (List Bool)} + (hA : A ∈ NTIME encBits fun n => n) : A ∈ NTIME encBits fun n => n := by + obtain ⟨V, c, hV, hmem⟩ := exists_verifier_of_mem_NTIME hA + have h := setOf_exists_mem_NTIME (ℓ := fun x : List Bool => c * x.length + c) + (t := fun n => n) (C := c + 4) + (computableInO_linear_unary c) hV fun x w hw => by + simp only [encBits_apply, encPair_apply, List.length_append, length_frame, hw] + nlinarith + have hset : {x : List Bool | ∃ w : List Bool, w.length = c * x.length + c ∧ + V (x, w) = true} = A := by + ext x + exact (hmem x _ le_rfl).symm + rwa [hset] at h + +/-- The sampler copies the framed word `[true]` and guesses a two-bit certificate. -/ +example : ProbComp.eval (MultiTapePTM.pairSampler.runClosed 6 (frame [true] ++ [false, false])) = + (BitString.uniformList 2).map (frame [true] ++ ·) := by + simpa using MultiTapePTM.eval_pairSampler [true] [false, false] + +end ComplexityTests.NondeterministicTimeVerifiers From 4a2a973544622f80458d196f4924f6dfd2bf2c68 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 08:42:09 -0400 Subject: [PATCH 2/9] feat(Classes/Hierarchy): coarse nondeterministic time hierarchy by lazy diagonalization (#1572) For every degree d, NTIME((n+1)^d) is strictly contained in NTIME((n+1)^e) whenever 6d + 14 <= e, separated by the explicit lazy diagonal problem. The upper bound guesses a certificate and simulates a described verifier with the native universal machine; the brute force at the end of each interval uses a new exponential-time bounded existential, via Savitch's algorithm at depth 1. The lower bound diagonalizes against the linear-time verifier of #2025. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Hierarchy/NondeterministicTime.lean | 791 ++++++++++++++++++ .../Classes/Time/BoundedExists.lean | 218 +++++ .../NondeterministicTimeHierarchy.lean | 44 + ROADMAP.md | 8 +- references.bib | 20 + 6 files changed, 1080 insertions(+), 3 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean create mode 100644 Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean create mode 100644 ComplexityTests/NondeterministicTimeHierarchy.lean diff --git a/Complexity.lean b/Complexity.lean index 689f8d2667..4a04db677a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1172,6 +1172,7 @@ public import Complexity.Computability.Complexity.Classes.FunctionTime 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.NondeterministicTime public import Complexity.Computability.Complexity.Classes.Hierarchy.Polynomial public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc public import Complexity.Computability.Complexity.Classes.Hierarchy.Space @@ -1334,6 +1335,7 @@ public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Princi public import Complexity.Computability.Complexity.Classes.Tally public import Complexity.Computability.Complexity.Classes.Time public import Complexity.Computability.Complexity.Classes.Time.AcceptCount +public import Complexity.Computability.Complexity.Classes.Time.BoundedExists public import Complexity.Computability.Complexity.Classes.Time.Polynomial public import Complexity.Computability.Complexity.Classes.Time.Verifier public import Complexity.Computability.Complexity.Classes.Toda diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean new file mode 100644 index 0000000000..1f0e01fc6c --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean @@ -0,0 +1,791 @@ +/- +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.Complexity.Classes.Hierarchy.Time +public import Complexity.Foundations.Data.BitString.Enumeration +import Complexity.Computability.Complexity.Classes.Time.BoundedExists +import Complexity.Computability.Complexity.Classes.Time.Verifier +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential + +/-! +# A nondeterministic time hierarchy by lazy diagonalization + +For every degree `d`, nondeterministic time `O((n + 1) ^ d)` is strictly contained in +nondeterministic time `O((n + 1) ^ e)` on bit strings whenever `6 * d + 14 ≤ e` +(`Cslib.Complexity.NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le`). This is a coarse form of the +nondeterministic time hierarchy theorem [Arora and Barak, Theorem 3.3][AroraBarak07], proved by +lazy diagonalization [Žák][Zak1983]. The separating problem is explicit: the lazy diagonal +`Cslib.Complexity.lazyDiagonal d`. + +## The lazy diagonal + +A diagonal for nondeterministic time cannot simply negate the answer of the machine it +simulates: that answer is an existential over certificates. Lazy diagonalization negates it only +once per interval of lengths, where the input is long enough to try every certificate. + +An input `x` carries a word `w` framed at its start, and `w` carries the description +`unframe w` of a deterministic verifier on pairs framed at its start, followed by arbitrary +padding. The padding of `w` gives each description infinitely many words `w`. The interval of +`w` consists of the lengths from `P = 2 * w.length + 1`, the length of `frame w`, to +`2 ^ clock d P - 1`, where `clock d m = (m + 1) ^ (d + 3)`. On the input `x` of length `n` in +this interval, with a certificate `v` of length `certLen d (n + 1) = (n + 2) ^ (d + 2)`, the +verifier `Cslib.Complexity.LazyDiagonal.verifier d` + +* below the end of the interval, runs the described verifier on the one bit longer input + `x ++ [false]` and the certificate `v` for `clock d (n + 1)` steps with the universal function + (`Cslib.Complexity.LazyDiagonal.accepts`); +* at the end of the interval, accepts when the described verifier accepts no certificate of + length `certLen d P` on `frame w`, trying them all. + +The lazy diagonal is the problem of the inputs with an accepted certificate. + +* **Upper bound** (`Cslib.Complexity.lazyDiagonal_mem_NTIME`). Guess the certificate and run the + verifier (`Cslib.Complexity.setOf_exists_mem_NTIME`). The simulation takes time + `O((n + 1) ^ (6 * d + 14))`: polynomial in the input, the certificate and the clock, through the + native universal machine. The brute force takes time `2 ^ O((P + 1) ^ (d + 2))` + (`Cslib.Complexity.exists_computableInO_any_enumList`), which is `O(n)` at the end of the + interval, where `n + 1 = 2 ^ ((P + 1) ^ (d + 3))`. +* **Lower bound** (`Cslib.Complexity.lazyDiagonal_notMem_NTIME`). A nondeterministic machine + deciding the problem within time `O((n + 1) ^ d)` has a deterministic verifier on pairs within + linear time, accepting certificates of every length at least `c * (n + 1) ^ d + c` + (`Cslib.Complexity.exists_verifier_of_mem_NTIME`). On the interval of a word `w` describing that + verifier, with enough padding, the universal function runs it exactly. Then each input of the + interval is in the problem exactly when the next one is, and the last exactly when the first is + not. + +Arora and Barak enumerate nondeterministic machines and use one global sequence of intervals; this +construction gives each word `w` its own interval instead, and diagonalizes against verifiers. +The gap `6 * d + 14` is the polynomial overhead of the native universal machine and of the +certificate length, not the textbook `f (n + 1) = o (g n)`. + +## Main definitions + +* `Cslib.Complexity.LazyDiagonal.verifier`: the verifier of the lazy diagonal. +* `Cslib.Complexity.lazyDiagonal`: the lazy diagonal problem for degree `d`. + +## Main results + +* `Cslib.Complexity.lazyDiagonal_mem_NTIME`: the lazy diagonal is in + `NTIME ((n + 1) ^ (6 * d + 14))`. +* `Cslib.Complexity.lazyDiagonal_notMem_NTIME`: the lazy diagonal is not in `NTIME ((n + 1) ^ d)`. +* `Cslib.Complexity.NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le`: the hierarchy. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, web draft of January + 2007][AroraBarak07] +* [S. Žák, *A Turing machine time hierarchy*][Zak1983] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Universal + +namespace LazyDiagonal + +/-- The certificate length of the lazy diagonal on words of length `m`: `(m + 1) ^ (d + 2)`. -/ +def certLen (d m : ℕ) : ℕ := (m + 1) ^ (d + 2) + +/-- The clock of the lazy diagonal on words of length `m`: `(m + 1) ^ (d + 3)`. It bounds the +simulated steps on `m`, and the interval of lengths starting at `m` ends below `2 ^ clock d m`. -/ +def clock (d m : ℕ) : ℕ := (m + 1) ^ (d + 3) + +/-- The machine described by `c`, run as a verifier on the pair `(y, v)` (encoded as +`frame y ++ v`) for `clock d y.length` steps with the universal function, has halted with output +`[true]`. -/ +def accepts (d : ℕ) (c y v : List Bool) : Bool := + !Diagonal.verdict (universal (decodeDesc c, (frame y ++ v).map eBit, clock d y.length)) + +/-- **The verifier of the lazy diagonal**, on an input `x` and a certificate `v`. The input carries +a word `w` framed at its start, and `w` carries the description `unframe w` framed at its start. +When the description is short (`Cslib.Complexity.Diagonal.shortDesc`), the lengths from +`P = 2 * w.length + 1` to `2 ^ clock d P - 1` form an interval: + +* below its end, accept when the described verifier accepts `v` on the input one bit longer; +* at its end, accept when the described verifier accepts no certificate on `frame w`, the input of + length `P`, by trying them all; +* elsewhere, reject. -/ +def verifier (d : ℕ) (p : List Bool × List Bool) : Bool := + if Diagonal.shortDesc (unframe p.1) then + if Nat.size (p.1.length + 1) ≤ clock d (2 * (unframe p.1).length + 1) then + accepts d (unframe (unframe p.1)) (p.1 ++ [false]) p.2 + else if Nat.size p.1.length ≤ clock d (2 * (unframe p.1).length + 1) then + !(Cslib.BitString.enumList (certLen d (2 * (unframe p.1).length + 1))).any + (accepts d (unframe (unframe p.1)) (frame (unframe p.1))) + else false + else false + +end LazyDiagonal + +open LazyDiagonal + +/-- **The lazy diagonal language** for degree `d`: the words `x` with a certificate of length +`(x.length + 2) ^ (d + 2)` accepted by `Cslib.Complexity.LazyDiagonal.verifier d`. -/ +def lazyDiagonal (d : ℕ) : Set (List Bool) := + {x | ∃ v : List Bool, v.length = certLen d (x.length + 1) ∧ verifier d (x, v) = true} + +/-! ### The lazy diagonal is not in `NTIME ((n + 1) ^ d)` -/ + +/-- The lengths at which certificates of length `certLen d m` and `clock d m` simulated steps +suffice for a verifier with constants `c` and `c₂`. -/ +private theorem exists_le_certLen_clock (d c c₂ : ℕ) : ∃ M, ∀ m, M ≤ m → + c * (m + 1) ^ d + c ≤ certLen d m ∧ c₂ * (2 * m + 1 + certLen d m + 1) ≤ clock d m := by + refine ⟨2 * c + 3 * c₂, fun m hm => ⟨?_, ?_⟩⟩ + · have hX : 1 ≤ (m + 1) ^ d := Nat.one_le_pow _ _ (by omega) + have e : certLen d m = (m + 1) ^ d * ((m + 1) * (m + 1)) := by + simp only [certLen]; ring + rw [e] + have : 2 * c ≤ (m + 1) * (m + 1) := by nlinarith + nlinarith + · have hX : 1 ≤ (m + 1) ^ d := Nat.one_le_pow _ _ (by omega) + have e₁ : certLen d m = (m + 1) ^ d * ((m + 1) * (m + 1)) := by + simp only [certLen]; ring + have e₂ : clock d m = (m + 1) ^ d * ((m + 1) * (m + 1)) * (m + 1) := by + simp only [clock]; ring + rw [e₁, e₂] + set Y := (m + 1) ^ d * ((m + 1) * (m + 1)) + have hY : 2 * m + 2 ≤ 2 * Y := by + have h₁ : m + 1 ≤ (m + 1) * (m + 1) := Nat.le_mul_of_pos_left _ (by omega) + have h₂ : (m + 1) * (m + 1) ≤ Y := Nat.le_mul_of_pos_left _ hX + omega + have : c₂ * (2 * m + 1 + Y + 1) ≤ c₂ * (3 * Y) := Nat.mul_le_mul_left _ (by omega) + nlinarith + +/-- **The lazy diagonal is not decidable in nondeterministic time `O((n + 1) ^ d)`.** A +nondeterministic machine deciding it has a verifier on pairs within linear time +(`Cslib.Complexity.exists_verifier_of_mem_NTIME`), described by a word `code`. On the interval of +lengths of `w = frame code ++ pad` with a long enough `pad`, the universal function runs that +verifier exactly. Each word of the interval is then in the language exactly when the next one is, +and the last exactly when the first is not. -/ +theorem lazyDiagonal_notMem_NTIME (d : ℕ) : + lazyDiagonal d ∉ NTIME encBits fun n => (n + 1) ^ d := by + intro hD + obtain ⟨V, c, hV, hmem⟩ := exists_verifier_of_mem_NTIME hD + obtain ⟨c₂, ⟨k, State, hfin, tm, htm⟩, -⟩ := hV + have := Fintype.ofFinite State + let eS : State ↪ ℕ := (Fintype.equivFin State).toEmbedding.trans Fin.valEmbedding + set code := eDesc (desc eS eBit tm) with hcode + obtain ⟨M, hM⟩ := exists_le_certLen_clock d c c₂ + -- the universal function runs the verifier exactly on long enough words + have hsim (y v : List Bool) (hy : M ≤ y.length) (hv : v.length = certLen d y.length) : + accepts d code y v = V (y, v) := by + have hclock : c₂ * ((encPair encBits encBits (y, v)).length + 1) ≤ clock d y.length := by + have := (hM y.length hy).2 + simp only [encPair_apply, encBits_apply, List.length_append, length_frame, hv] + omega + obtain ⟨hhalt, hout⟩ := (htm (y, v)).runFrom_of_le hclock + simp only [encPair_apply, encBits_apply, encBool_apply] at hhalt hout + rw [accepts, hcode, decodeDesc_eDesc, universal_desc, hout] + simp only [List.map_cons, List.map_nil, Cfg.Halted] at hhalt ⊢ + rw [hhalt] + cases V (y, v) <;> simp [Diagonal.verdict, eBit] + -- on long enough words, membership is acceptance by the simulated verifier + have hiff (y : List Bool) (hy : M ≤ y.length) : y ∈ lazyDiagonal d ↔ + ∃ v : List Bool, v.length = certLen d y.length ∧ accepts d code y v = true := by + have h := hmem y (certLen d y.length) (by simpa [encBits_apply] using (hM y.length hy).1) + rw [h] + exact exists_congr fun v => and_congr_right fun hv => by rw [hsim y v hy hv] + -- the interval of `w` + set w := frame code ++ List.replicate (2 ^ code.length + M) true with hw + set P := 2 * w.length + 1 with hP + set E := clock d P with hE + set x : ℕ → List Bool := fun m => frame w ++ List.replicate (m - P) false with hx + have hwlen : w.length = 2 * code.length + 1 + (2 ^ code.length + M) := by + simp [w] + have hMP : M ≤ P := by + have := hwlen + generalize 2 ^ code.length = e at this + omega + have hxlen (m : ℕ) (hm : P ≤ m) : (x m).length = m := by + simp only [x, List.length_append, length_frame, List.length_replicate] + omega + have hshort : Diagonal.shortDesc w = true := by + have hc : unframe w = code := unframe_frame_append _ _ + rw [Diagonal.shortDesc, decide_eq_true_eq, hc, hwlen] + omega + have hverifier (m : ℕ) (hm : P ≤ m) (v : List Bool) : verifier d (x m, v) = + if Nat.size (m + 1) ≤ E then accepts d code (x m ++ [false]) v + else if Nat.size m ≤ E then + !(Cslib.BitString.enumList (certLen d P)).any (accepts d code (frame w)) + else false := by + have hu : unframe (x m) = w := unframe_frame_append _ _ + have hc : unframe w = code := unframe_frame_append _ _ + simp only [verifier, hu, hc, hshort, hxlen m hm, ← hP, ← hE, ↓reduceIte] + have hPE : P + 1 < 2 ^ E := by + have : P + 1 ≤ E := by + simp only [hE, clock] + exact (Nat.le_self_pow (by omega) _) + exact this.trans_lt Nat.lt_two_pow_self + set U := 2 ^ E - 1 with hU + -- each word below the end of the interval is in the language exactly when the next one is + have hstep (m : ℕ) (hm : P ≤ m) (hmU : m < U) : + x m ∈ lazyDiagonal d ↔ x (m + 1) ∈ lazyDiagonal d := by + have hsize : Nat.size (m + 1) ≤ E := Nat.size_le.mpr (by omega) + have hnext : x m ++ [false] = x (m + 1) := by + simp only [x, List.append_assoc, ← List.replicate_succ'] + congr 2 + omega + rw [hiff (x (m + 1)) (by rw [hxlen _ (by omega)]; omega), lazyDiagonal, Set.mem_ofPred_eq, + hxlen (m + 1) (by omega), hxlen m hm] + refine exists_congr fun v => and_congr_right fun _ => ?_ + simp only [hverifier m hm v, hsize, ↓reduceIte, hnext] + -- the end of the interval is in the language exactly when its start is not + have hend : x U ∈ lazyDiagonal d ↔ x P ∉ lazyDiagonal d := by + have hUP : P ≤ U := by omega + have hsize₁ : ¬Nat.size (U + 1) ≤ E := by + rw [Nat.size_le, hU, Nat.sub_add_cancel Nat.one_le_two_pow] + exact lt_irrefl _ + have hsize₂ : Nat.size U ≤ E := Nat.size_le.mpr (by omega) + have hbase : x P = frame w := by simp [x] + rw [hiff (x P) (by rw [hxlen P le_rfl]; omega), hxlen P le_rfl, hbase, lazyDiagonal, + Set.mem_ofPred_eq] + simp only [hverifier U hUP, hsize₁, hsize₂, ↓reduceIte, Bool.not_eq_true', + List.any_eq_false, Cslib.BitString.mem_enumList, not_exists, not_and, Bool.not_eq_true] + constructor + · rintro ⟨-, -, h⟩ v hv + exact h v hv + · intro h + exact ⟨List.replicate _ false, List.length_replicate .., h⟩ + -- the chain from the start of the interval to its end + have hchain (j : ℕ) (hj : j ≤ U - P) : x (U - j) ∈ lazyDiagonal d ↔ x U ∈ lazyDiagonal d := by + induction j with + | zero => rfl + | succ j ih => + rw [← ih (by omega), hstep (U - (j + 1)) (by omega) (by omega)] + congr! 2 + omega + have h := hchain (U - P) le_rfl + rw [Nat.sub_sub_self (by omega), hend] at h + exact iff_not_self h + +/-! ### The lazy diagonal is in nondeterministic polynomial time -/ + +/-- The bound on the simulation of `Cslib.Complexity.LazyDiagonal.accepts`, for a decoder of +degree below `D`. -/ +private def accBound (d D : ℕ) (q : List Bool × List Bool × List Bool) : ℕ := + ((q.1.length + 1) ^ D + q.2.1.length + q.2.2.length + 1) ^ 4 * (q.2.1.length + 1) ^ (2 * d + 6) + +/-- The binary length of the clock is linear in the length of the input. -/ +private theorem length_encNat_clock_le (d y : ℕ) : + (encNat ((y + 1) ^ (d + 3))).length ≤ (d + 3) * (y + 1) := by + rw [encNat_apply, Nat.size_eq_bits_len, Nat.size_le, mul_comm, pow_mul] + exact Nat.pow_lt_pow_left Nat.lt_two_pow_self (by omega) + +/-- The numeric core of the resources of the simulation: for an encoded input of length `N`, a +decoding time `A`, a word `W = frame y ++ v`, a decoded description of encoded length `Dl`, encoded +symbols of length `Nl`, a clock `Y` of `Ll` binary digits and a result of encoded length `E`, +everything is within `K * X ^ 4 * Y ^ 2`. -/ +private theorem accBound_aux (d cD cO : ℕ) : ∃ K, ∀ {N A W Dl Nl Ll X Y E : ℕ}, + N ≤ 2 * X → A ≤ X → W ≤ 2 * X → Dl ≤ cD * (N + A + 1) → Nl ≤ 3 * W → + Ll ≤ (d + 4) * X → 1 ≤ X → 1 ≤ Y → + E ≤ cO * (N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) + 1) → + N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 4 * (Y + 1) ^ 2 + + (E + 1) ^ 2 + 1 ≤ K * (X ^ 4 * Y ^ 2) ∧ + N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) + E + 1 ≤ + K * (X ^ 4 * Y ^ 2) := by + set C₁ := 8 * cD + d + 19 + set C₂ := 11 + 2 * C₁ ^ 2 + refine ⟨10 + 4 * C₁ ^ 4 + (cO * C₂ + 1) ^ 2 + 1 + C₂ * (cO + 1), + fun {N A W Dl Nl Ll X Y E} hN hA hW hD hNl hLl hX hY hE => ?_⟩ + have hIn : 2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1 ≤ C₁ * X := by + have h₁ : cD * (N + A + 1) ≤ cD * (4 * X) := Nat.mul_le_mul_left _ (by omega) + have h₂ : (d + 4) * X = d * X + 4 * X := by ring + have h₃ : d * X ≤ d * X := le_rfl + have e : C₁ * X = 8 * (cD * X) + d * X + 19 * X := by simp only [C₁]; ring + have e' : cD * (4 * X) = 4 * (cD * X) := by ring + omega + have hXY : X * Y ≤ X ^ 2 * Y := Nat.mul_le_mul_right _ (Nat.le_self_pow (by norm_num) _) + have hX2Y : X ^ 2 * Y ≤ X ^ 4 * Y ^ 2 := + Nat.mul_le_mul (Nat.pow_le_pow_right hX (by norm_num)) (Nat.le_self_pow (by norm_num) _) + have hpre : N + A + (N + W + (N + Y)) ≤ 10 * (X * Y) := by + have h₁ : X ≤ X * Y := Nat.le_mul_of_pos_right _ hY + have h₂ : Y ≤ X * Y := Nat.le_mul_of_pos_left _ hX + omega + have hY1 : Y + 1 ≤ 2 * Y := by omega + have hU₂ : (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) ≤ 2 * C₁ ^ 2 * (X ^ 2 * Y) := + calc _ ≤ (C₁ * X) ^ 2 * (2 * Y) := Nat.mul_le_mul (Nat.pow_le_pow_left hIn 2) hY1 + _ = 2 * C₁ ^ 2 * (X ^ 2 * Y) := by ring + have hU₄ : (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 4 * (Y + 1) ^ 2 ≤ + 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) := + calc _ ≤ (C₁ * X) ^ 4 * (2 * Y) ^ 2 := + Nat.mul_le_mul (Nat.pow_le_pow_left hIn 4) (Nat.pow_le_pow_left hY1 2) + _ = 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) := by ring + have hS : N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) + 1 ≤ + C₂ * (X ^ 2 * Y) := by + have h₁ : 1 ≤ X ^ 2 * Y := Nat.mul_pos (Nat.pow_pos hX) hY + have e : C₂ * (X ^ 2 * Y) = 11 * (X ^ 2 * Y) + 2 * C₁ ^ 2 * (X ^ 2 * Y) := by + simp only [C₂]; ring + omega + have hE' : E ≤ cO * C₂ * (X ^ 2 * Y) := + hE.trans ((Nat.mul_le_mul_left cO hS).trans_eq (by ring)) + have hE2 : (E + 1) ^ 2 ≤ (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) := by + have h₁ : 1 ≤ X ^ 2 * Y := Nat.mul_pos (Nat.pow_pos hX) hY + have h₂ : E + 1 ≤ (cO * C₂ + 1) * (X ^ 2 * Y) := by + have e : (cO * C₂ + 1) * (X ^ 2 * Y) = cO * C₂ * (X ^ 2 * Y) + X ^ 2 * Y := by ring + omega + calc (E + 1) ^ 2 ≤ ((cO * C₂ + 1) * (X ^ 2 * Y)) ^ 2 := Nat.pow_le_pow_left h₂ 2 + _ = (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) := by ring + have h1 : 1 ≤ X ^ 4 * Y ^ 2 := Nat.mul_pos (Nat.pow_pos hX) (Nat.pow_pos hY) + have hXYW : X * Y ≤ X ^ 4 * Y ^ 2 := hXY.trans hX2Y + have hU₂' := hU₂.trans (Nat.mul_le_mul_left (2 * C₁ ^ 2) hX2Y) + constructor + · have e : (10 + 4 * C₁ ^ 4 + (cO * C₂ + 1) ^ 2 + 1 + C₂ * (cO + 1)) * (X ^ 4 * Y ^ 2) = + 10 * (X ^ 4 * Y ^ 2) + 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) + + (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) + X ^ 4 * Y ^ 2 + + C₂ * (cO + 1) * (X ^ 4 * Y ^ 2) := by + ring + have := Nat.mul_le_mul_left 10 hXYW + omega + · have e : (10 + 4 * C₁ ^ 4 + (cO * C₂ + 1) ^ 2 + 1 + C₂ * (cO + 1)) * (X ^ 4 * Y ^ 2) = + 10 * (X ^ 4 * Y ^ 2) + 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) + + (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) + X ^ 4 * Y ^ 2 + + (C₂ * (X ^ 4 * Y ^ 2) + cO * C₂ * (X ^ 4 * Y ^ 2)) := by + ring + have h₁ := Nat.mul_le_mul_left C₂ hX2Y + have h₂ := Nat.mul_le_mul_left (cO * C₂) hX2Y + omega + +/-- The simulation runs within time polynomial in the description, the input and the +certificate. -/ +private theorem exists_computableInO_accepts (d : ℕ) : ∃ D, ComputableInO + (fun q : List Bool × List Bool × List Bool => accepts d q.1 q.2.1 q.2.2) + (encPair encBits (encPair encBits encBits)) encBool (accBound d D) (accBound d D) := by + obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc + set enc := encPair encBits (encPair encBits encBits) + have hdesc := hdec.inO.comp (ComputableInO.fst encBits (encPair encBits encBits)) + have hword : ComputableInO (fun q : List Bool × List Bool × List Bool => frame q.2.1 ++ q.2.2) + enc encBits (fun q => (enc q).length) (fun q => (enc q).length) := + (ComputableInO.snd encBits (encPair encBits encBits)).of_enc_eq fun _ => rfl + have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one.computableInO.comp hword + have hy := (ComputableInO.snd encBits (encPair encBits encBits)).fst' + have hclock := (timeConstructible_succ_pow (k := d + 3) (by omega)).computableInO.comp hy + have hU := computableInO_universal.comp (hdesc.prod (hsym.prod hclock)) + have hv := Diagonal.computableInO_verdict.comp hU + have hnot := (ComputableInDegree.of_finite (encIn := encBool) (encMid := encBool) + (fun b : Bool => !b)).inO_one.comp hv + obtain ⟨cD, hcD⟩ := hdesc.length_le + obtain ⟨cO, hcO⟩ := hU.length_le + obtain ⟨K, hK⟩ := accBound_aux d cD cO + have hbounds (q : List Bool × List Bool × List Bool) := by + have hD := hcD q + have hE := hcO q + have hNl : (encList encUnary ((frame q.2.1 ++ q.2.2).map eBit)).length ≤ + 3 * (frame q.2.1 ++ q.2.2).length := + (length_encList_le encUnary _ (b := 1) fun s hs => by + obtain ⟨b, -, rfl⟩ := List.mem_map.mp hs + cases b + · exact Nat.zero_le _ + · exact le_rfl).trans (by rw [List.length_map]; omega) + have hc : q.1.length + 1 ≤ (q.1.length + 1) ^ (dd + 1) := + Nat.le_self_pow (by omega) _ + have hA : (q.1.length + 1) ^ dd ≤ (q.1.length + 1) ^ (dd + 1) := + Nat.pow_le_pow_right (by omega) (by omega) + have hL := length_encNat_clock_le d q.2.1.length + simp only [Function.comp_apply, encBits_apply, enc, length_encPair, List.length_append, + length_frame] at hD hE hNl ⊢ + refine hK (X := (q.1.length + 1) ^ (dd + 1) + q.2.1.length + q.2.2.length + 1) + (by omega) (by omega) (by omega) hD hNl ?_ (by omega) (Nat.one_le_pow _ _ (by omega)) hE + have : (d + 3) * (q.2.1.length + 1) ≤ (d + 4) * (q.2.1.length + 1) := + Nat.mul_le_mul_right _ (by omega) + have : (d + 4) * (q.2.1.length + 1) ≤ + (d + 4) * ((q.1.length + 1) ^ (dd + 1) + q.2.1.length + q.2.2.length + 1) := + Nat.mul_le_mul_left _ (by omega) + omega + have e (q : List Bool × List Bool × List Bool) : accBound d (dd + 1) q = + ((q.1.length + 1) ^ (dd + 1) + q.2.1.length + q.2.2.length + 1) ^ 4 * + ((q.2.1.length + 1) ^ (d + 3)) ^ 2 := by + rw [accBound, ← pow_mul, show (d + 3) * 2 = 2 * d + 6 by ring] + have hb (b : Bool) : (encBool b).length = 1 := rfl + refine ⟨dd + 1, (hnot.mono K (fun q => ?_) fun q => ?_).of_enc_eq fun q => rfl⟩ + · refine le_trans ?_ (Nat.mul_le_mul_left K (Nat.le_succ _)) + rw [e] + have h := (hbounds q).1 + simp only [Function.comp_apply, encBits_apply, enc, length_encPair, List.length_append, + length_frame] at ⊢ + simp only [hb] at h ⊢ + omega + · refine le_trans ?_ (Nat.mul_le_mul_left K (Nat.le_succ _)) + rw [e] + have h := (hbounds q).2 + simp only [Function.comp_apply, encBits_apply, enc, length_encPair, List.length_append, + length_frame] at ⊢ + simp only [hb] at h ⊢ + omega + +attribute [local fun_prop] ComputableInPolyTime.fst' ComputableInPolyTime.snd' in +/-- The brute force at the end of an interval runs within time exponential in the description, +the input and the certificate length. -/ +private theorem exists_computableInO_brute (d : ℕ) : ∃ K, ComputableInO + (fun q : List Bool × List Bool => + (Cslib.BitString.enumList (certLen d q.2.length)).any (accepts d q.1 q.2)) + (encPair encBits encBits) encBool + (fun q => 2 ^ (K * ((encPair encBits encBits q).length + certLen d q.2.length))) + (fun q => 2 ^ (K * ((encPair encBits encBits q).length + certLen d q.2.length))) := by + obtain ⟨D, hacc⟩ := exists_computableInO_accepts d + set enc := encPair (encPair encBits encBits) encBits + have hre := ((ComputableInO.fst (encPair encBits encBits) encBits).fst').prod + (((ComputableInO.fst (encPair encBits encBits) encBits).snd').prod + (ComputableInO.snd (encPair encBits encBits) encBits)) + have hf := hacc.comp hre + have hsize (q : (List Bool × List Bool) × List Bool) : + q.1.1.length ≤ (enc q).length ∧ q.1.2.length ≤ (enc q).length ∧ + q.2.length ≤ (enc q).length := by + simp only [enc, length_encPair, encBits_apply] + omega + have hpoly : PolyBounded (fun q => (enc q).length) fun q => + (enc q).length + ((enc q).length + (enc q).length) + + accBound d D (q.1.1, q.1.2, q.2) := + ((PolyBounded.self.add (PolyBounded.self.add .self)).add + ((PolyBounded.of_polynomiallyBounded (fun q => (enc q).length) + (bound := fun n => ((n + 1) ^ D + n + n + 1) ^ 4 * (n + 1) ^ (2 * d + 6)) + (by fun_prop)).mono fun q => by + obtain ⟨h₁, h₂, h₃⟩ := hsize q + simp only [accBound] + gcongr)) + have hℓ : ComputableInPolyTime (fun q : List Bool × List Bool => certLen d q.2.length) + (encPair encBits encBits) encUnary := by + unfold certLen + fun_prop + exact exists_computableInO_any_enumList hf hpoly hpoly hℓ + +/-- Weaken only the time bound, keeping the space bound. -/ +private theorem _root_.Turing.MultiTapeTM.ComputableInO.mono_time {α β : Type*} {f : α → β} + {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' : α → ℕ} + (h : ComputableInO f encIn encOut T S) (k : ℕ) (hT : ∀ a, T a ≤ k * (T' a + 1)) : + ComputableInO f encIn encOut T' S := + h.mono (k + 1) (fun a => (hT a).trans (Nat.mul_le_mul_right _ (Nat.le_succ k))) + fun _ => (Nat.le_succ _).trans (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) + +/-- The cost of the tests of the verifier: quadratic in the encoded input, times a power of the +length of the input that pays for the clock in unary. -/ +private def cheap (d : ℕ) (p : List Bool × List Bool) : ℕ := + ((encPair encBits encBits p).length + 1) ^ 2 * ((p.1.length + 1) ^ (d + 3)) ^ 2 + +/-- The numeric facts behind `cheap`, for an encoded input of length `N`, an input of length `n` +and a clock `Z` of at most `G * Y`. -/ +private theorem cheap_aux (G : ℕ) {N n Z Y : ℕ} (hn : n ≤ N) (hY : 1 ≤ Y) (hZ : Z ≤ G * Y) : + N + 1 ≤ (N + 1) ^ 2 * Y ^ 2 ∧ (Z + 1) ^ 2 ≤ (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) ∧ + (2 * N + 4 + Z) ^ 2 ≤ (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) := by + have hY2 : 1 ≤ Y ^ 2 := Nat.one_le_pow _ _ hY + have hN2 : N + 1 ≤ (N + 1) ^ 2 := Nat.le_self_pow (by norm_num) _ + have hsq : (2 * N + 4 + Z) ^ 2 ≤ (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) := + calc (2 * N + 4 + Z) ^ 2 ≤ ((G + 4) * ((N + 1) * Y)) ^ 2 := by + apply Nat.pow_le_pow_left + have h₁ : N + 1 ≤ (N + 1) * Y := Nat.le_mul_of_pos_right _ hY + have h₂ : Y ≤ (N + 1) * Y := Nat.le_mul_of_pos_left _ (by omega) + have e : (G + 4) * ((N + 1) * Y) = G * ((N + 1) * Y) + 4 * ((N + 1) * Y) := by ring + have := Nat.mul_le_mul_left G h₂ + omega + _ = (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) := by ring + refine ⟨hN2.trans (Nat.le_mul_of_pos_right _ hY2), + (Nat.pow_le_pow_left (by omega) 2).trans hsq, hsq⟩ + +/-- **The verifier of the lazy diagonal is computable**, within the cost of its tests plus the +cost of the branch taken: the simulation, or the brute force at the end of an interval. -/ +private theorem exists_computableInO_verifier (d : ℕ) : + ∃ (D K : ℕ) (S : List Bool × List Bool → ℕ), + ComputableInO (verifier d) (encPair encBits encBits) encBool + (fun p => cheap d p + if Diagonal.shortDesc (unframe p.1) then + (cheap d p + if Nat.size (p.1.length + 1) ≤ clock d (2 * (unframe p.1).length + 1) then + cheap d p + accBound d D (unframe (unframe p.1), p.1 ++ [false], p.2) + else (cheap d p + if Nat.size p.1.length ≤ clock d (2 * (unframe p.1).length + 1) then + cheap d p + 2 ^ (K * ((encPair encBits encBits (unframe (unframe p.1), + frame (unframe p.1))).length + certLen d (2 * (unframe p.1).length + 1))) + else cheap d p)) + else cheap d p) S := by + obtain ⟨D, hacc⟩ := exists_computableInO_accepts d + obtain ⟨K, hbrute⟩ := exists_computableInO_brute d + have hx := ComputableInO.fst encBits encBits + have hun : ComputableInO unframe encBits encBits (fun z => z.length) (fun z => z.length) := + ComputableInO.of_linear (.of_unframe fun _ => rfl) + have hfr : ComputableInO frame encBits encBits (fun z => z.length) (fun z => z.length) := + ComputableInO.of_linear (.of_frame fun _ => rfl) + have hw := hun.comp hx + have hcode := hun.comp hw + have hbase := hfr.comp hw + have hsnoc : ComputableInO (fun p : List Bool × List Bool => p.1 ++ [false]) + (encPair encBits encBits) encBits + (fun p => (encPair encBits encBits p).length + (encPair encBits encBits p).length) + (fun p => (encPair encBits encBits p).length + (encPair encBits encBits p).length) := + hx.append (ComputableInO.const (encMid := encBits) [false]) fun _ => rfl + have hsz : ComputableInO (fun z : List Bool => Nat.size z.length) encBits encUnary + (fun z => (z.length + 1) ^ 2 + (encNat z.length).length) + (fun z => z.length + 1 + (encNat z.length).length) := + (ComputableInO.lengthUnary.comp (ComputableInO.lengthNat.of_enc_eq (encC := encBits) + (g := fun z : List Bool => encNat z.length) fun _ => rfl)).of_enc_eq fun z => by + simp [encNat_apply, Nat.size_eq_bits_len] + have hE := ComputableInO.natToUnary.comp + ((timeConstructible_succ_pow (k := d + 3) (by omega)).computableInO.comp hbase) + -- the numeric facts about the tests + set G := 2 ^ (d + 3) + have hfacts (p : List Bool × List Bool) : (unframe p.1).length ≤ p.1.length ∧ + p.1.length ≤ (encPair encBits encBits p).length ∧ + (encPair encBits encBits p).length + 1 ≤ cheap d p ∧ + ((2 * (unframe p.1).length + 1 + 1) ^ (d + 3) + 1) ^ 2 ≤ (G + 4) ^ 2 * cheap d p ∧ + (2 * (encPair encBits encBits p).length + 4 + + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3)) ^ 2 ≤ (G + 4) ^ 2 * cheap d p := by + have hu := length_unframe_le p.1 + have hn : p.1.length ≤ (encPair encBits encBits p).length := by + simp only [length_encPair, encBits_apply] + omega + have hZ : (2 * (unframe p.1).length + 1 + 1) ^ (d + 3) ≤ + 2 ^ (d + 3) * (p.1.length + 1) ^ (d + 3) := by + rw [← mul_pow] + exact Nat.pow_le_pow_left (by omega) _ + exact ⟨hu, hn, cheap_aux G hn (Nat.one_le_pow _ _ (by omega)) hZ⟩ + have e (p : List Bool × List Bool) : (8 + 4 * (G + 4) ^ 2) * (cheap d p + 1) = + 8 * cheap d p + 4 * ((G + 4) ^ 2 * cheap d p) + (8 + 4 * (G + 4) ^ 2) := by ring + have hc₀ := (Diagonal.computableInO_shortDesc.comp hw).mono_time (T' := cheap d) + (8 + 4 * (G + 4) ^ 2) fun p => by + obtain ⟨hu, hn, h₁, -, h₃⟩ := hfacts p + have : ((unframe p.1).length + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + simp only [Function.comp_apply] at ⊢ + have := e p + omega + have hc₁ := (ComputableInO.unaryLe.comp ((hsz.comp hsnoc).prod hE)).mono_time + (T' := cheap d) (8 + 4 * (G + 4) ^ 2) fun p => by + obtain ⟨hu, hn, h₁, h₂, h₃⟩ := hfacts p + have hs := Nat.size_le.mpr (Nat.lt_two_pow_self (n := p.1.length + 1)) + have he := Universal.length_encNat_le (p.1.length + 1) + have hsq : (p.1.length + 1 + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hsq' : (2 * Nat.size (p.1.length + 1) + 1 + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3) + + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3)) ^ 2 := + Nat.pow_le_pow_left (by omega) 2 + have hZ : (2 * (unframe p.1).length + 1 + 1) ^ (d + 3) ≤ + ((2 * (unframe p.1).length + 1 + 1) ^ (d + 3) + 1) ^ 2 := by + nlinarith [Nat.le_self_pow (n := 2) (by norm_num) + ((2 * (unframe p.1).length + 1 + 1) ^ (d + 3) + 1)] + simp only [Function.comp_apply, length_encPair (enc₁ := encUnary) (enc₂ := encUnary), + encUnary_apply, List.length_replicate, List.length_append, List.length_singleton, + length_frame] at ⊢ + have := e p + omega + have hc₂ := (ComputableInO.unaryLe.comp ((hsz.comp hx).prod hE)).mono_time + (T' := cheap d) (8 + 4 * (G + 4) ^ 2) fun p => by + obtain ⟨hu, hn, h₁, h₂, h₃⟩ := hfacts p + have hs := Nat.size_le.mpr (Nat.lt_two_pow_self (n := p.1.length)) + have he := Universal.length_encNat_le p.1.length + have hsq : (p.1.length + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hsq' : (2 * Nat.size p.1.length + 1 + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3) + + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + (2 * (unframe p.1).length + 1 + 1) ^ (d + 3)) ^ 2 := + Nat.pow_le_pow_left (by omega) 2 + have hZ : (2 * (unframe p.1).length + 1 + 1) ^ (d + 3) ≤ + ((2 * (unframe p.1).length + 1 + 1) ^ (d + 3) + 1) ^ 2 := by + nlinarith [Nat.le_self_pow (n := 2) (by norm_num) + ((2 * (unframe p.1).length + 1 + 1) ^ (d + 3) + 1)] + simp only [Function.comp_apply, length_encPair (enc₁ := encUnary) (enc₂ := encUnary), + encUnary_apply, List.length_replicate, length_frame] at ⊢ + have := e p + omega + have hc₁' := hc₁.of_enc_eq (encC := encBool) (g := fun p : List Bool × List Bool => + decide (Nat.size (p.1.length + 1) ≤ clock d (2 * (unframe p.1).length + 1))) fun p => by + simp only [Function.comp_apply, clock, length_frame, List.length_append, + List.length_singleton] + rfl + have hc₂' := hc₂.of_enc_eq (encC := encBool) (g := fun p : List Bool × List Bool => + decide (Nat.size p.1.length ≤ clock d (2 * (unframe p.1).length + 1))) fun p => by + simp only [Function.comp_apply, clock, length_frame] + rfl + have hf₁ := (hacc.comp (hcode.prod (hsnoc.prod (ComputableInO.snd encBits encBits)))).mono_time + (T' := fun p => cheap d p + accBound d D (unframe (unframe p.1), p.1 ++ [false], p.2)) 7 + fun p => by + obtain ⟨hu, hn, h₁, -⟩ := hfacts p + simp only [Function.comp_apply] at ⊢ + have e : 7 * (cheap d p + accBound d D (unframe (unframe p.1), p.1 ++ [false], p.2) + 1) = + 7 * cheap d p + 7 * accBound d D (unframe (unframe p.1), p.1 ++ [false], p.2) + 7 := by + ring + omega + have hf₂ := ((ComputableInDegree.of_finite (encIn := encBool) (encMid := encBool) + (fun b : Bool => !b)).inO_one.comp (hbrute.comp (hcode.prod hbase))).mono_time + (T' := fun p => cheap d p + 2 ^ (K * ((encPair encBits encBits (unframe (unframe p.1), + frame (unframe p.1))).length + certLen d (2 * (unframe p.1).length + 1)))) 7 + fun p => by + obtain ⟨hu, hn, h₁, -⟩ := hfacts p + have hb : (encBool ((Cslib.BitString.enumList (certLen d (frame (unframe p.1)).length)).any + (accepts d (unframe (unframe p.1)) (frame (unframe p.1))))).length = 1 := rfl + simp only [Function.comp_apply, hb] at ⊢ + rw [length_frame] + set B := 2 ^ (K * ((encPair encBits encBits (unframe (unframe p.1), + frame (unframe p.1))).length + certLen d (2 * (unframe p.1).length + 1))) + have e : 7 * (cheap d p + B + 1) = 7 * cheap d p + 7 * B + 7 := by ring + omega + have hfalse := (ComputableInO.const (encIn := encPair encBits encBits) (encMid := encBool) + false).mono_time (T' := cheap d) 1 fun p => by + obtain ⟨hu, hn, h₁, -⟩ := hfacts p + omega + have h := hc₀.ite (hc₁'.ite hf₁ (hc₂'.ite hf₂ hfalse)) hfalse + refine ⟨D, K, _, (h.of_enc_eq fun p => ?_).mono_le (fun p => le_of_eq ?_) fun p => le_rfl⟩ + · congr 1 + simp only [verifier, Function.comp_apply, decide_eq_true_eq, length_frame] + · simp only [Function.comp_apply, decide_eq_true_eq] + +/-- **The lazy diagonal is decidable in nondeterministic time `O((n + 1) ^ (6 * d + 14))`.** Guess +a certificate of length `(n + 2) ^ (d + 2)` and run the verifier +(`Cslib.Complexity.setOf_exists_mem_NTIME`). Below the end of an interval, the verifier simulates +a verifier on the input one bit longer with a certificate of that length, within time polynomial +in both. At the end of an interval of start `P`, it tries every certificate on the input of +length `P`, within time `2 ^ O((P + 1) ^ (d + 2))`, which is linear in the length `n` of the +input, since `n + 1 = 2 ^ ((P + 1) ^ (d + 3))` there. -/ +theorem lazyDiagonal_mem_NTIME (d : ℕ) : + lazyDiagonal d ∈ NTIME encBits fun n => (n + 1) ^ (6 * d + 14) := by + obtain ⟨D, K, S, hV⟩ := exists_computableInO_verifier d + have hsnoc : ComputableInO (fun x : List Bool => x ++ [false]) encBits encBits + (fun x => x.length + x.length) (fun x => x.length + x.length) := + (ComputableInO.of_eq (f := fun x : List Bool => x) (encIn := encBits) (encMid := encBits) + fun _ => rfl).append (ComputableInO.const (encMid := encBits) [false]) fun _ => rfl + have hℓ := (ComputableInO.natToUnary.comp + ((timeConstructible_succ_pow (k := d + 2) (by omega)).computableInO.comp hsnoc)).of_enc_eq + (encC := encUnary) (g := fun x : List Bool => certLen d (x.length + 1)) fun x => by + simp [certLen] + obtain ⟨CD, hCD⟩ := PolynomiallyBounded.exists_le_mul_two_pow (p := fun m => (m + 1) ^ D) + (by fun_prop) + set B₀ := 3 * K * (3 * K) ^ (d + 2) + set A₁ := 9 * 2 ^ (2 * d + 4) + set A₂ := (CD + 3) ^ 4 * 2 ^ (6 * d + 14) + set A₃ := 7 * 2 ^ (2 * d + 4) + refine setOf_exists_mem_NTIME hℓ hV (C := 2 + A₃ + 4 * A₁ + A₂ + 2 ^ B₀) fun x v hv => ?_ + simp only [encBits_apply] + set n := x.length with hn + have hv' : v.length = (n + 2) ^ (d + 2) := by + rw [hv] + rfl + set M := (n + 1) ^ (6 * d + 14) + have h2 (k : ℕ) : (n + 2) ^ k ≤ 2 ^ k * (n + 1) ^ k := by + rw [← mul_pow] + exact Nat.pow_le_pow_left (by omega) k + have hMk (k : ℕ) (hk : k ≤ 6 * d + 14) : (n + 1) ^ k ≤ M := Nat.pow_le_pow_right (by omega) hk + have hnM : n + 1 ≤ M := by simpa using hMk 1 (by omega) + -- the tests + have hcheap : cheap d (x, v) ≤ A₁ * M := by + have hN : (encPair encBits encBits (x, v)).length + 1 ≤ 3 * (n + 2) ^ (d + 2) := by + simp only [length_encPair, encBits_apply, hv'] + have : n + 2 ≤ (n + 2) ^ (d + 2) := Nat.le_self_pow (by omega) _ + omega + calc cheap d (x, v) = ((encPair encBits encBits (x, v)).length + 1) ^ 2 * + ((n + 1) ^ (d + 3)) ^ 2 := rfl + _ ≤ (3 * (n + 2) ^ (d + 2)) ^ 2 * ((n + 1) ^ (d + 3)) ^ 2 := + Nat.mul_le_mul_right _ (Nat.pow_le_pow_left hN 2) + _ = 9 * (n + 2) ^ (2 * d + 4) * (n + 1) ^ (2 * d + 6) := by ring + _ ≤ 9 * (2 ^ (2 * d + 4) * (n + 1) ^ (2 * d + 4)) * (n + 1) ^ (2 * d + 6) := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ (h2 _)) + _ = A₁ * (n + 1) ^ (4 * d + 10) := by ring + _ ≤ A₁ * M := Nat.mul_le_mul_left _ (hMk _ (by omega)) + -- the simulation, when the description is short + have hacc (h₀ : Diagonal.shortDesc (unframe x) = true) : + accBound d D (unframe (unframe x), x ++ [false], v) ≤ A₂ * M := by + have hs : 2 ^ (unframe (unframe x)).length ≤ (unframe x).length := of_decide_eq_true h₀ + have hu := length_unframe_le x + have hD : ((unframe (unframe x)).length + 1) ^ D ≤ CD * n := + (hCD _).trans (Nat.mul_le_mul_left _ (hs.trans hu)) + have hb : ((unframe (unframe x)).length + 1) ^ D + (n + 1) + (n + 2) ^ (d + 2) + 1 ≤ + (CD + 3) * (n + 2) ^ (d + 2) := by + have h₁ : n + 2 ≤ (n + 2) ^ (d + 2) := Nat.le_self_pow (by omega) _ + have h₂ : CD * n ≤ CD * (n + 2) ^ (d + 2) := Nat.mul_le_mul_left _ (by omega) + have e : (CD + 3) * (n + 2) ^ (d + 2) = CD * (n + 2) ^ (d + 2) + 3 * (n + 2) ^ (d + 2) := by + ring + omega + calc accBound d D (unframe (unframe x), x ++ [false], v) = + (((unframe (unframe x)).length + 1) ^ D + (n + 1) + (n + 2) ^ (d + 2) + 1) ^ 4 * + (n + 2) ^ (2 * d + 6) := by + simp only [accBound, List.length_append, List.length_singleton, hv', ← hn, add_assoc, + Nat.reduceAdd] + _ ≤ ((CD + 3) * (n + 2) ^ (d + 2)) ^ 4 * (n + 2) ^ (2 * d + 6) := + Nat.mul_le_mul_right _ (Nat.pow_le_pow_left hb 4) + _ = (CD + 3) ^ 4 * (n + 2) ^ (6 * d + 14) := by ring + _ ≤ (CD + 3) ^ 4 * (2 ^ (6 * d + 14) * M) := Nat.mul_le_mul_left _ (h2 _) + _ = A₂ * M := by ring + -- the brute force, at the end of an interval + have hbrute (h₁ : ¬Nat.size (n + 1) ≤ clock d (2 * (unframe x).length + 1)) : + 2 ^ (K * ((encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen d (2 * (unframe x).length + 1))) ≤ n + 1 + 2 ^ B₀ := by + set P := 2 * (unframe x).length + 1 with hP + have hE : 2 ^ clock d P ≤ n + 1 := by + rw [Nat.size_le, not_lt] at h₁ + exact h₁ + have hc := length_unframe_le (unframe x) + have hlen : (encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen d P ≤ 3 * (P + 1) ^ (d + 2) := by + simp only [length_encPair, encBits_apply, length_frame, certLen] + have : P + 1 ≤ (P + 1) ^ (d + 2) := Nat.le_self_pow (by omega) _ + omega + rcases le_or_gt (3 * K) (P + 1) with hK | hK + · have hle : K * ((encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen d P) ≤ clock d P := + calc _ ≤ K * (3 * (P + 1) ^ (d + 2)) := Nat.mul_le_mul_left _ hlen + _ = 3 * K * (P + 1) ^ (d + 2) := by ring + _ ≤ (P + 1) * (P + 1) ^ (d + 2) := Nat.mul_le_mul_right _ hK + _ = clock d P := by rw [clock]; ring + exact ((Nat.pow_le_pow_right (by norm_num) hle).trans hE).trans (Nat.le_add_right _ _) + · have hle : K * ((encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen d P) ≤ B₀ := + calc _ ≤ K * (3 * (P + 1) ^ (d + 2)) := Nat.mul_le_mul_left _ hlen + _ = 3 * K * (P + 1) ^ (d + 2) := by ring + _ ≤ 3 * K * (3 * K) ^ (d + 2) := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hK.le _) + exact (Nat.pow_le_pow_right (by norm_num) hle).trans (Nat.le_add_left _ _) + -- the certificate length + have hTℓ : n + n + ((x ++ [false]).length + 1) ^ (d + 2) + + (((fun x : List Bool => (x.length + 1) ^ (d + 2)) ∘ fun x => x ++ [false]) x + 1) ^ 2 ≤ + A₃ * M := by + simp only [Function.comp_apply, List.length_append, List.length_singleton, add_assoc, + Nat.reduceAdd, ← hn] + have h₁ : n + 2 ≤ (n + 2) ^ (d + 2) := Nat.le_self_pow (by omega) _ + have h₂ : ((n + 2) ^ (d + 2) + 1) ^ 2 ≤ 4 * (n + 2) ^ (2 * d + 4) := by + calc _ ≤ (2 * (n + 2) ^ (d + 2)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + _ = 4 * (n + 2) ^ (2 * d + 4) := by ring + have h₃ : (n + 2) ^ (d + 2) ≤ (n + 2) ^ (2 * d + 4) := + Nat.pow_le_pow_right (by omega) (by omega) + have h₄ : 7 * (n + 2) ^ (2 * d + 4) ≤ A₃ * M := + calc _ ≤ 7 * (2 ^ (2 * d + 4) * (n + 1) ^ (2 * d + 4)) := Nat.mul_le_mul_left _ (h2 _) + _ = A₃ * (n + 1) ^ (2 * d + 4) := by ring + _ ≤ A₃ * M := Nat.mul_le_mul_left _ (hMk _ (by omega)) + omega + have e : (2 + A₃ + 4 * A₁ + A₂ + 2 ^ B₀) * M = + 2 * M + A₃ * M + 4 * (A₁ * M) + A₂ * M + 2 ^ B₀ * M := by ring + have hB : 2 ^ B₀ ≤ 2 ^ B₀ * M := Nat.le_mul_of_pos_right _ (by omega) + clear_value M A₁ A₂ A₃ B₀ + generalize 2 + A₃ + 4 * A₁ + A₂ + 2 ^ B₀ = C at * + generalize 2 ^ B₀ = P at * + split_ifs with h₀ h₁ h₂ + · have := hacc h₀ + omega + · have := hbrute h₁ + omega + · omega + · omega + +/-! ### The hierarchy -/ + +/-- **A nondeterministic time hierarchy for polynomial degrees.** For every degree `d`, +nondeterministic time `O((n + 1) ^ d)` is strictly contained in nondeterministic time +`O((n + 1) ^ e)` whenever `6 * d + 14 ≤ e`. The lazy diagonal `Cslib.Complexity.lazyDiagonal d` +separates them (`Cslib.Complexity.lazyDiagonal_mem_NTIME`, +`Cslib.Complexity.lazyDiagonal_notMem_NTIME`). This is a coarse form of the nondeterministic time +hierarchy theorem [Arora and Barak, Theorem 3.3][AroraBarak07]: the gap is the polynomial +overhead of the native universal machine and of the certificates, not `f (n + 1) = o (g n)`. -/ +theorem NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le {d e : ℕ} (h : 6 * d + 14 ≤ e) : + NTIME encBits (fun n => (n + 1) ^ d) ⊂ NTIME encBits fun n => (n + 1) ^ e := by + have hsub : ∀ {a b : ℕ}, a ≤ b → + NTIME encBits (fun n => (n + 1) ^ a) ⊆ NTIME encBits fun n => (n + 1) ^ b := + fun hab => NTIME_mono fun n => Nat.pow_le_pow_right (by omega) hab + exact (Set.ssubset_iff_of_subset (hsub (by omega))).mpr + ⟨lazyDiagonal d, hsub h (lazyDiagonal_mem_NTIME d), lazyDiagonal_notMem_NTIME d⟩ + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean b/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean new file mode 100644 index 0000000000..8ba1e0dd5a --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean @@ -0,0 +1,218 @@ +/- +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.Space.Reachability +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +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.Foundations.Data.Nat.PolynomialBound.Closure +import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential + +/-! +# Bounded existential quantification in exponential time + +A test `f` that is computable in polynomial time can be tried on every word of length `ℓ x`, +for `ℓ` computable in polynomial time, within time `2 ^ O(|x| + ℓ x)` +(`Cslib.Complexity.exists_computableInO_any_enumList`). The candidates are enumerated in place: +the existential is reachability within two steps from the all-zero word to the all-one word of +width `ℓ x + 1`, along an edge to `true :: w` for each accepted `w` and from every word starting +with `true` to the all-one word (`Cslib.Complexity.boundedExistsEdge`). Savitch's algorithm +decides it at depth `1` (`Cslib.Reachability.computableInO_savitch`). Every polynomial in the +cost is absorbed by the exponential, so the exponent is linear in `|x| + ℓ x`, with a constant +that depends on the test. + +This brute force is the last step of lazy diagonalization for nondeterministic time, which +must decide deterministically whether some certificate is accepted. + +## Main definitions + +* `Cslib.Complexity.boundedExistsEdge`: the edges of the two-step reachability problem. + +## Main results + +* `Cslib.Complexity.savitch_boundedExistsEdge`: Savitch's algorithm at depth `1` on these edges + decides the bounded existential. +* `Cslib.Complexity.exists_computableInO_any_enumList`: the bounded existential within time and + space `2 ^ O(|x| + ℓ x)`. +-/ + +public section + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM + +/-- The edges of the graph on words of width `n + 1` whose reachability within two steps from the +all-zero word to the all-one word is a bounded existential over `f`: an edge from the all-zero word +to `true :: w` when `f (x, w)`, and from every word starting with `true` to the all-one word. -/ +def boundedExistsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (u v : List Bool) : Bool := + if !(u.any fun b => b) && v.headD false then f (x, v.tail) + else u.headD false && !(v.any fun b => !b) + +/-- Savitch's algorithm at depth `1` on the edges of `Cslib.Complexity.boundedExistsEdge` decides +the bounded existential. -/ +theorem savitch_boundedExistsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (n : ℕ) : + Cslib.Reachability.savitch (boundedExistsEdge f x) (n + 1) 1 (List.replicate (n + 1) false) + (List.replicate (n + 1) true) = true ↔ ∃ w : List Bool, w.length = n ∧ f (x, w) = true := by + rw [Cslib.Reachability.savitch_eq] + simp only [Cslib.Reachability.reach, List.any_eq_true, Cslib.BitString.mem_enumList, + Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq] + constructor + · rintro ⟨m, hm, h₁ | h₁, h₂ | h₂⟩ + · subst h₁ + exact absurd h₂ (by simp [List.replicate_succ]) + · subst h₁ + refine ⟨List.replicate n true, List.length_replicate .., ?_⟩ + simpa [boundedExistsEdge, List.replicate_succ] using h₂ + · subst h₂ + refine ⟨List.replicate n true, List.length_replicate .., ?_⟩ + simpa [boundedExistsEdge, List.replicate_succ] using h₁ + · obtain ⟨b, w, rfl⟩ := List.exists_cons_of_length_eq_add_one hm + refine ⟨w, by simpa using hm, ?_⟩ + cases b <;> simp_all [boundedExistsEdge, List.replicate_succ] + · rintro ⟨w, hw, hf⟩ + refine ⟨true :: w, by simp [hw], Or.inr ?_, Or.inr ?_⟩ + · 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 +time and space polynomial in its encoded input, and `ℓ` is computable in unary in polynomial time, +then whether some word of length `ℓ x` passes `f` with `x` is computable within time and space +`2 ^ (K * ((encB x).length + ℓ x))` for a constant `K`. Savitch's algorithm decides it at depth `1` +on the edges of `Cslib.Complexity.boundedExistsEdge`. -/ +theorem exists_computableInO_any_enumList {β : Type} {encB : β ↪ List Bool} + {f : β × List Bool → Bool} {Tf Sf : β × List Bool → ℕ} + (hf : ComputableInO f (encPair encB encBits) encBool Tf Sf) + (hTf : PolyBounded (fun q => (encPair encB encBits q).length) Tf) + (hSf : PolyBounded (fun q => (encPair encB encBits q).length) Sf) + {ℓ : β → ℕ} (hℓ : ComputableInPolyTime ℓ encB encUnary) : + ∃ K, ComputableInO (fun x => (Cslib.BitString.enumList (ℓ x)).any fun w => f (x, w)) encB + encBool (fun x => 2 ^ (K * ((encB x).length + ℓ x))) + (fun x => 2 ^ (K * ((encB x).length + ℓ x))) := by + set encQ := encPair encB (encPair encBits encBits) + -- the edge test: polynomial-time tests around one call of `f` + have hg : ComputableInPolyTime (fun q : β × List Bool × List Bool => (q.1, q.2.2.tail)) + encQ (encPair encB encBits) := by fun_prop + have hc : ComputableInPolyTime + (fun q : β × List Bool × List Bool => !(q.2.1.any fun b => b) && q.2.2.headD false) + encQ encBool := by fun_prop + have he : ComputableInPolyTime + (fun q : β × List Bool × List Bool => q.2.1.headD false && !(q.2.2.any fun b => !b)) + encQ encBool := by fun_prop + obtain ⟨Tg, Sg, hTg, hSg, hgO⟩ := hg.exists_computableInO + obtain ⟨Tc, Sc, hTc, hSc, hcO⟩ := hc.exists_computableInO + obtain ⟨Te, Se, hTe, hSe, heO⟩ := he.exists_computableInO + have hedge := hcO.ite (hf.comp hgO) heO + -- the arguments of Savitch's algorithm + have hin : ComputableInPolyTime + (fun x => (x, ℓ x + 1, 1, List.replicate (ℓ x + 1) false, List.replicate (ℓ x + 1) true)) + encB (Cslib.Reachability.encArgs encB) := by + unfold Cslib.Reachability.encArgs + fun_prop + obtain ⟨Ti, Si, hTi, hSi, hinO⟩ := hin.exists_computableInO + have h := Cslib.Reachability.computableInO_savitch (edge := boundedExistsEdge f) (par := id) + hedge hinO (fun _ => List.length_replicate ..) fun _ => List.length_replicate .. + -- every polynomial is within a constant multiple of an exponential + have hpoly (T₁ T₂ T₃ : β × List Bool × List Bool → ℕ) (T : β × List Bool → ℕ) + (h₁ : PolyBounded (fun q => (encQ q).length) T₁) + (h₂ : PolyBounded (fun q => (encQ q).length) T₂) + (h₃ : PolyBounded (fun q => (encQ q).length) T₃) + (hT : PolyBounded (fun q => (encPair encB encBits q).length) T) : + ∃ C, ∀ q, (T₁ q + if !(q.2.1.any fun b => b) && q.2.2.headD false then + T₂ q + T (q.1, q.2.2.tail) else T₃ q) ≤ C * 2 ^ (encQ q).length := by + have hcomp : PolyBounded (fun q => (encQ q).length) fun q => T (q.1, q.2.2.tail) := + hT.comp hg.polyBounded_length + refine PolyBounded.exists_le_mul_two_pow + ((h₁.add ((h₂.add hcomp).add h₃)).mono fun q => ?_) + split_ifs <;> omega + obtain ⟨CT, hCT⟩ := hpoly Tc Tg Te Tf hTc hTg hTe hTf + obtain ⟨CS, hCS⟩ := hpoly Sc Sg Se Sf hSc hSg hSe hSf + obtain ⟨CI, hCI⟩ := PolyBounded.exists_le_mul_two_pow hTi + obtain ⟨CJ, hCJ⟩ := PolyBounded.exists_le_mul_two_pow hSi + -- the edge queries on words of width `ℓ x + 1` + have hq (x : β) {u v : List Bool} (hu : u ∈ Cslib.BitString.enumList (ℓ x + 1)) + (hv : v ∈ Cslib.BitString.enumList (ℓ x + 1)) : + (encQ (x, u, v)).length = 2 * (encB x).length + 3 * ℓ x + 5 := by + simp only [encQ, length_encPair, encBits_apply, Cslib.BitString.mem_enumList.mp hu, + Cslib.BitString.mem_enumList.mp hv] + ring + refine ⟨12, (h.mono ((CI + CJ + CT + CS + 1) * 2 ^ 26) (fun x => ?_) fun x => ?_).of_enc_eq + fun x => ?_⟩ + · -- time + set n := (encB x).length + set L := ℓ x + have hmax := listMax_le (f := fun u => listMax (fun v => (Tc (x, u, v) + + if !(u.any fun b => b) && v.headD false then Tg (x, u, v) + Tf (x, v.tail) + else Te (x, u, v))) (Cslib.BitString.enumList (L + 1))) + (l := Cslib.BitString.enumList (L + 1)) (b := CT * 2 ^ (2 * n + 3 * L + 5)) + fun u hu => listMax_le fun v hv => (hCT (x, u, v)).trans_eq (by rw [hq x hu hv]) + change Ti x + 2 ^ ((L + 1 + 2) * (1 + 1)) * (((1 + 1) * (1 + (L + 1) + 1) + n + 1) ^ 2 + + Cslib.Reachability.edgeMax _ x (L + 1)) ≤ _ + unfold Cslib.Reachability.edgeMax + have hTi := hCI x + have hsq : ((1 + 1) * (1 + (L + 1) + 1) + n + 1) ^ 2 ≤ 2 ^ (2 * (2 * L + n + 7)) := + calc _ ≤ (2 * L + n + 7) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + _ ≤ (2 ^ (2 * L + n + 7)) ^ 2 := Nat.pow_le_pow_left Nat.lt_two_pow_self.le 2 + _ = _ := by rw [← pow_mul, mul_comm] + have hE : 2 ^ ((L + 1 + 2) * (1 + 1)) * (2 ^ (2 * (2 * L + n + 7)) + + CT * 2 ^ (2 * n + 3 * L + 5)) ≤ (CT + 1) * 2 ^ (12 * (n + L)) * 2 ^ 26 := by + have h₁ : 2 ^ ((L + 1 + 2) * (1 + 1)) * 2 ^ (2 * (2 * L + n + 7)) ≤ + 2 ^ (12 * (n + L)) * 2 ^ 26 := by + rw [← pow_add, ← pow_add] + exact Nat.pow_le_pow_right (by norm_num) (by ring_nf; omega) + have h₂ : 2 ^ ((L + 1 + 2) * (1 + 1)) * 2 ^ (2 * n + 3 * L + 5) ≤ + 2 ^ (12 * (n + L)) * 2 ^ 26 := by + rw [← pow_add, ← pow_add] + exact Nat.pow_le_pow_right (by norm_num) (by ring_nf; omega) + have := Nat.mul_le_mul_left CT h₂ + nlinarith + have hI : 2 ^ n ≤ 2 ^ (12 * (n + L)) := Nat.pow_le_pow_right (by norm_num) (by omega) + have hmono := Nat.mul_le_mul_left (2 ^ ((L + 1 + 2) * (1 + 1))) + (Nat.add_le_add hsq hmax) + have hX : 1 ≤ 2 ^ (12 * (n + L)) := Nat.one_le_two_pow + calc _ ≤ CI * 2 ^ n + (CT + 1) * 2 ^ (12 * (n + L)) * 2 ^ 26 := + Nat.add_le_add hTi (hmono.trans hE) + _ ≤ _ := by nlinarith + · -- space + set n := (encB x).length + set L := ℓ x + have hmax := listMax_le (f := fun u => listMax (fun v => (Sc (x, u, v) + + if !(u.any fun b => b) && v.headD false then Sg (x, u, v) + Sf (x, v.tail) + else Se (x, u, v))) (Cslib.BitString.enumList (L + 1))) + (l := Cslib.BitString.enumList (L + 1)) (b := CS * 2 ^ (2 * n + 3 * L + 5)) + fun u hu => listMax_le fun v hv => (hCS (x, u, v)).trans_eq (by rw [hq x hu hv]) + change Si x + (1 + 1) * (1 + (L + 1) + 1) + n + Cslib.Reachability.edgeMax _ x (L + 1) ≤ _ + unfold Cslib.Reachability.edgeMax + have hSi := hCJ x + have hX : 2 ^ (2 * n + 3 * L + 5) ≤ 2 ^ (12 * (n + L)) * 2 ^ 5 := by + rw [← pow_add] + exact Nat.pow_le_pow_right (by norm_num) (by omega) + have hI : 2 ^ n ≤ 2 ^ (12 * (n + L)) := Nat.pow_le_pow_right (by norm_num) (by omega) + have hL : (1 + 1) * (1 + (L + 1) + 1) + n ≤ 6 * 2 ^ (12 * (n + L)) := by + have : n + L < 2 ^ (n + L) := Nat.lt_two_pow_self + have : 2 ^ (n + L) ≤ 2 ^ (12 * (n + L)) := Nat.pow_le_pow_right (by norm_num) (by omega) + omega + have := Nat.mul_le_mul_left CS hX + nlinarith + · congr 1 + rw [Bool.eq_iff_iff, id, savitch_boundedExistsEdge f x (ℓ x)] + simp only [List.any_eq_true, Cslib.BitString.mem_enumList] + +end Cslib.Complexity diff --git a/ComplexityTests/NondeterministicTimeHierarchy.lean b/ComplexityTests/NondeterministicTimeHierarchy.lean new file mode 100644 index 0000000000..f688a9c506 --- /dev/null +++ b/ComplexityTests/NondeterministicTimeHierarchy.lean @@ -0,0 +1,44 @@ +/- +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.NondeterministicTime + +/-! The coarse nondeterministic time hierarchy on concrete degrees. The lazy diagonal for degree +`1` is in nondeterministic time `O((n + 1) ^ 20)` and not in nondeterministic linear time, so the +two classes differ; degree `0` separates constant from `O((n + 1) ^ 14)` nondeterministic time. +The verifier rejects inputs without a short description, such as the empty input. -/ + +public section + +namespace ComplexityTests.NondeterministicTimeHierarchy + +open Cslib Cslib.Complexity Turing Turing.MultiTapeTM + +/-- The lazy diagonal for degree `1` separates nondeterministic linear time from nondeterministic +time `O((n + 1) ^ 20)`, at the separating problem itself. -/ +example : lazyDiagonal 1 ∈ NTIME encBits (fun n => (n + 1) ^ 20) ∧ + lazyDiagonal 1 ∉ NTIME encBits (fun n => (n + 1) ^ 1) := + ⟨lazyDiagonal_mem_NTIME 1, lazyDiagonal_notMem_NTIME 1⟩ + +/-- Nondeterministic linear time is strictly inside nondeterministic time `O((n + 1) ^ 20)`. -/ +example : NTIME encBits (fun n => n + 1) ⊂ NTIME encBits fun n => (n + 1) ^ 20 := by + simpa using NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le (d := 1) (e := 20) le_rfl + +/-- Nondeterministic constant time is strictly inside nondeterministic time `O((n + 1) ^ 14)`. -/ +example : NTIME encBits (fun _ => 1) ⊂ NTIME encBits fun n => (n + 1) ^ 14 := by + simpa using NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le (d := 0) (e := 14) le_rfl + +/-- The empty input carries no short description, so the verifier rejects it with every +certificate, and the empty input is not in the lazy diagonal. -/ +example (d : ℕ) (v : List Bool) : LazyDiagonal.verifier d ([], v) = false := by + simp [LazyDiagonal.verifier, Diagonal.shortDesc, unframe] + +example (d : ℕ) : [] ∉ lazyDiagonal d := by + simp [lazyDiagonal, LazyDiagonal.verifier, Diagonal.shortDesc, unframe] + +end ComplexityTests.NondeterministicTimeHierarchy diff --git a/ROADMAP.md b/ROADMAP.md index 0c5c4eba03..cda927d2c7 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -180,9 +180,11 @@ index links to canonical definitions rather than keeping a second set. completeness, padding, self-reducibility, relativization and oracle separations, preserving each reduction's resource bound. - **Time hierarchies** ([#1572]): native polynomial padding separates every pair of integer - degrees `1 ≤ a < b`. Remaining targets include the general deterministic `f log f` hierarchy - with its simulation bound ([#800]), noninteger polynomial degrees and finer logarithmic - gaps, and sharp nondeterministic and alternating time hierarchies with certified simulators. + degrees `1 ≤ a < b`. For nondeterministic time, lazy diagonalization separates degree `d` + from degree `6 * d + 14`. Remaining targets include the general deterministic `f log f` + hierarchy with its simulation bound ([#800]), noninteger polynomial degrees and finer + logarithmic gaps, the nondeterministic hierarchy at every pair of integer degrees by padding, + and sharp nondeterministic and alternating time hierarchies with certified simulators. - The space hierarchy for `log n ≤ g n`, which needs a universal simulation that does not hold its input. - **Space:** Savitch bounds for general space-constructible functions. diff --git a/references.bib b/references.bib index 1b676dfaec..fc2d472320 100644 --- a/references.bib +++ b/references.bib @@ -280,6 +280,15 @@ @article{AngluinLaird1988 doi = {10.1007/BF00116829} } +@misc{AroraBarak07, + author = {Sanjeev Arora and + Boaz Barak}, + title = {Computational Complexity: {A} Modern Approach}, + howpublished = {Draft of a book, web draft dated 2007-01-08}, + year = {2007}, + url = {https://theory.cs.princeton.edu/complexity/book.pdf} +} + @book{AroraBarak09, author = {Sanjeev Arora and Boaz Barak}, @@ -5225,6 +5234,17 @@ @inproceedings{Yao1982 doi = {10.1109/SFCS.1982.45} } +@article{Zak1983, + author = {{\v{Z}}{\'a}k, Stanislav}, + title = {A {T}uring Machine Time Hierarchy}, + journal = {Theoretical Computer Science}, + volume = {26}, + number = {3}, + pages = {327--333}, + year = {1983}, + doi = {10.1016/0304-3975(83)90015-4} +} + @misc{Zhao2023, author = {Zhao, Yufei}, title = {Probabilistic Methods in Combinatorics}, From 123ef60b54a1d95d083f457280122e5303fff8d7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 08:44:37 -0400 Subject: [PATCH 3/9] refactor(Classes/Space): use the public bounded-existential edges in setOf_exists_mem_PSPACE The private existsEdge and savitch_existsEdge duplicated the public boundedExistsEdge and savitch_boundedExistsEdge; expose the definition so clients can match it against Savitch's edge test. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/Space/Closure.lean | 44 +++---------------- .../Classes/Time/BoundedExists.lean | 10 +++-- 2 files changed, 13 insertions(+), 41 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Space/Closure.lean b/Complexity/Computability/Complexity/Classes/Space/Closure.lean index 57946f366b..06a0adcb03 100644 --- a/Complexity/Computability/Complexity/Classes/Space/Closure.lean +++ b/Complexity/Computability/Complexity/Classes/Space/Closure.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Complexity.Reduction public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace public import Complexity.Foundations.Order.BooleanSubalgebra import Complexity.Computability.Complexity.Classes.Space.Savitch +import Complexity.Computability.Complexity.Classes.Time.BoundedExists import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat @@ -146,47 +147,14 @@ theorem PolyTimeReducible.mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : exact mem_PSPACE_of_computableInPolySpace (hf.comp (.of_polyTime hg)) fun a => (hAB a).trans (hB (g a)) -/-- The edges of the graph on words of width `n + 1` whose reachability within two steps from the -all-zero word to the all-one word is a bounded existential over `f`: an edge from the all-zero word -to `true :: w` when `f (x, w)`, and from every word starting with `true` to the all-one word. -/ -private def existsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (u v : List Bool) : Bool := - if !(u.any fun b => b) && v.headD false then f (x, v.tail) - else u.headD false && !(v.any fun b => !b) - -/-- Savitch's algorithm at depth `1` on the edges of `existsEdge` decides the bounded -existential. -/ -private theorem savitch_existsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (n : ℕ) : - Cslib.Reachability.savitch (existsEdge f x) (n + 1) 1 (List.replicate (n + 1) false) - (List.replicate (n + 1) true) = true ↔ ∃ w : List Bool, w.length = n ∧ f (x, w) = true := by - rw [Cslib.Reachability.savitch_eq] - simp only [Cslib.Reachability.reach, List.any_eq_true, Cslib.BitString.mem_enumList, - Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq] - constructor - · rintro ⟨m, hm, h₁ | h₁, h₂ | h₂⟩ - · subst h₁ - exact absurd h₂ (by simp [List.replicate_succ]) - · subst h₁ - refine ⟨List.replicate n true, List.length_replicate .., ?_⟩ - simpa [existsEdge, List.replicate_succ] using h₂ - · subst h₂ - refine ⟨List.replicate n true, List.length_replicate .., ?_⟩ - simpa [existsEdge, List.replicate_succ] using h₁ - · obtain ⟨b, w, rfl⟩ := List.exists_cons_of_length_eq_add_one hm - refine ⟨w, by simpa using hm, ?_⟩ - cases b <;> simp_all [existsEdge, List.replicate_succ] - · rintro ⟨w, hw, hf⟩ - refine ⟨true :: w, by simp [hw], Or.inr ?_, Or.inr ?_⟩ - · simp [existsEdge, List.replicate_succ, hf] - · simp [existsEdge, List.replicate_succ] - attribute [local fun_prop] ComputableInPolyTime.fst' ComputableInPolyTime.snd' ComputableInPolyTime.bool_and' in /-- **`PSPACE` is closed under polynomially bounded existential quantification**: if `B ⊆ β × List Bool` is in `PSPACE` and `ℓ` is polynomial-time, then so is the set of the `x` for which some word `w` of length `ℓ x` has `(x, w) ∈ B`. The candidates are enumerated in place: this is reachability -within two steps between two words of width `ℓ x + 1` (`existsEdge`), which Savitch's algorithm -decides at depth `1`, reusing the space of the decider of `B` for every candidate -(`Cslib.Reachability.computableInO_savitch`). -/ +within two steps between two words of width `ℓ x + 1` (`Cslib.Complexity.boundedExistsEdge`), +which Savitch's algorithm decides at depth `1`, reusing the space of the decider of `B` for every +candidate (`Cslib.Reachability.computableInO_savitch`). -/ theorem setOf_exists_mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set (β × List Bool)} {ℓ : β → ℕ} (hB : B ∈ PSPACE (encPair encB encBits)) (hℓ : ComputableInPolyTime ℓ encB encUnary) : @@ -213,7 +181,7 @@ theorem setOf_exists_mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set ( unfold Cslib.Reachability.encArgs fun_prop obtain ⟨Ti, Si, -, hSi, hinO⟩ := hin.exists_computableInO - have h := Cslib.Reachability.computableInO_savitch (edge := existsEdge f) (par := id) + have h := Cslib.Reachability.computableInO_savitch (edge := boundedExistsEdge f) (par := id) hedge hinO (fun _ => List.length_replicate ..) fun _ => List.length_replicate .. -- the space is polynomial have hSedge : PolyBounded (fun q => (encQ q).length) fun q => @@ -250,6 +218,6 @@ theorem setOf_exists_mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set ( Si x + 2 * (ℓ x + 3) + (encB x).length + cE * (2 * (encB x).length + 3 * ℓ x + 6) ^ dE omega · simp only [Set.mem_ofPred_eq, hB, id] - exact (savitch_existsEdge f x (ℓ x)).symm + exact (savitch_boundedExistsEdge f x (ℓ x)).symm end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean b/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean index 8ba1e0dd5a..eb926ceb84 100644 --- a/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean +++ b/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean @@ -28,8 +28,11 @@ decides it at depth `1` (`Cslib.Reachability.computableInO_savitch`). Every poly cost is absorbed by the exponential, so the exponent is linear in `|x| + ℓ x`, with a constant that depends on the test. -This brute force is the last step of lazy diagonalization for nondeterministic time, which -must decide deterministically whether some certificate is accepted. +The same edges give the closure of `PSPACE` under bounded existential quantification +(`Cslib.Complexity.setOf_exists_mem_PSPACE`), where the point is the space of the run. Here the +time is the point: this brute force is the last step of lazy diagonalization for +nondeterministic time, which must decide deterministically whether some certificate is +accepted. ## Main definitions @@ -52,7 +55,8 @@ open _root_.Turing _root_.Turing.MultiTapeTM /-- The edges of the graph on words of width `n + 1` whose reachability within two steps from the all-zero word to the all-one word is a bounded existential over `f`: an edge from the all-zero word to `true :: w` when `f (x, w)`, and from every word starting with `true` to the all-one word. -/ -def boundedExistsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (u v : List Bool) : Bool := +@[expose] def boundedExistsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (u v : List Bool) : + Bool := if !(u.any fun b => b) && v.headD false then f (x, v.tail) else u.headD false && !(v.any fun b => !b) From ba518a6f89f0837daa7e6a4c09a9ef989ad5432b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 08:47:10 -0400 Subject: [PATCH 4/9] doc(Classes/Hierarchy): state the interval cases of the lazy diagonal verifier precisely Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Hierarchy/NondeterministicTime.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean index 1f0e01fc6c..38d0ff53de 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean @@ -108,15 +108,16 @@ def clock (d m : ℕ) : ℕ := (m + 1) ^ (d + 3) def accepts (d : ℕ) (c y v : List Bool) : Bool := !Diagonal.verdict (universal (decodeDesc c, (frame y ++ v).map eBit, clock d y.length)) -/-- **The verifier of the lazy diagonal**, on an input `x` and a certificate `v`. The input carries -a word `w` framed at its start, and `w` carries the description `unframe w` framed at its start. -When the description is short (`Cslib.Complexity.Diagonal.shortDesc`), the lengths from -`P = 2 * w.length + 1` to `2 ^ clock d P - 1` form an interval: - -* below its end, accept when the described verifier accepts `v` on the input one bit longer; -* at its end, accept when the described verifier accepts no certificate on `frame w`, the input of - length `P`, by trying them all; -* elsewhere, reject. -/ +/-- **The verifier of the lazy diagonal**, on an input `x` of length `n` and a certificate `v`. +The input carries a word `w` framed at its start, and `w` carries the description `unframe w` +framed at its start. When the description is short (`Cslib.Complexity.Diagonal.shortDesc w`), +let `P = 2 * w.length + 1`; the lengths from `P` to `2 ^ clock d P - 1` form the interval of `w`. + +* If `n + 1 < 2 ^ clock d P`, below the end of the interval, accept when the described verifier + accepts `v` on the input one bit longer. +* If `n + 1 = 2 ^ clock d P`, at the end of the interval, accept when the described verifier + accepts no certificate on `frame w`, the input of length `P`, by trying them all. +* Otherwise, and when the description is not short, reject. -/ def verifier (d : ℕ) (p : List Bool × List Bool) : Bool := if Diagonal.shortDesc (unframe p.1) then if Nat.size (p.1.length + 1) ≤ clock d (2 * (unframe p.1).length + 1) then From e3a2699c5617a8dffa8716fd7f120b589b7a6828 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:53:33 -0400 Subject: [PATCH 5/9] feat(Classes/Hierarchy): nondeterministic exponential time hierarchy by lazy diagonalization (#1539 M2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `NTIME (2 ^ (k * n)) ⊂ NTIME (2 ^ (e * n))` on bit strings whenever `8 * k + 16 ≤ e`, separated by the explicit `expLazyDiagonal k`, and so `NE ⊄ NTIME (2 ^ (k * n))`. This reruns the lazy diagonal of `Hierarchy/NondeterministicTime` with exponential certificates; the simulation clock is the square of the length of the simulated pair, so the brute force at the end of an interval stays a polynomial-time test tried on every certificate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../NondeterministicExponentialTime.lean | 924 ++++++++++++++++++ ...deterministicExponentialTimeHierarchy.lean | 51 + ROADMAP.md | 11 +- 4 files changed, 982 insertions(+), 5 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean create mode 100644 ComplexityTests/NondeterministicExponentialTimeHierarchy.lean diff --git a/Complexity.lean b/Complexity.lean index b7729ca7f9..439294de66 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1176,6 +1176,7 @@ public import Complexity.Computability.Complexity.Classes.FunctionTime 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.NondeterministicTime public import Complexity.Computability.Complexity.Classes.Hierarchy.Polynomial public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean new file mode 100644 index 0000000000..93bc07f01e --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean @@ -0,0 +1,924 @@ +/- +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.Complexity.Classes.EXP +public import Complexity.Computability.Complexity.Classes.Hierarchy.Time +public import Complexity.Foundations.Data.BitString.Enumeration +import Complexity.Computability.Complexity.Classes.Time.BoundedExists +import Complexity.Computability.Complexity.Classes.Time.Verifier +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential + +/-! +# A nondeterministic exponential time hierarchy by lazy diagonalization + +For every `k`, nondeterministic time `O(2 ^ (k * n))` is strictly contained in nondeterministic +time `O(2 ^ (e * n))` on bit strings whenever `8 * k + 16 ≤ e` +(`Cslib.Complexity.NTIME_two_pow_ssubset_NTIME_two_pow_of_le`). In particular `NE` is not contained +in `NTIME (2 ^ (k * n))` for any `k` (`Cslib.Complexity.exists_mem_NE_notMem_NTIME_two_pow`). This +is a coarse exponential form of the nondeterministic time hierarchy theorem +[Arora and Barak, Theorem 3.3][AroraBarak07], proved by lazy diagonalization [Žák][Zak1983]. +The separating problem is explicit: `Cslib.Complexity.expLazyDiagonal k`. + +Padding transfers inclusions between nondeterministic time classes only upward, so the +polynomial hierarchy of `Cslib.Complexity.NTIME_succ_pow_ssubset_NTIME_succ_pow_of_le` does not give +this separation; the lazy diagonal is run again with exponential certificates. + +## The lazy diagonal + +An input `x` carries a word `w` framed at its start, and `w` carries the description +`unframe w` of a deterministic verifier on pairs framed at its start, followed by arbitrary +padding. The interval of `w` consists of the lengths from `P = 2 * w.length + 1`, the length of +`frame w`, to `2 ^ horizon k P - 1`, where `horizon k m = 2 ^ ((k + 2) * (m + 1))`. On the input `x` +of length `n` in this interval, with a certificate `v` of length +`certLen k (n + 1) = 2 ^ ((k + 1) * (n + 2))`, the verifier +`Cslib.Complexity.ExpLazyDiagonal.verifier k` + +* below the end of the interval, runs the described verifier on the one bit longer input + `x ++ [false]` and the certificate `v` with the universal function, for the square of the + length of the encoded pair (`Cslib.Complexity.ExpLazyDiagonal.accepts`); +* at the end of the interval, accepts when the described verifier accepts no certificate of + length `certLen k P` on `frame w`, trying them all. + +The lazy diagonal is the problem of the inputs with an accepted certificate. + +* **Upper bound** (`Cslib.Complexity.expLazyDiagonal_mem_NTIME`). Guess the certificate and run the + verifier (`Cslib.Complexity.setOf_exists_mem_NTIME`). The simulation takes time polynomial in the + certificate, `O(2 ^ ((8 * k + 16) * n))`. The brute force takes time `2 ^ O(certLen k P)` + (`Cslib.Complexity.exists_computableInO_any_enumList`), which is `O(n)` at the end of the + interval, where `n + 1 = 2 ^ horizon k P` and `horizon k P = 2 ^ (P + 1) * certLen k P`. +* **Lower bound** (`Cslib.Complexity.expLazyDiagonal_notMem_NTIME`). A nondeterministic machine + deciding the problem within time `O(2 ^ (k * n))` has a deterministic verifier on pairs within + linear time, accepting certificates of every length at least `c * 2 ^ (k * n) + c` + (`Cslib.Complexity.exists_verifier_of_mem_NTIME`). On the interval of a word `w` describing that + verifier, with enough padding, the universal function runs it exactly. Then each input of the + interval is in the problem exactly when the next one is, and the last exactly when the first is + not. + +Unlike `Cslib.Complexity.lazyDiagonal`, the simulation clock is the square of the length of the +simulated pair rather than a function of the input length alone. It is then polynomial in the +certificate, so the brute force at the end of an interval is a polynomial-time test tried on every +certificate. + +## Main definitions + +* `Cslib.Complexity.ExpLazyDiagonal.verifier`: the verifier of the lazy diagonal. +* `Cslib.Complexity.expLazyDiagonal`: the exponential lazy diagonal problem for `k`. + +## Main results + +* `Cslib.Complexity.expLazyDiagonal_mem_NTIME`: the lazy diagonal is in + `NTIME (2 ^ ((8 * k + 16) * n))`. +* `Cslib.Complexity.expLazyDiagonal_notMem_NTIME`: the lazy diagonal is not in + `NTIME (2 ^ (k * n))`. +* `Cslib.Complexity.NTIME_two_pow_ssubset_NTIME_two_pow_of_le`: the hierarchy. +* `Cslib.Complexity.exists_mem_NE_notMem_NTIME_two_pow`: `NE ⊄ NTIME (2 ^ (k * n))`. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, web draft of January + 2007][AroraBarak07] +* [S. Žák, *A Turing machine time hierarchy*][Zak1983] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Universal + +namespace ExpLazyDiagonal + +/-- The certificate length of the lazy diagonal on words of length `m`: +`2 ^ ((k + 1) * (m + 1))`. -/ +def certLen (k m : ℕ) : ℕ := 2 ^ ((k + 1) * (m + 1)) + +/-- The horizon of the lazy diagonal: the interval of lengths starting at `m` ends below +`2 ^ horizon k m`, where `horizon k m = 2 ^ ((k + 2) * (m + 1)) = 2 ^ (m + 1) * certLen k m`. -/ +def horizon (k m : ℕ) : ℕ := 2 ^ ((k + 2) * (m + 1)) + +/-- The machine described by `c`, run as a verifier on the pair `(y, v)` (encoded as +`frame y ++ v`) with the universal function for `((frame y ++ v).length + 1) ^ 2` steps, has +halted with output `[true]`. -/ +def accepts (c y v : List Bool) : Bool := + !Diagonal.verdict + (universal (decodeDesc c, (frame y ++ v).map eBit, ((frame y ++ v).length + 1) ^ 2)) + +/-- **The verifier of the exponential lazy diagonal**, on an input `x` of length `n` and a +certificate `v`. The input carries a word `w` framed at its start, and `w` carries the description +`unframe w` framed at its start. When the description is short +(`Cslib.Complexity.Diagonal.shortDesc w`), let `P = 2 * w.length + 1`; the lengths from `P` to +`2 ^ horizon k P - 1` form the interval of `w`. + +* If `n + 1 < 2 ^ horizon k P`, below the end of the interval, accept when the described verifier + accepts `v` on the input one bit longer. +* If `n + 1 = 2 ^ horizon k P`, at the end of the interval, accept when the described verifier + accepts no certificate on `frame w`, the input of length `P`, by trying them all. +* Otherwise, and when the description is not short, reject. -/ +def verifier (k : ℕ) (p : List Bool × List Bool) : Bool := + if Diagonal.shortDesc (unframe p.1) then + if Nat.size (p.1.length + 1) ≤ horizon k (2 * (unframe p.1).length + 1) then + accepts (unframe (unframe p.1)) (p.1 ++ [false]) p.2 + else if Nat.size p.1.length ≤ horizon k (2 * (unframe p.1).length + 1) then + !(Cslib.BitString.enumList (certLen k (2 * (unframe p.1).length + 1))).any + (accepts (unframe (unframe p.1)) (frame (unframe p.1))) + else false + else false + +end ExpLazyDiagonal + +open ExpLazyDiagonal + +/-- **The exponential lazy diagonal language** for `k`: the words `x` with a certificate of length +`2 ^ ((k + 1) * (x.length + 2))` accepted by `Cslib.Complexity.ExpLazyDiagonal.verifier k`. -/ +def expLazyDiagonal (k : ℕ) : Set (List Bool) := + {x | ∃ v : List Bool, v.length = certLen k (x.length + 1) ∧ verifier k (x, v) = true} + +/-! ### The lazy diagonal is not in `NTIME (2 ^ (k * n))` -/ + +/-- The lengths at which certificates of length `certLen k m` suffice for a verifier with constant +`c`. -/ +private theorem exists_le_certLen (k c : ℕ) : + ∃ M, ∀ m, M ≤ m → c * 2 ^ (k * m) + c ≤ certLen k m := by + refine ⟨c, fun m hm => ?_⟩ + have hX : 1 ≤ 2 ^ (k * m) := Nat.one_le_two_pow + have hc : 2 * c ≤ 2 ^ (m + 1) := by + have := Nat.lt_two_pow_self (n := m) + rw [pow_succ] + omega + have e : certLen k m = 2 ^ (k * m) * 2 ^ k * 2 ^ (m + 1) := by + simp only [certLen, ← pow_add] + congr 1 + ring + rw [e] + calc c * 2 ^ (k * m) + c ≤ 2 * c * 2 ^ (k * m) := by nlinarith + _ ≤ 2 ^ (m + 1) * 2 ^ (k * m) := Nat.mul_le_mul_right _ hc + _ ≤ 2 ^ (k * m) * 2 ^ k * 2 ^ (m + 1) := by + rw [mul_comm (2 ^ (m + 1)), mul_assoc] + exact Nat.mul_le_mul_left _ (Nat.le_mul_of_pos_left _ Nat.one_le_two_pow) + +/-- **The exponential lazy diagonal is not decidable in nondeterministic time +`O(2 ^ (k * n))`.** A nondeterministic machine deciding it has a verifier on pairs within linear +time (`Cslib.Complexity.exists_verifier_of_mem_NTIME`), described by a word `code`. On the interval +of lengths of `w = frame code ++ pad` with a long enough `pad`, the universal function runs that +verifier exactly. Each word of the interval is then in the language exactly when the next one is, +and the last exactly when the first is not. -/ +theorem expLazyDiagonal_notMem_NTIME (k : ℕ) : + expLazyDiagonal k ∉ NTIME encBits fun n => 2 ^ (k * n) := by + intro hD + obtain ⟨V, c, hV, hmem⟩ := exists_verifier_of_mem_NTIME hD + obtain ⟨c₂, ⟨k', State, hfin, tm, htm⟩, -⟩ := hV + have := Fintype.ofFinite State + let eS : State ↪ ℕ := (Fintype.equivFin State).toEmbedding.trans Fin.valEmbedding + set code := eDesc (desc eS eBit tm) with hcode + obtain ⟨M₁, hM₁⟩ := exists_le_certLen k c + set M := M₁ + c₂ with hM + -- the universal function runs the verifier exactly on long enough words + have hsim (y v : List Bool) (hy : M ≤ y.length) : accepts code y v = V (y, v) := by + have hclock : c₂ * ((encPair encBits encBits (y, v)).length + 1) ≤ + ((frame y ++ v).length + 1) ^ 2 := by + simp only [encPair_apply, encBits_apply, List.length_append, length_frame] + rw [sq] + exact Nat.mul_le_mul_right _ (by omega) + obtain ⟨hhalt, hout⟩ := (htm (y, v)).runFrom_of_le hclock + simp only [encPair_apply, encBits_apply, encBool_apply] at hhalt hout + rw [accepts, hcode, decodeDesc_eDesc, universal_desc, hout] + simp only [List.map_cons, List.map_nil, Cfg.Halted] at hhalt ⊢ + rw [hhalt] + cases V (y, v) <;> simp [Diagonal.verdict, eBit] + -- on long enough words, membership is acceptance by the simulated verifier + have hiff (y : List Bool) (hy : M ≤ y.length) : y ∈ expLazyDiagonal k ↔ + ∃ v : List Bool, v.length = certLen k y.length ∧ accepts code y v = true := by + have h := hmem y (certLen k y.length) + (by simpa [encBits_apply] using hM₁ y.length (by omega)) + rw [h] + exact exists_congr fun v => and_congr_right fun _ => by rw [hsim y v hy] + -- the interval of `w` + set w := frame code ++ List.replicate (2 ^ code.length + M) true with hw + set P := 2 * w.length + 1 with hP + set E := horizon k P with hE + set x : ℕ → List Bool := fun m => frame w ++ List.replicate (m - P) false with hx + have hwlen : w.length = 2 * code.length + 1 + (2 ^ code.length + M) := by + simp [w] + have hMP : M ≤ P := by + have := hwlen + generalize 2 ^ code.length = e at this + omega + have hxlen (m : ℕ) (hm : P ≤ m) : (x m).length = m := by + simp only [x, List.length_append, length_frame, List.length_replicate] + omega + have hshort : Diagonal.shortDesc w = true := by + have hc : unframe w = code := unframe_frame_append _ _ + rw [Diagonal.shortDesc, decide_eq_true_eq, hc, hwlen] + omega + have hverifier (m : ℕ) (hm : P ≤ m) (v : List Bool) : verifier k (x m, v) = + if Nat.size (m + 1) ≤ E then accepts code (x m ++ [false]) v + else if Nat.size m ≤ E then + !(Cslib.BitString.enumList (certLen k P)).any (accepts code (frame w)) + else false := by + have hu : unframe (x m) = w := unframe_frame_append _ _ + have hc : unframe w = code := unframe_frame_append _ _ + simp only [verifier, hu, hc, hshort, hxlen m hm, ← hP, ← hE, ↓reduceIte] + have hPE : P + 1 < 2 ^ E := by + have : P + 1 ≤ E := + calc P + 1 ≤ 2 ^ (P + 1) := Nat.lt_two_pow_self.le + _ ≤ E := Nat.pow_le_pow_right (by norm_num) (Nat.le_mul_of_pos_left _ (by omega)) + exact this.trans_lt Nat.lt_two_pow_self + set U := 2 ^ E - 1 with hU + -- each word below the end of the interval is in the language exactly when the next one is + have hstep (m : ℕ) (hm : P ≤ m) (hmU : m < U) : + x m ∈ expLazyDiagonal k ↔ x (m + 1) ∈ expLazyDiagonal k := by + have hsize : Nat.size (m + 1) ≤ E := Nat.size_le.mpr (by omega) + have hnext : x m ++ [false] = x (m + 1) := by + simp only [x, List.append_assoc, ← List.replicate_succ'] + congr 2 + omega + rw [hiff (x (m + 1)) (by rw [hxlen _ (by omega)]; omega), expLazyDiagonal, Set.mem_ofPred_eq, + hxlen (m + 1) (by omega), hxlen m hm] + refine exists_congr fun v => and_congr_right fun _ => ?_ + simp only [hverifier m hm v, hsize, ↓reduceIte, hnext] + -- the end of the interval is in the language exactly when its start is not + have hend : x U ∈ expLazyDiagonal k ↔ x P ∉ expLazyDiagonal k := by + have hUP : P ≤ U := by omega + have hsize₁ : ¬Nat.size (U + 1) ≤ E := by + rw [Nat.size_le, hU, Nat.sub_add_cancel Nat.one_le_two_pow] + exact lt_irrefl _ + have hsize₂ : Nat.size U ≤ E := Nat.size_le.mpr (by omega) + have hbase : x P = frame w := by simp [x] + rw [hiff (x P) (by rw [hxlen P le_rfl]; omega), hxlen P le_rfl, hbase, expLazyDiagonal, + Set.mem_ofPred_eq] + simp only [hverifier U hUP, hsize₁, hsize₂, ↓reduceIte, Bool.not_eq_true', + List.any_eq_false, Cslib.BitString.mem_enumList, not_exists, not_and, Bool.not_eq_true] + constructor + · rintro ⟨-, -, h⟩ v hv + exact h v hv + · intro h + exact ⟨List.replicate _ false, List.length_replicate .., h⟩ + -- the chain from the start of the interval to its end + have hchain (j : ℕ) (hj : j ≤ U - P) : + x (U - j) ∈ expLazyDiagonal k ↔ x U ∈ expLazyDiagonal k := by + induction j with + | zero => rfl + | succ j ih => + rw [← ih (by omega), hstep (U - (j + 1)) (by omega) (by omega)] + congr! 2 + omega + have h := hchain (U - P) le_rfl + rw [Nat.sub_sub_self (by omega), hend] at h + exact iff_not_self h + +/-! ### The lazy diagonal is in nondeterministic exponential time -/ + +/-- The bound on the simulation of `Cslib.Complexity.ExpLazyDiagonal.accepts`, for a decoder of +degree below `D`: polynomial in the description, the input and the certificate. -/ +private def accBound (D : ℕ) (q : List Bool × List Bool × List Bool) : ℕ := + ((q.1.length + 1) ^ D + q.2.1.length + q.2.2.length + 1) ^ 4 * + ((frame q.2.1 ++ q.2.2).length + 1) ^ 4 + +/-- The binary length of the clock is linear in the length of the simulated word. -/ +private theorem length_encNat_sq_le (W : ℕ) : (encNat ((W + 1) ^ 2)).length ≤ 2 * (W + 1) := by + rw [encNat_apply, Nat.size_eq_bits_len, Nat.size_le, mul_comm, pow_mul] + exact Nat.pow_lt_pow_left Nat.lt_two_pow_self (by omega) + +/-- The numeric core of the resources of the simulation: for an encoded input of length `N`, a +decoding time `A`, a word `W = frame y ++ v`, a decoded description of encoded length `Dl`, encoded +symbols of length `Nl`, a clock `Y` of `Ll` binary digits and a result of encoded length `E`, +everything is within `K * X ^ 4 * Y ^ 2`. -/ +private theorem accBound_aux (d cD cO : ℕ) : ∃ K, ∀ {N A W Dl Nl Ll X Y E : ℕ}, + N ≤ 2 * X → A ≤ X → W ≤ 2 * X → Dl ≤ cD * (N + A + 1) → Nl ≤ 3 * W → + Ll ≤ (d + 4) * X → 1 ≤ X → 1 ≤ Y → + E ≤ cO * (N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) + 1) → + N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 4 * (Y + 1) ^ 2 + + (E + 1) ^ 2 + 1 ≤ K * (X ^ 4 * Y ^ 2) ∧ + N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) + E + 1 ≤ + K * (X ^ 4 * Y ^ 2) := by + set C₁ := 8 * cD + d + 19 + set C₂ := 11 + 2 * C₁ ^ 2 + refine ⟨10 + 4 * C₁ ^ 4 + (cO * C₂ + 1) ^ 2 + 1 + C₂ * (cO + 1), + fun {N A W Dl Nl Ll X Y E} hN hA hW hD hNl hLl hX hY hE => ?_⟩ + have hIn : 2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1 ≤ C₁ * X := by + have h₁ : cD * (N + A + 1) ≤ cD * (4 * X) := Nat.mul_le_mul_left _ (by omega) + have h₂ : (d + 4) * X = d * X + 4 * X := by ring + have h₃ : d * X ≤ d * X := le_rfl + have e : C₁ * X = 8 * (cD * X) + d * X + 19 * X := by simp only [C₁]; ring + have e' : cD * (4 * X) = 4 * (cD * X) := by ring + omega + have hXY : X * Y ≤ X ^ 2 * Y := Nat.mul_le_mul_right _ (Nat.le_self_pow (by norm_num) _) + have hX2Y : X ^ 2 * Y ≤ X ^ 4 * Y ^ 2 := + Nat.mul_le_mul (Nat.pow_le_pow_right hX (by norm_num)) (Nat.le_self_pow (by norm_num) _) + have hpre : N + A + (N + W + (N + Y)) ≤ 10 * (X * Y) := by + have h₁ : X ≤ X * Y := Nat.le_mul_of_pos_right _ hY + have h₂ : Y ≤ X * Y := Nat.le_mul_of_pos_left _ hX + omega + have hY1 : Y + 1 ≤ 2 * Y := by omega + have hU₂ : (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) ≤ 2 * C₁ ^ 2 * (X ^ 2 * Y) := + calc _ ≤ (C₁ * X) ^ 2 * (2 * Y) := Nat.mul_le_mul (Nat.pow_le_pow_left hIn 2) hY1 + _ = 2 * C₁ ^ 2 * (X ^ 2 * Y) := by ring + have hU₄ : (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 4 * (Y + 1) ^ 2 ≤ + 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) := + calc _ ≤ (C₁ * X) ^ 4 * (2 * Y) ^ 2 := + Nat.mul_le_mul (Nat.pow_le_pow_left hIn 4) (Nat.pow_le_pow_left hY1 2) + _ = 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) := by ring + have hS : N + A + (N + W + (N + Y)) + (2 * Dl + 1 + (2 * Nl + 1 + Ll) + 1) ^ 2 * (Y + 1) + 1 ≤ + C₂ * (X ^ 2 * Y) := by + have h₁ : 1 ≤ X ^ 2 * Y := Nat.mul_pos (Nat.pow_pos hX) hY + have e : C₂ * (X ^ 2 * Y) = 11 * (X ^ 2 * Y) + 2 * C₁ ^ 2 * (X ^ 2 * Y) := by + simp only [C₂]; ring + omega + have hE' : E ≤ cO * C₂ * (X ^ 2 * Y) := + hE.trans ((Nat.mul_le_mul_left cO hS).trans_eq (by ring)) + have hE2 : (E + 1) ^ 2 ≤ (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) := by + have h₁ : 1 ≤ X ^ 2 * Y := Nat.mul_pos (Nat.pow_pos hX) hY + have h₂ : E + 1 ≤ (cO * C₂ + 1) * (X ^ 2 * Y) := by + have e : (cO * C₂ + 1) * (X ^ 2 * Y) = cO * C₂ * (X ^ 2 * Y) + X ^ 2 * Y := by ring + omega + calc (E + 1) ^ 2 ≤ ((cO * C₂ + 1) * (X ^ 2 * Y)) ^ 2 := Nat.pow_le_pow_left h₂ 2 + _ = (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) := by ring + have h1 : 1 ≤ X ^ 4 * Y ^ 2 := Nat.mul_pos (Nat.pow_pos hX) (Nat.pow_pos hY) + have hXYW : X * Y ≤ X ^ 4 * Y ^ 2 := hXY.trans hX2Y + have hU₂' := hU₂.trans (Nat.mul_le_mul_left (2 * C₁ ^ 2) hX2Y) + constructor + · have e : (10 + 4 * C₁ ^ 4 + (cO * C₂ + 1) ^ 2 + 1 + C₂ * (cO + 1)) * (X ^ 4 * Y ^ 2) = + 10 * (X ^ 4 * Y ^ 2) + 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) + + (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) + X ^ 4 * Y ^ 2 + + C₂ * (cO + 1) * (X ^ 4 * Y ^ 2) := by + ring + have := Nat.mul_le_mul_left 10 hXYW + omega + · have e : (10 + 4 * C₁ ^ 4 + (cO * C₂ + 1) ^ 2 + 1 + C₂ * (cO + 1)) * (X ^ 4 * Y ^ 2) = + 10 * (X ^ 4 * Y ^ 2) + 4 * C₁ ^ 4 * (X ^ 4 * Y ^ 2) + + (cO * C₂ + 1) ^ 2 * (X ^ 4 * Y ^ 2) + X ^ 4 * Y ^ 2 + + (C₂ * (X ^ 4 * Y ^ 2) + cO * C₂ * (X ^ 4 * Y ^ 2)) := by + ring + have h₁ := Nat.mul_le_mul_left C₂ hX2Y + have h₂ := Nat.mul_le_mul_left (cO * C₂) hX2Y + omega + +/-- The simulation runs within time polynomial in the description, the input and the +certificate. -/ +private theorem exists_computableInO_accepts : ∃ D, ComputableInO + (fun q : List Bool × List Bool × List Bool => accepts q.1 q.2.1 q.2.2) + (encPair encBits (encPair encBits encBits)) encBool (accBound D) (accBound D) := by + obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc + set enc := encPair encBits (encPair encBits encBits) + have hdesc := hdec.inO.comp (ComputableInO.fst encBits (encPair encBits encBits)) + have hword : ComputableInO (fun q : List Bool × List Bool × List Bool => frame q.2.1 ++ q.2.2) + enc encBits (fun q => (enc q).length) (fun q => (enc q).length) := + (ComputableInO.snd encBits (encPair encBits encBits)).of_enc_eq fun _ => rfl + have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one.computableInO.comp hword + have hclock := timeConstructible_succ_sq.computableInO.comp hword + have hU := computableInO_universal.comp (hdesc.prod (hsym.prod hclock)) + have hv := Diagonal.computableInO_verdict.comp hU + have hnot := (ComputableInDegree.of_finite (encIn := encBool) (encMid := encBool) + (fun b : Bool => !b)).inO_one.comp hv + obtain ⟨cD, hcD⟩ := hdesc.length_le + obtain ⟨cO, hcO⟩ := hU.length_le + obtain ⟨K, hK⟩ := accBound_aux 0 cD cO + have hbounds (q : List Bool × List Bool × List Bool) := by + have hD := hcD q + have hE := hcO q + have hNl : (encList encUnary ((frame q.2.1 ++ q.2.2).map eBit)).length ≤ + 3 * (frame q.2.1 ++ q.2.2).length := + (length_encList_le encUnary _ (b := 1) fun s hs => by + obtain ⟨b, -, rfl⟩ := List.mem_map.mp hs + cases b + · exact Nat.zero_le _ + · exact le_rfl).trans (by rw [List.length_map]; omega) + have hc : q.1.length + 1 ≤ (q.1.length + 1) ^ (dd + 1) := + Nat.le_self_pow (by omega) _ + have hA : (q.1.length + 1) ^ dd ≤ (q.1.length + 1) ^ (dd + 1) := + Nat.pow_le_pow_right (by omega) (by omega) + have hL := length_encNat_sq_le (frame q.2.1 ++ q.2.2).length + simp only [Function.comp_apply, encBits_apply, enc, length_encPair, List.length_append, + length_frame] at hD hE hNl hL ⊢ + refine hK (X := (q.1.length + 1) ^ (dd + 1) + q.2.1.length + q.2.2.length + 1) + (by omega) (by omega) (by omega) hD hNl (by omega) (by omega) (Nat.one_le_pow _ _ (by omega)) + hE + have e (q : List Bool × List Bool × List Bool) : accBound (dd + 1) q = + ((q.1.length + 1) ^ (dd + 1) + q.2.1.length + q.2.2.length + 1) ^ 4 * + (((frame q.2.1 ++ q.2.2).length + 1) ^ 2) ^ 2 := by + rw [accBound, ← pow_mul] + have hb (b : Bool) : (encBool b).length = 1 := rfl + refine ⟨dd + 1, (hnot.mono K (fun q => ?_) fun q => ?_).of_enc_eq fun q => rfl⟩ + · refine le_trans ?_ (Nat.mul_le_mul_left K (Nat.le_succ _)) + rw [e] + have h := (hbounds q).1 + simp only [Function.comp_apply, encBits_apply, enc, length_encPair, List.length_append, + length_frame] at ⊢ + simp only [hb] at h ⊢ + omega + · refine le_trans ?_ (Nat.mul_le_mul_left K (Nat.le_succ _)) + rw [e] + have h := (hbounds q).2 + simp only [Function.comp_apply, encBits_apply, enc, length_encPair, List.length_append, + length_frame] at ⊢ + simp only [hb] at h ⊢ + omega + +/-- 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 _)⟩ + +/-- **`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)`. -/ +private theorem 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₁⟩ := PolyBounded.exists_le_mul_two_pow' hT + obtain ⟨C₂, hC₂⟩ := PolyBounded.exists_le_mul_two_pow' hS + 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 + +/-- The numeric facts behind the bound of the brute force: the encoded pair of length `N`, the +certificate length `c`, the unary certificate length and the search. -/ +private theorem brute_bound_aux (C K₀ N c : ℕ) (hc : 1 ≤ c) : + N + (C * 2 ^ N + c * c) + 2 ^ (K₀ * (2 * N + 1 + c + c)) ≤ + (C + 3) * (2 ^ ((3 * K₀ + 4) * (N + c)) + 1) := by + set B := 2 ^ ((3 * K₀ + 4) * (N + c)) + have hN : 2 ^ N ≤ B := Nat.pow_le_pow_right (by norm_num) (by nlinarith) + have hN' : N < 2 ^ N := Nat.lt_two_pow_self + have hcc : c * c ≤ B := by + have h₁ : c * c ≤ 2 ^ c * 2 ^ c := + Nat.mul_le_mul Nat.lt_two_pow_self.le Nat.lt_two_pow_self.le + rw [← pow_add] at h₁ + exact h₁.trans (Nat.pow_le_pow_right (by norm_num) (by nlinarith)) + have hs : 2 ^ (K₀ * (2 * N + 1 + c + c)) ≤ B := + Nat.pow_le_pow_right (by norm_num) (by nlinarith) + have hC : C * 2 ^ N ≤ C * B := Nat.mul_le_mul_left _ hN + have e : (C + 3) * (B + 1) = C * B + 3 * B + (C + 3) := by ring + omega + +attribute [local fun_prop] ComputableInPolyTime.fst' ComputableInPolyTime.snd' in +/-- The brute force at the end of an interval runs within time exponential in the description, +the input and the certificate length. The certificate length is first written in unary, and every +certificate of that length is tried with the polynomial-time simulation. -/ +private theorem exists_computableInO_brute (k : ℕ) : ∃ K, ComputableInO + (fun q : List Bool × List Bool => + (Cslib.BitString.enumList (certLen k q.2.length)).any (accepts q.1 q.2)) + (encPair encBits encBits) encBool + (fun q => 2 ^ (K * ((encPair encBits encBits q).length + certLen k q.2.length))) + (fun q => 2 ^ (K * ((encPair encBits encBits q).length + certLen k q.2.length))) := by + obtain ⟨D, hacc⟩ := exists_computableInO_accepts + set encQ := encPair encBits encBits with hencQ + set encB := encPair encQ encUnary with hencB + set enc := encPair encB encBits with henc + -- the search, with the certificate length given in unary + have hB := ComputableInO.fst encB encBits + have hre := (hB.fst'.fst').prod (hB.fst'.snd'.prod (ComputableInO.snd encB encBits)) + have hf := hacc.comp hre + have hlen (r : ((List Bool × List Bool) × ℕ) × List Bool) : + r.1.1.1.length ≤ (enc r).length ∧ r.1.1.2.length ≤ (enc r).length ∧ + r.2.length ≤ (enc r).length ∧ (encB r.1).length ≤ (enc r).length := by + have e₁ : (enc r).length = 2 * (encB r.1).length + 1 + r.2.length := by + rw [henc, length_encPair, encBits_apply] + have e₂ : (encB r.1).length = 2 * (encQ r.1.1).length + 1 + r.1.2 := by + rw [hencB, length_encPair, encUnary_apply, List.length_replicate] + have e₃ : (encQ r.1.1).length = 2 * r.1.1.1.length + 1 + r.1.1.2.length := by + rw [hencQ, length_encPair, encBits_apply, encBits_apply] + omega + have hf' : ComputableInO (fun r : ((List Bool × List Bool) × ℕ) × List Bool => + accepts r.1.1.1 r.1.1.2 r.2) enc encBool + (fun r => 6 * (enc r).length + accBound D (r.1.1.1, r.1.1.2, r.2)) + (fun r => 6 * (enc r).length + accBound D (r.1.1.1, r.1.1.2, r.2)) := by + refine hf.mono_le (fun r => ?_) (fun r => ?_) <;> + · rw [← henc] + omega + have hpoly : PolyBounded (fun r => (enc r).length) fun r => + 6 * (enc r).length + accBound D (r.1.1.1, r.1.1.2, r.2) := + (PolyBounded.of_polynomiallyBounded (fun r => (enc r).length) + (bound := fun n => 6 * n + ((n + 1) ^ D + n + n + 1) ^ 4 * (2 * n + 1 + n + 1) ^ 4) + (by fun_prop)).mono fun r => by + obtain ⟨h₁, h₂, h₃, -⟩ := hlen r + simp only [accBound, List.length_append, length_frame] + gcongr + have hℓ : ComputableInPolyTime (fun b : (List Bool × List Bool) × ℕ => b.2) encB encUnary := by + fun_prop + obtain ⟨K₀, hsearch⟩ := exists_computableInO_any_enumList hf' hpoly hpoly hℓ + -- the certificate length in unary + have hL : ComputableInPolyTime (fun q : List Bool × List Bool => (k + 1) * (q.2.length + 1)) + encQ encUnary := by + fun_prop + obtain ⟨C, hcl⟩ := exists_computableInO_unary_two_pow hL + have hpair := (ComputableInO.of_eq (f := fun q : List Bool × List Bool => q) (encIn := encQ) + (encMid := encQ) fun _ => rfl).prod hcl + have h := hsearch.comp hpair + -- the bounds + refine ⟨3 * K₀ + 4, (h.mono (C + 3) (fun q => ?_) fun q => ?_).of_enc_eq fun q => rfl⟩ + all_goals + have e₁ : (encB (q, 2 ^ ((k + 1) * (q.2.length + 1)))).length = + 2 * (encQ q).length + 1 + 2 ^ ((k + 1) * (q.2.length + 1)) := by + rw [hencB, length_encPair, encUnary_apply, List.length_replicate] + have e₂ : (4 : ℕ) ^ ((k + 1) * (q.2.length + 1)) = + 2 ^ ((k + 1) * (q.2.length + 1)) * 2 ^ ((k + 1) * (q.2.length + 1)) := by + rw [← mul_pow] + norm_num + have hc : 1 ≤ 2 ^ ((k + 1) * (q.2.length + 1)) := Nat.one_le_two_pow + have h := brute_bound_aux C K₀ (encQ q).length _ hc + have hcc := Nat.le_mul_of_pos_left (2 ^ ((k + 1) * (q.2.length + 1))) hc + simp only [e₁, e₂, certLen] at h ⊢ + omega + +/-- Weaken only the time bound, keeping the space bound. -/ +private theorem computableInO_mono_time {α β : Type*} {f : α → β} + {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' : α → ℕ} + (h : ComputableInO f encIn encOut T S) (k : ℕ) (hT : ∀ a, T a ≤ k * (T' a + 1)) : + ComputableInO f encIn encOut T' S := + h.mono (k + 1) (fun a => (hT a).trans (Nat.mul_le_mul_right _ (Nat.le_succ k))) + fun _ => (Nat.le_succ _).trans (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) + +/-- The cost of the tests of the verifier: quadratic in the encoded input, times the square of a +bound `4 ^ ((k + 2) * (n + 1))` on the horizon, which the tests write in unary. -/ +private def cheap (k : ℕ) (p : List Bool × List Bool) : ℕ := + ((encPair encBits encBits p).length + 1) ^ 2 * (4 ^ ((k + 2) * (p.1.length + 1))) ^ 2 + +/-- The numeric facts behind `cheap`, for an encoded input of length `N`, an input of length `n` +and a horizon `Z` of at most `G * Y`. -/ +private theorem cheap_aux (G : ℕ) {N n Z Y : ℕ} (hn : n ≤ N) (hY : 1 ≤ Y) (hZ : Z ≤ G * Y) : + N + 1 ≤ (N + 1) ^ 2 * Y ^ 2 ∧ (Z + 1) ^ 2 ≤ (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) ∧ + (2 * N + 4 + Z) ^ 2 ≤ (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) := by + have hY2 : 1 ≤ Y ^ 2 := Nat.one_le_pow _ _ hY + have hN2 : N + 1 ≤ (N + 1) ^ 2 := Nat.le_self_pow (by norm_num) _ + have hsq : (2 * N + 4 + Z) ^ 2 ≤ (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) := + calc (2 * N + 4 + Z) ^ 2 ≤ ((G + 4) * ((N + 1) * Y)) ^ 2 := by + apply Nat.pow_le_pow_left + have h₁ : N + 1 ≤ (N + 1) * Y := Nat.le_mul_of_pos_right _ hY + have h₂ : Y ≤ (N + 1) * Y := Nat.le_mul_of_pos_left _ (by omega) + have e : (G + 4) * ((N + 1) * Y) = G * ((N + 1) * Y) + 4 * ((N + 1) * Y) := by ring + have := Nat.mul_le_mul_left G h₂ + omega + _ = (G + 4) ^ 2 * ((N + 1) ^ 2 * Y ^ 2) := by ring + refine ⟨hN2.trans (Nat.le_mul_of_pos_right _ hY2), + (Nat.pow_le_pow_left (by omega) 2).trans hsq, hsq⟩ + +/-- The horizon of the interval of `unframe x` is at most `4 ^ ((k + 2) * (x.length + 1))`, and the +cost of writing it in unary is at most twice that bound plus its square. -/ +private theorem horizon_le (k C : ℕ) (x : List Bool) : + horizon k (2 * (unframe x).length + 1) ≤ 4 ^ ((k + 2) * (x.length + 1)) ∧ + C * 2 ^ (2 * (unframe x).length + 1) + 4 ^ ((k + 2) * (2 * (unframe x).length + 1 + 1)) ≤ + 2 * C * 4 ^ ((k + 2) * (x.length + 1)) + (4 ^ ((k + 2) * (x.length + 1))) ^ 2 := by + have hu := length_unframe_le x + have h4 (a : ℕ) : (4 : ℕ) ^ a = 2 ^ (2 * a) := by rw [pow_mul]; norm_num + refine ⟨?_, ?_⟩ + · rw [horizon, h4] + exact Nat.pow_le_pow_right (by norm_num) (by nlinarith) + · have h₁ : 2 ^ (2 * (unframe x).length + 1) ≤ 2 * 4 ^ ((k + 2) * (x.length + 1)) := by + rw [h4, pow_succ, mul_comm] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) (by nlinarith)) + have h₂ : 4 ^ ((k + 2) * (2 * (unframe x).length + 1 + 1)) ≤ + (4 ^ ((k + 2) * (x.length + 1))) ^ 2 := by + rw [← pow_mul] + exact Nat.pow_le_pow_right (by norm_num) (by nlinarith) + have := Nat.mul_le_mul_left C h₁ + have e : C * (2 * 4 ^ ((k + 2) * (x.length + 1))) = 2 * C * 4 ^ ((k + 2) * (x.length + 1)) := by + ring + omega + +attribute [local fun_prop] ComputableInPolyTime.fst' ComputableInPolyTime.snd' in +/-- **The verifier of the exponential lazy diagonal is computable**, within the cost of its tests +plus the cost of the branch taken: the simulation, or the brute force at the end of an interval. -/ +private theorem exists_computableInO_verifier (k : ℕ) : + ∃ (D K : ℕ) (S : List Bool × List Bool → ℕ), + ComputableInO (verifier k) (encPair encBits encBits) encBool + (fun p => cheap k p + if Diagonal.shortDesc (unframe p.1) then + (cheap k p + if Nat.size (p.1.length + 1) ≤ horizon k (2 * (unframe p.1).length + 1) then + cheap k p + accBound D (unframe (unframe p.1), p.1 ++ [false], p.2) + else (cheap k p + if Nat.size p.1.length ≤ horizon k (2 * (unframe p.1).length + 1) then + cheap k p + 2 ^ (K * ((encPair encBits encBits (unframe (unframe p.1), + frame (unframe p.1))).length + certLen k (2 * (unframe p.1).length + 1))) + else cheap k p)) + else cheap k p) S := by + obtain ⟨D, hacc⟩ := exists_computableInO_accepts + obtain ⟨K, hbrute⟩ := exists_computableInO_brute k + have hx := ComputableInO.fst encBits encBits + have hun : ComputableInO unframe encBits encBits (fun z => z.length) (fun z => z.length) := + ComputableInO.of_linear (.of_unframe fun _ => rfl) + have hfr : ComputableInO frame encBits encBits (fun z => z.length) (fun z => z.length) := + ComputableInO.of_linear (.of_frame fun _ => rfl) + have hw := hun.comp hx + have hcode := hun.comp hw + have hbase := hfr.comp hw + have hsnoc : ComputableInO (fun p : List Bool × List Bool => p.1 ++ [false]) + (encPair encBits encBits) encBits + (fun p => (encPair encBits encBits p).length + (encPair encBits encBits p).length) + (fun p => (encPair encBits encBits p).length + (encPair encBits encBits p).length) := + hx.append (ComputableInO.const (encMid := encBits) [false]) fun _ => rfl + have hsz : ComputableInO (fun z : List Bool => Nat.size z.length) encBits encUnary + (fun z => (z.length + 1) ^ 2 + (encNat z.length).length) + (fun z => z.length + 1 + (encNat z.length).length) := + (ComputableInO.lengthUnary.comp (ComputableInO.lengthNat.of_enc_eq (encC := encBits) + (g := fun z : List Bool => encNat z.length) fun _ => rfl)).of_enc_eq fun z => by + simp [encNat_apply, Nat.size_eq_bits_len] + have hL : ComputableInPolyTime (fun z : List Bool => (k + 2) * (z.length + 1)) encBits + encUnary := by + fun_prop + obtain ⟨CE, hE₀⟩ := exists_computableInO_unary_two_pow hL + have hE := hE₀.comp hbase + -- the numeric facts about the tests + have hfacts (p : List Bool × List Bool) : (unframe p.1).length ≤ p.1.length ∧ + p.1.length ≤ (encPair encBits encBits p).length ∧ + (encPair encBits encBits p).length + 1 ≤ cheap k p ∧ + (horizon k (2 * (unframe p.1).length + 1) + 1) ^ 2 ≤ 25 * cheap k p ∧ + (2 * (encPair encBits encBits p).length + 4 + + horizon k (2 * (unframe p.1).length + 1)) ^ 2 ≤ 25 * cheap k p ∧ + CE * 2 ^ (2 * (unframe p.1).length + 1) + + 4 ^ ((k + 2) * (2 * (unframe p.1).length + 1 + 1)) ≤ (2 * CE + 1) * cheap k p := by + have hu := length_unframe_le p.1 + have hn : p.1.length ≤ (encPair encBits encBits p).length := by + simp only [length_encPair, encBits_apply] + omega + obtain ⟨hZ, hE'⟩ := horizon_le k CE p.1 + set Y := 4 ^ ((k + 2) * (p.1.length + 1)) + have hY : 1 ≤ Y := Nat.one_le_pow _ _ (by norm_num) + obtain ⟨h₁, h₂, h₃⟩ := cheap_aux 1 hn hY + (Z := horizon k (2 * (unframe p.1).length + 1)) (by omega) + have hc : cheap k p = ((encPair encBits encBits p).length + 1) ^ 2 * Y ^ 2 := rfl + have hY₁ : Y ≤ Y ^ 2 := Nat.le_self_pow (by norm_num) _ + have hY₂ : Y ^ 2 ≤ cheap k p := by + rw [hc] + exact Nat.le_mul_of_pos_left _ (Nat.pow_pos (by omega)) + have e : (2 * CE + 1) * cheap k p = 2 * CE * cheap k p + cheap k p := by ring + have := Nat.mul_le_mul_left (2 * CE) (hY₁.trans hY₂) + norm_num only at h₂ h₃ + rw [hc] + exact ⟨hu, hn, hc ▸ h₁, h₂, h₃, by rw [← hc]; omega⟩ + set A := 8 + 4 * 25 + (2 * CE + 1) + have e (p : List Bool × List Bool) : A * (cheap k p + 1) = + 8 * cheap k p + 4 * (25 * cheap k p) + (2 * CE + 1) * cheap k p + A := by ring + have hc₀ := computableInO_mono_time (Diagonal.computableInO_shortDesc.comp hw) (T' := cheap k) + A fun p => by + obtain ⟨hu, hn, h₁, -, h₃, -⟩ := hfacts p + have : ((unframe p.1).length + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + horizon k (2 * (unframe p.1).length + 1)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + simp only [Function.comp_apply] at ⊢ + have := e p + omega + have hc₁ := computableInO_mono_time (ComputableInO.unaryLe.comp ((hsz.comp hsnoc).prod hE)) + (T' := cheap k) A fun p => by + obtain ⟨hu, hn, h₁, h₂, h₃, h₄⟩ := hfacts p + have hs := Nat.size_le.mpr (Nat.lt_two_pow_self (n := p.1.length + 1)) + have he := Universal.length_encNat_le (p.1.length + 1) + have hsq : (p.1.length + 1 + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + horizon k (2 * (unframe p.1).length + 1)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hsq' : (2 * Nat.size (p.1.length + 1) + 1 + horizon k (2 * (unframe p.1).length + 1) + + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + horizon k (2 * (unframe p.1).length + 1)) ^ 2 := + Nat.pow_le_pow_left (by omega) 2 + simp only [Function.comp_apply, length_encPair (enc₁ := encUnary) (enc₂ := encUnary), + encUnary_apply, List.length_replicate, List.length_append, List.length_singleton, + length_frame, encBits_apply] at ⊢ + simp only [horizon] at hsq hsq' h₂ h₃ + have := e p + omega + have hc₂ := computableInO_mono_time (ComputableInO.unaryLe.comp ((hsz.comp hx).prod hE)) + (T' := cheap k) A fun p => by + obtain ⟨hu, hn, h₁, h₂, h₃, h₄⟩ := hfacts p + have hs := Nat.size_le.mpr (Nat.lt_two_pow_self (n := p.1.length)) + have he := Universal.length_encNat_le p.1.length + have hsq : (p.1.length + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + horizon k (2 * (unframe p.1).length + 1)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hsq' : (2 * Nat.size p.1.length + 1 + horizon k (2 * (unframe p.1).length + 1) + + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + + horizon k (2 * (unframe p.1).length + 1)) ^ 2 := + Nat.pow_le_pow_left (by omega) 2 + simp only [Function.comp_apply, length_encPair (enc₁ := encUnary) (enc₂ := encUnary), + encUnary_apply, List.length_replicate, length_frame, encBits_apply] at ⊢ + simp only [horizon] at hsq hsq' h₂ h₃ + have := e p + omega + have hc₁' := hc₁.of_enc_eq (encC := encBool) (g := fun p : List Bool × List Bool => + decide (Nat.size (p.1.length + 1) ≤ horizon k (2 * (unframe p.1).length + 1))) fun p => by + simp only [Function.comp_apply, horizon, length_frame, List.length_append, + List.length_singleton] + rfl + have hc₂' := hc₂.of_enc_eq (encC := encBool) (g := fun p : List Bool × List Bool => + decide (Nat.size p.1.length ≤ horizon k (2 * (unframe p.1).length + 1))) fun p => by + simp only [Function.comp_apply, horizon, length_frame] + rfl + have hf₁ := computableInO_mono_time + (hacc.comp (hcode.prod (hsnoc.prod (ComputableInO.snd encBits encBits)))) + (T' := fun p => cheap k p + accBound D (unframe (unframe p.1), p.1 ++ [false], p.2)) 7 + fun p => by + obtain ⟨hu, hn, h₁, -⟩ := hfacts p + simp only [Function.comp_apply] at ⊢ + have e : 7 * (cheap k p + accBound D (unframe (unframe p.1), p.1 ++ [false], p.2) + 1) = + 7 * cheap k p + 7 * accBound D (unframe (unframe p.1), p.1 ++ [false], p.2) + 7 := by + ring + omega + have hf₂ := computableInO_mono_time ((ComputableInDegree.of_finite (encIn := encBool) + (encMid := encBool) (fun b : Bool => !b)).inO_one.comp (hbrute.comp (hcode.prod hbase))) + (T' := fun p => cheap k p + 2 ^ (K * ((encPair encBits encBits (unframe (unframe p.1), + frame (unframe p.1))).length + certLen k (2 * (unframe p.1).length + 1)))) 7 + fun p => by + obtain ⟨hu, hn, h₁, -⟩ := hfacts p + have hb : (encBool ((Cslib.BitString.enumList (certLen k (frame (unframe p.1)).length)).any + (accepts (unframe (unframe p.1)) (frame (unframe p.1))))).length = 1 := rfl + simp only [Function.comp_apply, hb] at ⊢ + rw [length_frame] + set B := 2 ^ (K * ((encPair encBits encBits (unframe (unframe p.1), + frame (unframe p.1))).length + certLen k (2 * (unframe p.1).length + 1))) + have e : 7 * (cheap k p + B + 1) = 7 * cheap k p + 7 * B + 7 := by ring + omega + have hfalse := computableInO_mono_time (ComputableInO.const (encIn := encPair encBits encBits) + (encMid := encBool) false) (T' := cheap k) 1 fun p => by + obtain ⟨hu, hn, h₁, -⟩ := hfacts p + omega + have h := hc₀.ite (hc₁'.ite hf₁ (hc₂'.ite hf₂ hfalse)) hfalse + refine ⟨D, K, _, (h.of_enc_eq fun p => ?_).mono_le (fun p => le_of_eq ?_) fun p => le_rfl⟩ + · congr 1 + simp only [verifier, Function.comp_apply, decide_eq_true_eq, length_frame] + · simp only [Function.comp_apply, decide_eq_true_eq] + +/-- `2 ^ a ≤ 2 ^ b * 2 ^ c` whenever `a ≤ c + b`. -/ +private theorem two_pow_le_two_pow_mul {a b c : ℕ} (h : a ≤ c + b) : 2 ^ a ≤ 2 ^ b * 2 ^ c := by + rw [← pow_add] + exact Nat.pow_le_pow_right (by norm_num) (by omega) + +/-- **The exponential lazy diagonal is decidable in nondeterministic time +`O(2 ^ ((8 * k + 16) * n))`.** Guess a certificate of length `2 ^ ((k + 1) * (n + 2))` and run the +verifier (`Cslib.Complexity.setOf_exists_mem_NTIME`). Below the end of an interval, the verifier +simulates a verifier on the input one bit longer with a certificate of that length, within time +polynomial in the certificate. At the end of an interval of start `P`, it tries every certificate +on the input of length `P`, within time `2 ^ O(certLen k P)`, which is linear in the length `n` of +the input, since `n + 1 = 2 ^ horizon k P` there and `horizon k P = 2 ^ (P + 1) * certLen k P`. -/ +theorem expLazyDiagonal_mem_NTIME (k : ℕ) : + expLazyDiagonal k ∈ NTIME encBits fun n => 2 ^ ((8 * k + 16) * n) := by + obtain ⟨D, K, S, hV⟩ := exists_computableInO_verifier k + have hL : ComputableInPolyTime (fun x : List Bool => (k + 1) * (x.length + 2)) encBits + encUnary := by + fun_prop + obtain ⟨Cℓ, hℓ₀⟩ := exists_computableInO_unary_two_pow hL + have hℓ := hℓ₀.of_enc_eq (encC := encUnary) + (g := fun x : List Bool => certLen k (x.length + 1)) fun x => rfl + obtain ⟨CD, hCD⟩ := PolynomiallyBounded.exists_le_mul_two_pow (p := fun m => (m + 1) ^ D) + (by fun_prop) + set B₀ := 3 * K * 2 ^ ((k + 1) * (3 * K)) + set A₁ := 2 ^ (8 * k + 14) + set A₂ := 81 * (CD + 3) ^ 4 * 2 ^ (16 * k + 16) + set A₃ := Cℓ + 2 ^ (4 * k + 4) + refine setOf_exists_mem_NTIME hℓ hV (C := 2 + A₃ + 4 * A₁ + A₂ + 2 ^ B₀) fun x v hv => ?_ + simp only [encBits_apply] + set n := x.length with hn + set V := 2 ^ ((k + 1) * (n + 2)) with hVdef + have hv' : v.length = V := by + rw [hv] + rfl + set M := 2 ^ ((8 * k + 16) * n) + have hnV : 4 * n + 4 ≤ V := + calc 4 * n + 4 ≤ 2 ^ (n + 2) := by + have := Nat.lt_two_pow_self (n := n) + rw [pow_succ, pow_succ] + omega + _ ≤ V := Nat.pow_le_pow_right (by norm_num) (Nat.le_mul_of_pos_left _ (by omega)) + have hnM : n + 1 ≤ M := by + calc n + 1 ≤ 2 ^ n := Nat.lt_two_pow_self + _ ≤ M := Nat.pow_le_pow_right (by norm_num) (Nat.le_mul_of_pos_left _ (by omega)) + -- the tests + have hcheap : cheap k (x, v) ≤ A₁ * M := by + have hN : (encPair encBits encBits (x, v)).length + 1 ≤ 2 * V := by + simp only [length_encPair, encBits_apply, hv', ← hn] + omega + calc cheap k (x, v) = ((encPair encBits encBits (x, v)).length + 1) ^ 2 * + (4 ^ ((k + 2) * (n + 1))) ^ 2 := rfl + _ ≤ (2 * V) ^ 2 * (4 ^ ((k + 2) * (n + 1))) ^ 2 := + Nat.mul_le_mul_right _ (Nat.pow_le_pow_left hN 2) + _ = 2 ^ (2 + 2 * ((k + 1) * (n + 2)) + 4 * ((k + 2) * (n + 1))) := by + rw [hVdef, show (4 : ℕ) = 2 ^ 2 by rfl] + simp only [mul_pow, ← pow_mul, ← pow_add] + ring_nf + _ ≤ A₁ * M := two_pow_le_two_pow_mul (by ring_nf; nlinarith [Nat.zero_le (k * n)]) + -- the simulation, when the description is short + have hacc (h₀ : Diagonal.shortDesc (unframe x) = true) : + accBound D (unframe (unframe x), x ++ [false], v) ≤ A₂ * M := by + have hs : 2 ^ (unframe (unframe x)).length ≤ (unframe x).length := of_decide_eq_true h₀ + have hu := length_unframe_le x + have hD : ((unframe (unframe x)).length + 1) ^ D ≤ CD * n := + (hCD _).trans (Nat.mul_le_mul_left _ (hs.trans hu)) + have hb : ((unframe (unframe x)).length + 1) ^ D + (n + 1) + V + 1 ≤ (CD + 3) * V := by + have h₂ : CD * n ≤ CD * V := Nat.mul_le_mul_left _ (by omega) + have e : (CD + 3) * V = CD * V + 3 * V := by ring + omega + have hw : (frame (x ++ [false]) ++ v).length + 1 ≤ 3 * V := by + simp only [List.length_append, length_frame, List.length_singleton, hv', ← hn] + omega + calc accBound D (unframe (unframe x), x ++ [false], v) = + (((unframe (unframe x)).length + 1) ^ D + (n + 1) + V + 1) ^ 4 * + ((frame (x ++ [false]) ++ v).length + 1) ^ 4 := by + simp only [accBound, List.length_append, List.length_singleton, hv', ← hn] + _ ≤ ((CD + 3) * V) ^ 4 * (3 * V) ^ 4 := + Nat.mul_le_mul (Nat.pow_le_pow_left hb 4) (Nat.pow_le_pow_left hw 4) + _ = 81 * (CD + 3) ^ 4 * 2 ^ (8 * ((k + 1) * (n + 2))) := by + rw [hVdef] + simp only [mul_pow, ← pow_mul] + ring + _ ≤ 81 * (CD + 3) ^ 4 * (2 ^ (16 * k + 16) * M) := + Nat.mul_le_mul_left _ (two_pow_le_two_pow_mul (by ring_nf; nlinarith)) + _ = A₂ * M := by ring + -- the brute force, at the end of an interval + have hbrute (h₁ : ¬Nat.size (n + 1) ≤ horizon k (2 * (unframe x).length + 1)) : + 2 ^ (K * ((encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen k (2 * (unframe x).length + 1))) ≤ n + 1 + 2 ^ B₀ := by + set P := 2 * (unframe x).length + 1 with hP + have hE : 2 ^ horizon k P ≤ n + 1 := by + rw [Nat.size_le, not_lt] at h₁ + exact h₁ + have hc := length_unframe_le (unframe x) + have hPc : P + 1 ≤ certLen k P := + calc P + 1 ≤ 2 ^ (P + 1) := Nat.lt_two_pow_self.le + _ ≤ certLen k P := Nat.pow_le_pow_right (by norm_num) (Nat.le_mul_of_pos_left _ (by omega)) + have hlen : (encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen k P ≤ 3 * certLen k P := by + simp only [length_encPair, encBits_apply, length_frame] + omega + rcases le_or_gt (3 * K) (2 ^ (P + 1)) with hK | hK + · have hle : K * ((encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen k P) ≤ horizon k P := + calc _ ≤ K * (3 * certLen k P) := Nat.mul_le_mul_left _ hlen + _ = 3 * K * certLen k P := by ring + _ ≤ 2 ^ (P + 1) * certLen k P := Nat.mul_le_mul_right _ hK + _ = horizon k P := by + rw [certLen, horizon, ← pow_add] + congr 1 + ring + exact ((Nat.pow_le_pow_right (by norm_num) hle).trans hE).trans (Nat.le_add_right _ _) + · have hP3 : P + 1 ≤ 3 * K := (Nat.lt_two_pow_self.trans hK).le + have hle : K * ((encPair encBits encBits (unframe (unframe x), frame (unframe x))).length + + certLen k P) ≤ B₀ := + calc _ ≤ K * (3 * certLen k P) := Nat.mul_le_mul_left _ hlen + _ = 3 * K * certLen k P := by ring + _ ≤ 3 * K * 2 ^ ((k + 1) * (3 * K)) := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) + (Nat.mul_le_mul_left _ hP3)) + exact (Nat.pow_le_pow_right (by norm_num) hle).trans (Nat.le_add_left _ _) + -- the certificate length + have hTℓ : Cℓ * 2 ^ n + 4 ^ ((k + 1) * (n + 2)) ≤ A₃ * M := by + have h₁ : 2 ^ n ≤ M := Nat.pow_le_pow_right (by norm_num) (Nat.le_mul_of_pos_left _ (by omega)) + have h₂ : 4 ^ ((k + 1) * (n + 2)) ≤ 2 ^ (4 * k + 4) * M := by + rw [show (4 : ℕ) = 2 ^ 2 by rfl, ← pow_mul] + exact two_pow_le_two_pow_mul (by ring_nf; nlinarith) + have e : A₃ * M = Cℓ * M + 2 ^ (4 * k + 4) * M := by ring + have := Nat.mul_le_mul_left Cℓ h₁ + omega + have e : (2 + A₃ + 4 * A₁ + A₂ + 2 ^ B₀) * M = + 2 * M + A₃ * M + 4 * (A₁ * M) + A₂ * M + 2 ^ B₀ * M := by ring + have hB : 2 ^ B₀ ≤ 2 ^ B₀ * M := Nat.le_mul_of_pos_right _ (by omega) + clear_value M A₁ A₂ A₃ B₀ + generalize 2 + A₃ + 4 * A₁ + A₂ + 2 ^ B₀ = C at * + generalize 2 ^ B₀ = Q at * + split_ifs with h₀ h₁ h₂ + · have := hacc h₀ + omega + · have := hbrute h₁ + omega + · omega + · omega + +/-! ### The hierarchy -/ + +/-- **A nondeterministic exponential time hierarchy.** For every `k`, nondeterministic time +`O(2 ^ (k * n))` is strictly contained in nondeterministic time `O(2 ^ (e * n))` whenever +`8 * k + 16 ≤ e`. The exponential lazy diagonal `Cslib.Complexity.expLazyDiagonal k` separates them +(`Cslib.Complexity.expLazyDiagonal_mem_NTIME`, `Cslib.Complexity.expLazyDiagonal_notMem_NTIME`). +This is a coarse exponential form of the nondeterministic time hierarchy theorem +[Arora and Barak, Theorem 3.3][AroraBarak07]. -/ +theorem NTIME_two_pow_ssubset_NTIME_two_pow_of_le {k e : ℕ} (h : 8 * k + 16 ≤ e) : + NTIME encBits (fun n => 2 ^ (k * n)) ⊂ NTIME encBits fun n => 2 ^ (e * n) := by + have hsub : ∀ {a b : ℕ}, a ≤ b → + NTIME encBits (fun n => 2 ^ (a * n)) ⊆ NTIME encBits fun n => 2 ^ (b * n) := + fun hab => NTIME_mono fun n => Nat.pow_le_pow_right (by norm_num) (Nat.mul_le_mul_right _ hab) + exact (Set.ssubset_iff_of_subset (hsub (by omega))).mpr + ⟨expLazyDiagonal k, hsub h (expLazyDiagonal_mem_NTIME k), expLazyDiagonal_notMem_NTIME k⟩ + +/-- **`NE` is not contained in `NTIME (2 ^ (k * n))`**, for any `k`: the exponential lazy diagonal +`Cslib.Complexity.expLazyDiagonal k` is in `NE` and not in `NTIME (2 ^ (k * n))`. -/ +theorem exists_mem_NE_notMem_NTIME_two_pow (k : ℕ) : + ∃ H ∈ NE encBits, H ∉ NTIME encBits fun n => 2 ^ (k * n) := + ⟨expLazyDiagonal k, Set.mem_iUnion.mpr ⟨_, expLazyDiagonal_mem_NTIME k⟩, + expLazyDiagonal_notMem_NTIME k⟩ + +end Cslib.Complexity diff --git a/ComplexityTests/NondeterministicExponentialTimeHierarchy.lean b/ComplexityTests/NondeterministicExponentialTimeHierarchy.lean new file mode 100644 index 0000000000..a978ef3fbc --- /dev/null +++ b/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 diff --git a/ROADMAP.md b/ROADMAP.md index c6c58938ad..57cba26c4b 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -183,11 +183,12 @@ index links to canonical definitions rather than keeping a second set. degrees `1 ≤ a < b`, and the `O(t log t)` universal simulation ([#800]) gives `DTIME f ⊂ DTIME g` for time-constructible `f ≥ n` once `(f + 1) * polylog f ≤ g`, with an absolute exponent (`Hierarchy/TimePolylog`). For nondeterministic time, lazy diagonalization - separates degree `d` from degree `6 * d + 14`. 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, the nondeterministic hierarchy at every pair of integer - degrees by padding, and sharp nondeterministic and alternating time hierarchies with certified - simulators. + separates degree `d` from degree `6 * d + 14`, and `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, the nondeterministic hierarchy at every + pair of integer degrees by padding, and sharp nondeterministic and alternating time + hierarchies with certified simulators. - The space hierarchy for `log n ≤ g n`, which needs a universal simulation that does not hold its input. - **Space:** Savitch bounds for general space-constructible functions. From 48a6545c6091b21f6b1d19854e8be746217cbef9 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:07:01 -0400 Subject: [PATCH 6/9] refactor(Machines/PTM): make the pair sampler's proof configurations private The induction configurations `PairSampler.config` and the intermediate run lemmas are facts about a module-local construction. Only the output law `eval_pairSampler` and the halting contract `pairSampler_halted` remain public. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../MultiTape/Probabilistic/PairSampler.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean index 7b6a8192b7..bce12d8550 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean @@ -81,7 +81,7 @@ def pairSampler : MultiTapePTM 0 Bool Phase where namespace PairSampler /-- The sampler at an input position, with the output written so far. -/ -def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : List Bool) +private def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : List Bool) (h : index ≤ input.length) : Config 0 Bool Phase Empty input where tapes := { state := state @@ -91,7 +91,7 @@ def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : Li output := output } /-- Reading a remaining symbol writes the emitted symbol and advances once. -/ -theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) +private theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) (q : Phase) (o : Option Bool) (s : Option Phase) : (config input (some q) index output (by lia)).step { inputTape := 1, workTapes := Fin.elim0, output := o, state := s } @@ -105,7 +105,7 @@ theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) rfl /-- One live transition at a remaining symbol: draw a coin and take the selected step. -/ -theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < input.length) +private theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < input.length) (q : Phase) (fuel : ℕ) : ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) (config input (some q) index output (by lia))) = @@ -121,7 +121,7 @@ theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < inpu rfl /-- At the right boundary the sampler halts, drawing and discarding one coin. -/ -theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : +private theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) (config input (some q) input.length output le_rfl)) = PMF.pure (config input none input.length output le_rfl) := by @@ -160,7 +160,7 @@ theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : rw [hhalt, PMF.bind_const] /-- The tail phase: one fresh fair bit per remaining symbol, then halting at the boundary. -/ -theorem eval_run_tail (input : List Bool) (remaining : ℕ) : +private theorem eval_run_tail (input : List Bool) (remaining : ℕ) : ∀ (index : ℕ) (output : List Bool) (h : index + remaining = input.length), ProbComp.eval (pairSampler.runClosedConfigFrom (remaining + 1) (config input (some .tail) index output (by lia))) = @@ -183,7 +183,7 @@ theorem eval_run_tail (input : List Bool) (remaining : ℕ) : List.append_assoc, List.singleton_append] /-- The copying phase: a framed word is copied verbatim, ignoring the coins drawn meanwhile. -/ -theorem eval_run_frame (input rest : List Bool) (fuel : ℕ) (y : List Bool) : +private theorem eval_run_frame (input rest : List Bool) (fuel : ℕ) (y : List Bool) : ∀ (pre output : List Bool) (hin : input = pre ++ frame y ++ rest), ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y).length + fuel) (config input (some .tag) pre.length output (by subst hin; simp))) = @@ -234,7 +234,7 @@ open PairSampler /-- The final configuration retains the framed word and a uniform certificate, and has halted at the right boundary. -/ -theorem eval_runClosedConfig_pairSampler (y r : List Bool) : +private theorem eval_runClosedConfig_pairSampler (y r : List Bool) : ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y ++ r).length + 1) (pairSampler.initialConfig (frame y ++ r))) = (BitString.uniformList r.length).map (fun w => From 4e1cc48bf9f846fc5091d0433192dfc60fe689cb Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:08:39 -0400 Subject: [PATCH 7/9] refactor(BigO/Bounds): make ComputableInO.mono_time public Weakening only the time bound of `ComputableInO`, keeping the space bound, is a general monotonicity law. It now sits beside `ComputableInO.mono` instead of as a private copy in the lazy-diagonal hierarchy. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Classes/Hierarchy/NondeterministicTime.lean | 8 -------- .../Machines/Turing/MultiTape/Complexity/BigO/Bounds.lean | 6 ++++++ 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean index 38d0ff53de..4f2eb8644d 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean @@ -461,14 +461,6 @@ private theorem exists_computableInO_brute (d : ℕ) : ∃ K, ComputableInO fun_prop exact exists_computableInO_any_enumList hf hpoly hpoly hℓ -/-- Weaken only the time bound, keeping the space bound. -/ -private theorem _root_.Turing.MultiTapeTM.ComputableInO.mono_time {α β : Type*} {f : α → β} - {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' : α → ℕ} - (h : ComputableInO f encIn encOut T S) (k : ℕ) (hT : ∀ a, T a ≤ k * (T' a + 1)) : - ComputableInO f encIn encOut T' S := - h.mono (k + 1) (fun a => (hT a).trans (Nat.mul_le_mul_right _ (Nat.le_succ k))) - fun _ => (Nat.le_succ _).trans (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) - /-- The cost of the tests of the verifier: quadratic in the encoded input, times a power of the length of the input that pays for the clock in unary. -/ private def cheap (d : ℕ) (p : List Bool × List Bool) : ℕ := diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Bounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Bounds.lean index 048e3d7038..a38b07c63e 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Bounds.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Bounds.lean @@ -44,6 +44,12 @@ theorem mono {T' S' : α → ℕ} (h : ComputableInO f encIn encOut T S) (k : of_bounds hc (c * (k + 1)) (fun a => by nlinarith [hT a]) (fun a => by nlinarith [hS a]) (fun a => by nlinarith [hS a, hl a]) +/-- Weaken only the time bound up to a constant, keeping the space bound. -/ +theorem mono_time {T' : α → ℕ} (h : ComputableInO f encIn encOut T S) (k : ℕ) + (hT : ∀ a, T a ≤ k * (T' a + 1)) : ComputableInO f encIn encOut T' S := + h.mono (k + 1) (fun a => (hT a).trans (Nat.mul_le_mul_right _ (Nat.le_succ k))) + fun _ => (Nat.le_succ _).trans (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) + /-- Pointwise larger bounds retain the same encoded-output charge. -/ theorem mono_le {T' S' : α → ℕ} (h : ComputableInO f encIn encOut T S) (hT : ∀ a, T a ≤ T' a) (hS : ∀ a, S a ≤ S' a) : From 52a4e6ce3eb8b2c75d66b22da6d822b627df6503 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:09:28 -0400 Subject: [PATCH 8/9] refactor(Classes/Hierarchy): use the public ComputableInO.mono_time The exponential lazy diagonal drops its private copy of the time-only weakening and uses the public rule from `BigO/Bounds`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../NondeterministicExponentialTime.lean | 20 ++++++------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean index 93bc07f01e..a9f86f59af 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean @@ -544,14 +544,6 @@ private theorem exists_computableInO_brute (k : ℕ) : ∃ K, ComputableInO simp only [e₁, e₂, certLen] at h ⊢ omega -/-- Weaken only the time bound, keeping the space bound. -/ -private theorem computableInO_mono_time {α β : Type*} {f : α → β} - {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S T' : α → ℕ} - (h : ComputableInO f encIn encOut T S) (k : ℕ) (hT : ∀ a, T a ≤ k * (T' a + 1)) : - ComputableInO f encIn encOut T' S := - h.mono (k + 1) (fun a => (hT a).trans (Nat.mul_le_mul_right _ (Nat.le_succ k))) - fun _ => (Nat.le_succ _).trans (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) - /-- The cost of the tests of the verifier: quadratic in the encoded input, times the square of a bound `4 ^ ((k + 2) * (n + 1))` on the horizon, which the tests write in unary. -/ private def cheap (k : ℕ) (p : List Bool × List Bool) : ℕ := @@ -670,7 +662,7 @@ private theorem exists_computableInO_verifier (k : ℕ) : set A := 8 + 4 * 25 + (2 * CE + 1) have e (p : List Bool × List Bool) : A * (cheap k p + 1) = 8 * cheap k p + 4 * (25 * cheap k p) + (2 * CE + 1) * cheap k p + A := by ring - have hc₀ := computableInO_mono_time (Diagonal.computableInO_shortDesc.comp hw) (T' := cheap k) + have hc₀ := ComputableInO.mono_time (Diagonal.computableInO_shortDesc.comp hw) (T' := cheap k) A fun p => by obtain ⟨hu, hn, h₁, -, h₃, -⟩ := hfacts p have : ((unframe p.1).length + 1) ^ 2 ≤ (2 * (encPair encBits encBits p).length + 4 + @@ -678,7 +670,7 @@ private theorem exists_computableInO_verifier (k : ℕ) : simp only [Function.comp_apply] at ⊢ have := e p omega - have hc₁ := computableInO_mono_time (ComputableInO.unaryLe.comp ((hsz.comp hsnoc).prod hE)) + have hc₁ := ComputableInO.mono_time (ComputableInO.unaryLe.comp ((hsz.comp hsnoc).prod hE)) (T' := cheap k) A fun p => by obtain ⟨hu, hn, h₁, h₂, h₃, h₄⟩ := hfacts p have hs := Nat.size_le.mpr (Nat.lt_two_pow_self (n := p.1.length + 1)) @@ -695,7 +687,7 @@ private theorem exists_computableInO_verifier (k : ℕ) : simp only [horizon] at hsq hsq' h₂ h₃ have := e p omega - have hc₂ := computableInO_mono_time (ComputableInO.unaryLe.comp ((hsz.comp hx).prod hE)) + have hc₂ := ComputableInO.mono_time (ComputableInO.unaryLe.comp ((hsz.comp hx).prod hE)) (T' := cheap k) A fun p => by obtain ⟨hu, hn, h₁, h₂, h₃, h₄⟩ := hfacts p have hs := Nat.size_le.mpr (Nat.lt_two_pow_self (n := p.1.length)) @@ -720,7 +712,7 @@ private theorem exists_computableInO_verifier (k : ℕ) : decide (Nat.size p.1.length ≤ horizon k (2 * (unframe p.1).length + 1))) fun p => by simp only [Function.comp_apply, horizon, length_frame] rfl - have hf₁ := computableInO_mono_time + have hf₁ := ComputableInO.mono_time (hacc.comp (hcode.prod (hsnoc.prod (ComputableInO.snd encBits encBits)))) (T' := fun p => cheap k p + accBound D (unframe (unframe p.1), p.1 ++ [false], p.2)) 7 fun p => by @@ -730,7 +722,7 @@ private theorem exists_computableInO_verifier (k : ℕ) : 7 * cheap k p + 7 * accBound D (unframe (unframe p.1), p.1 ++ [false], p.2) + 7 := by ring omega - have hf₂ := computableInO_mono_time ((ComputableInDegree.of_finite (encIn := encBool) + have hf₂ := ComputableInO.mono_time ((ComputableInDegree.of_finite (encIn := encBool) (encMid := encBool) (fun b : Bool => !b)).inO_one.comp (hbrute.comp (hcode.prod hbase))) (T' := fun p => cheap k p + 2 ^ (K * ((encPair encBits encBits (unframe (unframe p.1), frame (unframe p.1))).length + certLen k (2 * (unframe p.1).length + 1)))) 7 @@ -744,7 +736,7 @@ private theorem exists_computableInO_verifier (k : ℕ) : frame (unframe p.1))).length + certLen k (2 * (unframe p.1).length + 1))) have e : 7 * (cheap k p + B + 1) = 7 * cheap k p + 7 * B + 7 := by ring omega - have hfalse := computableInO_mono_time (ComputableInO.const (encIn := encPair encBits encBits) + have hfalse := ComputableInO.mono_time (ComputableInO.const (encIn := encPair encBits encBits) (encMid := encBool) false) (T' := cheap k) 1 fun p => by obtain ⟨hu, hn, h₁, -⟩ := hfacts p omega From d6b78e14ffd557ebee01991f7be44bddd2124992 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 13:00:00 -0400 Subject: [PATCH 9/9] refactor(Machines/Complexity): share the exponential resource rules of the hierarchy proof - `PolyBounded.exists_le_mul_two_pow` is public in the new `Machines/Turing/MultiTape/ResourceBounds/Exponential.lean`, replacing the private copies in `Classes/Time/BoundedExists` and `Classes/Hierarchy/NondeterministicExponentialTime`. - The unary exponentiation rule is public as `ComputableInPolyTime.exists_computableInO_unary_two_pow` in the new `Machines/Turing/MultiTape/Complexity/BigO/TwoPow.lean`; the hierarchy proof imports it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../NondeterministicExponentialTime.lean | 37 ++---------- .../Classes/Time/BoundedExists.lean | 9 +-- .../MultiTape/Complexity/BigO/TwoPow.lean | 57 +++++++++++++++++++ .../MultiTape/ResourceBounds/Exponential.lean | 39 +++++++++++++ 5 files changed, 103 insertions(+), 41 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/TwoPow.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds/Exponential.lean diff --git a/Complexity.lean b/Complexity.lean index bb83bf7dfb..54211d7303 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1711,6 +1711,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 @@ -2043,6 +2044,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 diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean index a9f86f59af..5444a5c486 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean @@ -15,6 +15,7 @@ import Complexity.Computability.Complexity.Classes.Time.Verifier import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.TwoPow import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential @@ -425,36 +426,6 @@ private theorem exists_computableInO_accepts : ∃ D, ComputableInO simp only [hb] at h ⊢ omega -/-- 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 _)⟩ - -/-- **`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)`. -/ -private theorem 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₁⟩ := PolyBounded.exists_le_mul_two_pow' hT - obtain ⟨C₂, hC₂⟩ := PolyBounded.exists_le_mul_two_pow' hS - 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 - /-- The numeric facts behind the bound of the brute force: the encoded pair of length `N`, the certificate length `c`, the unary certificate length and the search. -/ private theorem brute_bound_aux (C K₀ N c : ℕ) (hc : 1 ≤ c) : @@ -524,7 +495,7 @@ private theorem exists_computableInO_brute (k : ℕ) : ∃ K, ComputableInO have hL : ComputableInPolyTime (fun q : List Bool × List Bool => (k + 1) * (q.2.length + 1)) encQ encUnary := by fun_prop - obtain ⟨C, hcl⟩ := exists_computableInO_unary_two_pow hL + obtain ⟨C, hcl⟩ := hL.exists_computableInO_unary_two_pow have hpair := (ComputableInO.of_eq (f := fun q : List Bool × List Bool => q) (encIn := encQ) (encMid := encQ) fun _ => rfl).prod hcl have h := hsearch.comp hpair @@ -629,7 +600,7 @@ private theorem exists_computableInO_verifier (k : ℕ) : have hL : ComputableInPolyTime (fun z : List Bool => (k + 2) * (z.length + 1)) encBits encUnary := by fun_prop - obtain ⟨CE, hE₀⟩ := exists_computableInO_unary_two_pow hL + obtain ⟨CE, hE₀⟩ := hL.exists_computableInO_unary_two_pow have hE := hE₀.comp hbase -- the numeric facts about the tests have hfacts (p : List Bool × List Bool) : (unframe p.1).length ≤ p.1.length ∧ @@ -764,7 +735,7 @@ theorem expLazyDiagonal_mem_NTIME (k : ℕ) : have hL : ComputableInPolyTime (fun x : List Bool => (k + 1) * (x.length + 2)) encBits encUnary := by fun_prop - obtain ⟨Cℓ, hℓ₀⟩ := exists_computableInO_unary_two_pow hL + obtain ⟨Cℓ, hℓ₀⟩ := hL.exists_computableInO_unary_two_pow have hℓ := hℓ₀.of_enc_eq (encC := encUnary) (g := fun x : List Bool => certLen k (x.length + 1)) fun x => rfl obtain ⟨CD, hCD⟩ := PolynomiallyBounded.exists_le_mul_two_pow (p := fun m => (m + 1) ^ D) diff --git a/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean b/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean index eb926ceb84..0c686e98a0 100644 --- a/Complexity/Computability/Complexity/Classes/Time/BoundedExists.lean +++ b/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 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/TwoPow.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/TwoPow.lean new file mode 100644 index 0000000000..d0254a26fd --- /dev/null +++ b/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 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds/Exponential.lean b/Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds/Exponential.lean new file mode 100644 index 0000000000..0d86255ffc --- /dev/null +++ b/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