feat(complexity): add function and counting time classes

Complexity.lean

@@ -1140,13 +1140,15 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Adm
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Assembly
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.BlockNetworks
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.Count
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAlgorithm
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Guarded
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces
 public import Complexity.Computability.Complexity.Classes.DP
 public import Complexity.Computability.Complexity.Classes.EXP
 public import Complexity.Computability.Complexity.Classes.FewP
 public import Complexity.Computability.Complexity.Classes.FewP.Machine
+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
@@ -1277,6 +1279,7 @@ public import Complexity.Computability.Complexity.Classes.SharpP.Power
 public import Complexity.Computability.Complexity.Classes.SharpP.Probability
 public import Complexity.Computability.Complexity.Classes.SharpP.Products
 public import Complexity.Computability.Complexity.Classes.SharpP.Space
+public import Complexity.Computability.Complexity.Classes.SharpP.Time
 public import Complexity.Computability.Complexity.Classes.SharpP.WeightedReplay
 public import Complexity.Computability.Complexity.Classes.Space
 public import Complexity.Computability.Complexity.Classes.Space.Basic
@@ -1784,6 +1787,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Altern
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Binary
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Certificate
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Checker
+public import Complexity.Computability.Machines.Turing.MultiTape.Counting.ChoiceTable
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Composition
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Deterministic
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Execution

Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean

@@ -35,9 +35,11 @@ network and an accumulator (`Cslib.Complexity.CountingSimulation.exists_computab
 With the clock `t = c * T n` of a time-constructible `T n ≥ max n 2`, the schedules number
 `3 ^ O(T / log T)`, so the total time is `2 ^ O(T / √(log T))` in the natural-number scale of
 `Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`, and the space is polynomial in `T`
-(`Cslib.Complexity.CountingSimulation.exists_computableInO_count`). The result may be any
-polynomial-time function of the padded time, in unary, and the count, such as a comparison
-deciding acceptance.
+(`Cslib.Complexity.CountingSimulation.exists_computableInO_count`). The counting core first
+returns the exact count and its padded clock
+(`Cslib.Complexity.CountingSimulation.exists_computableInO_countPair`). Polynomial-time
+postprocessing, including the comparisons deciding acceptance, is derived from that core by
+`Cslib.Complexity.CountingSimulation.exists_computableInO_countWith`.
 
 ## Main definitions
 
@@ -50,9 +52,11 @@ deciding acceptance.
 * `Cslib.Complexity.CountingSimulation.simulate_eq`: the simulation computes the count.
 * `Cslib.Complexity.CountingSimulation.exists_computableInO_simulate`: its time and space bounds in
   terms of the clock.
-* `Cslib.Complexity.CountingSimulation.exists_computableInO_count`: from a time-constructible bound,
-  the count at the padded clock, or any polynomial-time function of it and the padded time, within
-  time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d`.
+* `Cslib.Complexity.CountingSimulation.exists_computableInO_countPair`: the exact count and
+  padded clock within the claimed joint bounds.
+* `Cslib.Complexity.CountingSimulation.exists_computableInO_count`: the exact count alone.
+* `Cslib.Complexity.CountingSimulation.exists_computableInO_countWith`: polynomial-time
+  postprocessing of the clock and count within the same resource scale.
 -/
 
 public section
@@ -309,24 +313,22 @@ theorem exists_computableInO_simulate (F : NetworkFamily encN value Admissible c
       (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega)))
   exact (htime c).trans (Nat.mul_le_mul (Nat.mul_le_mul_right _ (hVk c)) hEk)
 
-/-- **The count within time `2 ^ O(T / √(log T))` and polynomial space** (conditional on the
-interfaces). Let `T` be time-constructible with `max n 2 ≤ T n`, let `c ≥ 1`, and let `rule` be a
-polynomial-time function of a padded time, in unary, and a count, in binary. Given a network family
-for `count`, with `count x τ ≤ 2 ^ τ`, and a contraction algorithm, the function sending `x` to
-`rule` of the padded clock `τ = paddedTime (c * T |x|)` and of `count x τ` is computable within
-time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d` on inputs of length `n`, for constants `C`
-and `d`. -/
-theorem exists_computableInO_count (F : NetworkFamily encN value Admissible count)
+/-- **Exact counting within time `2 ^ O(T / √(log T))` and polynomial space** (conditional on
+both interfaces). The result contains the padded clock in unary and the exact count in binary.
+No decision rule or postprocessing function is part of this theorem. -/
+theorem exists_computableInO_countPair (F : NetworkFamily encN value Admissible count)
     (A : ContractionAlgorithm encN value Admissible) (hcount : ∀ x τ, count x τ ≤ 2 ^ τ)
-    {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {c : ℕ} (hc : 1 ≤ c)
-    {β : Type} {encβ : β ↪ List Bool} {rule : ℕ × ℕ → β}
-    (hrule : ComputableInPolyTime rule (encPair encUnary encNat) encβ) :
+    {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {c : ℕ} (hc : 1 ≤ c) :
     ∃ C d : ℕ, ComputableInO
       (fun x : List Bool =>
-        rule (paddedTime (c * T x.length), count x (paddedTime (c * T x.length))))
-      encBits encβ
+        (paddedTime (c * T x.length), count x (paddedTime (c * T x.length))))
+      encBits (encPair encUnary encNat)
       (fun x => 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))))
       (fun x => T x.length ^ d) := by
+  let encβ := encPair encUnary encNat
+  let rule : ℕ × ℕ → ℕ × ℕ := id
+  have hrule : ComputableInPolyTime rule (encPair encUnary encNat) encβ :=
+    .of_eq fun _ => rfl
   obtain ⟨k, hsim⟩ := exists_computableInO_simulate F A
   -- Preparing the context `(x, c * T |x|)`, with the clock in unary.
   have hmul : ComputableInPolyTime (fun n : ℕ => c * n) encUnary encUnary := by fun_prop
@@ -429,6 +431,7 @@ theorem exists_computableInO_count (F : NetworkFamily encN value Admissible coun
       ((le_max_right _ _).trans (hTn _)).trans (Nat.le_mul_of_pos_left _ hc)
     simp only [Function.comp_apply]
     rw [simulate_eq F hnt h2t (hcount x _)]
+    rfl
   · set n := x.length
     have h2T : 2 ≤ T n := (le_max_right _ _).trans (hTn n)
     have hcostT := (hcost x).1
@@ -460,4 +463,85 @@ theorem exists_computableInO_count (F : NetworkFamily encN value Admissible coun
       _ = a * c ^ e * (T n + 1) ^ e + 0 := by rw [mul_pow, Nat.mul_assoc, add_zero]
       _ ≤ T n ^ (a * c ^ e + 0 + 2 * e) := Nat.mul_add_one_pow_add_le_pow h2T
 
+/-- Any polynomial-time function of the exact count and its padded clock has the same
+subexponential time and polynomial-space scale. This is postprocessing of
+`exists_computableInO_countPair`, rather than an additional counting algorithm. -/
+theorem exists_computableInO_countWith (F : NetworkFamily encN value Admissible count)
+    (A : ContractionAlgorithm encN value Admissible) (hcount : ∀ x τ, count x τ ≤ 2 ^ τ)
+    {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {c : ℕ} (hc : 1 ≤ c)
+    {β : Type} {encβ : β ↪ List Bool} {rule : ℕ × ℕ → β}
+    (hrule : ComputableInPolyTime rule (encPair encUnary encNat) encβ) :
+    ∃ C d : ℕ, ComputableInO
+      (fun x : List Bool =>
+        rule (paddedTime (c * T x.length), count x (paddedTime (c * T x.length))))
+      encBits encβ
+      (fun x => 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))))
+      (fun x => T x.length ^ d) := by
+  obtain ⟨C, d, h⟩ := exists_computableInO_countPair F A hcount hT hTn hc
+  have hlength := h
+  obtain ⟨K, -, hlen⟩ := hlength
+  let g : List Bool → ℕ × ℕ := fun x =>
+    (paddedTime (c * T x.length), count x (paddedTime (c * T x.length)))
+  let cg : NativeCertificate g encBits (encPair encUnary encNat) := ⟨_, _, h⟩
+  let cr := NativeCertificate.ofPolyTime hrule
+  let ctotal := cr.comp cg
+  obtain ⟨p, hp, mp, bp⟩ := exists_mono_poly_cert hrule
+  let P : ℕ → ℕ := fun n => n ^ d + p (K * (n ^ d + 1))
+  have hP : Cslib.PolynomiallyBounded P := by fun_prop
+  obtain ⟨a, e, hPe⟩ := Cslib.polynomiallyBounded_iff_le.mp hP
+  obtain ⟨C', hC'⟩ := Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two 0 1 e C
+  refine ⟨(a + 2) * (C' + 1), a + 2 * e, ctotal.computes.mono_le (fun x => ?_) fun x => ?_⟩
+  · have h2 : 2 ≤ T x.length := (le_max_right _ _).trans (hTn _)
+    have hpost := (bp (g x)).1.trans (mp (hlen x))
+    have hpoly := hPe (T x.length)
+    have hpost' : cr.time (g x) ≤ a * (T x.length + 1) ^ e :=
+      hpost.trans ((Nat.le_add_left _ _).trans hpoly)
+    have hmain := hC' (T x.length) h2
+    simp only [Nat.zero_mul, pow_zero, Nat.one_mul] at hmain
+    have hpow : 1 ≤ (T x.length + 1) ^ e := Nat.one_le_pow _ _ (by omega)
+    have hE : 1 ≤ 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))) :=
+      Nat.one_le_two_pow
+    have hfirst : 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))) ≤
+        (T x.length + 1) ^ e *
+          2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))) :=
+      Nat.le_mul_of_pos_left _ hpow
+    have hsecond : a * (T x.length + 1) ^ e ≤
+        a * ((T x.length + 1) ^ e *
+          2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length)))) :=
+      Nat.mul_le_mul_left _ (Nat.le_mul_of_pos_right _ hE)
+    calc ctotal.time x = 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))) +
+          cr.time (g x) := rfl
+      _ ≤ (a + 1) * ((T x.length + 1) ^ e *
+          2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length)))) := by
+        have := Nat.add_le_add hfirst (hpost'.trans hsecond)
+        nlinarith only [this]
+      _ ≤ (a + 1) * 2 ^ (C' * T x.length / Nat.sqrt (Nat.log 2 (T x.length))) :=
+        Nat.mul_le_mul_left _ hmain
+      _ ≤ 2 ^ ((a + 2) * (C' + 1) * T x.length /
+          Nat.sqrt (Nat.log 2 (T x.length))) := by
+        have := Nat.mul_two_pow_div_sqrt_log_two_add_le
+          (a := a + 1) (b := 0) (C := C') h2
+        simpa only [Nat.add_zero, Nat.add_assoc] using this
+  · have h2 : 2 ≤ T x.length := (le_max_right _ _).trans (hTn _)
+    have hpost := (bp (g x)).2.trans (mp (hlen x))
+    have hpoly := hPe (T x.length)
+    calc ctotal.space x = T x.length ^ d + cr.space (g x) := rfl
+      _ ≤ a * (T x.length + 1) ^ e :=
+        (Nat.add_le_add_left hpost _).trans hpoly
+      _ ≤ T x.length ^ (a + 2 * e) := by
+        have := Nat.mul_add_one_pow_add_le_pow (a := a) (b := 0) (d := e) h2
+        simpa only [Nat.add_zero] using this
+
+/-- The exact count at the padded clock, with binary output, inherits the counting core's
+subexponential time and polynomial workspace. -/
+theorem exists_computableInO_count (F : NetworkFamily encN value Admissible count)
+    (A : ContractionAlgorithm encN value Admissible) (hcount : ∀ x τ, count x τ ≤ 2 ^ τ)
+    {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {c : ℕ} (hc : 1 ≤ c) :
+    ∃ C d : ℕ, ComputableInO
+      (fun x : List Bool => count x (paddedTime (c * T x.length))) encBits encNat
+      (fun x => 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))))
+      (fun x => T x.length ^ d) :=
+  exists_computableInO_countWith F A hcount hT hTn hc
+    (rule := Prod.snd) (by fun_prop)
+
 end Cslib.Complexity.CountingSimulation

Complexity/Computability/Complexity/Classes/CountingSimulation/BlockNetworks.lean

@@ -65,6 +65,10 @@ heads), and the admissibility constant is `6 (3 k + 1) (s + k + 4)` for `s` stat
   `PPTIME_subset_iUnion_DTIME_of_contractionAlgorithm`: the class containments assuming only a
   contraction algorithm.
 
+* `SharpTIME_subset_iUnion_FTIME_of_contractionAlgorithm`: exact terminal counting with binary
+  output, assuming only a contraction algorithm.
+* `exists_computableInTimeAndSpace_of_mem_SharpTIME_of_contractionAlgorithm`: its joint
+  time and polynomial-workspace bound.
 * `exists_decidableInTimeAndSpace_of_mem_NTIME_of_contractionAlgorithm`,
   `exists_decidableInTimeAndSpace_of_mem_BPTIME_of_contractionAlgorithm`,
   `exists_decidableInTimeAndSpace_of_mem_PPTIME_of_contractionAlgorithm`: the joint time and
@@ -220,6 +224,26 @@ theorem networkFamilies_explicitAdmissible :
 
 variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ}
 
+/-- Exact terminal-path counting with subexponential time and polynomial workspace,
+conditional only on a contraction algorithm for admissible explicit networks. -/
+theorem exists_computableInTimeAndSpace_of_mem_SharpTIME_of_contractionAlgorithm
+    (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction)
+      ExplicitAdmissible) (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n)
+    {f : α → ℕ} (hf : f ∈ SharpTIME enc T) :
+    ∃ C d : ℕ, ComputableInTimeAndSpace f enc encNat
+      (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))))
+      (fun a => T (enc a).length ^ d) :=
+  exists_computableInTimeAndSpace_of_mem_SharpTIME networkFamilies_explicitAdmissible A hT hTn hf
+
+/-- The functional counting containment, assuming only the explicit-network contraction
+algorithm. Output is the exact natural count in binary. -/
+theorem SharpTIME_subset_iUnion_FTIME_of_contractionAlgorithm
+    (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction)
+      ExplicitAdmissible) (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
+    SharpTIME enc T ⊆ ⋃ C : ℕ,
+      FTIME enc encNat (fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))) :=
+  SharpTIME_subset_iUnion_FTIME networkFamilies_explicitAdmissible A hT hTn
+
 /-- **Nondeterministic time with polynomial workspace**, conditional only on a
 contraction algorithm for admissible explicit networks. For time-constructible `T` with
 `max n 2 ≤ T n`, one deterministic machine decides each problem in `NTIME[T]` within time

Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean

@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Computability.Complexity.Classes.CountingSimulation.Assembly
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.Count
 public import Complexity.Computability.Complexity.Classes.Time.AcceptCount
 public import Complexity.Computability.Complexity.Classes.PP.Time
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
@@ -27,7 +27,7 @@ Each class is reduced to the accept count `A_M(x)` of a fair-coin machine `M` at
 `BPTIME` and `PPTIME` (`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`,
 `Cslib.Complexity.exists_acceptCount_of_mem_BPTIME`,
 `Turing.MultiTapePTM.decidesByMajorityInTime_iff`). The count is computed by the simulation of
-`Cslib.Complexity.CountingSimulation.exists_computableInO_count`, and the comparison is a
+`Cslib.Complexity.CountingSimulation.exists_computableInO_countPair`, and the comparison is a
 polynomial-time function of the padded time and the count.
 
 The network hypothesis is discharged for explicit networks by
@@ -36,10 +36,6 @@ assuming only a contraction algorithm
 (`Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME_of_contractionAlgorithm` and its
 siblings).
 
-## Main definitions
-
-* `Cslib.Complexity.CountingSimulation.NetworkFamilies`: network families for all machines.
-
 ## Main results
 
 * `Cslib.Complexity.CountingSimulation.exists_decidableInTimeAndSpace_of_mem_NTIME`,
@@ -53,21 +49,11 @@ public section
 
 namespace Cslib.Complexity.CountingSimulation
 
-open Turing Turing.MultiTapeTM
+open _root_.Turing _root_.Turing.MultiTapeTM
 
 variable {N : Type} {encN : N ↪ List Bool} {value : N → ℕ} {Admissible : ℕ → ℕ → N → Prop}
   {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ}
 
-/-- **Network families for all machines**: for every finite-state fair-coin machine, a network
-family (`Cslib.Complexity.CountingSimulation.NetworkFamily`) for its accept count
-`Turing.MultiTapePTM.acceptCount`. This is the hypothesis supplied by the block-counting step of
-#1833. -/
-@[expose] def NetworkFamilies (encN : N ↪ List Bool) (value : N → ℕ)
-    (Admissible : ℕ → ℕ → N → Prop) :
-    Prop :=
-  ∀ (k : ℕ) (State : Type) [Finite State] (M : MultiTapePTM k Bool State),
-    Nonempty (NetworkFamily encN value Admissible fun x τ => M.acceptCount x τ)
-
 /-- A problem decided by a polynomial-time comparison of the padded time with the accept count of
 a finite-state fair-coin machine, at every padded time past a linear clock, is decided within time
 `2 ^ O(T / √(log T))` and space polynomial in `T`. -/
@@ -82,32 +68,15 @@ private theorem exists_decidableInTimeAndSpace_of_rule
     ∃ C d : ℕ, DecidableInTimeAndSpace L enc
       (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length))))
       (fun a => T (enc a).length ^ d) := by
-  obtain ⟨F⟩ := hnet k State M
-  obtain ⟨C, d, h⟩ := exists_computableInO_count F A
-    (fun x τ => Complexity.acceptCount_le_two_pow) hT hTn (c := c₁ + c₂ + 1) (by omega) hrule
-  obtain ⟨K, hK, -⟩ := h.of_encIn_eq enc fun a => rfl
-  refine ⟨(K + K + 1) * (C + 1), K + K + 2 * d,
-    decidableInTimeAndSpace_iff.mpr ⟨_, hK.mono (fun a => ?_) fun a => ?_, fun a => ?_⟩⟩
-  · have h2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _)
-    have := Nat.mul_two_pow_div_sqrt_log_two_add_le (a := K) (b := K) (C := C) h2
-    simp only [Function.comp_apply, Nat.mul_add, Nat.mul_one] at this ⊢
-    exact this
-  · have h2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _)
-    have hpow : T (enc a).length ^ d ≤ (T (enc a).length + 1) ^ d :=
-      Nat.pow_le_pow_left (Nat.le_succ _) d
-    have := Nat.mul_add_one_pow_add_le_pow (a := K) (b := K) (d := d) h2
-    simp only [Function.comp_apply]
-    calc K * (T (enc a).length ^ d + 1) ≤ K * (T (enc a).length + 1) ^ d + K := by
-          rw [Nat.mul_add, Nat.mul_one]
-          exact Nat.add_le_add_right (Nat.mul_le_mul_left _ hpow) _
-      _ ≤ _ := this
-  · have h2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _)
-    have hτ : c₁ * T (enc a).length + c₂ ≤
-        paddedTime ((c₁ + c₂ + 1) * T (enc a).length) := by
-      refine le_trans ?_ (le_paddedTime _)
-      nlinarith
-    simp only [Function.comp_apply]
-    exact hL a _ hτ
+  obtain ⟨C, d, h⟩ := exists_computableInTimeAndSpace_countWith hnet A hT hTn M
+    (c := c₁ + c₂ + 1) (by omega) hrule
+  refine ⟨C, d, decidableInTimeAndSpace_iff.mpr ⟨_, h, fun a => ?_⟩⟩
+  have h2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _)
+  have hτ : c₁ * T (enc a).length + c₂ ≤
+      paddedTime ((c₁ + c₂ + 1) * T (enc a).length) := by
+    refine le_trans ?_ (le_paddedTime _)
+    nlinarith
+  exact hL a _ hτ
 
 /-- **Nondeterministic time, deterministically** (conditional on the interfaces). For a
 time-constructible `T` with `max n 2 ≤ T n`, every problem in `NTIME[T]` is decided within time