From 6685d72f7c540f1b12457590861f064960f90029 Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 17:59:04 +0000 Subject: [PATCH 1/6] refactor(Complexity/FineGrained): move the function-rate tower to FunctionRates Move ComputableInTimeO/ExpTime/SubexpTime and their FTIME, decision and reduction-transfer lemmas verbatim from CountingExponents into a new FineGrained/FunctionRates module. CountingExponents re-exports it, and Randomized imports FunctionRates and Exponents instead of the #k-SAT module. Part of #4737 --- CslibFrontier.lean | 1 + .../FineGrained/CountingExponents.lean | 322 +--------------- .../Complexity/FineGrained/FunctionRates.lean | 352 ++++++++++++++++++ .../Complexity/FineGrained/Randomized.lean | 5 +- .../machines-and-classes/native-counting.md | 5 +- 5 files changed, 365 insertions(+), 320 deletions(-) create mode 100644 CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean diff --git a/CslibFrontier.lean b/CslibFrontier.lean index 532bdc3f6b..9e6e7c35db 100644 --- a/CslibFrontier.lean +++ b/CslibFrontier.lean @@ -2238,6 +2238,7 @@ public import CslibFrontier.Computability.Complexity.FineGrained.DensityBranchCo public import CslibFrontier.Computability.Complexity.FineGrained.Diameter public import CslibFrontier.Computability.Complexity.FineGrained.ExhaustiveSearch public import CslibFrontier.Computability.Complexity.FineGrained.Exponents +public import CslibFrontier.Computability.Complexity.FineGrained.FunctionRates public import CslibFrontier.Computability.Complexity.FineGrained.GapETH public import CslibFrontier.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule public import CslibFrontier.Computability.Complexity.FineGrained.GraphProblems diff --git a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean index 353000180c..b81a4e13bc 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean @@ -7,11 +7,10 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import CslibFrontier.Computability.Complexity.Classes.FunctionTime public import CslibFrontier.Computability.Complexity.FineGrained.Exponents +public import CslibFrontier.Computability.Complexity.FineGrained.FunctionRates public import CslibFrontier.Computability.Complexity.FineGrained.Reduction public import CslibFrontier.Computability.Complexity.Problems.SharpThreeSAT -import CslibFrontier.Computability.Complexity.FineGrained.Bounds import CslibFrontier.Computability.Complexity.FineGrained.CountingTreeBound import CslibFrontier.Computability.Complexity.FineGrained.Sparsification import CslibFrontier.Computability.Complexity.Problems.SAT.PolyTime @@ -31,13 +30,11 @@ import CslibFrontier.Foundations.Data.Nat.Power import Mathlib.Topology.Instances.Real.Lemmas /-! -# Counting runtime rates, `#k-SAT` exponents, `#ETH`, and `#SETH` +# `#k-SAT` exponents, `#ETH`, and `#SETH` -`Cslib.Complexity.DecidableInTimeO`, `DecidableInExpTime`, and `DecidableInSubexpTime` measure the -running time of decision problems in a structural parameter `μ : α → ℕ` of the instance rather than -in the bit length `L = (encIn a).length` alone. This module introduces the parallel function-time -notions `Cslib.Complexity.ComputableInTimeO`, `ComputableInExpTime`, and `ComputableInSubexpTime`, -bridges them to `Cslib.Complexity.FTIME`, and develops the exact-counting rate theory for `#k-SAT`: +This module develops the exact-counting rate theory for `#k-SAT`, measuring counters with the +function-time notions `Cslib.Complexity.ComputableInExpTime` and `ComputableInSubexpTime` of +`CslibFrontier.Computability.Complexity.FineGrained.FunctionRates`: * `Cslib.Complexity.SharpKSAT k` counts the satisfying assignments of width-`≤ k` formulas and returns `0` outside that syntax (`SharpKSAT 3 = SharpThreeSAT`). @@ -60,8 +57,6 @@ unconditionally via `toThreeSAT` clause-splitting and `3`-SAT sparsification, an ## Main definitions -* `Cslib.Complexity.ComputableInTimeO`, `Cslib.Complexity.ComputableInExpTime`, - `Cslib.Complexity.ComputableInSubexpTime`: parameterized time bounds for functions. * `Cslib.Complexity.SharpKSAT`, `Cslib.Complexity.sharpSatExponent`, `Cslib.Complexity.unrestrictedSatExponent`: `#k-SAT`, its exponent, and the unrestricted `SAT` exponent. @@ -70,12 +65,7 @@ unconditionally via `toThreeSAT` clause-splitting and `3`-SAT sparsification, an ## Main results -* `Cslib.Complexity.mem_FTIME_iff_computableInTimeO`: agreement with `FTIME` on length bounds. -* `Cslib.Complexity.DecidableInExpTime.of_computableInExpTime_polyBounded`, - `Cslib.Complexity.DecidableInExpTime.KSAT_of_SharpKSAT`: exact-rate decision from counting. -* `Cslib.Complexity.ComputableInExpTime.of_reduction`, - `Cslib.Complexity.ComputableInSubexpTime.of_reduction`: transfer along linear-parameter - parsimonious reductions. +* `Cslib.Complexity.DecidableInExpTime.KSAT_of_SharpKSAT`: exact-rate decision from counting. * `Cslib.Complexity.SharpSAT_computableInExpTime_one`, `Cslib.Complexity.SharpKSAT_computableInExpTime_one`: exhaustive counting in time `2 ^ n · poly`. * `Cslib.Complexity.sharpSatExponent_nonneg`, `Cslib.Complexity.sharpSatExponent_le_one`, @@ -105,306 +95,6 @@ namespace Cslib.Complexity open Cslib.Logic.PL Turing Turing.MultiTapeTM Filter Topology -/-! ### Parameterized function time bounds -/ - -section FunctionBounds - -variable {α β : Type*} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} - {f : α → β} {T T' : α → ℝ} - -/-- `f` is computable within time `O(T a)` on the instance `a`: within time `c * T a + c`, for a -constant `c`, by a native multi-tape machine reading `encIn a` and writing `encOut (f a)` with some -workspace bound. -/ -@[expose] def ComputableInTimeO (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) - (T : α → ℝ) : Prop := - ∃ c : ℕ, ∃ t s : α → ℕ, (∀ a, (t a : ℝ) ≤ c * T a + c) ∧ - ComputableInTimeAndSpace f encIn encOut t s - -/-- Weakening the bound of `ComputableInTimeO` up to constants. -/ -theorem ComputableInTimeO.mono (h : ComputableInTimeO f encIn encOut T) (c : ℕ) - (hT : ∀ a, T a ≤ c * T' a + c) (hT' : ∀ a, 0 ≤ T' a) : - ComputableInTimeO f encIn encOut T' := by - obtain ⟨c₀, t, s, ht, hf⟩ := h - refine ⟨c₀ * c + c₀, t, s, fun a => (ht a).trans ?_, hf⟩ - have h₁ := mul_le_mul_of_nonneg_left (hT a) (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) - have h₂ := mul_nonneg (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) (hT' a) - push_cast - nlinarith - -/-- `f` is computable within time `2 ^ (δ * μ a)` times a polynomial in the encoded input length: -within time `O(2 ^ (δ * μ a) * (L + 1) ^ e)` for some `e`. -/ -@[expose] def ComputableInExpTime (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) - (μ : α → ℕ) (δ : ℝ) : Prop := - ∃ e : ℕ, ComputableInTimeO f encIn encOut fun a => 2 ^ (δ * μ a) * ((encIn a).length + 1) ^ e - -/-- `f` is computable in subexponential time in `μ`: within time `2 ^ (δ * μ a)` times a polynomial -in the encoded input length for every `δ > 0` (the machine and polynomial degree may depend on -`δ`). -/ -@[expose] def ComputableInSubexpTime (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) - (μ : α → ℕ) : Prop := - ∀ δ : ℝ, 0 < δ → ComputableInExpTime f encIn encOut μ δ - -/-- Larger exponents allow more functions. -/ -theorem ComputableInExpTime.mono {μ : α → ℕ} {δ δ' : ℝ} - (h : ComputableInExpTime f encIn encOut μ δ) (hδ : δ ≤ δ') : - ComputableInExpTime f encIn encOut μ δ' := by - obtain ⟨e, h⟩ := h - refine ⟨e, h.mono 1 (fun a => ?_) fun a => by positivity⟩ - have h₁ : (2 : ℝ) ^ (δ * μ a) ≤ 2 ^ (δ' * μ a) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) - (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) - have h₂ := mul_le_mul_of_nonneg_right h₁ (by positivity : (0 : ℝ) ≤ ((encIn a).length + 1) ^ e) - push_cast - linarith - -/-- Rescaling the parameter linearly rescales the exponential rate. -/ -theorem ComputableInExpTime.mono_measure {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) - {δ : ℝ} (hδ : 0 ≤ δ) (h : ComputableInExpTime f encIn encOut μ δ) : - ComputableInExpTime f encIn encOut μ' (c * δ) := by - obtain ⟨e, h⟩ := h - refine ⟨e, h.mono ⌈(2 : ℝ) ^ (δ * c)⌉₊ (fun a => ?_) fun a => by positivity⟩ - have h₂ := two_rpow_le_natCeil_mul_of_le_mul_add hδ (hμ a) - have h₃ := mul_le_mul_of_nonneg_right h₂ - (by positivity : (0 : ℝ) ≤ ((encIn a).length + 1) ^ e) - have h₄ : (0 : ℝ) ≤ ⌈(2 : ℝ) ^ (δ * c)⌉₊ := Nat.cast_nonneg _ - nlinarith - -/-- Subexponential computability transfers to any parameter at least linear in `μ`. -/ -theorem ComputableInSubexpTime.mono_measure {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) - (h : ComputableInSubexpTime f encIn encOut μ) : - ComputableInSubexpTime f encIn encOut μ' := by - intro δ hδ - refine ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith - -end FunctionBounds - -section FunctionMachines - -variable {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} - {encOut : γ ↪ List Bool} {f : α → β} {T : α → ℝ} - -/-- **`FTIME` in terms of `ComputableInTimeO`.** For a bound depending only on the encoded input -length, `ComputableInTimeO` agrees with membership in `FTIME`. -/ -theorem mem_FTIME_iff_computableInTimeO {t : ℕ → ℕ} : - f ∈ FTIME encIn encMid t ↔ ComputableInTimeO f encIn encMid fun a => t (encIn a).length := by - constructor - · rintro ⟨c₁, c₂, s, hf⟩ - refine ⟨c₁ + c₂, _, _, fun a => ?_, hf⟩ - push_cast - nlinarith [(Nat.cast_nonneg (t (encIn a).length) : (0 : ℝ) ≤ _), - (Nat.cast_nonneg c₂ : (0 : ℝ) ≤ _), (Nat.cast_nonneg c₁ : (0 : ℝ) ≤ _)] - · rintro ⟨c, t', s, ht', hf⟩ - have ht : ∀ a, t' a ≤ c * t (encIn a).length + c := fun a => by - have := ht' a - simp only at this - exact_mod_cast this - obtain ⟨k, hf'⟩ := ComputableInTimeAndSpace.exists_space_linear hf - exact ⟨c, c, fun n => k * (c * t n + c) + k, - ComputableInTimeAndSpace.mono hf' ht fun a => by - have := Nat.mul_le_mul_left k (ht a) - simp only - omega⟩ - -/-- A function computable within time `O(T)` has a `ComputableInO` certificate within time and -charged workspace `O(t)`, for a natural clock `t` within `O(T)`. -/ -theorem ComputableInTimeO.exists_computableInO (h : ComputableInTimeO f encIn encMid T) : - ∃ (t : α → ℕ) (c : ℕ), ComputableInO f encIn encMid t t ∧ - ∀ a, (t a : ℝ) ≤ c * T a + c := by - obtain ⟨c, t, s, ht, hf⟩ := h - have hl : ∀ a, (encMid (f a)).length ≤ t a := hf.length_le - obtain ⟨k, hf'⟩ := ComputableInTimeAndSpace.exists_space_linear hf - refine ⟨t, c, ComputableInO.of_bounds hf' (k + 1) - (fun a => by nlinarith) (fun a => by nlinarith) (fun a => by nlinarith [hl a]), ht⟩ - -/-- A `ComputableInO` certificate within time `t ≤ T` gives `ComputableInTimeO` within `T`. -/ -theorem ComputableInTimeO.of_computableInO {t S : α → ℕ} - (hf : ComputableInO f encIn encMid t S) (hT : ∀ a, (t a : ℝ) ≤ T a) : - ComputableInTimeO f encIn encMid T := by - obtain ⟨c, hf', -⟩ := hf - refine ⟨c, _, _, fun a => ?_, hf'⟩ - push_cast - nlinarith [hT a, (Nat.cast_nonneg c : (0 : ℝ) ≤ c)] - -/-- `DecidableInTimeO` is `ComputableInTimeO` of a Boolean indicator function. -/ -theorem decidableInTimeO_iff_exists_computableInTimeO {A : Set α} : - DecidableInTimeO A encIn T ↔ - ∃ g : α → Bool, (∀ a, a ∈ A ↔ g a = true) ∧ ComputableInTimeO g encIn encBool T := by - constructor - · rintro ⟨c, t, s, ht, h⟩ - obtain ⟨g, hg, hA⟩ := decidableInTimeAndSpace_iff.mp h - exact ⟨g, hA, c, t, s, ht, hg⟩ - · rintro ⟨g, hA, c, t, s, ht, hg⟩ - exact ⟨c, t, s, ht, decidableInTimeAndSpace_iff.mpr ⟨g, hg, hA⟩⟩ - -/-- A `ComputableInO` certificate within `c * (2 ^ (δ * μ a) * (L + 1) ^ e)` gives -`ComputableInExpTime`. -/ -theorem ComputableInExpTime.of_computableInO {μ : α → ℕ} {δ : ℝ} {t S : α → ℕ} - (hf : ComputableInO f encIn encMid t S) (c e : ℕ) - (ht : ∀ a, (t a : ℝ) ≤ c * (2 ^ (δ * μ a) * ((encIn a).length + 1) ^ e)) : - ComputableInExpTime f encIn encMid μ δ := - ⟨e, (ComputableInTimeO.of_computableInO hf ht).mono c - (fun _ => le_add_of_nonneg_right (Nat.cast_nonneg c)) fun _ => by positivity⟩ - -/-- Every polynomial-time computable function has exponential rate `0` in any parameter `μ`. -/ -theorem ComputableInExpTime.of_computableInPolyTime {μ : α → ℕ} - (hf : ComputableInPolyTime f encIn encMid) : - ComputableInExpTime f encIn encMid μ 0 := by - obtain ⟨d, _, hf'⟩ := hf.exists_degree - refine ComputableInExpTime.of_computableInO hf'.inO 1 d fun a => ?_ - simp - -/-- Guarding an exponential-time function by a polynomial-time test and fallback preserves rate -`δ ≥ 0`. -/ -theorem ComputableInExpTime.ite_polyTime {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) {p : α → Bool} - {g : α → β} (hp : ComputableInPolyTime p encIn encBool) - (hf : ComputableInExpTime f encIn encMid μ δ) - (hg : ComputableInPolyTime g encIn encMid) : - ComputableInExpTime (fun a => if p a then f a else g a) encIn encMid μ δ := by - obtain ⟨e, hf⟩ := hf - obtain ⟨t, c, hfO, ht⟩ := hf.exists_computableInO - obtain ⟨dp, _, hp'⟩ := hp.exists_degree - obtain ⟨dg, _, hg'⟩ := hg.exists_degree - have hcomb := hp'.inO.ite hfO hg'.inO - refine ComputableInExpTime.of_computableInO hcomb (2 * c + 3) (dp + dg + e) fun a => ?_ - set L : ℝ := ((encIn a).length : ℝ) - have hL1 : (1 : ℝ) ≤ L + 1 := by - dsimp only [L] - linarith [(Nat.cast_nonneg (encIn a).length : (0 : ℝ) ≤ _)] - have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have hdp : (L + 1) ^ dp ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) - have hdg : (L + 1) ^ dg ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) - have he : (L + 1) ^ e ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) - have hbase : (L + 1) ^ (dp + dg + e) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := - le_mul_of_one_le_left (by positivity) hX1 - have hc0 : (0 : ℝ) ≤ c := Nat.cast_nonneg c - have hpos : (0 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := by positivity - have ht_le : (t a : ℝ) ≤ (2 * c + 1) * (2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e)) := by - have hta := ht a - have hmul := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - have hmulc := mul_le_mul_of_nonneg_left hmul hc0 - have hc1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := - one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hL1) - have hcc := mul_le_mul_of_nonneg_left hc1 hc0 - dsimp only [L] at * - nlinarith - change ((((encIn a).length + 1) ^ dp + - if p a then t a else ((encIn a).length + 1) ^ dg : ℕ) : ℝ) ≤ _ - split_ifs - · push_cast - dsimp only [L] at * - nlinarith [hdp.trans hbase] - · push_cast - dsimp only [L] at * - nlinarith [hdp.trans hbase, hdg.trans hbase] - -/-- **Exact-rate decision from function computation.** If `f` is computable in time -`2 ^ (δ * μ a) · poly(|a|)` (`δ ≥ 0`) and its encoded output length is polynomially bounded in -`|a|`, then any polynomial-time test on `f a` decides `{a | test (f a) = true}` at the same -exponential rate `δ`. -/ -theorem DecidableInExpTime.of_computableInExpTime_polyBounded {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) - (hf : ComputableInExpTime f encIn encMid μ δ) - (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (encMid (f a)).length)) - {test : β → Bool} (htest : ComputableInPolyTime test encMid encBool) : - DecidableInExpTime {a | test (f a) = true} encIn μ δ := by - obtain ⟨e, hf⟩ := hf - obtain ⟨t, c, hfO, ht⟩ := hf.exists_computableInO - obtain ⟨d, _, htest'⟩ := htest.exists_degree - obtain ⟨p, q, hp⟩ := hlen.exists_le - have hcomp := htest'.inO.comp hfO - refine DecidableInExpTime.of_computableInO hcomp (fun _ => Iff.rfl) - (2 * c + 1 + (p + 1) ^ d) (e + q * d) fun a => ?_ - set L : ℕ := (encIn a).length - have hL1 : 1 ≤ L + 1 := Nat.le_add_left 1 L - have hLR1 : (1 : ℝ) ≤ (L : ℝ) + 1 := by exact_mod_cast hL1 - have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have hout_pow : ((encMid (f a)).length + 1) ^ d ≤ (p + 1) ^ d * (L + 1) ^ (q * d) := - Nat.add_one_pow_le_of_le_mul_pow hL1 (hp a) d - have hqd : (((L : ℝ) + 1)) ^ (q * d) ≤ ((L : ℝ) + 1) ^ (e + q * d) := - pow_le_pow_right₀ hLR1 (Nat.le_add_left _ _) - have he : (((L : ℝ) + 1)) ^ e ≤ ((L : ℝ) + 1) ^ (e + q * d) := - pow_le_pow_right₀ hLR1 (Nat.le_add_right _ _) - have houtR : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ - ((p + 1) ^ d : ℕ) * (2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by - have h1 : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ - ((p + 1) ^ d : ℕ) * ((L : ℝ) + 1) ^ (q * d) := by exact_mod_cast hout_pow - have h2 : ((L : ℝ) + 1) ^ (q * d) ≤ 2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d) := - hqd.trans (le_mul_of_one_le_left (by positivity) hX1) - exact h1.trans (mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg _)) - have htR : (t a : ℝ) ≤ (2 * c + 1 : ℕ) * (2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by - have hta := ht a - have h1 := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - have h2 := mul_le_mul_of_nonneg_left h1 (Nat.cast_nonneg c) - have h3 : (1 : ℝ) ≤ 2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d) := - one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hLR1) - have h4 := mul_le_mul_of_nonneg_left h3 (Nat.cast_nonneg c) - push_cast - dsimp only [L] at * - linarith - change ((t a + ((encMid (f a)).length + 1) ^ d : ℕ) : ℝ) ≤ _ - push_cast - dsimp only [L] at * - push_cast at htR houtR - linarith - -/-- Subexponential function computation with polynomially bounded output length transfers to -subexponential decision for any polynomial-time output predicate. -/ -theorem DecidableInSubexpTime.of_computableInSubexpTime_polyBounded {μ : α → ℕ} - (hf : ComputableInSubexpTime f encIn encMid μ) - (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (encMid (f a)).length)) - {test : β → Bool} (htest : ComputableInPolyTime test encMid encBool) : - DecidableInSubexpTime {a | test (f a) = true} encIn μ := - fun δ hδ => .of_computableInExpTime_polyBounded hδ.le (hf δ hδ) hlen htest - -/-- **Transfer along linear-parameter parsimonious reductions.** If `r : α → β` is computable in -polynomial time with `μB (r a) ≤ c * μA a + c`, and `g : β → γ` is computable in time -`2 ^ (δ * μB b) · poly(|b|)` (`δ ≥ 0`), then `g ∘ r` is computable in time -`2 ^ (c * δ * μA a) · poly(|a|)`. -/ -theorem ComputableInExpTime.of_reduction {μA : α → ℕ} {μB : β → ℕ} {r : α → β} {g : β → γ} - (hr : ComputableInPolyTime r encIn encMid) {c : ℕ} - (hμ : ∀ a, μB (r a) ≤ c * μA a + c) {δ : ℝ} (hδ : 0 ≤ δ) - (hg : ComputableInExpTime g encMid encOut μB δ) : - ComputableInExpTime (g ∘ r) encIn encOut μA (c * δ) := by - obtain ⟨e, hg⟩ := hg - obtain ⟨t, k, hgO, ht⟩ := hg.exists_computableInO - obtain ⟨d, _, hr'⟩ := hr.exists_degree - obtain ⟨l, hl⟩ := hr'.inO.length_le_time - refine ComputableInExpTime.of_computableInO (hgO.comp hr'.inO) - ⌈(1 + k * 2 ^ (δ * c) * (2 * l + 1) ^ e + k : ℝ)⌉₊ (d * (e + 1)) fun a => ?_ - set P : ℝ := ((encIn a).length + 1 : ℝ) ^ d - set X : ℝ := 2 ^ (c * δ * μA a) - have hP : 1 ≤ P := one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _)) - have hX : 1 ≤ X := Real.one_le_rpow (by norm_num) (by positivity) - have hn : ((encMid (r a)).length : ℝ) ≤ l * (P + 1) := by - dsimp only [P] - exact_mod_cast hl a - have hexp : (2 : ℝ) ^ (δ * μB (r a)) ≤ 2 ^ (δ * c) * X := by - rw [← Real.rpow_add (by norm_num)] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - have : (μB (r a) : ℝ) ≤ c * μA a + c := by exact_mod_cast hμ a - nlinarith - have hsum := reduction_add_time_le (C := (2 : ℝ) ^ (δ * c)) - hP hX (by positivity) hn hexp (ht (r a)) - change ((((encIn a).length + 1) ^ d + t (r a) : ℕ) : ℝ) ≤ _ - push_cast - rw [pow_mul] - exact hsum.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil _) (by positivity)) - -/-- Subexponential function computation transfers along linear-parameter polynomial-time -reductions. -/ -theorem ComputableInSubexpTime.of_reduction {μA : α → ℕ} {μB : β → ℕ} {r : α → β} {g : β → γ} - (hr : ComputableInPolyTime r encIn encMid) {c : ℕ} - (hμ : ∀ a, μB (r a) ≤ c * μA a + c) - (hg : ComputableInSubexpTime g encMid encOut μB) : - ComputableInSubexpTime (g ∘ r) encIn encOut μA := by - intro δ hδ - refine ((hg (δ / (c + 1)) (by positivity)).of_reduction hr hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith - -end FunctionMachines - /-! ### `#k-SAT` and exhaustive model counting -/ /-- `#k-SAT`: the number of satisfying assignments of `φ` on its occurring variables when every diff --git a/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean new file mode 100644 index 0000000000..6084ba4ed4 --- /dev/null +++ b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean @@ -0,0 +1,352 @@ +/- +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 CslibFrontier.Computability.Complexity.Classes.FunctionTime +public import CslibFrontier.Computability.Complexity.FineGrained +import CslibFrontier.Computability.Complexity.FineGrained.Bounds +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds +import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts +import CslibFrontier.Foundations.Data.Nat.Power + +/-! +# Parameterized time bounds for functions + +`Cslib.Complexity.DecidableInTimeO`, `DecidableInExpTime` and `DecidableInSubexpTime` measure the +running time of decision problems in a structural parameter `μ : α → ℕ` of the instance rather than +in the bit length `L = (encIn a).length` alone. This module develops the same three notions for +functions: `f` is computable within time `O(T a)`, within time `2 ^ (δ * μ a)` times a polynomial in +`L`, and within that time for every `δ > 0`. It bridges them to `Cslib.Complexity.FTIME` and to +decision, and transfers them along polynomial-time reductions that change the parameter linearly. + +## Main definitions + +* `Cslib.Complexity.ComputableInTimeO`, `Cslib.Complexity.ComputableInExpTime`, + `Cslib.Complexity.ComputableInSubexpTime`: parameterized time bounds for functions. + +## Main results + +* `Cslib.Complexity.mem_FTIME_iff_computableInTimeO`: agreement with `FTIME` on length bounds. +* `Cslib.Complexity.decidableInTimeO_iff_exists_computableInTimeO`: decision as computation of a + Boolean indicator. +* `Cslib.Complexity.DecidableInExpTime.of_computableInExpTime_polyBounded`: a polynomial-time test + on a function value with polynomially bounded output length is decided at the function's rate. +* `Cslib.Complexity.ComputableInExpTime.of_reduction`, + `Cslib.Complexity.ComputableInSubexpTime.of_reduction`: transfer along linear-parameter + polynomial-time reductions. +-/ + +public section + +namespace Cslib.Complexity + +open Turing Turing.MultiTapeTM + +/-! ### Parameterized function time bounds -/ + +section FunctionBounds + +variable {α β : Type*} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} + {f : α → β} {T T' : α → ℝ} + +/-- `f` is computable within time `O(T a)` on the instance `a`: within time `c * T a + c`, for a +constant `c`, by a native multi-tape machine reading `encIn a` and writing `encOut (f a)` with some +workspace bound. -/ +@[expose] def ComputableInTimeO (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) + (T : α → ℝ) : Prop := + ∃ c : ℕ, ∃ t s : α → ℕ, (∀ a, (t a : ℝ) ≤ c * T a + c) ∧ + ComputableInTimeAndSpace f encIn encOut t s + +/-- Weakening the bound of `ComputableInTimeO` up to constants. -/ +theorem ComputableInTimeO.mono (h : ComputableInTimeO f encIn encOut T) (c : ℕ) + (hT : ∀ a, T a ≤ c * T' a + c) (hT' : ∀ a, 0 ≤ T' a) : + ComputableInTimeO f encIn encOut T' := by + obtain ⟨c₀, t, s, ht, hf⟩ := h + refine ⟨c₀ * c + c₀, t, s, fun a => (ht a).trans ?_, hf⟩ + have h₁ := mul_le_mul_of_nonneg_left (hT a) (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) + have h₂ := mul_nonneg (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) (hT' a) + push_cast + nlinarith + +/-- `f` is computable within time `2 ^ (δ * μ a)` times a polynomial in the encoded input length: +within time `O(2 ^ (δ * μ a) * (L + 1) ^ e)` for some `e`. -/ +@[expose] def ComputableInExpTime (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) + (μ : α → ℕ) (δ : ℝ) : Prop := + ∃ e : ℕ, ComputableInTimeO f encIn encOut fun a => 2 ^ (δ * μ a) * ((encIn a).length + 1) ^ e + +/-- `f` is computable in subexponential time in `μ`: within time `2 ^ (δ * μ a)` times a polynomial +in the encoded input length for every `δ > 0` (the machine and polynomial degree may depend on +`δ`). -/ +@[expose] def ComputableInSubexpTime (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) + (μ : α → ℕ) : Prop := + ∀ δ : ℝ, 0 < δ → ComputableInExpTime f encIn encOut μ δ + +/-- Larger exponents allow more functions. -/ +theorem ComputableInExpTime.mono {μ : α → ℕ} {δ δ' : ℝ} + (h : ComputableInExpTime f encIn encOut μ δ) (hδ : δ ≤ δ') : + ComputableInExpTime f encIn encOut μ δ' := by + obtain ⟨e, h⟩ := h + refine ⟨e, h.mono 1 (fun a => ?_) fun a => by positivity⟩ + have h₁ : (2 : ℝ) ^ (δ * μ a) ≤ 2 ^ (δ' * μ a) := + Real.rpow_le_rpow_of_exponent_le (by norm_num) + (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) + have h₂ := mul_le_mul_of_nonneg_right h₁ (by positivity : (0 : ℝ) ≤ ((encIn a).length + 1) ^ e) + push_cast + linarith + +/-- Rescaling the parameter linearly rescales the exponential rate. -/ +theorem ComputableInExpTime.mono_measure {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) + {δ : ℝ} (hδ : 0 ≤ δ) (h : ComputableInExpTime f encIn encOut μ δ) : + ComputableInExpTime f encIn encOut μ' (c * δ) := by + obtain ⟨e, h⟩ := h + refine ⟨e, h.mono ⌈(2 : ℝ) ^ (δ * c)⌉₊ (fun a => ?_) fun a => by positivity⟩ + have h₂ := two_rpow_le_natCeil_mul_of_le_mul_add hδ (hμ a) + have h₃ := mul_le_mul_of_nonneg_right h₂ + (by positivity : (0 : ℝ) ≤ ((encIn a).length + 1) ^ e) + have h₄ : (0 : ℝ) ≤ ⌈(2 : ℝ) ^ (δ * c)⌉₊ := Nat.cast_nonneg _ + nlinarith + +/-- Subexponential computability transfers to any parameter at least linear in `μ`. -/ +theorem ComputableInSubexpTime.mono_measure {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) + (h : ComputableInSubexpTime f encIn encOut μ) : + ComputableInSubexpTime f encIn encOut μ' := by + intro δ hδ + refine ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono ?_ + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + +end FunctionBounds + +section FunctionMachines + +variable {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} + {encOut : γ ↪ List Bool} {f : α → β} {T : α → ℝ} + +/-- **`FTIME` in terms of `ComputableInTimeO`.** For a bound depending only on the encoded input +length, `ComputableInTimeO` agrees with membership in `FTIME`. -/ +theorem mem_FTIME_iff_computableInTimeO {t : ℕ → ℕ} : + f ∈ FTIME encIn encMid t ↔ ComputableInTimeO f encIn encMid fun a => t (encIn a).length := by + constructor + · rintro ⟨c₁, c₂, s, hf⟩ + refine ⟨c₁ + c₂, _, _, fun a => ?_, hf⟩ + push_cast + nlinarith [(Nat.cast_nonneg (t (encIn a).length) : (0 : ℝ) ≤ _), + (Nat.cast_nonneg c₂ : (0 : ℝ) ≤ _), (Nat.cast_nonneg c₁ : (0 : ℝ) ≤ _)] + · rintro ⟨c, t', s, ht', hf⟩ + have ht : ∀ a, t' a ≤ c * t (encIn a).length + c := fun a => by + have := ht' a + simp only at this + exact_mod_cast this + obtain ⟨k, hf'⟩ := ComputableInTimeAndSpace.exists_space_linear hf + exact ⟨c, c, fun n => k * (c * t n + c) + k, + ComputableInTimeAndSpace.mono hf' ht fun a => by + have := Nat.mul_le_mul_left k (ht a) + simp only + omega⟩ + +/-- A function computable within time `O(T)` has a `ComputableInO` certificate within time and +charged workspace `O(t)`, for a natural clock `t` within `O(T)`. -/ +theorem ComputableInTimeO.exists_computableInO (h : ComputableInTimeO f encIn encMid T) : + ∃ (t : α → ℕ) (c : ℕ), ComputableInO f encIn encMid t t ∧ + ∀ a, (t a : ℝ) ≤ c * T a + c := by + obtain ⟨c, t, s, ht, hf⟩ := h + have hl : ∀ a, (encMid (f a)).length ≤ t a := hf.length_le + obtain ⟨k, hf'⟩ := ComputableInTimeAndSpace.exists_space_linear hf + refine ⟨t, c, ComputableInO.of_bounds hf' (k + 1) + (fun a => by nlinarith) (fun a => by nlinarith) (fun a => by nlinarith [hl a]), ht⟩ + +/-- A `ComputableInO` certificate within time `t ≤ T` gives `ComputableInTimeO` within `T`. -/ +theorem ComputableInTimeO.of_computableInO {t S : α → ℕ} + (hf : ComputableInO f encIn encMid t S) (hT : ∀ a, (t a : ℝ) ≤ T a) : + ComputableInTimeO f encIn encMid T := by + obtain ⟨c, hf', -⟩ := hf + refine ⟨c, _, _, fun a => ?_, hf'⟩ + push_cast + nlinarith [hT a, (Nat.cast_nonneg c : (0 : ℝ) ≤ c)] + +/-- `DecidableInTimeO` is `ComputableInTimeO` of a Boolean indicator function. -/ +theorem decidableInTimeO_iff_exists_computableInTimeO {A : Set α} : + DecidableInTimeO A encIn T ↔ + ∃ g : α → Bool, (∀ a, a ∈ A ↔ g a = true) ∧ ComputableInTimeO g encIn encBool T := by + constructor + · rintro ⟨c, t, s, ht, h⟩ + obtain ⟨g, hg, hA⟩ := decidableInTimeAndSpace_iff.mp h + exact ⟨g, hA, c, t, s, ht, hg⟩ + · rintro ⟨g, hA, c, t, s, ht, hg⟩ + exact ⟨c, t, s, ht, decidableInTimeAndSpace_iff.mpr ⟨g, hg, hA⟩⟩ + +/-- A `ComputableInO` certificate within `c * (2 ^ (δ * μ a) * (L + 1) ^ e)` gives +`ComputableInExpTime`. -/ +theorem ComputableInExpTime.of_computableInO {μ : α → ℕ} {δ : ℝ} {t S : α → ℕ} + (hf : ComputableInO f encIn encMid t S) (c e : ℕ) + (ht : ∀ a, (t a : ℝ) ≤ c * (2 ^ (δ * μ a) * ((encIn a).length + 1) ^ e)) : + ComputableInExpTime f encIn encMid μ δ := + ⟨e, (ComputableInTimeO.of_computableInO hf ht).mono c + (fun _ => le_add_of_nonneg_right (Nat.cast_nonneg c)) fun _ => by positivity⟩ + +/-- Every polynomial-time computable function has exponential rate `0` in any parameter `μ`. -/ +theorem ComputableInExpTime.of_computableInPolyTime {μ : α → ℕ} + (hf : ComputableInPolyTime f encIn encMid) : + ComputableInExpTime f encIn encMid μ 0 := by + obtain ⟨d, _, hf'⟩ := hf.exists_degree + refine ComputableInExpTime.of_computableInO hf'.inO 1 d fun a => ?_ + simp + +/-- Guarding an exponential-time function by a polynomial-time test and fallback preserves rate +`δ ≥ 0`. -/ +theorem ComputableInExpTime.ite_polyTime {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) {p : α → Bool} + {g : α → β} (hp : ComputableInPolyTime p encIn encBool) + (hf : ComputableInExpTime f encIn encMid μ δ) + (hg : ComputableInPolyTime g encIn encMid) : + ComputableInExpTime (fun a => if p a then f a else g a) encIn encMid μ δ := by + obtain ⟨e, hf⟩ := hf + obtain ⟨t, c, hfO, ht⟩ := hf.exists_computableInO + obtain ⟨dp, _, hp'⟩ := hp.exists_degree + obtain ⟨dg, _, hg'⟩ := hg.exists_degree + have hcomb := hp'.inO.ite hfO hg'.inO + refine ComputableInExpTime.of_computableInO hcomb (2 * c + 3) (dp + dg + e) fun a => ?_ + set L : ℝ := ((encIn a).length : ℝ) + have hL1 : (1 : ℝ) ≤ L + 1 := by + dsimp only [L] + linarith [(Nat.cast_nonneg (encIn a).length : (0 : ℝ) ≤ _)] + have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) + have hdp : (L + 1) ^ dp ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) + have hdg : (L + 1) ^ dg ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) + have he : (L + 1) ^ e ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) + have hbase : (L + 1) ^ (dp + dg + e) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := + le_mul_of_one_le_left (by positivity) hX1 + have hc0 : (0 : ℝ) ≤ c := Nat.cast_nonneg c + have hpos : (0 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := by positivity + have ht_le : (t a : ℝ) ≤ (2 * c + 1) * (2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e)) := by + have hta := ht a + have hmul := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) + have hmulc := mul_le_mul_of_nonneg_left hmul hc0 + have hc1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := + one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hL1) + have hcc := mul_le_mul_of_nonneg_left hc1 hc0 + dsimp only [L] at * + nlinarith + change ((((encIn a).length + 1) ^ dp + + if p a then t a else ((encIn a).length + 1) ^ dg : ℕ) : ℝ) ≤ _ + split_ifs + · push_cast + dsimp only [L] at * + nlinarith [hdp.trans hbase] + · push_cast + dsimp only [L] at * + nlinarith [hdp.trans hbase, hdg.trans hbase] + +/-- **Exact-rate decision from function computation.** If `f` is computable in time +`2 ^ (δ * μ a) · poly(|a|)` (`δ ≥ 0`) and its encoded output length is polynomially bounded in +`|a|`, then any polynomial-time test on `f a` decides `{a | test (f a) = true}` at the same +exponential rate `δ`. -/ +theorem DecidableInExpTime.of_computableInExpTime_polyBounded {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) + (hf : ComputableInExpTime f encIn encMid μ δ) + (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (encMid (f a)).length)) + {test : β → Bool} (htest : ComputableInPolyTime test encMid encBool) : + DecidableInExpTime {a | test (f a) = true} encIn μ δ := by + obtain ⟨e, hf⟩ := hf + obtain ⟨t, c, hfO, ht⟩ := hf.exists_computableInO + obtain ⟨d, _, htest'⟩ := htest.exists_degree + obtain ⟨p, q, hp⟩ := hlen.exists_le + have hcomp := htest'.inO.comp hfO + refine DecidableInExpTime.of_computableInO hcomp (fun _ => Iff.rfl) + (2 * c + 1 + (p + 1) ^ d) (e + q * d) fun a => ?_ + set L : ℕ := (encIn a).length + have hL1 : 1 ≤ L + 1 := Nat.le_add_left 1 L + have hLR1 : (1 : ℝ) ≤ (L : ℝ) + 1 := by exact_mod_cast hL1 + have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) + have hout_pow : ((encMid (f a)).length + 1) ^ d ≤ (p + 1) ^ d * (L + 1) ^ (q * d) := + Nat.add_one_pow_le_of_le_mul_pow hL1 (hp a) d + have hqd : (((L : ℝ) + 1)) ^ (q * d) ≤ ((L : ℝ) + 1) ^ (e + q * d) := + pow_le_pow_right₀ hLR1 (Nat.le_add_left _ _) + have he : (((L : ℝ) + 1)) ^ e ≤ ((L : ℝ) + 1) ^ (e + q * d) := + pow_le_pow_right₀ hLR1 (Nat.le_add_right _ _) + have houtR : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ + ((p + 1) ^ d : ℕ) * (2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by + have h1 : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ + ((p + 1) ^ d : ℕ) * ((L : ℝ) + 1) ^ (q * d) := by exact_mod_cast hout_pow + have h2 : ((L : ℝ) + 1) ^ (q * d) ≤ 2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d) := + hqd.trans (le_mul_of_one_le_left (by positivity) hX1) + exact h1.trans (mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg _)) + have htR : (t a : ℝ) ≤ (2 * c + 1 : ℕ) * (2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by + have hta := ht a + have h1 := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) + have h2 := mul_le_mul_of_nonneg_left h1 (Nat.cast_nonneg c) + have h3 : (1 : ℝ) ≤ 2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d) := + one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hLR1) + have h4 := mul_le_mul_of_nonneg_left h3 (Nat.cast_nonneg c) + push_cast + dsimp only [L] at * + linarith + change ((t a + ((encMid (f a)).length + 1) ^ d : ℕ) : ℝ) ≤ _ + push_cast + dsimp only [L] at * + push_cast at htR houtR + linarith + +/-- Subexponential function computation with polynomially bounded output length transfers to +subexponential decision for any polynomial-time output predicate. -/ +theorem DecidableInSubexpTime.of_computableInSubexpTime_polyBounded {μ : α → ℕ} + (hf : ComputableInSubexpTime f encIn encMid μ) + (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (encMid (f a)).length)) + {test : β → Bool} (htest : ComputableInPolyTime test encMid encBool) : + DecidableInSubexpTime {a | test (f a) = true} encIn μ := + fun δ hδ => .of_computableInExpTime_polyBounded hδ.le (hf δ hδ) hlen htest + +/-- **Transfer along linear-parameter parsimonious reductions.** If `r : α → β` is computable in +polynomial time with `μB (r a) ≤ c * μA a + c`, and `g : β → γ` is computable in time +`2 ^ (δ * μB b) · poly(|b|)` (`δ ≥ 0`), then `g ∘ r` is computable in time +`2 ^ (c * δ * μA a) · poly(|a|)`. -/ +theorem ComputableInExpTime.of_reduction {μA : α → ℕ} {μB : β → ℕ} {r : α → β} {g : β → γ} + (hr : ComputableInPolyTime r encIn encMid) {c : ℕ} + (hμ : ∀ a, μB (r a) ≤ c * μA a + c) {δ : ℝ} (hδ : 0 ≤ δ) + (hg : ComputableInExpTime g encMid encOut μB δ) : + ComputableInExpTime (g ∘ r) encIn encOut μA (c * δ) := by + obtain ⟨e, hg⟩ := hg + obtain ⟨t, k, hgO, ht⟩ := hg.exists_computableInO + obtain ⟨d, _, hr'⟩ := hr.exists_degree + obtain ⟨l, hl⟩ := hr'.inO.length_le_time + refine ComputableInExpTime.of_computableInO (hgO.comp hr'.inO) + ⌈(1 + k * 2 ^ (δ * c) * (2 * l + 1) ^ e + k : ℝ)⌉₊ (d * (e + 1)) fun a => ?_ + set P : ℝ := ((encIn a).length + 1 : ℝ) ^ d + set X : ℝ := 2 ^ (c * δ * μA a) + have hP : 1 ≤ P := one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _)) + have hX : 1 ≤ X := Real.one_le_rpow (by norm_num) (by positivity) + have hn : ((encMid (r a)).length : ℝ) ≤ l * (P + 1) := by + dsimp only [P] + exact_mod_cast hl a + have hexp : (2 : ℝ) ^ (δ * μB (r a)) ≤ 2 ^ (δ * c) * X := by + rw [← Real.rpow_add (by norm_num)] + refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ + have : (μB (r a) : ℝ) ≤ c * μA a + c := by exact_mod_cast hμ a + nlinarith + have hsum := reduction_add_time_le (C := (2 : ℝ) ^ (δ * c)) + hP hX (by positivity) hn hexp (ht (r a)) + change ((((encIn a).length + 1) ^ d + t (r a) : ℕ) : ℝ) ≤ _ + push_cast + rw [pow_mul] + exact hsum.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil _) (by positivity)) + +/-- Subexponential function computation transfers along linear-parameter polynomial-time +reductions. -/ +theorem ComputableInSubexpTime.of_reduction {μA : α → ℕ} {μB : β → ℕ} {r : α → β} {g : β → γ} + (hr : ComputableInPolyTime r encIn encMid) {c : ℕ} + (hμ : ∀ a, μB (r a) ≤ c * μA a + c) + (hg : ComputableInSubexpTime g encMid encOut μB) : + ComputableInSubexpTime (g ∘ r) encIn encOut μA := by + intro δ hδ + refine ((hg (δ / (c + 1)) (by positivity)).of_reduction hr hμ (by positivity)).mono ?_ + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + +end FunctionMachines + +end Cslib.Complexity diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean b/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean index f70431990f..207286564d 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean @@ -10,7 +10,8 @@ module public import CslibFrontier.Computability.Complexity.AcceptCount public import CslibFrontier.Computability.Complexity.Classes.BPP public import CslibFrontier.Computability.Complexity.Classes.RP -public import CslibFrontier.Computability.Complexity.FineGrained.CountingExponents +public import CslibFrontier.Computability.Complexity.FineGrained.Exponents +public import CslibFrontier.Computability.Complexity.FineGrained.FunctionRates public import CslibFrontier.Computability.Machines.Turing.MultiTape.Probabilistic.Closed public import CslibFrontier.Probability.BitString import CslibFrontier.Computability.Complexity.Classes.Promise.Probabilistic @@ -67,7 +68,7 @@ promise-problem runtime bounds: `ε ∈ (0, 1 / 2)` (and any one-sided threshold `ε ∈ (0, 1)`) defines the exact same runtime rates and exponents. * **Randomized `k`-SAT exponents and hypotheses** (`rSatExponent`, `rpSatExponent`, `rETH`, - `rSETH`): `0 ≤ rSatExponent k ≤ rpSatExponent k ≤ satExponent k ≤ sharpSatExponent k ≤ 1`, + `rSETH`): `0 ≤ rSatExponent k ≤ rpSatExponent k ≤ satExponent k ≤ 1`, `rETH ↔ 0 < rSatExponent 3`, `rSETH ↔ Tendsto rSatExponent atTop (𝓝 1)`, `rETH → ETH`, and `rSETH → SETH`. diff --git a/manual/machines-and-classes/native-counting.md b/manual/machines-and-classes/native-counting.md index 374540230d..688f296930 100644 --- a/manual/machines-and-classes/native-counting.md +++ b/manual/machines-and-classes/native-counting.md @@ -55,9 +55,10 @@ The library also retains [ETH-conditional Partial MCSP results](../circuits-logi ### Extended rates, single-machine bounds, randomized amplification, and Gap-ETH -Four classical modules develop the algorithmic transfer theorems, error models, and exponent inequalities without importing `CountingNativeEndpoint`, and a fifth leaf module connects the native declared/model counters to those interfaces. Their shared scalar estimates for measure rescaling and reduction-time composition live in [`Bounds`](../../CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean). +Five classical modules develop the algorithmic transfer theorems, error models, and exponent inequalities without importing `CountingNativeEndpoint`, and a sixth leaf module connects the native declared/model counters to those interfaces. Their shared scalar estimates for measure rescaling and reduction-time composition live in [`Bounds`](../../CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean). -- **Counting rates (`#k-SAT`, `#ETH`, `#SETH`)** in [`CountingExponents`](../../CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean): `ComputableInTimeO`, `ComputableInExpTime`, and `ComputableInSubexpTime` parameterize function runtimes by `μ : α → ℕ` without constraining workspace length (`mem_FTIME_iff_computableInTimeO`). `SharpKSAT k` (`SharpKSAT 3 = SharpThreeSAT`) has binary output length bounded linearly in `|encCNF φ|`, so counting rates transfer without exponent loss to decision rates (`satExponent k ≤ sharpSatExponent k ≤ 1`), infima over `δ ≥ 0` match infima over `δ > 0` (`satExponent_eq_sInf_pos`, `sharpSatExponent_eq_sInf_pos`), finite-prefix suprema characterize `SETH` and `SharpSETH` (`SETH_iff_iSup_ge_three_eq_one`, `SharpSETH_iff_iSup_ge_three_eq_one`), clause-splitting plus IPZ sparsification proves `SETH.eth` (`SETH → ETH`) without invoking native refutations, `unrestrictedSatExponent` distinguishes unbounded-width `SAT` from the supremum of `satExponent k` over fixed widths `k` (this supremum `≤ unrestrictedSatExponent ≤ 1`, and `SETH → unrestrictedSatExponent = 1`), and disjoint counting sparsification transfers clause-measured rates to variable-measured rates (`exists_computableInExpTime_SharpKSAT_numVars_of_length`, `SharpETH_iff_not_computableInSubexpTime_length`). +- **Function rates** in [`FunctionRates`](../../CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean): `ComputableInTimeO`, `ComputableInExpTime`, and `ComputableInSubexpTime` parameterize function runtimes by `μ : α → ℕ` without constraining workspace length (`mem_FTIME_iff_computableInTimeO`). +- **Counting rates (`#k-SAT`, `#ETH`, `#SETH`)** in [`CountingExponents`](../../CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean): `SharpKSAT k` (`SharpKSAT 3 = SharpThreeSAT`) has binary output length bounded linearly in `|encCNF φ|`, so counting rates transfer without exponent loss to decision rates (`satExponent k ≤ sharpSatExponent k ≤ 1`), infima over `δ ≥ 0` match infima over `δ > 0` (`satExponent_eq_sInf_pos`, `sharpSatExponent_eq_sInf_pos`), finite-prefix suprema characterize `SETH` and `SharpSETH` (`SETH_iff_iSup_ge_three_eq_one`, `SharpSETH_iff_iSup_ge_three_eq_one`), clause-splitting plus IPZ sparsification proves `SETH.eth` (`SETH → ETH`) without invoking native refutations, `unrestrictedSatExponent` distinguishes unbounded-width `SAT` from the supremum of `satExponent k` over fixed widths `k` (this supremum `≤ unrestrictedSatExponent ≤ 1`, and `SETH → unrestrictedSatExponent = 1`), and disjoint counting sparsification transfers clause-measured rates to variable-measured rates (`exists_computableInExpTime_SharpKSAT_numVars_of_length`, `SharpETH_iff_not_computableInSubexpTime_length`). - **Single-machine subexponential time (`2 ^ o(μ)`) vs. rate families (`∀ δ > 0`)** in [`SingleSubexp`](../../CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean): `DecidableInSingleSubexpTime` and `ComputableInSingleSubexpTime` ask for one native machine running within `2 ^ s(μ a) · poly(L)` for `s = o(n)` (`decidableInSingleSubexpTime_iff_exists_machine`, `computableInSingleSubexpTime_iff_exists_machine`, using the sublinear envelopes in [`SublinearEnvelope`](../../CslibFrontier/Foundations/Analysis/SublinearEnvelope.lean)), strictly reversing the `∀ δ > 0, ∃ M_δ` quantifier order of `DecidableInSubexpTime`. Conversely, `DecidableInSingleSubexpTime.of_uniformFamily` and `ComputableInSingleSubexpTime.of_uniformFamily` convert a single `PrecisionInput`-encoded family machine back to `2 ^ o(μ)` time given a polynomial runtime bound `O((m + 1) ^ d * 2 ^ (μ a / (m + 1)) * (L + 1) ^ e)` in the unary precision `m` and encoded input length `L` together with a polynomial-time unary schedule `sched` tending to infinity with `μ a`. - **Randomized fine-grained rates (`rETH`, `rSETH`)** in [`Randomized`](../../CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean): `ErrorModel` packages asymmetric `(yesErr, noErr)` profiles (`deterministic`, `twoSided`, `bounded`, `oneSidedRP`, `rp`, `oneSidedCoRP`, `coRP`). `SolvesWithErrorInTimeO` charges unary coin-count computation, input/seed framing, and deterministic verification on `w.length = ℓ a`, compiling under `0 ≤ T a` to halting fair-coin `MultiTapePTM`s (`exists_ptm_of_solvesWithErrorInTimeO`) and matching `PromiseBPP`, `PromiseRP`, and `PromiseCoRP` on polynomial length bounds. Under `0 ≤ T a`, constant-factor majority voting (via [`MajorityVote`](../../CslibFrontier/Probability/MajorityVote.lean)) and `OR`-amplification (`amplify_twoSided`, `amplify_oneSidedRP`) preserve `O(T a)` and therefore every exponential rate `δ ≥ 0`, making `rSatExponent k` and `rpSatExponent k` invariant across `(0, 1 / 2)` and `(0, 1)` respectively (`0 ≤ rSatExponent k ≤ rpSatExponent k ≤ satExponent k`). - **Gap `k`-SAT and Gap-ETH (`GapETH`, `rGapETH`)** in [`GapETH`](../../CslibFrontier/Computability/Complexity/FineGrained/GapETH.lean): `GapKSAT P` (`P : GapKSATSpec`, with `0 ≤ soundness < completeness ≤ 1`) specializes definitionally at `(3, 1, s)` to `GapThreeSAT s` [dinur2016][dinur2016], [manurangsiraghavendra2017][manurangsiraghavendra2017]. Choosing a rational midpoint reduces every `GapKSAT P` (including imperfect completeness `c < 1`) with zero variable blowup to `MaxKSATThreshold P.width`, giving `0 ≤ rGapSatExponent P ≤ gapSatExponent P ≤ 1` unconditionally. Perfect completeness (`c = 1`) reduces directly to `KSAT k`, yielding the positive conditional implications `rGapETH → GapETH → ETH → SingleETH → SingleSharpETH` and `rGapETH → rETH → ETH → SharpETH → SingleSharpETH`. Imperfect-completeness subexponential MAX-`k`-SAT is not claimed. From b8a75c16f8962494a92a46c9b1e8567beeed7503 Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 18:35:37 +0000 Subject: [PATCH 2/6] refactor(Complexity/FineGrained): shared envelope and rescale lemmas in Bounds Add exponential-times-polynomial envelope lemmas (one_le_two_rpow_mul_pow, two_rpow_mul_pow_le_two_rpow_mul_pow, pow_le_two_rpow_mul_pow, two_rpow_mul_pow_le_natCeil_mul_add, le_two_mul_mul_of_le_mul_add) and the subexponential rescaling step natCast_mul_div_add_one_le to FineGrained/Bounds, and use them for the TimeO/ExpTime/SubexpTime monotonicity, intersection, if-then-else and measure-change transfers in FineGrained, FunctionRates, Exponents, CountingExponents and Randomized. Also folds in the #4747 review nits: drop CountingExponents' unused Nat.Power and ResourceFacts imports, and list FunctionRates among RatesNativeEndpoint's classical modules. Part of #4737. --- .../Computability/Complexity/FineGrained.lean | 35 ++--- .../Complexity/FineGrained/Bounds.lean | 93 +++++++++++-- .../FineGrained/CountingExponents.lean | 60 +++------ .../Complexity/FineGrained/Exponents.lean | 42 +++--- .../Complexity/FineGrained/FunctionRates.lean | 122 +++++------------- .../Complexity/FineGrained/Randomized.lean | 104 +++++---------- .../FineGrained/RatesNativeEndpoint.lean | 11 +- .../machines-and-classes/native-counting.md | 2 +- 8 files changed, 196 insertions(+), 273 deletions(-) diff --git a/CslibFrontier/Computability/Complexity/FineGrained.lean b/CslibFrontier/Computability/Complexity/FineGrained.lean index 65876883d1..ad5a9d08f4 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained.lean @@ -12,6 +12,7 @@ public import CslibFrontier.Computability.Complexity.Problems.ThreeSAT public import CslibFrontier.Logics.Propositional.CNF.ModelCount public import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.BigO public import Mathlib.Analysis.SpecialFunctions.Pow.Real +import CslibFrontier.Computability.Complexity.FineGrained.Bounds import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCombinators @@ -216,13 +217,9 @@ def DecidableInSubexpTime (A : Set α) (enc : α ↪ List Bool) (μ : α → ℕ theorem DecidableInExpTime.mono {μ : α → ℕ} {δ δ' : ℝ} (h : DecidableInExpTime A enc μ δ) (hδ : δ ≤ δ') : DecidableInExpTime A enc μ δ' := by obtain ⟨e, h⟩ := h - refine ⟨e, h.mono 1 (fun a => ?_) fun a => by positivity⟩ - have h₁ : (2 : ℝ) ^ (δ * μ a) ≤ 2 ^ (δ' * μ a) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) - (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) - have h₂ := mul_le_mul_of_nonneg_right h₁ (by positivity : (0 : ℝ) ≤ ((enc a).length + 1) ^ e) - push_cast - linarith + exact ⟨e, h.mono 1 (fun a => (two_rpow_mul_pow_le_two_rpow_mul_pow + (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) le_rfl).trans (by simp)) + fun a => by positivity⟩ section Machines @@ -244,24 +241,12 @@ theorem DecidableInExpTime.inter {μ : α → ℕ} {δ : ℝ} {p : α → Bool} obtain ⟨e, h⟩ := h obtain ⟨e', h⟩ := h.inter hp fun a => by positivity refine ⟨e + e', h.mono 2 (fun a => ?_) fun a => by positivity⟩ - have hL : (1 : ℝ) ≤ (enc a).length + 1 := by - linarith [(Nat.cast_nonneg (enc a).length : (0 : ℝ) ≤ _)] - have h₁ : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have h₂ : (((enc a).length : ℝ) + 1) ^ e ≤ ((enc a).length + 1) ^ (e + e') := - pow_le_pow_right₀ hL (Nat.le_add_right e e') - have h₃ : (((enc a).length : ℝ) + 1) ^ e' ≤ ((enc a).length + 1) ^ (e + e') := - pow_le_pow_right₀ hL (Nat.le_add_left e' e) - have h₄ := mul_le_mul_of_nonneg_left h₂ (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - have h₅ : (((enc a).length : ℝ) + 1) ^ (e + e') ≤ - 2 ^ (δ * μ a) * ((enc a).length + 1) ^ (e + e') := - le_mul_of_one_le_left (by positivity) h₁ - have h₆ : (if p a = true then 2 ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e else 0) ≤ - 2 ^ (δ * μ a) * ((enc a).length + 1) ^ (e + e') := by - split_ifs - · exact h₄ - · positivity - push_cast - nlinarith + have hx : 0 ≤ δ * μ a := by positivity + have h₁ := two_rpow_mul_pow_le_two_rpow_mul_pow (L := (enc a).length) (x := δ * μ a) le_rfl + (Nat.le_add_right e e') + have h₂ := pow_le_two_rpow_mul_pow (L := (enc a).length) hx (Nat.le_add_left e' e) + have h₃ : (0 : ℝ) ≤ 2 ^ (δ * μ a) * ((enc a).length + 1) ^ (e + e') := by positivity + split_ifs <;> push_cast <;> linarith end Machines diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean b/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean index d5603934e2..ff8dace1df 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean @@ -18,14 +18,23 @@ import Mathlib.Tactic.Positivity # Scalar bounds for fine-grained runtime transfers These arithmetic estimates absorb additive linear changes of a natural parameter into a fixed -exponential factor and bound the time of a polynomial-time reduction followed by a computation. -They are shared by decision, function-computation and randomized runtime transfers without -mentioning a machine or error model. +exponential factor, compare and absorb terms into exponential-times-polynomial envelopes +`2 ^ x * (L + 1) ^ e`, and bound the time of a polynomial-time reduction followed by a +computation. They are shared by decision, function-computation and randomized runtime transfers +without mentioning a machine or error model. ## Main results -* `Cslib.Complexity.two_rpow_le_natCeil_mul_of_le_mul_add`: rescale an exponential rate under an - additive linear parameter bound. +* `Cslib.Complexity.two_rpow_le_natCeil_mul_of_le_mul_add`, + `Cslib.Complexity.two_rpow_mul_pow_le_natCeil_mul_add`: rescale an exponential rate, alone or + in an envelope, under an additive linear parameter bound. +* `Cslib.Complexity.natCast_mul_div_add_one_le`: the rate rescaling `c * (δ / (c + 1)) ≤ δ` behind + subexponential transfers. +* `Cslib.Complexity.one_le_two_rpow_mul_pow`, + `Cslib.Complexity.two_rpow_mul_pow_le_two_rpow_mul_pow`, + `Cslib.Complexity.pow_le_two_rpow_mul_pow`: envelopes are at least `1`, monotone in the exponent + and degree, and dominate polynomials of lower degree. +* `Cslib.Complexity.le_two_mul_mul_of_le_mul_add`: absorb an additive constant into an envelope. * `Cslib.Complexity.reduction_add_time_le`: combine reduction and target runtimes while retaining the target's exponential envelope and the polynomial input-length factor. -/ @@ -34,17 +43,77 @@ public section namespace Cslib.Complexity +/-- An additive linear bound on a natural parameter splits its exponential at rate `δ ≥ 0` into a +constant factor and an exponential at rate `c * δ`. -/ +theorem two_rpow_le_two_rpow_mul_of_le_mul_add {δ : ℝ} {n m c : ℕ} + (hδ : 0 ≤ δ) (hn : n ≤ c * m + c) : + (2 : ℝ) ^ (δ * n) ≤ 2 ^ (δ * c) * 2 ^ (c * δ * m) := by + rw [← Real.rpow_add (by norm_num)] + refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ + have : (n : ℝ) ≤ c * m + c := by exact_mod_cast hn + nlinarith + /-- An additive linear bound on a natural parameter rescales its exponential rate, with the additive part absorbed by a natural ceiling constant. -/ theorem two_rpow_le_natCeil_mul_of_le_mul_add {δ : ℝ} {n m c : ℕ} (hδ : 0 ≤ δ) (hn : n ≤ c * m + c) : - (2 : ℝ) ^ (δ * n) ≤ (⌈(2 : ℝ) ^ (δ * c)⌉₊ : ℝ) * 2 ^ (c * δ * m) := by - have hexp : (2 : ℝ) ^ (δ * n) ≤ 2 ^ (δ * c) * 2 ^ (c * δ * m) := by - rw [← Real.rpow_add (by norm_num)] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - have : (n : ℝ) ≤ c * m + c := by exact_mod_cast hn - nlinarith - exact hexp.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil _) (Real.rpow_nonneg (by norm_num) _)) + (2 : ℝ) ^ (δ * n) ≤ (⌈(2 : ℝ) ^ (δ * c)⌉₊ : ℝ) * 2 ^ (c * δ * m) := + (two_rpow_le_two_rpow_mul_of_le_mul_add hδ hn).trans + (mul_le_mul_of_nonneg_right (Nat.le_ceil _) (Real.rpow_nonneg (by norm_num) _)) + +/-- Rescaling a rate `δ ≥ 0` by `1 / (c + 1)` leaves room for a factor `c`: the step that +transfers a bound for every rate `δ > 0` along a parameter change by the factor `c`. -/ +theorem natCast_mul_div_add_one_le {δ : ℝ} (hδ : 0 ≤ δ) (c : ℕ) : c * (δ / (c + 1)) ≤ δ := by + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + +/-! ### Exponential-times-polynomial envelopes + +Exponential runtime bounds have the form `2 ^ x * (L + 1) ^ e` for an exponent `x ≥ 0` and the +length `L` of the encoded input. The envelope is at least `1`, grows in `x` and `e`, and absorbs +polynomials of lower degree and additive constants. -/ + +section Envelope + +variable {x y : ℝ} {L d e : ℕ} + +/-- An exponential-times-polynomial envelope with nonnegative exponent is at least `1`. -/ +theorem one_le_two_rpow_mul_pow (hx : 0 ≤ x) : 1 ≤ (2 : ℝ) ^ x * ((L : ℝ) + 1) ^ e := + one_le_mul_of_one_le_of_one_le (Real.one_le_rpow (by norm_num) hx) + (one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg L))) + +/-- An exponential-times-polynomial envelope grows with its exponent and its degree. -/ +theorem two_rpow_mul_pow_le_two_rpow_mul_pow (hxy : x ≤ y) (hde : d ≤ e) : + (2 : ℝ) ^ x * ((L : ℝ) + 1) ^ d ≤ 2 ^ y * ((L : ℝ) + 1) ^ e := + mul_le_mul (Real.rpow_le_rpow_of_exponent_le (by norm_num) hxy) + (pow_le_pow_right₀ (le_add_of_nonneg_left (Nat.cast_nonneg L)) hde) (by positivity) + (by positivity) + +/-- A polynomial of degree `d ≤ e` is below the envelope `2 ^ x * (L + 1) ^ e`, `x ≥ 0`. -/ +theorem pow_le_two_rpow_mul_pow (hx : 0 ≤ x) (hde : d ≤ e) : + ((L : ℝ) + 1) ^ d ≤ 2 ^ x * ((L : ℝ) + 1) ^ e := + (pow_le_pow_right₀ (le_add_of_nonneg_left (Nat.cast_nonneg L)) hde).trans + (le_mul_of_one_le_left (by positivity) (Real.one_le_rpow (by norm_num) hx)) + +/-- An additive linear bound on a natural parameter rescales an exponential-times-polynomial +envelope at rate `δ ≥ 0` to one at rate `c * δ`, up to a natural ceiling constant: the bound that +`TimeO.mono` needs to transfer an exponential runtime along the parameter change. -/ +theorem two_rpow_mul_pow_le_natCeil_mul_add {δ : ℝ} {n m c : ℕ} (hδ : 0 ≤ δ) + (hn : n ≤ c * m + c) : + (2 : ℝ) ^ (δ * n) * ((L : ℝ) + 1) ^ e ≤ + ⌈(2 : ℝ) ^ (δ * c)⌉₊ * (2 ^ (c * δ * m) * ((L : ℝ) + 1) ^ e) + ⌈(2 : ℝ) ^ (δ * c)⌉₊ := by + rw [← mul_assoc] + exact le_add_of_le_of_nonneg (mul_le_mul_of_nonneg_right + (two_rpow_le_natCeil_mul_of_le_mul_add hδ hn) (by positivity)) (Nat.cast_nonneg _) + +end Envelope + +/-- A runtime `t ≤ c * Y + c` with `Y ≤ X` and `1 ≤ X` is at most `2 * c * X`: an additive +constant is absorbed into an envelope that is at least `1`. -/ +theorem le_two_mul_mul_of_le_mul_add {t X Y : ℝ} {c : ℕ} (ht : t ≤ c * Y + c) (hY : Y ≤ X) + (hX : 1 ≤ X) : t ≤ 2 * c * X := by + have hc : (0 : ℝ) ≤ c := Nat.cast_nonneg c + nlinarith /-- **Running a computation on a reduced instance.** If the reduction runs within time `P ≥ 1` and its output has length `n ≤ l * (P + 1)`, a subsequent computation with time diff --git a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean index b81a4e13bc..894f0083ca 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean @@ -11,6 +11,7 @@ public import CslibFrontier.Computability.Complexity.FineGrained.Exponents public import CslibFrontier.Computability.Complexity.FineGrained.FunctionRates public import CslibFrontier.Computability.Complexity.FineGrained.Reduction public import CslibFrontier.Computability.Complexity.Problems.SharpThreeSAT +import CslibFrontier.Computability.Complexity.FineGrained.Bounds import CslibFrontier.Computability.Complexity.FineGrained.CountingTreeBound import CslibFrontier.Computability.Complexity.FineGrained.Sparsification import CslibFrontier.Computability.Complexity.Problems.SAT.PolyTime @@ -23,10 +24,8 @@ import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.NatPower import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.Structure import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCombinators import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration -import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts import CslibFrontier.Foundations.Analysis.SublinearEnvelope import CslibFrontier.Foundations.Data.List.OfFn -import CslibFrontier.Foundations.Data.Nat.Power import Mathlib.Topology.Instances.Real.Lemmas /-! @@ -705,45 +704,32 @@ theorem ComputableInExpTime.SharpKSAT_length_of_numVars {k : ℕ} {δ : ℝ} (h · simp only [SharpKSAT, hφ, ↓reduceIte] · simp only [SharpKSAT, hφ, Bool.false_eq_true, ↓reduceIte] refine ComputableInExpTime.of_computableInO hite (2 * c + 3) (dw + dc + e) fun φ => ?_ - set L : ℝ := ((encCNF φ).length : ℝ) - have hL1 : (1 : ℝ) ≤ L + 1 := by - dsimp only [L] - linarith [(Nat.cast_nonneg (encCNF φ).length : (0 : ℝ) ≤ _)] - have hX1 : (1 : ℝ) ≤ 2 ^ (k * δ * φ.length) := Real.one_le_rpow (by norm_num) (by positivity) - have hdw : (L + 1) ^ dw ≤ 2 ^ (k * δ * φ.length) * (L + 1) ^ (dw + dc + e) := - (pow_le_pow_right₀ hL1 (by omega)).trans (le_mul_of_one_le_left (by positivity) hX1) - have hdc : (L + 1) ^ dc ≤ 2 ^ (k * δ * φ.length) * (L + 1) ^ (dw + dc + e) := - (pow_le_pow_right₀ hL1 (by omega)).trans (le_mul_of_one_le_left (by positivity) hX1) - have he : (L + 1) ^ e ≤ (L + 1) ^ (dw + dc + e) := pow_le_pow_right₀ hL1 (by omega) - have hc_nn : (0 : ℝ) ≤ c := Nat.cast_nonneg c - have hpos : (0 : ℝ) ≤ 2 ^ (k * δ * φ.length) * (L + 1) ^ (dw + dc + e) := by positivity + have hx : 0 ≤ k * δ * φ.length := by positivity + have hX := one_le_two_rpow_mul_pow (L := (encCNF φ).length) (e := dw + dc + e) hx + have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) + have hdw := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dw) (e := dw + dc + e) hx + (by omega) + have hdc := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dc) (e := dw + dc + e) hx + (by omega) change ((((encCNF φ).length + 1) ^ dw + if φ.all (fun cl => decide (cl.length ≤ k)) then t φ else ((encCNF φ).length + 1) ^ dc : ℕ) : ℝ) ≤ _ split_ifs with hφ · simp only [List.all_eq_true, decide_eq_true_eq] at hφ have hn : (φ.numVars : ℝ) ≤ k * φ.length := by exact_mod_cast CNF.numVars_le_mul_length hφ - have hexp : (2 : ℝ) ^ (δ * φ.numVars) ≤ 2 ^ (k * δ * φ.length) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) (by nlinarith) - have hmul := mul_le_mul hexp he (by positivity) (by positivity) - have hmulc := mul_le_mul_of_nonneg_left hmul hc_nn - have hc1 : (c : ℝ) ≤ c * (2 ^ (k * δ * φ.length) * (L + 1) ^ (dw + dc + e)) := - le_mul_of_one_le_right hc_nn (one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hL1)) + have ht' := le_two_mul_mul_of_le_mul_add (ht φ) + (two_rpow_mul_pow_le_two_rpow_mul_pow (by nlinarith) (by omega)) hX push_cast - dsimp only [L] at * - nlinarith [ht φ] + linarith · push_cast - dsimp only [L] at * - nlinarith + linarith /-- Subexponential `#k-SAT` counting in `numVars` gives subexponential counting in `length`. -/ theorem ComputableInSubexpTime.SharpKSAT_length_of_numVars {k : ℕ} (h : ComputableInSubexpTime (SharpKSAT k) encCNF encNat CNF.numVars) : - ComputableInSubexpTime (SharpKSAT k) encCNF encNat List.length := by - intro δ hδ - refine ((h (δ / (k + 1)) (by positivity)).SharpKSAT_length_of_numVars (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + ComputableInSubexpTime (SharpKSAT k) encCNF encNat List.length := fun δ hδ => + ((h (δ / (k + 1)) (by positivity)).SharpKSAT_length_of_numVars (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le k) /-- **From clauses to variables via disjoint counting sparsification.** For every width `k` and every `ε > 0`, there is a constant `c` such that any `#k-SAT` counter within time @@ -783,13 +769,9 @@ theorem exists_computableInExpTime_SharpKSAT_numVars_of_length (k : ℕ) {ε : (1 / B + occBound K M * δ) := by refine ComputableInExpTime.of_computableInO hsearchO (2 * C₀ + 1) E fun φ => ?_ have hTφ := hT φ - have h1 : (1 : ℝ) ≤ (2 : ℝ) ^ ((1 / (B : ℝ) + occBound K M * δ) * φ.numVars) * - (((encCNF φ).length : ℝ) + 1) ^ E := - one_le_mul_of_one_le_of_one_le (Real.one_le_rpow (by norm_num) (by positivity)) - (one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _))) - have hC₀ : (C₀ : ℝ) ≤ C₀ * ((2 : ℝ) ^ ((1 / (B : ℝ) + occBound K M * δ) * φ.numVars) * - (((encCNF φ).length : ℝ) + 1) ^ E) := - le_mul_of_one_le_right (Nat.cast_nonneg C₀) h1 + have h1 := one_le_two_rpow_mul_pow (L := (encCNF φ).length) (e := E) + (by positivity : 0 ≤ (1 / (B : ℝ) + occBound K M * δ) * φ.numVars) + have hC₀ := le_mul_of_one_le_right (Nat.cast_nonneg C₀ : (0 : ℝ) ≤ C₀) h1 push_cast linarith exact hrate.mono (by linarith) @@ -803,11 +785,7 @@ theorem ComputableInSubexpTime.SharpKSAT_numVars_of_length {k : ℕ} obtain ⟨c, hc⟩ := exists_computableInExpTime_SharpKSAT_numVars_of_length k (half_pos hδ) have hδ' : 0 < δ / 2 / (c + 1) := by positivity refine (hc _ hδ'.le (h _ hδ')).mono ?_ - have hc0 : (0 : ℝ) ≤ c := Nat.cast_nonneg c - have : (c : ℝ) * (δ / 2 / (c + 1)) ≤ δ / 2 := by - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith - linarith + linarith [natCast_mul_div_add_one_le (half_pos hδ).le c] /-- **`#ETH` in terms of clauses:** `SharpETH` holds iff `#3-SAT` is not computable in subexponential time in the number of clauses. -/ diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Exponents.lean b/CslibFrontier/Computability/Complexity/FineGrained/Exponents.lean index 4900d20087..2d1b635d16 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Exponents.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Exponents.lean @@ -9,6 +9,7 @@ module public import CslibFrontier.Computability.Complexity.FineGrained.BruteForce public import Mathlib.Topology.Order.Real +import CslibFrontier.Computability.Complexity.FineGrained.Bounds import Mathlib.Topology.Instances.Real.Lemmas /-! @@ -159,29 +160,18 @@ theorem DecidableInExpTime.length_of_numVars {k : ℕ} {δ : ℝ} (hδ : 0 ≤ obtain ⟨e', h⟩ := h.inter (computableInPolyTime_all_length_le k) fun φ => by positivity rw [← KSAT_eq_inter k le_rfl (KSAT_subset_SAT k)] at h refine ⟨e + e', h.mono 2 (fun φ => ?_) fun φ => by positivity⟩ - have hL : (1 : ℝ) ≤ (encCNF φ).length + 1 := by - linarith [(Nat.cast_nonneg (encCNF φ).length : (0 : ℝ) ≤ _)] - have h₁ : (1 : ℝ) ≤ 2 ^ (k * δ * φ.length) := Real.one_le_rpow (by norm_num) (by positivity) - have h₂ : (((encCNF φ).length : ℝ) + 1) ^ e ≤ ((encCNF φ).length + 1) ^ (e + e') := - pow_le_pow_right₀ hL (Nat.le_add_right e e') - have h₃ : (((encCNF φ).length : ℝ) + 1) ^ e' ≤ ((encCNF φ).length + 1) ^ (e + e') := - pow_le_pow_right₀ hL (Nat.le_add_left e' e) - have h₅ : (((encCNF φ).length : ℝ) + 1) ^ (e + e') ≤ - 2 ^ (k * δ * φ.length) * ((encCNF φ).length + 1) ^ (e + e') := - le_mul_of_one_le_left (by positivity) h₁ - have h₆ : (if (φ.all fun c => decide (c.length ≤ k)) = true then - 2 ^ (δ * φ.numVars) * (((encCNF φ).length : ℝ) + 1) ^ e else 0) ≤ - 2 ^ (k * δ * φ.length) * ((encCNF φ).length + 1) ^ (e + e') := by - split_ifs with hw - · simp only [List.all_eq_true, decide_eq_true_eq] at hw - have hn : (φ.numVars : ℝ) ≤ k * φ.length := by - exact_mod_cast CNF.numVars_le_mul_length hw - have h₇ : (2 : ℝ) ^ (δ * φ.numVars) ≤ 2 ^ (k * δ * φ.length) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) (by nlinarith) - exact mul_le_mul h₇ h₂ (by positivity) (by positivity) - · positivity - push_cast - nlinarith + have h₂ := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (by positivity : 0 ≤ k * δ * φ.length) + (Nat.le_add_left e' e) + have h₃ : (0 : ℝ) ≤ 2 ^ (k * δ * φ.length) * ((encCNF φ).length + 1) ^ (e + e') := by positivity + split_ifs with hw + · simp only [List.all_eq_true, decide_eq_true_eq] at hw + have hn : (φ.numVars : ℝ) ≤ k * φ.length := by exact_mod_cast CNF.numVars_le_mul_length hw + have h₁ := two_rpow_mul_pow_le_two_rpow_mul_pow (L := (encCNF φ).length) + (by nlinarith : δ * φ.numVars ≤ k * δ * φ.length) (Nat.le_add_right e e') + push_cast + linarith + · push_cast + linarith /-- **From variables to clauses.** If `k`-SAT is decidable in subexponential time in the number of variables, it is decidable in subexponential time in the number of clauses. -/ @@ -189,10 +179,8 @@ theorem DecidableInSubexpTime.length_of_numVars {k : ℕ} (h : DecidableInSubexpTime (KSAT k) encCNF CNF.numVars) : DecidableInSubexpTime (KSAT k) encCNF List.length := by intro δ hδ - have h' := (h (δ / (k + 1)) (by positivity)).length_of_numVars (by positivity) - refine h'.mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + exact ((h (δ / (k + 1)) (by positivity)).length_of_numVars (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le k) /-- **The exponential time hypothesis from clauses**: if 3SAT is not decidable in subexponential time in the number of clauses, then `ETH`. -/ diff --git a/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean index 6084ba4ed4..63b3016dbf 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean @@ -93,34 +93,23 @@ theorem ComputableInExpTime.mono {μ : α → ℕ} {δ δ' : ℝ} (h : ComputableInExpTime f encIn encOut μ δ) (hδ : δ ≤ δ') : ComputableInExpTime f encIn encOut μ δ' := by obtain ⟨e, h⟩ := h - refine ⟨e, h.mono 1 (fun a => ?_) fun a => by positivity⟩ - have h₁ : (2 : ℝ) ^ (δ * μ a) ≤ 2 ^ (δ' * μ a) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) - (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) - have h₂ := mul_le_mul_of_nonneg_right h₁ (by positivity : (0 : ℝ) ≤ ((encIn a).length + 1) ^ e) - push_cast - linarith + exact ⟨e, h.mono 1 (fun a => (two_rpow_mul_pow_le_two_rpow_mul_pow + (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) le_rfl).trans (by simp)) + fun a => by positivity⟩ /-- Rescaling the parameter linearly rescales the exponential rate. -/ theorem ComputableInExpTime.mono_measure {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) {δ : ℝ} (hδ : 0 ≤ δ) (h : ComputableInExpTime f encIn encOut μ δ) : - ComputableInExpTime f encIn encOut μ' (c * δ) := by - obtain ⟨e, h⟩ := h - refine ⟨e, h.mono ⌈(2 : ℝ) ^ (δ * c)⌉₊ (fun a => ?_) fun a => by positivity⟩ - have h₂ := two_rpow_le_natCeil_mul_of_le_mul_add hδ (hμ a) - have h₃ := mul_le_mul_of_nonneg_right h₂ - (by positivity : (0 : ℝ) ≤ ((encIn a).length + 1) ^ e) - have h₄ : (0 : ℝ) ≤ ⌈(2 : ℝ) ^ (δ * c)⌉₊ := Nat.cast_nonneg _ - nlinarith + ComputableInExpTime f encIn encOut μ' (c * δ) := + let ⟨e, h⟩ := h + ⟨e, h.mono _ (fun a => two_rpow_mul_pow_le_natCeil_mul_add hδ (hμ a)) fun a => by positivity⟩ /-- Subexponential computability transfers to any parameter at least linear in `μ`. -/ theorem ComputableInSubexpTime.mono_measure {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) (h : ComputableInSubexpTime f encIn encOut μ) : - ComputableInSubexpTime f encIn encOut μ' := by - intro δ hδ - refine ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + ComputableInSubexpTime f encIn encOut μ' := fun δ hδ => + ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le c) end FunctionBounds @@ -212,36 +201,18 @@ theorem ComputableInExpTime.ite_polyTime {μ : α → ℕ} {δ : ℝ} (hδ : 0 obtain ⟨dg, _, hg'⟩ := hg.exists_degree have hcomb := hp'.inO.ite hfO hg'.inO refine ComputableInExpTime.of_computableInO hcomb (2 * c + 3) (dp + dg + e) fun a => ?_ - set L : ℝ := ((encIn a).length : ℝ) - have hL1 : (1 : ℝ) ≤ L + 1 := by - dsimp only [L] - linarith [(Nat.cast_nonneg (encIn a).length : (0 : ℝ) ≤ _)] - have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have hdp : (L + 1) ^ dp ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) - have hdg : (L + 1) ^ dg ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) - have he : (L + 1) ^ e ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) - have hbase : (L + 1) ^ (dp + dg + e) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := - le_mul_of_one_le_left (by positivity) hX1 - have hc0 : (0 : ℝ) ≤ c := Nat.cast_nonneg c - have hpos : (0 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := by positivity - have ht_le : (t a : ℝ) ≤ (2 * c + 1) * (2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e)) := by - have hta := ht a - have hmul := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - have hmulc := mul_le_mul_of_nonneg_left hmul hc0 - have hc1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := - one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hL1) - have hcc := mul_le_mul_of_nonneg_left hc1 hc0 - dsimp only [L] at * - nlinarith + have hx : 0 ≤ δ * μ a := by positivity + have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := dp + dg + e) hx + have ht' : (t a : ℝ) ≤ 2 * c * (2 ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ (dp + dg + e)) := + le_two_mul_mul_of_le_mul_add (ht a) (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega)) hX + have hdp := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dp) (e := dp + dg + e) hx + (by omega) + have hdg := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dg) (e := dp + dg + e) hx + (by omega) + have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) change ((((encIn a).length + 1) ^ dp + if p a then t a else ((encIn a).length + 1) ^ dg : ℕ) : ℝ) ≤ _ - split_ifs - · push_cast - dsimp only [L] at * - nlinarith [hdp.trans hbase] - · push_cast - dsimp only [L] at * - nlinarith [hdp.trans hbase, hdg.trans hbase] + split_ifs <;> push_cast <;> linarith /-- **Exact-rate decision from function computation.** If `f` is computable in time `2 ^ (δ * μ a) · poly(|a|)` (`δ ≥ 0`) and its encoded output length is polynomially bounded in @@ -259,37 +230,17 @@ theorem DecidableInExpTime.of_computableInExpTime_polyBounded {μ : α → ℕ} have hcomp := htest'.inO.comp hfO refine DecidableInExpTime.of_computableInO hcomp (fun _ => Iff.rfl) (2 * c + 1 + (p + 1) ^ d) (e + q * d) fun a => ?_ - set L : ℕ := (encIn a).length - have hL1 : 1 ≤ L + 1 := Nat.le_add_left 1 L - have hLR1 : (1 : ℝ) ≤ (L : ℝ) + 1 := by exact_mod_cast hL1 - have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have hout_pow : ((encMid (f a)).length + 1) ^ d ≤ (p + 1) ^ d * (L + 1) ^ (q * d) := - Nat.add_one_pow_le_of_le_mul_pow hL1 (hp a) d - have hqd : (((L : ℝ) + 1)) ^ (q * d) ≤ ((L : ℝ) + 1) ^ (e + q * d) := - pow_le_pow_right₀ hLR1 (Nat.le_add_left _ _) - have he : (((L : ℝ) + 1)) ^ e ≤ ((L : ℝ) + 1) ^ (e + q * d) := - pow_le_pow_right₀ hLR1 (Nat.le_add_right _ _) - have houtR : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ - ((p + 1) ^ d : ℕ) * (2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by - have h1 : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ - ((p + 1) ^ d : ℕ) * ((L : ℝ) + 1) ^ (q * d) := by exact_mod_cast hout_pow - have h2 : ((L : ℝ) + 1) ^ (q * d) ≤ 2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d) := - hqd.trans (le_mul_of_one_le_left (by positivity) hX1) - exact h1.trans (mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg _)) - have htR : (t a : ℝ) ≤ (2 * c + 1 : ℕ) * (2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by - have hta := ht a - have h1 := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - have h2 := mul_le_mul_of_nonneg_left h1 (Nat.cast_nonneg c) - have h3 : (1 : ℝ) ≤ 2 ^ (δ * μ a) * ((L : ℝ) + 1) ^ (e + q * d) := - one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hLR1) - have h4 := mul_le_mul_of_nonneg_left h3 (Nat.cast_nonneg c) - push_cast - dsimp only [L] at * - linarith + have hx : 0 ≤ δ * μ a := by positivity + have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := e + q * d) hx + have ht' : (t a : ℝ) ≤ 2 * c * (2 ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ (e + q * d)) := + le_two_mul_mul_of_le_mul_add (ht a) (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega)) hX + have hout : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ + ((p + 1) ^ d : ℕ) * (((encIn a).length : ℝ) + 1) ^ (q * d) := by + exact_mod_cast Nat.add_one_pow_le_of_le_mul_pow (Nat.le_add_left 1 _) (hp a) d + have hq := mul_le_mul_of_nonneg_left (pow_le_two_rpow_mul_pow (L := (encIn a).length) + (d := q * d) (e := e + q * d) hx (by omega)) (Nat.cast_nonneg ((p + 1) ^ d) : (0 : ℝ) ≤ _) change ((t a + ((encMid (f a)).length + 1) ^ d : ℕ) : ℝ) ≤ _ - push_cast - dsimp only [L] at * - push_cast at htR houtR + push_cast at hout hq ⊢ linarith /-- Subexponential function computation with polynomially bounded output length transfers to @@ -323,13 +274,8 @@ theorem ComputableInExpTime.of_reduction {μA : α → ℕ} {μB : β → ℕ} { have hn : ((encMid (r a)).length : ℝ) ≤ l * (P + 1) := by dsimp only [P] exact_mod_cast hl a - have hexp : (2 : ℝ) ^ (δ * μB (r a)) ≤ 2 ^ (δ * c) * X := by - rw [← Real.rpow_add (by norm_num)] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - have : (μB (r a) : ℝ) ≤ c * μA a + c := by exact_mod_cast hμ a - nlinarith have hsum := reduction_add_time_le (C := (2 : ℝ) ^ (δ * c)) - hP hX (by positivity) hn hexp (ht (r a)) + hP hX (by positivity) hn (two_rpow_le_two_rpow_mul_of_le_mul_add hδ (hμ a)) (ht (r a)) change ((((encIn a).length + 1) ^ d + t (r a) : ℕ) : ℝ) ≤ _ push_cast rw [pow_mul] @@ -341,11 +287,9 @@ theorem ComputableInSubexpTime.of_reduction {μA : α → ℕ} {μB : β → ℕ (hr : ComputableInPolyTime r encIn encMid) {c : ℕ} (hμ : ∀ a, μB (r a) ≤ c * μA a + c) (hg : ComputableInSubexpTime g encMid encOut μB) : - ComputableInSubexpTime (g ∘ r) encIn encOut μA := by - intro δ hδ - refine ((hg (δ / (c + 1)) (by positivity)).of_reduction hr hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + ComputableInSubexpTime (g ∘ r) encIn encOut μA := fun δ hδ => + ((hg (δ / (c + 1)) (by positivity)).of_reduction hr hμ (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le c) end FunctionMachines diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean b/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean index 207286564d..c9dec4dc41 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean @@ -280,11 +280,9 @@ theorem SolvesPromiseInExpTime.mono_measure {Q : PromiseProblem α} {μ μ' : α /-- Subexponential deterministic promise solving transfers along linear parameter bounds. -/ theorem SolvesPromiseInSubexpTime.mono_measure {Q : PromiseProblem α} {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) (h : SolvesPromiseInSubexpTime Q enc μ) : - SolvesPromiseInSubexpTime Q enc μ' := by - intro δ hδ - refine ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + SolvesPromiseInSubexpTime Q enc μ' := fun δ hδ => + ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le c) /-- Transfer of `SolvesPromiseInExpTime` along a linear-parameter polynomial-time promise reduction. -/ @@ -307,12 +305,9 @@ theorem SolvesPromiseInSubexpTime.of_promiseReduction {X : PromiseProblem α} {Y (hyes : ∀ a ∈ X.yes, r a ∈ Y.yes) (hno : ∀ a ∈ X.no, r a ∈ Y.no) {c : ℕ} (hμ : ∀ a, μB (r a) ≤ c * μA a + c) (hY : SolvesPromiseInSubexpTime Y encB μB) : - SolvesPromiseInSubexpTime X enc μA := by - intro δ hδ - refine ((hY (δ / (c + 1)) (by positivity)).of_promiseReduction hr hyes hno hμ - (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + SolvesPromiseInSubexpTime X enc μA := fun δ hδ => + ((hY (δ / (c + 1)) (by positivity)).of_promiseReduction hr hyes hno hμ + (by positivity)).mono (natCast_mul_div_add_one_le hδ.le c) /-- On `PromiseProblem.ofSet A`, `SolvesPromiseInTimeO` agrees with `DecidableInTimeO`. -/ theorem solvesPromiseInTimeO_ofSet_iff {A : Set α} {T : α → ℝ} : @@ -418,14 +413,9 @@ theorem SolvesWithErrorInExpTime.mono {Q : PromiseProblem α} {E : ErrorModel} { {δ δ' : ℝ} (h : SolvesWithErrorInExpTime Q enc E μ δ) (hδ : δ ≤ δ') : SolvesWithErrorInExpTime Q enc E μ δ' := by obtain ⟨e, h⟩ := h - refine ⟨e, h.mono 1 (fun a => ?_) fun _ => by positivity⟩ - have h₁ : (2 : ℝ) ^ (δ * μ a) ≤ 2 ^ (δ' * μ a) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) - (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) - have h₂ := mul_le_mul_of_nonneg_right h₁ - (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e) - push_cast - linarith + exact ⟨e, h.mono 1 (fun a => (two_rpow_mul_pow_le_two_rpow_mul_pow + (mul_le_mul_of_nonneg_right hδ (Nat.cast_nonneg _)) le_rfl).trans (by simp)) + fun _ => by positivity⟩ /-- Relaxing the error bounds preserves `SolvesWithErrorInExpTime`. -/ theorem SolvesWithErrorInExpTime.mono_error {Q : PromiseProblem α} {E₁ E₂ : ErrorModel} @@ -437,24 +427,17 @@ theorem SolvesWithErrorInExpTime.mono_error {Q : PromiseProblem α} {E₁ E₂ : theorem SolvesWithErrorInExpTime.mono_measure {Q : PromiseProblem α} {E : ErrorModel} {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) {δ : ℝ} (hδ : 0 ≤ δ) (h : SolvesWithErrorInExpTime Q enc E μ δ) : - SolvesWithErrorInExpTime Q enc E μ' (c * δ) := by - obtain ⟨e, h⟩ := h - refine ⟨e, h.mono ⌈(2 : ℝ) ^ (δ * c)⌉₊ (fun a => ?_) fun _ => by positivity⟩ - have h₂ := two_rpow_le_natCeil_mul_of_le_mul_add hδ (hμ a) - have h₃ := mul_le_mul_of_nonneg_right h₂ - (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e) - have h₄ : (0 : ℝ) ≤ ⌈(2 : ℝ) ^ (δ * c)⌉₊ := Nat.cast_nonneg _ - nlinarith + SolvesWithErrorInExpTime Q enc E μ' (c * δ) := + let ⟨e, h⟩ := h + ⟨e, h.mono _ (fun a => two_rpow_mul_pow_le_natCeil_mul_add hδ (hμ a)) fun _ => by positivity⟩ /-- Subexponential randomized promise solving transfers along linear parameter bounds. -/ theorem SolvesWithErrorInSubexpTime.mono_measure {Q : PromiseProblem α} {E : ErrorModel} {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) (h : SolvesWithErrorInSubexpTime Q enc E μ) : - SolvesWithErrorInSubexpTime Q enc E μ' := by - intro δ hδ - refine ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + SolvesWithErrorInSubexpTime Q enc E μ' := fun δ hδ => + ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le c) private theorem computableInO_bool_not_linear : ComputableInO Bool.not encBool encBool (fun b => (encBool b).length) @@ -558,44 +541,22 @@ theorem solvesWithErrorInExpTime_deterministic_iff {Q : PromiseProblem α} {μ : (hδ : 0 ≤ δ) : SolvesWithErrorInExpTime Q enc ErrorModel.deterministic μ δ ↔ SolvesPromiseInExpTime Q enc μ δ := by - have hL_deg (e : ℕ) (he : 1 ≤ e) (a : α) : - ((enc a).length : ℝ) ≤ 2 ^ (δ * μ a) * ((enc a).length + 1) ^ e := by - have hL1 : (1 : ℝ) ≤ ((enc a).length : ℝ) + 1 := - le_add_of_nonneg_left (Nat.cast_nonneg _) - have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have hpow : ((enc a).length : ℝ) + 1 ≤ (((enc a).length : ℝ) + 1) ^ e := - le_self_pow₀ hL1 (by omega) - have hmul : (((enc a).length : ℝ) + 1) ^ e ≤ - 2 ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e := - le_mul_of_one_le_left (by positivity) hX1 - linarith [hpow.trans hmul] + have hL (e : ℕ) (a : α) : + ((enc a).length : ℝ) ≤ 2 ^ (δ * μ a) * ((enc a).length + 1) ^ (max e 1) := by + have := pow_le_two_rpow_mul_pow (L := (enc a).length) (d := 1) (e := max e 1) + (mul_nonneg hδ (Nat.cast_nonneg (μ a))) (le_max_right e 1) + rw [pow_one] at this + linarith + have hmax (e : ℕ) (a : α) : (2 : ℝ) ^ (δ * μ a) * ((enc a).length + 1) ^ e ≤ + ((1 : ℕ) : ℝ) * (2 ^ (δ * μ a) * ((enc a).length + 1) ^ (max e 1)) + ((1 : ℕ) : ℝ) := + (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (le_max_left e 1)).trans (by simp) constructor · rintro ⟨e, h⟩ - have h' : SolvesWithErrorInTimeO Q enc ErrorModel.deterministic - fun a => 2 ^ (δ * μ a) * ((enc a).length + 1) ^ (max e 1) := by - refine h.mono 1 (fun a => ?_) fun _ => by positivity - have hL1 : (1 : ℝ) ≤ ((enc a).length : ℝ) + 1 := - le_add_of_nonneg_left (Nat.cast_nonneg _) - have hpow : (((enc a).length : ℝ) + 1) ^ e ≤ - (((enc a).length : ℝ) + 1) ^ (max e 1) := pow_le_pow_right₀ hL1 (le_max_left e 1) - have hmul := mul_le_mul_of_nonneg_left hpow (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - push_cast - linarith - exact ⟨max e 1, (solvesWithErrorInTimeO_deterministic_iff - (hL_deg (max e 1) (le_max_right e 1))).mp h'⟩ + exact ⟨max e 1, (solvesWithErrorInTimeO_deterministic_iff (hL e)).mp + (h.mono 1 (hmax e) fun _ => by positivity)⟩ · rintro ⟨e, g, hQ, hg⟩ - have hg' : SolvesPromiseInTimeO Q enc - fun a => 2 ^ (δ * μ a) * ((enc a).length + 1) ^ (max e 1) := by - refine ⟨g, hQ, hg.mono 1 (fun a => ?_) fun _ => by positivity⟩ - have hL1 : (1 : ℝ) ≤ ((enc a).length : ℝ) + 1 := - le_add_of_nonneg_left (Nat.cast_nonneg _) - have hpow : (((enc a).length : ℝ) + 1) ^ e ≤ - (((enc a).length : ℝ) + 1) ^ (max e 1) := pow_le_pow_right₀ hL1 (le_max_left e 1) - have hmul := mul_le_mul_of_nonneg_left hpow (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - push_cast - linarith - exact ⟨max e 1, (solvesWithErrorInTimeO_deterministic_iff - (hL_deg (max e 1) (le_max_right e 1))).mpr hg'⟩ + exact ⟨max e 1, (solvesWithErrorInTimeO_deterministic_iff (hL e)).mpr + ⟨g, hQ, hg.mono 1 (hmax e) fun _ => by positivity⟩⟩ /-- Every deterministic `2 ^ (δ * μ a) · poly(L)` promise solver (`δ ≥ 0`) solves `Q` under any error profile `E`. -/ @@ -717,12 +678,9 @@ theorem SolvesWithErrorInSubexpTime.of_promiseReduction {X : PromiseProblem α} (hyes : ∀ a ∈ X.yes, r a ∈ Y.yes) (hno : ∀ a ∈ X.no, r a ∈ Y.no) {c : ℕ} (hμ : ∀ a, μB (r a) ≤ c * μA a + c) (hY : SolvesWithErrorInSubexpTime Y encB E μB) : - SolvesWithErrorInSubexpTime X enc E μA := by - intro δ hδ - refine ((hY (δ / (c + 1)) (by positivity)).of_promiseReduction hr hyes hno hμ - (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + SolvesWithErrorInSubexpTime X enc E μA := fun δ hδ => + ((hY (δ / (c + 1)) (by positivity)).of_promiseReduction hr hyes hno hμ + (by positivity)).mono (natCast_mul_div_add_one_le hδ.le c) /-! ### Bridges to `MultiTapePTM`, `PromiseBPP`, `PromiseRP`, and `PromiseCoRP` -/ diff --git a/CslibFrontier/Computability/Complexity/FineGrained/RatesNativeEndpoint.lean b/CslibFrontier/Computability/Complexity/FineGrained/RatesNativeEndpoint.lean index 546a7a7322..51822a3e1d 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/RatesNativeEndpoint.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/RatesNativeEndpoint.lean @@ -23,11 +23,12 @@ import CslibFrontier.Foundations.Data.Nat.Power /-! # Native model-counter consequences across counting, single-machine, randomized, and gap hypotheses -`CslibFrontier.Computability.Complexity.FineGrained.CountingExponents`, `SingleSubexp`, -`Randomized`, and `GapETH` develop the classical fine-grained rate, error-model, and reduction -hierarchy without importing `CountingNativeEndpoint`. Mirroring how `CountingNativeEndpoint` -instantiates `Exponents`, this leaf module connects `CountingNativeEndpoint.exists_declaredCounter` -and `CountingNativeEndpoint.exists_modelCounter` to those interfaces: +`CslibFrontier.Computability.Complexity.FineGrained.FunctionRates`, `CountingExponents`, +`SingleSubexp`, `Randomized`, and `GapETH` develop the classical fine-grained rate, error-model, +and reduction hierarchy without importing `CountingNativeEndpoint`. Mirroring how +`CountingNativeEndpoint` instantiates `Exponents`, this leaf module connects +`CountingNativeEndpoint.exists_declaredCounter` and `CountingNativeEndpoint.exists_modelCounter` to +those interfaces: 1. **Single-machine `2 ^ o(n)` counting and decision:** because `exists_declaredCounter` adapts its branching divisor dynamically with the declared variable count (`interpolationScale =o[atTop] diff --git a/manual/machines-and-classes/native-counting.md b/manual/machines-and-classes/native-counting.md index 688f296930..9b4d461f29 100644 --- a/manual/machines-and-classes/native-counting.md +++ b/manual/machines-and-classes/native-counting.md @@ -55,7 +55,7 @@ The library also retains [ETH-conditional Partial MCSP results](../circuits-logi ### Extended rates, single-machine bounds, randomized amplification, and Gap-ETH -Five classical modules develop the algorithmic transfer theorems, error models, and exponent inequalities without importing `CountingNativeEndpoint`, and a sixth leaf module connects the native declared/model counters to those interfaces. Their shared scalar estimates for measure rescaling and reduction-time composition live in [`Bounds`](../../CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean). +Five classical modules develop the algorithmic transfer theorems, error models, and exponent inequalities without importing `CountingNativeEndpoint`, and a sixth leaf module connects the native declared/model counters to those interfaces. Their shared scalar estimates for measure rescaling, exponential-times-polynomial envelopes `2 ^ x * (L + 1) ^ e`, and reduction-time composition live in [`Bounds`](../../CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean). - **Function rates** in [`FunctionRates`](../../CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean): `ComputableInTimeO`, `ComputableInExpTime`, and `ComputableInSubexpTime` parameterize function runtimes by `μ : α → ℕ` without constraining workspace length (`mem_FTIME_iff_computableInTimeO`). - **Counting rates (`#k-SAT`, `#ETH`, `#SETH`)** in [`CountingExponents`](../../CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean): `SharpKSAT k` (`SharpKSAT 3 = SharpThreeSAT`) has binary output length bounded linearly in `|encCNF φ|`, so counting rates transfer without exponent loss to decision rates (`satExponent k ≤ sharpSatExponent k ≤ 1`), infima over `δ ≥ 0` match infima over `δ > 0` (`satExponent_eq_sInf_pos`, `sharpSatExponent_eq_sInf_pos`), finite-prefix suprema characterize `SETH` and `SharpSETH` (`SETH_iff_iSup_ge_three_eq_one`, `SharpSETH_iff_iSup_ge_three_eq_one`), clause-splitting plus IPZ sparsification proves `SETH.eth` (`SETH → ETH`) without invoking native refutations, `unrestrictedSatExponent` distinguishes unbounded-width `SAT` from the supremum of `satExponent k` over fixed widths `k` (this supremum `≤ unrestrictedSatExponent ≤ 1`, and `SETH → unrestrictedSatExponent = 1`), and disjoint counting sparsification transfers clause-measured rates to variable-measured rates (`exists_computableInExpTime_SharpKSAT_numVars_of_length`, `SharpETH_iff_not_computableInSubexpTime_length`). From 26b0b01162dbfb99eb1526093935e4f277b44fdd Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 19:10:53 +0000 Subject: [PATCH 3/6] refactor(Complexity/FineGrained): absorb single-machine exponentials with the Bounds envelope lemmas Add two_rpow_mul_pow_le_natCeil_mul_add_of_le and use the envelope lemmas in SingleSubexp (subexp transfer, machine characterisations, mono_measure, ite_polyTime, polyBounded decision, SharpKSAT_length_of_numVars). --- .../Complexity/FineGrained/Bounds.lean | 18 +- .../Complexity/FineGrained/SingleSubexp.lean | 193 ++++++------------ 2 files changed, 80 insertions(+), 131 deletions(-) diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean b/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean index ff8dace1df..89f1169421 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean @@ -28,6 +28,8 @@ without mentioning a machine or error model. * `Cslib.Complexity.two_rpow_le_natCeil_mul_of_le_mul_add`, `Cslib.Complexity.two_rpow_mul_pow_le_natCeil_mul_add`: rescale an exponential rate, alone or in an envelope, under an additive linear parameter bound. +* `Cslib.Complexity.two_rpow_mul_pow_le_natCeil_mul_add_of_le`: replace the exponential factor of + an envelope by one that dominates it up to a constant factor. * `Cslib.Complexity.natCast_mul_div_add_one_le`: the rate rescaling `c * (δ / (c + 1)) ≤ δ` behind subexponential transfers. * `Cslib.Complexity.one_le_two_rpow_mul_pow`, @@ -95,16 +97,24 @@ theorem pow_le_two_rpow_mul_pow (hx : 0 ≤ x) (hde : d ≤ e) : (pow_le_pow_right₀ (le_add_of_nonneg_left (Nat.cast_nonneg L)) hde).trans (le_mul_of_one_le_left (by positivity) (Real.one_le_rpow (by norm_num) hx)) +/-- An exponential factor bounded by `K` times another one passes to the envelopes, with `K` +rounded up to a natural constant: the bound that `TimeO.mono` needs to replace one exponential +rate by another. -/ +theorem two_rpow_mul_pow_le_natCeil_mul_add_of_le {K : ℝ} (h : (2 : ℝ) ^ x ≤ K * 2 ^ y) : + (2 : ℝ) ^ x * ((L : ℝ) + 1) ^ e ≤ ⌈K⌉₊ * (2 ^ y * ((L : ℝ) + 1) ^ e) + ⌈K⌉₊ := by + rw [← mul_assoc] + exact le_add_of_le_of_nonneg (mul_le_mul_of_nonneg_right + (h.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity))) (by positivity)) + (Nat.cast_nonneg _) + /-- An additive linear bound on a natural parameter rescales an exponential-times-polynomial envelope at rate `δ ≥ 0` to one at rate `c * δ`, up to a natural ceiling constant: the bound that `TimeO.mono` needs to transfer an exponential runtime along the parameter change. -/ theorem two_rpow_mul_pow_le_natCeil_mul_add {δ : ℝ} {n m c : ℕ} (hδ : 0 ≤ δ) (hn : n ≤ c * m + c) : (2 : ℝ) ^ (δ * n) * ((L : ℝ) + 1) ^ e ≤ - ⌈(2 : ℝ) ^ (δ * c)⌉₊ * (2 ^ (c * δ * m) * ((L : ℝ) + 1) ^ e) + ⌈(2 : ℝ) ^ (δ * c)⌉₊ := by - rw [← mul_assoc] - exact le_add_of_le_of_nonneg (mul_le_mul_of_nonneg_right - (two_rpow_le_natCeil_mul_of_le_mul_add hδ hn) (by positivity)) (Nat.cast_nonneg _) + ⌈(2 : ℝ) ^ (δ * c)⌉₊ * (2 ^ (c * δ * m) * ((L : ℝ) + 1) ^ e) + ⌈(2 : ℝ) ^ (δ * c)⌉₊ := + two_rpow_mul_pow_le_natCeil_mul_add_of_le (two_rpow_le_two_rpow_mul_of_le_mul_add hδ hn) end Envelope diff --git a/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean b/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean index 8bd9b64d8d..ec27b6dbc0 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean @@ -164,13 +164,8 @@ theorem DecidableInSingleSubexpTime.decidableInSubexpTime {A : Set α} {enc : α obtain ⟨s, e, _, hs_o, hO⟩ := h intro δ hδ obtain ⟨K, _, hK⟩ := exists_two_pow_le_of_isLittleO hs_o hδ - refine ⟨e, hO.mono ⌈K⌉₊ (fun a => ?_) fun _ => by positivity⟩ - have h1 : (2 : ℝ) ^ s (μ a) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := - (hK (μ a)).trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity)) - have h2 := mul_le_mul_of_nonneg_right h1 - (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e) - have h3 : (0 : ℝ) ≤ ⌈K⌉₊ := Nat.cast_nonneg _ - nlinarith + exact ⟨e, hO.mono _ (fun a => two_rpow_mul_pow_le_natCeil_mul_add_of_le (hK (μ a))) + fun _ => by positivity⟩ /-- **Single-machine implies family subexponential function computation.** -/ theorem ComputableInSingleSubexpTime.computableInSubexpTime {f : α → β} @@ -180,13 +175,8 @@ theorem ComputableInSingleSubexpTime.computableInSubexpTime {f : α → β} obtain ⟨s, e, _, hs_o, hO⟩ := h intro δ hδ obtain ⟨K, _, hK⟩ := exists_two_pow_le_of_isLittleO hs_o hδ - refine ⟨e, hO.mono ⌈K⌉₊ (fun a => ?_) fun _ => by positivity⟩ - have h1 : (2 : ℝ) ^ s (μ a) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := - (hK (μ a)).trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity)) - have h2 := mul_le_mul_of_nonneg_right h1 - (by positivity : (0 : ℝ) ≤ (((encIn a).length : ℝ) + 1) ^ e) - have h3 : (0 : ℝ) ≤ ⌈K⌉₊ := Nat.cast_nonneg _ - nlinarith + exact ⟨e, hO.mono _ (fun a => two_rpow_mul_pow_le_natCeil_mul_add_of_le (hK (μ a))) + fun _ => by positivity⟩ /-! ### Quantifier-order characterization (`∃ (M, e), ∀ δ > 0, ∃ c`) -/ @@ -277,15 +267,12 @@ theorem decidableInSingleSubexpTime_iff_exists_machine {A : Set α} {enc : α refine ⟨t, sp, e, hdec, fun δ hδ => ?_⟩ obtain ⟨K, _, hK⟩ := exists_two_pow_le_of_isLittleO hs_o hδ refine ⟨c₀ * ⌈K⌉₊ + c₀, fun a => (ht a).trans ?_⟩ - have h1 : (2 : ℝ) ^ s (μ a) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := - (hK (μ a)).trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity)) - have h2 := mul_le_mul_of_nonneg_right h1 - (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e) - have h3 := mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg c₀) - have hpos : (0 : ℝ) ≤ (2 : ℝ) ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e := by positivity - have hc0 : (0 : ℝ) ≤ c₀ := Nat.cast_nonneg c₀ + have h := mul_le_mul_of_nonneg_left (two_rpow_mul_pow_le_natCeil_mul_add_of_le + (L := (enc a).length) (e := e) (hK (μ a))) (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) + have hpos := mul_nonneg (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) + (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e) push_cast - nlinarith + linarith · rintro ⟨t, sp, e, hdec, h⟩ obtain ⟨s, hnn, hs_o, hbound⟩ := exists_isLittleO_of_forall_exp_bound h refine ⟨s, e, hnn, hs_o, 1, t, sp, fun a => ?_, hdec⟩ @@ -307,15 +294,12 @@ theorem computableInSingleSubexpTime_iff_exists_machine {f : α → β} {encIn : refine ⟨t, sp, e, hcomp, fun δ hδ => ?_⟩ obtain ⟨K, _, hK⟩ := exists_two_pow_le_of_isLittleO hs_o hδ refine ⟨c₀ * ⌈K⌉₊ + c₀, fun a => (ht a).trans ?_⟩ - have h1 : (2 : ℝ) ^ s (μ a) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := - (hK (μ a)).trans (mul_le_mul_of_nonneg_right (Nat.le_ceil K) (by positivity)) - have h2 := mul_le_mul_of_nonneg_right h1 - (by positivity : (0 : ℝ) ≤ (((encIn a).length : ℝ) + 1) ^ e) - have h3 := mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg c₀) - have hpos : (0 : ℝ) ≤ (2 : ℝ) ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ e := by positivity - have hc0 : (0 : ℝ) ≤ c₀ := Nat.cast_nonneg c₀ + have h := mul_le_mul_of_nonneg_left (two_rpow_mul_pow_le_natCeil_mul_add_of_le + (L := (encIn a).length) (e := e) (hK (μ a))) (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) + have hpos := mul_nonneg (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) + (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ e) push_cast - nlinarith + linarith · rintro ⟨t, sp, e, hcomp, h⟩ obtain ⟨s, hnn, hs_o, hbound⟩ := exists_isLittleO_of_forall_exp_bound h refine ⟨s, e, hnn, hs_o, 1, t, sp, fun a => ?_, hcomp⟩ @@ -334,11 +318,8 @@ theorem DecidableInSingleSubexpTime.mono_measure {A : Set α} {enc : α ↪ List refine ⟨fun n => sBar (c * n + c), e, fun n => hnnBar _, isLittleO_comp_linear_of_nonneg hnnBar hsBar_o c c, hO.mono 1 (fun a => ?_) fun _ => by positivity⟩ - have h1 : s (μ a) ≤ sBar (c * μ' a + c) := (hle (μ a)).trans (hmono (hμ a)) - have h2 : (2 : ℝ) ^ s (μ a) ≤ 2 ^ sBar (c * μ' a + c) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) h1 - have h3 := mul_le_mul_of_nonneg_right h2 - (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e) + have h := two_rpow_mul_pow_le_two_rpow_mul_pow (L := (enc a).length) (d := e) (e := e) + ((hle (μ a)).trans (hmono (hμ a))) le_rfl push_cast linarith @@ -353,11 +334,8 @@ theorem ComputableInSingleSubexpTime.mono_measure {f : α → β} {encIn : α refine ⟨fun n => sBar (c * n + c), e, fun n => hnnBar _, isLittleO_comp_linear_of_nonneg hnnBar hsBar_o c c, hO.mono 1 (fun a => ?_) fun _ => by positivity⟩ - have h1 : s (μ a) ≤ sBar (c * μ' a + c) := (hle (μ a)).trans (hmono (hμ a)) - have h2 : (2 : ℝ) ^ s (μ a) ≤ 2 ^ sBar (c * μ' a + c) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) h1 - have h3 := mul_le_mul_of_nonneg_right h2 - (by positivity : (0 : ℝ) ≤ (((encIn a).length : ℝ) + 1) ^ e) + have h := two_rpow_mul_pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := e) (e := e) + ((hle (μ a)).trans (hmono (hμ a))) le_rfl push_cast linarith @@ -403,37 +381,26 @@ theorem ComputableInSingleSubexpTime.ite_polyTime {f g : α → β} {p : α → ⟨_, _, dp + dg + e, hcomb_ts, fun δ hδ => ?_⟩ obtain ⟨c, hc⟩ := hbound δ hδ refine ⟨c_comb * (2 * c + 4), fun a => ?_⟩ - set L : ℝ := ((encIn a).length : ℝ) - have hL1 : (1 : ℝ) ≤ L + 1 := by - dsimp only [L] - linarith [(Nat.cast_nonneg (encIn a).length : (0 : ℝ) ≤ _)] - have hX1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have hdp : (L + 1) ^ dp ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := - (pow_le_pow_right₀ hL1 (by omega)).trans (le_mul_of_one_le_left (by positivity) hX1) - have hdg : (L + 1) ^ dg ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := - (pow_le_pow_right₀ hL1 (by omega)).trans (le_mul_of_one_le_left (by positivity) hX1) - have he : (L + 1) ^ e ≤ (L + 1) ^ (dp + dg + e) := pow_le_pow_right₀ hL1 (by omega) - have hc0 : (0 : ℝ) ≤ c := Nat.cast_nonneg c - have hcc0 : (0 : ℝ) ≤ c_comb := Nat.cast_nonneg c_comb - have hpos : (0 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := by positivity - have ht_le : (t a : ℝ) ≤ (2 * c + 1) * (2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e)) := by - have hmul := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a)) - have hmulc := mul_le_mul_of_nonneg_left hmul hc0 - have hc1 : (c : ℝ) ≤ c * (2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e)) := - le_mul_of_one_le_right hc0 (one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hL1)) - dsimp only [L] at * - nlinarith [hc a] - have h1 : (1 : ℝ) ≤ 2 ^ (δ * μ a) * (L + 1) ^ (dp + dg + e) := - one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hL1) + have hx : 0 ≤ δ * μ a := by positivity + have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := dp + dg + e) hx + have ht := le_two_mul_mul_of_le_mul_add (hc a) + (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega : e ≤ dp + dg + e)) hX + have hdp := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dp) (e := dp + dg + e) hx + (by omega) + have hdg := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dg) (e := dp + dg + e) hx + (by omega) + have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) + -- the guarded runtime is at most `(2 * c + 4)` envelopes, in either branch + have hsum : ((((encIn a).length + 1) ^ dp + + if p a then t a else ((encIn a).length + 1) ^ dg) + 1 : ℕ) ≤ + (2 * c + 4) * (2 ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ (dp + dg + e)) := by + split_ifs <;> push_cast <;> linarith + have hmul := mul_le_mul_of_nonneg_left hsum (Nat.cast_nonneg c_comb : (0 : ℝ) ≤ c_comb) + have hpos : (0 : ℝ) ≤ (c_comb * (2 * c + 4) : ℕ) := Nat.cast_nonneg _ change ((c_comb * ((((encIn a).length + 1) ^ dp + if p a then t a else ((encIn a).length + 1) ^ dg) + 1) : ℕ) : ℝ) ≤ _ - split_ifs - · push_cast - dsimp only [L] at * - nlinarith - · push_cast - dsimp only [L] at * - nlinarith + push_cast at hmul hpos ⊢ + linarith /-- **Single-machine decision from function computation.** Composing a single-machine subexponential function of polynomially bounded output length with a polynomial-time test yields a @@ -451,43 +418,25 @@ theorem DecidableInSingleSubexpTime.of_computableInSingleSubexpTime_polyBounded obtain ⟨c_comp, hcomp_ts, -⟩ := htest'.inO.comp hfO refine ⟨s, e + q * d, hnn, hs_o, c_comp * (2 * c + 2 + (p + 1) ^ d), _, _, fun a => ?_, decidableInTimeAndSpace_iff.mpr ⟨test ∘ f, hcomp_ts, fun _ => Iff.rfl⟩⟩ - set L : ℕ := (encIn a).length - have hL1 : 1 ≤ L + 1 := Nat.le_add_left 1 L - have hLR1 : (1 : ℝ) ≤ (L : ℝ) + 1 := by exact_mod_cast hL1 - have hX1 : (1 : ℝ) ≤ 2 ^ s (μ a) := Real.one_le_rpow (by norm_num) (hnn (μ a)) - have hout_pow : ((encMid (f a)).length + 1) ^ d ≤ (p + 1) ^ d * (L + 1) ^ (q * d) := - Nat.add_one_pow_le_of_le_mul_pow hL1 (hp a) d - have hqd : ((L : ℝ) + 1) ^ (q * d) ≤ ((L : ℝ) + 1) ^ (e + q * d) := - pow_le_pow_right₀ hLR1 (Nat.le_add_left _ _) - have he : ((L : ℝ) + 1) ^ e ≤ ((L : ℝ) + 1) ^ (e + q * d) := - pow_le_pow_right₀ hLR1 (Nat.le_add_right _ _) - have houtR : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ - ((p + 1) ^ d : ℕ) * (2 ^ s (μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by - have h1 : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ - ((p + 1) ^ d : ℕ) * ((L : ℝ) + 1) ^ (q * d) := by exact_mod_cast hout_pow - have h2 : ((L : ℝ) + 1) ^ (q * d) ≤ 2 ^ s (μ a) * ((L : ℝ) + 1) ^ (e + q * d) := - hqd.trans (le_mul_of_one_le_left (by positivity) hX1) - exact h1.trans (mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg _)) - have htR : (t a : ℝ) ≤ (2 * c + 1 : ℕ) * (2 ^ s (μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by - have h1 := mul_le_mul_of_nonneg_left he (by positivity : (0 : ℝ) ≤ 2 ^ s (μ a)) - have h2 := mul_le_mul_of_nonneg_left h1 (Nat.cast_nonneg c) - have h3 : (1 : ℝ) ≤ 2 ^ s (μ a) * ((L : ℝ) + 1) ^ (e + q * d) := - one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hLR1) - have h4 := mul_le_mul_of_nonneg_left h3 (Nat.cast_nonneg c) - push_cast - dsimp only [L] at * - linarith [ht a] - have h1 : (1 : ℝ) ≤ 2 ^ s (μ a) * ((L : ℝ) + 1) ^ (e + q * d) := - one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hLR1) - have hsum : (t a : ℝ) + (((encMid (f a)).length : ℝ) + 1) ^ d + 1 ≤ - (2 * c + 2 + (p + 1) ^ d : ℕ) * (2 ^ s (μ a) * ((L : ℝ) + 1) ^ (e + q * d)) := by - push_cast at htR houtR ⊢ + have hx : 0 ≤ s (μ a) := hnn (μ a) + have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := e + q * d) hx + have ht' : (t a : ℝ) ≤ 2 * c * (2 ^ s (μ a) * (((encIn a).length : ℝ) + 1) ^ (e + q * d)) := + le_two_mul_mul_of_le_mul_add (ht a) (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega)) hX + have hout : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ + ((p + 1) ^ d : ℕ) * (((encIn a).length : ℝ) + 1) ^ (q * d) := by + exact_mod_cast Nat.add_one_pow_le_of_le_mul_pow (Nat.le_add_left 1 _) (hp a) d + have hq := mul_le_mul_of_nonneg_left (pow_le_two_rpow_mul_pow (L := (encIn a).length) + (d := q * d) (e := e + q * d) hx (by omega)) (Nat.cast_nonneg ((p + 1) ^ d) : (0 : ℝ) ≤ _) + -- the composed runtime is at most `2 * c + 2 + (p + 1) ^ d` envelopes + have hsum : ((t a + ((encMid (f a)).length + 1) ^ d + 1 : ℕ) : ℝ) ≤ + (2 * c + 2 + (p + 1) ^ d : ℕ) * + (2 ^ s (μ a) * (((encIn a).length : ℝ) + 1) ^ (e + q * d)) := by + push_cast at hout hq ⊢ linarith - have hmul := mul_le_mul_of_nonneg_left hsum (Nat.cast_nonneg c_comp) - have hnonneg : (0 : ℝ) ≤ (c_comp * (2 * c + 2 + (p + 1) ^ d) : ℕ) := Nat.cast_nonneg _ + have hmul := mul_le_mul_of_nonneg_left hsum (Nat.cast_nonneg c_comp : (0 : ℝ) ≤ c_comp) + have hpos : (0 : ℝ) ≤ (c_comp * (2 * c + 2 + (p + 1) ^ d) : ℕ) := Nat.cast_nonneg _ change ((c_comp * ((t a + ((encMid (f a)).length + 1) ^ d) + 1) : ℕ) : ℝ) ≤ _ - push_cast at hmul hnonneg ⊢ - dsimp only [L] at * + push_cast at hmul hpos ⊢ linarith /-- **Transfer along linear-parameter parsimonious reductions (`SingleSubexp`).** -/ @@ -761,35 +710,25 @@ theorem ComputableInSingleSubexpTime.SharpKSAT_length_of_numVars {k : ℕ} isLittleO_comp_linear_of_nonneg hnnBar hsBar_o k 0, (ComputableInTimeO.of_computableInO hite fun _ => le_rfl).mono (2 * c + 3) (fun φ => ?_) fun _ => by positivity⟩ - set L : ℝ := ((encCNF φ).length : ℝ) - have hL1 : (1 : ℝ) ≤ L + 1 := by - dsimp only [L] - linarith [(Nat.cast_nonneg (encCNF φ).length : (0 : ℝ) ≤ _)] - have hX1 : (1 : ℝ) ≤ 2 ^ s' φ.length := Real.one_le_rpow (by norm_num) (hnnBar _) - have hdw : (L + 1) ^ dw ≤ 2 ^ s' φ.length * (L + 1) ^ (dw + dc + e) := - (pow_le_pow_right₀ hL1 (by omega)).trans (le_mul_of_one_le_left (by positivity) hX1) - have hdc : (L + 1) ^ dc ≤ 2 ^ s' φ.length * (L + 1) ^ (dw + dc + e) := - (pow_le_pow_right₀ hL1 (by omega)).trans (le_mul_of_one_le_left (by positivity) hX1) - have he : (L + 1) ^ e ≤ (L + 1) ^ (dw + dc + e) := pow_le_pow_right₀ hL1 (by omega) - have hc_nn : (0 : ℝ) ≤ c := Nat.cast_nonneg c - have hpos : (0 : ℝ) ≤ 2 ^ s' φ.length * (L + 1) ^ (dw + dc + e) := by positivity + have hx : 0 ≤ s' φ.length := hnnBar _ + have hX := one_le_two_rpow_mul_pow (L := (encCNF φ).length) (e := dw + dc + e) hx + have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) + have hdw := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dw) (e := dw + dc + e) hx + (by omega) + have hdc := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dc) (e := dw + dc + e) hx + (by omega) change ((((encCNF φ).length + 1) ^ dw + if φ.all (fun cl => decide (cl.length ≤ k)) then t φ else ((encCNF φ).length + 1) ^ dc : ℕ) : ℝ) ≤ _ split_ifs with hφ · simp only [List.all_eq_true, decide_eq_true_eq] at hφ - have hexp : (2 : ℝ) ^ s φ.numVars ≤ 2 ^ s' φ.length := by - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - exact (hle _).trans (hmono (by simpa only [Nat.add_zero] using CNF.numVars_le_mul_length hφ)) - have hmul := mul_le_mul hexp he (by positivity) (by positivity) - have hmulc := mul_le_mul_of_nonneg_left hmul hc_nn - have hc1 : (c : ℝ) ≤ c * (2 ^ s' φ.length * (L + 1) ^ (dw + dc + e)) := - le_mul_of_one_le_right hc_nn (one_le_mul_of_one_le_of_one_le hX1 (one_le_pow₀ hL1)) + have hexp : s φ.numVars ≤ s' φ.length := + (hle _).trans (hmono (by simpa only [Nat.add_zero] using CNF.numVars_le_mul_length hφ)) + have ht' := le_two_mul_mul_of_le_mul_add (ht φ) + (two_rpow_mul_pow_le_two_rpow_mul_pow hexp (by omega)) hX push_cast - dsimp only [L] at * - nlinarith [ht φ] + linarith · push_cast - dsimp only [L] at * - nlinarith + linarith end Cslib.Complexity From 92cc59391c35072aba999a9ee9da75a8dd91a5b5 Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 19:36:54 +0000 Subject: [PATCH 4/6] refactor(Complexity/FineGrained): finish the Bounds migration in Reduction, Sparsification, ExhaustiveSearch and Randomized Use two_rpow_mul_pow_le_natCeil_mul_add, two_rpow_le_two_rpow_mul_of_le_mul_add and natCast_mul_div_add_one_le for the remaining inline copies; list two_rpow_le_two_rpow_mul_of_le_mul_add in the Bounds main results. --- .../Complexity/FineGrained/Bounds.lean | 3 +- .../FineGrained/ExhaustiveSearch.lean | 5 +-- .../Complexity/FineGrained/Randomized.lean | 7 +--- .../Complexity/FineGrained/Reduction.lean | 38 ++++++------------- .../FineGrained/Sparsification.lean | 6 +-- 5 files changed, 20 insertions(+), 39 deletions(-) diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean b/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean index 89f1169421..b28a275084 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Bounds.lean @@ -25,7 +25,8 @@ without mentioning a machine or error model. ## Main results -* `Cslib.Complexity.two_rpow_le_natCeil_mul_of_le_mul_add`, +* `Cslib.Complexity.two_rpow_le_two_rpow_mul_of_le_mul_add`, + `Cslib.Complexity.two_rpow_le_natCeil_mul_of_le_mul_add`, `Cslib.Complexity.two_rpow_mul_pow_le_natCeil_mul_add`: rescale an exponential rate, alone or in an envelope, under an additive linear parameter bound. * `Cslib.Complexity.two_rpow_mul_pow_le_natCeil_mul_add_of_le`: replace the exponential factor of diff --git a/CslibFrontier/Computability/Complexity/FineGrained/ExhaustiveSearch.lean b/CslibFrontier/Computability/Complexity/FineGrained/ExhaustiveSearch.lean index 7d02ccafee..4eaa3e0fb2 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/ExhaustiveSearch.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/ExhaustiveSearch.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import CslibFrontier.Computability.Complexity.FineGrained +import CslibFrontier.Computability.Complexity.FineGrained.Bounds import CslibFrontier.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds @@ -349,9 +350,7 @@ theorem DecidableInSubexpTime.of_exhaustiveSearch {f : α × ℕ → β} {ν : have hδ : 0 < δ := by positivity refine ((h δ hδ).of_exhaustiveSearch hf hν hfA hμ hK hδ.le).mono ?_ have hcδ : (c : ℝ) * δ ≤ ε / 2 := by - simp only [δ] - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + simpa only [δ, div_div] using natCast_mul_div_add_one_le (half_pos hε).le c linarith end Cslib.Complexity diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean b/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean index c9dec4dc41..0d31cf65fb 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Randomized.lean @@ -599,11 +599,8 @@ theorem SolvesWithErrorInExpTime.of_promiseReduction {X : PromiseProblem α} {Y have hn0 : ((encB (r a)).length : ℝ) ≤ l * ((((enc a).length : ℝ) + 1) ^ d + 1) := by exact_mod_cast hl a nlinarith [(Nat.cast_nonneg l : (0 : ℝ) ≤ l)] - have hexp : (2 : ℝ) ^ (δ * μB (r a)) ≤ 2 ^ (δ * c) * X := by - rw [← Real.rpow_add (by norm_num)] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - have : (μB (r a) : ℝ) ≤ c * μA a + c := by exact_mod_cast hμ a - nlinarith + have hexp : (2 : ℝ) ^ (δ * μB (r a)) ≤ 2 ^ (δ * c) * X := + two_rpow_le_two_rpow_mul_of_le_mul_add hδ (hμ a) have hpow : (((encB (r a)).length : ℝ) + 1) ^ e ≤ (2 * l + 1) ^ e * P ^ e := by rw [← mul_pow] exact pow_le_pow_left₀ (by positivity) (by nlinarith) e diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Reduction.lean b/CslibFrontier/Computability/Complexity/FineGrained/Reduction.lean index 564f7caf97..a640132d5e 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Reduction.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Reduction.lean @@ -81,23 +81,16 @@ variable {α : Type*} {enc : α ↪ List Bool} {A : Set α} {μ μ' : α → ℕ /-- A decider within time `2 ^ (δ * μ a)` times a polynomial, for a measure `μ ≤ c * μ' + c`, decides within time `2 ^ (c * δ * μ' a)` times a polynomial. -/ theorem DecidableInExpTime.mono_measure {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) {δ : ℝ} - (hδ : 0 ≤ δ) (h : DecidableInExpTime A enc μ δ) : DecidableInExpTime A enc μ' (c * δ) := by - obtain ⟨e, h⟩ := h - refine ⟨e, h.mono ⌈(2 : ℝ) ^ (δ * c)⌉₊ (fun a => ?_) fun a => by positivity⟩ - have h₂ := two_rpow_le_natCeil_mul_of_le_mul_add hδ (hμ a) - have h₃ := mul_le_mul_of_nonneg_right h₂ (by positivity : - (0 : ℝ) ≤ ((enc a).length + 1) ^ e) - have h₄ : (0 : ℝ) ≤ ⌈(2 : ℝ) ^ (δ * c)⌉₊ := Nat.cast_nonneg _ - nlinarith + (hδ : 0 ≤ δ) (h : DecidableInExpTime A enc μ δ) : DecidableInExpTime A enc μ' (c * δ) := + let ⟨e, h⟩ := h + ⟨e, h.mono _ (fun a => two_rpow_mul_pow_le_natCeil_mul_add hδ (hμ a)) fun a => by positivity⟩ /-- Subexponential time in a measure `μ ≤ c * μ' + c` gives subexponential time in `μ'`. So a lower bound for `μ'` gives the lower bound for `μ`. -/ theorem DecidableInSubexpTime.mono_measure {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) - (h : DecidableInSubexpTime A enc μ) : DecidableInSubexpTime A enc μ' := by - intro δ hδ - refine ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + (h : DecidableInSubexpTime A enc μ) : DecidableInSubexpTime A enc μ' := fun δ hδ => + ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le c) end Measure @@ -123,11 +116,8 @@ theorem DecidableInExpTime.of_reduction {f : α → β} -- run the reduction, then the decider on its output refine DecidableInExpTime.of_computableInO (hg.comp hf.inO) (fun a => (hfA a).trans (hgB (f a))) ⌈(1 + k * 2 ^ (δ * c) * (2 * l + 1) ^ e + k : ℝ)⌉₊ (d * (e + 1)) fun a => ?_ - have hexp : (2 : ℝ) ^ (δ * μB (f a)) ≤ 2 ^ (δ * c) * 2 ^ (c * δ * μA a) := by - rw [← Real.rpow_add (by norm_num)] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - have : (μB (f a) : ℝ) ≤ c * μA a + c := by exact_mod_cast hμ a - nlinarith + have hexp : (2 : ℝ) ^ (δ * μB (f a)) ≤ 2 ^ (δ * c) * 2 ^ (c * δ * μA a) := + two_rpow_le_two_rpow_mul_of_le_mul_add hδ (hμ a) have key := reduction_add_time_le (P := ((encA a).length + 1 : ℝ) ^ d) (C := (2 : ℝ) ^ (δ * c)) (one_le_pow₀ (le_add_of_nonneg_left (Nat.cast_nonneg _))) @@ -143,11 +133,9 @@ decidable in subexponential time in `μA`. -/ theorem DecidableInSubexpTime.of_reduction {f : α → β} (hf : ComputableInPolyTime f encA encB) (hfA : ∀ a, a ∈ A ↔ f a ∈ B) {c : ℕ} (hμ : ∀ a, μB (f a) ≤ c * μA a + c) (h : DecidableInSubexpTime B encB μB) : - DecidableInSubexpTime A encA μA := by - intro δ hδ - refine ((h (δ / (c + 1)) (by positivity)).of_reduction hf hfA hμ (by positivity)).mono ?_ - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + DecidableInSubexpTime A encA μA := fun δ hδ => + ((h (δ / (c + 1)) (by positivity)).of_reduction hf hfA hμ (by positivity)).mono + (natCast_mul_div_add_one_le hδ.le c) /-- **Lower bounds from the exponential time hypothesis** [ImpagliazzoPaturiZane2001] [CyganEtAl2015, Chapter 14]. Under `ETH`, if `f` is computable in polynomial time and, on formulas @@ -254,9 +242,7 @@ theorem DecidableInSubexpTime.of_expReduction {f : α → β} {m : α → ℕ} rfl have hexp : (2 : ℝ) ^ (δ * μB (f a)) ≤ 2 ^ (δ * c) * X₁ := by have hcδ : (c : ℝ) * δ ≤ ε / 2 := by - simp only [δ] - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + simpa only [δ, div_div] using natCast_mul_div_add_one_le (half_pos hε).le c rw [← Real.rpow_add (by norm_num)] refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ have hμ' : (μB (f a) : ℝ) ≤ c * (m a * Nat.log 2 (m a) : ℕ) + c := by diff --git a/CslibFrontier/Computability/Complexity/FineGrained/Sparsification.lean b/CslibFrontier/Computability/Complexity/FineGrained/Sparsification.lean index 024c534875..d885de1c43 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/Sparsification.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/Sparsification.lean @@ -11,6 +11,7 @@ public import CslibFrontier.Computability.Complexity.FineGrained.Exponents public import CslibFrontier.Computability.Complexity.FineGrained.SparsificationRounds public import CslibFrontier.Logics.Propositional.ClauseSet.Sparsification.Tree public import CslibFrontier.Logics.Propositional.ClauseSet.Sparsification.PolyTime +import CslibFrontier.Computability.Complexity.FineGrained.Bounds import CslibFrontier.Computability.Complexity.Problems.SAT.PolyTime import CslibFrontier.Foundations.Data.List.Fold import CslibFrontier.Foundations.Data.Nat.Power @@ -762,10 +763,7 @@ theorem DecidableInSubexpTime.numVars_of_length {k : ℕ} obtain ⟨c, hc⟩ := exists_decidableInExpTime_numVars_of_length k (half_pos hδ) have hδ' : 0 < δ / 2 / (c + 1) := by positivity refine (hc _ hδ'.le (h _ hδ')).mono ?_ - have hc0 : (0 : ℝ) ≤ c := Nat.cast_nonneg c - have : (c : ℝ) * (δ / 2 / (c + 1)) ≤ δ / 2 := by - rw [mul_div_assoc', div_le_iff₀ (by positivity)] - nlinarith + have h := natCast_mul_div_add_one_le (half_pos hδ).le c linarith /-- **The exponential time hypothesis in terms of clauses** [ImpagliazzoPaturiZane2001]: `ETH` From c388f02567bf32b2dfe5bca7fc39c72d0dad2930 Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 20:09:24 +0000 Subject: [PATCH 5/6] refactor(Complexity/FineGrained): share guarded and polyBounded rate bounds across exponent towers Prove ComputableInTimeO.ite_polyTime_of_le and DecidableInTimeO.of_computableInTimeO_polyBounded once for an arbitrary nonnegative exponent x, and derive the ExpTime and single-machine subexponential versions (ite_polyTime, of_*_polyBounded, SharpKSAT_length_of_numVars) from them. Add ite_all_length_le_SharpKSAT for the #k-SAT width guard. Shorten the CountingEndpoint interpolationScale bridges with the Bounds absorption lemma and derive exists_two_pow_mul_interpolationScale_le from exists_two_pow_le_of_isLittleO. Part of #4737. --- .../FineGrained/CountingEndpoint.lean | 34 +----- .../FineGrained/CountingExponents.lean | 62 ++++------- .../Complexity/FineGrained/CountingScale.lean | 23 +--- .../Complexity/FineGrained/FunctionRates.lean | 101 +++++++++++------ .../Complexity/FineGrained/SingleSubexp.lean | 105 +++--------------- 5 files changed, 112 insertions(+), 213 deletions(-) diff --git a/CslibFrontier/Computability/Complexity/FineGrained/CountingEndpoint.lean b/CslibFrontier/Computability/Complexity/FineGrained/CountingEndpoint.lean index 5b53527ab0..e2327dc516 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/CountingEndpoint.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/CountingEndpoint.lean @@ -10,6 +10,7 @@ module public import CslibFrontier.Computability.Complexity.FineGrained.CountingScale public import CslibFrontier.Computability.Complexity.FineGrained.Reduction public import CslibFrontier.Logics.Propositional.CNF.ModelCount.DenseRelabel +import CslibFrontier.Computability.Complexity.FineGrained.Bounds import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary @@ -105,13 +106,8 @@ theorem DecidableInSubexpTime.of_interpolationScale {α : Type} {enc : α ↪ Li DecidableInSubexpTime A enc μ := by intro δ hδ obtain ⟨K, _, hK⟩ := exists_two_pow_mul_interpolationScale_le A₀ hδ - refine ⟨d, h.mono ⌈K⌉₊ (fun a => ?_) fun a => by positivity⟩ - have hceil : K ≤ ⌈K⌉₊ := Nat.le_ceil K - have h1 : (2 : ℝ) ^ (A₀ * interpolationScale (μ a)) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := - (hK (μ a)).trans (mul_le_mul_of_nonneg_right hceil (by positivity)) - have h2 := mul_le_mul_of_nonneg_right h1 - (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ d) - linarith + exact ⟨d, h.mono _ (fun a => two_rpow_mul_pow_le_natCeil_mul_add_of_le (hK (μ a))) + fun _ => by positivity⟩ /-- If `f : α → Bool` decides `A` in `ComputableInO` time bounded by `c * (2 ^ (A₀ * interpolationScale (μ a)) * (|enc a| + 1) ^ e) + c`, then `A` is decidable in @@ -122,27 +118,9 @@ theorem DecidableInSubexpTime.of_computableInO_interpolationScale {α : Type} {e {A₀ : ℝ} {c e : ℕ} (ht : ∀ a, (t a : ℝ) ≤ c * ((2 : ℝ) ^ (A₀ * interpolationScale (μ a)) * (((enc a).length : ℝ) + 1) ^ e) + c) : - DecidableInSubexpTime A enc μ := by - intro δ hδ - obtain ⟨K, _, hK⟩ := exists_two_pow_mul_interpolationScale_le A₀ hδ - refine DecidableInExpTime.of_computableInO hf hfA (c * ⌈K⌉₊ + c) e fun a => ?_ - refine (ht a).trans ?_ - have hceil : K ≤ ⌈K⌉₊ := Nat.le_ceil K - have hX1 : (1 : ℝ) ≤ (2 : ℝ) ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) - have hP1 : (1 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e := - one_le_pow₀ (by linarith [(Nat.cast_nonneg (enc a).length : (0 : ℝ) ≤ _)]) - have hXP1 : (1 : ℝ) ≤ (2 : ℝ) ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e := - one_le_mul_of_one_le_of_one_le hX1 hP1 - have hcXP : (c : ℝ) ≤ (c : ℝ) * ((2 : ℝ) ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e) := - le_mul_of_one_le_right (Nat.cast_nonneg c) hXP1 - have h1 : (2 : ℝ) ^ (A₀ * interpolationScale (μ a)) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := - (hK (μ a)).trans (mul_le_mul_of_nonneg_right hceil (by positivity)) - have h2 := mul_le_mul_of_nonneg_right h1 - (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e) - rw [mul_assoc] at h2 - have h3 := mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg c) - push_cast - linarith + DecidableInSubexpTime A enc μ := + DecidableInSubexpTime.of_interpolationScale + ((DecidableInTimeO.of_computableInO hf hfA fun _ => le_rfl).mono c ht fun _ => by positivity) /-! ### From dense-variable model counting to `DecidableInSubexpTime (KSAT k)` -/ diff --git a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean index 894f0083ca..31ce21f4f2 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean @@ -140,6 +140,16 @@ theorem SharpKSAT_of_not_width {k : ℕ} {φ : CNF ℕ} (h : ¬∀ c ∈ φ, c.l exact fun hall => h fun c hc => decide_eq_true_eq.mp (hall c hc) simp only [SharpKSAT, hw, Bool.false_eq_true, ↓reduceIte] +/-- Guarding a `#k'-SAT` count by the width test of `k ≤ k'` gives the `#k-SAT` count. -/ +theorem ite_all_length_le_SharpKSAT {k k' : ℕ} (hk : k ≤ k') (φ : CNF ℕ) : + (if φ.all (fun c => decide (c.length ≤ k)) then SharpKSAT k' φ else 0) = SharpKSAT k φ := by + unfold SharpKSAT + split_ifs with h₁ h₂ + · rfl + · simp only [List.all_eq_true, decide_eq_true_eq] at h₁ h₂ + exact absurd (fun c hc => (h₁ c hc).trans hk) h₂ + · rfl + /-- The binary encoding of `SharpSAT φ` has length bounded linearly in `(encCNF φ).length`. -/ theorem polyBounded_length_encNat_SharpSAT : PolyBounded (fun φ : CNF ℕ => (encCNF φ).length) (fun φ => (encNat (SharpSAT φ)).length) := by @@ -398,18 +408,8 @@ theorem DecidableInSubexpTime.KSAT_of_SharpKSAT {k : ℕ} theorem ComputableInExpTime.SharpKSAT_of_le {k k' : ℕ} (hk : k ≤ k') {δ : ℝ} (hδ : 0 ≤ δ) (h : ComputableInExpTime (SharpKSAT k') encCNF encNat CNF.numVars δ) : ComputableInExpTime (SharpKSAT k) encCNF encNat CNF.numVars δ := by - have hite := h.ite_polyTime hδ (computableInPolyTime_all_length_le k) - (ComputableInPolyTime.const 0) - have heq : (fun φ : CNF ℕ => if φ.all (fun c => decide (c.length ≤ k)) then SharpKSAT k' φ - else 0) = SharpKSAT k := by - funext φ - unfold SharpKSAT - split_ifs with h₁ h₂ - · rfl - · simp only [List.all_eq_true, decide_eq_true_eq] at h₁ h₂ - exact absurd (fun c hc => (h₁ c hc).trans hk) h₂ - · rfl - rwa [heq] at hite + simpa only [ite_all_length_le_SharpKSAT hk] using + h.ite_polyTime hδ (computableInPolyTime_all_length_le k) (ComputableInPolyTime.const 0) /-! ### The `#k-SAT` exponent `sharpSatExponent`, `SharpETH`, and `SharpSETH` -/ @@ -695,34 +695,16 @@ at most `k * m` variables, a `#k-SAT` counter at variable rate `δ ≥ 0` runs a theorem ComputableInExpTime.SharpKSAT_length_of_numVars {k : ℕ} {δ : ℝ} (hδ : 0 ≤ δ) (h : ComputableInExpTime (SharpKSAT k) encCNF encNat CNF.numVars δ) : ComputableInExpTime (SharpKSAT k) encCNF encNat List.length (k * δ) := by - obtain ⟨e, h⟩ := h - obtain ⟨t, c, hO, ht⟩ := h.exists_computableInO - obtain ⟨dw, _, hw⟩ := (computableInPolyTime_all_length_le k).exists_degree - obtain ⟨dc, _, hc0⟩ := (ComputableInPolyTime.const (encIn := encCNF) (0 : ℕ)).exists_degree - have hite := (hw.inO.ite hO hc0.inO).of_enc_eq (g := SharpKSAT k) fun φ => congrArg encNat <| by - split_ifs with hφ - · simp only [SharpKSAT, hφ, ↓reduceIte] - · simp only [SharpKSAT, hφ, Bool.false_eq_true, ↓reduceIte] - refine ComputableInExpTime.of_computableInO hite (2 * c + 3) (dw + dc + e) fun φ => ?_ - have hx : 0 ≤ k * δ * φ.length := by positivity - have hX := one_le_two_rpow_mul_pow (L := (encCNF φ).length) (e := dw + dc + e) hx - have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) - have hdw := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dw) (e := dw + dc + e) hx - (by omega) - have hdc := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dc) (e := dw + dc + e) hx - (by omega) - change ((((encCNF φ).length + 1) ^ dw + - if φ.all (fun cl => decide (cl.length ≤ k)) then t φ - else ((encCNF φ).length + 1) ^ dc : ℕ) : ℝ) ≤ _ - split_ifs with hφ - · simp only [List.all_eq_true, decide_eq_true_eq] at hφ - have hn : (φ.numVars : ℝ) ≤ k * φ.length := by exact_mod_cast CNF.numVars_le_mul_length hφ - have ht' := le_two_mul_mul_of_le_mul_add (ht φ) - (two_rpow_mul_pow_le_two_rpow_mul_pow (by nlinarith) (by omega)) hX - push_cast - linarith - · push_cast - linarith + obtain ⟨_, h⟩ := h + obtain ⟨e', hite⟩ := h.ite_polyTime_of_le (computableInPolyTime_all_length_le k) + (ComputableInPolyTime.const 0) (y := fun φ => k * δ * φ.length) + (fun φ => mul_nonneg (mul_nonneg (Nat.cast_nonneg k) hδ) (Nat.cast_nonneg _)) fun φ hφ => by + have hn : (φ.numVars : ℝ) ≤ k * φ.length := by + exact_mod_cast CNF.numVars_le_mul_length + (by simpa only [List.all_eq_true, decide_eq_true_eq] using hφ) + change δ * φ.numVars ≤ k * δ * φ.length + nlinarith + exact ⟨e', by simpa only [ite_all_length_le_SharpKSAT le_rfl] using hite⟩ /-- Subexponential `#k-SAT` counting in `numVars` gives subexponential counting in `length`. -/ theorem ComputableInSubexpTime.SharpKSAT_length_of_numVars {k : ℕ} diff --git a/CslibFrontier/Computability/Complexity/FineGrained/CountingScale.lean b/CslibFrontier/Computability/Complexity/FineGrained/CountingScale.lean index 17b890b828..0425dc6abb 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/CountingScale.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/CountingScale.lean @@ -9,6 +9,7 @@ module public import CslibFrontier.Init public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics +import CslibFrontier.Foundations.Analysis.SublinearEnvelope import Mathlib.Analysis.Asymptotics.Lemmas import Mathlib.Analysis.Complex.ExponentialBounds @@ -135,25 +136,7 @@ theorem interpolationScale_pos {n : ℕ} (hn : 1 ≤ n) : 0 < interpolationScale /-- For any multiplier `A` and any `ε > 0`, `2 ^ (A * interpolationScale n)` is globally bounded by a constant multiple of `2 ^ (ε * n)`. -/ theorem exists_two_pow_mul_interpolationScale_le (A : ℝ) {ε : ℝ} (hε : 0 < ε) : - ∃ K : ℝ, 1 ≤ K ∧ ∀ n : ℕ, (2 : ℝ) ^ (A * interpolationScale n) ≤ K * (2 : ℝ) ^ (ε * n) := by - obtain ⟨N₀, hN₀⟩ := eventually_atTop.mp (eventually_mul_interpolationScale_le A hε) - let K : ℝ := 1 + ∑ m ∈ Finset.range N₀, (2 : ℝ) ^ (A * interpolationScale m) - have hsum_nonneg : 0 ≤ ∑ m ∈ Finset.range N₀, (2 : ℝ) ^ (A * interpolationScale m) := - Finset.sum_nonneg fun m _ => by positivity - have hK1 : 1 ≤ K := by dsimp [K]; linarith - refine ⟨K, hK1, fun n => ?_⟩ - have h2ε : (1 : ℝ) ≤ (2 : ℝ) ^ (ε * n) := Real.one_le_rpow (by norm_num) (by positivity) - by_cases hn : n < N₀ - · have hmem : n ∈ Finset.range N₀ := Finset.mem_range.mpr hn - have hle_sum : (2 : ℝ) ^ (A * interpolationScale n) ≤ - ∑ m ∈ Finset.range N₀, (2 : ℝ) ^ (A * interpolationScale m) := - Finset.single_le_sum (f := fun m => (2 : ℝ) ^ (A * interpolationScale m)) - (fun m _ => by positivity) hmem - have hle_K : (2 : ℝ) ^ (A * interpolationScale n) ≤ K := by dsimp [K]; linarith - exact hle_K.trans (le_mul_of_one_le_right (by positivity) h2ε) - · have hle : A * interpolationScale n ≤ ε * n := hN₀ n (not_lt.mp hn) - have hrpow : (2 : ℝ) ^ (A * interpolationScale n) ≤ (2 : ℝ) ^ (ε * n) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) hle - exact hrpow.trans (le_mul_of_one_le_left (by positivity) hK1) + ∃ K : ℝ, 1 ≤ K ∧ ∀ n : ℕ, (2 : ℝ) ^ (A * interpolationScale n) ≤ K * (2 : ℝ) ^ (ε * n) := + exists_two_pow_le_of_isLittleO (isLittleO_interpolationScale.const_mul_left A) hε end Cslib.Complexity.SubexponentialSAT diff --git a/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean index 63b3016dbf..76b4385c24 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean @@ -36,6 +36,11 @@ decision, and transfers them along polynomial-time reductions that change the pa * `Cslib.Complexity.mem_FTIME_iff_computableInTimeO`: agreement with `FTIME` on length bounds. * `Cslib.Complexity.decidableInTimeO_iff_exists_computableInTimeO`: decision as computation of a Boolean indicator. +* `Cslib.Complexity.ComputableInTimeO.ite_polyTime_of_le`, + `Cslib.Complexity.DecidableInTimeO.of_computableInTimeO_polyBounded`: guarding by a + polynomial-time test, and deciding a polynomial-time test on a function value, within + `O(2 ^ x a * (L + 1) ^ e)` for any nonnegative exponent `x`. The exponential-rate and + single-machine subexponential versions are both corollaries. * `Cslib.Complexity.DecidableInExpTime.of_computableInExpTime_polyBounded`: a polynomial-time test on a function value with polynomially bounded output length is decided at the function's rate. * `Cslib.Complexity.ComputableInExpTime.of_reduction`, @@ -188,61 +193,89 @@ theorem ComputableInExpTime.of_computableInPolyTime {μ : α → ℕ} refine ComputableInExpTime.of_computableInO hf'.inO 1 d fun a => ?_ simp -/-- Guarding an exponential-time function by a polynomial-time test and fallback preserves rate -`δ ≥ 0`. -/ -theorem ComputableInExpTime.ite_polyTime {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) {p : α → Bool} - {g : α → β} (hp : ComputableInPolyTime p encIn encBool) - (hf : ComputableInExpTime f encIn encMid μ δ) - (hg : ComputableInPolyTime g encIn encMid) : - ComputableInExpTime (fun a => if p a then f a else g a) encIn encMid μ δ := by - obtain ⟨e, hf⟩ := hf +/-- **Guarding by a polynomial-time test.** If `f` is computable within time +`O(2 ^ x a * (L + 1) ^ e)` and `p`, `g` are computable in polynomial time, then +`if p a then f a else g a` is computable within time `O(2 ^ y a * (L + 1) ^ e')` for some `e'`, +for any nonnegative exponent `y` that is at least `x` wherever the test `p` passes. -/ +theorem ComputableInTimeO.ite_polyTime_of_le {x y : α → ℝ} {e : ℕ} {p : α → Bool} {g : α → β} + (hf : ComputableInTimeO f encIn encMid fun a => 2 ^ x a * ((encIn a).length + 1) ^ e) + (hp : ComputableInPolyTime p encIn encBool) (hg : ComputableInPolyTime g encIn encMid) + (hy : ∀ a, 0 ≤ y a) (hxy : ∀ a, p a = true → x a ≤ y a) : + ∃ e', ComputableInTimeO (fun a => if p a then f a else g a) encIn encMid + fun a => 2 ^ y a * ((encIn a).length + 1) ^ e' := by obtain ⟨t, c, hfO, ht⟩ := hf.exists_computableInO obtain ⟨dp, _, hp'⟩ := hp.exists_degree obtain ⟨dg, _, hg'⟩ := hg.exists_degree - have hcomb := hp'.inO.ite hfO hg'.inO - refine ComputableInExpTime.of_computableInO hcomb (2 * c + 3) (dp + dg + e) fun a => ?_ - have hx : 0 ≤ δ * μ a := by positivity - have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := dp + dg + e) hx - have ht' : (t a : ℝ) ≤ 2 * c * (2 ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ (dp + dg + e)) := - le_two_mul_mul_of_le_mul_add (ht a) (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega)) hX - have hdp := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dp) (e := dp + dg + e) hx + refine ⟨dp + dg + e, (ComputableInTimeO.of_computableInO (hp'.inO.ite hfO hg'.inO) + fun _ => le_rfl).mono (2 * c + 3) (fun a => ?_) fun _ => by positivity⟩ + have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := dp + dg + e) (hy a) + have hdp := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dp) (e := dp + dg + e) (hy a) (by omega) - have hdg := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dg) (e := dp + dg + e) hx + have hdg := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dg) (e := dp + dg + e) (hy a) (by omega) - have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) + have hc : (0 : ℝ) ≤ c := Nat.cast_nonneg c + have hcX := mul_nonneg hc (zero_le_one.trans hX) change ((((encIn a).length + 1) ^ dp + if p a then t a else ((encIn a).length + 1) ^ dg : ℕ) : ℝ) ≤ _ - split_ifs <;> push_cast <;> linarith + split_ifs with hpa + · have ht' := le_two_mul_mul_of_le_mul_add (ht a) + (two_rpow_mul_pow_le_two_rpow_mul_pow (hxy a hpa) (by omega : e ≤ dp + dg + e)) hX + push_cast + linarith + · push_cast + linarith -/-- **Exact-rate decision from function computation.** If `f` is computable in time -`2 ^ (δ * μ a) · poly(|a|)` (`δ ≥ 0`) and its encoded output length is polynomially bounded in -`|a|`, then any polynomial-time test on `f a` decides `{a | test (f a) = true}` at the same -exponential rate `δ`. -/ -theorem DecidableInExpTime.of_computableInExpTime_polyBounded {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) +/-- Guarding an exponential-time function by a polynomial-time test and fallback preserves rate +`δ ≥ 0`. -/ +theorem ComputableInExpTime.ite_polyTime {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) {p : α → Bool} + {g : α → β} (hp : ComputableInPolyTime p encIn encBool) (hf : ComputableInExpTime f encIn encMid μ δ) + (hg : ComputableInPolyTime g encIn encMid) : + ComputableInExpTime (fun a => if p a then f a else g a) encIn encMid μ δ := by + obtain ⟨_, hf⟩ := hf + exact hf.ite_polyTime_of_le hp hg (fun _ => by positivity) fun _ _ => le_rfl + +/-- **Decision from function computation.** If `f` is computable within time +`O(2 ^ x a * (L + 1) ^ e)` for a nonnegative exponent `x` and its encoded output length is +polynomially bounded in `L`, then any polynomial-time test on `f a` decides +`{a | test (f a) = true}` within time `O(2 ^ x a * (L + 1) ^ e')` for some `e'`. -/ +theorem DecidableInTimeO.of_computableInTimeO_polyBounded {x : α → ℝ} {e : ℕ} + (hx : ∀ a, 0 ≤ x a) + (hf : ComputableInTimeO f encIn encMid fun a => 2 ^ x a * ((encIn a).length + 1) ^ e) (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (encMid (f a)).length)) {test : β → Bool} (htest : ComputableInPolyTime test encMid encBool) : - DecidableInExpTime {a | test (f a) = true} encIn μ δ := by - obtain ⟨e, hf⟩ := hf + ∃ e', DecidableInTimeO {a | test (f a) = true} encIn + fun a => 2 ^ x a * ((encIn a).length + 1) ^ e' := by obtain ⟨t, c, hfO, ht⟩ := hf.exists_computableInO obtain ⟨d, _, htest'⟩ := htest.exists_degree obtain ⟨p, q, hp⟩ := hlen.exists_le - have hcomp := htest'.inO.comp hfO - refine DecidableInExpTime.of_computableInO hcomp (fun _ => Iff.rfl) - (2 * c + 1 + (p + 1) ^ d) (e + q * d) fun a => ?_ - have hx : 0 ≤ δ * μ a := by positivity - have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := e + q * d) hx - have ht' : (t a : ℝ) ≤ 2 * c * (2 ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ (e + q * d)) := - le_two_mul_mul_of_le_mul_add (ht a) (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega)) hX + refine ⟨e + q * d, (DecidableInTimeO.of_computableInO (htest'.inO.comp hfO) (fun _ => Iff.rfl) + fun _ => le_rfl).mono (2 * c + 1 + (p + 1) ^ d) (fun a => ?_) fun _ => by positivity⟩ + have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := e + q * d) (hx a) + have ht' := le_two_mul_mul_of_le_mul_add (ht a) + (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega : e ≤ e + q * d)) hX have hout : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ ((p + 1) ^ d : ℕ) * (((encIn a).length : ℝ) + 1) ^ (q * d) := by exact_mod_cast Nat.add_one_pow_le_of_le_mul_pow (Nat.le_add_left 1 _) (hp a) d have hq := mul_le_mul_of_nonneg_left (pow_le_two_rpow_mul_pow (L := (encIn a).length) - (d := q * d) (e := e + q * d) hx (by omega)) (Nat.cast_nonneg ((p + 1) ^ d) : (0 : ℝ) ≤ _) + (d := q * d) (e := e + q * d) (hx a) (by omega)) (Nat.cast_nonneg ((p + 1) ^ d) : (0 : ℝ) ≤ _) + have hC : (0 : ℝ) ≤ (2 * c + 1 + (p + 1) ^ d : ℕ) := Nat.cast_nonneg _ change ((t a + ((encMid (f a)).length + 1) ^ d : ℕ) : ℝ) ≤ _ - push_cast at hout hq ⊢ + push_cast at hout hq hC ⊢ linarith +/-- **Exact-rate decision from function computation.** If `f` is computable in time +`2 ^ (δ * μ a) · poly(|a|)` (`δ ≥ 0`) and its encoded output length is polynomially bounded in +`|a|`, then any polynomial-time test on `f a` decides `{a | test (f a) = true}` at the same +exponential rate `δ`. -/ +theorem DecidableInExpTime.of_computableInExpTime_polyBounded {μ : α → ℕ} {δ : ℝ} (hδ : 0 ≤ δ) + (hf : ComputableInExpTime f encIn encMid μ δ) + (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (encMid (f a)).length)) + {test : β → Bool} (htest : ComputableInPolyTime test encMid encBool) : + DecidableInExpTime {a | test (f a) = true} encIn μ δ := by + obtain ⟨_, hf⟩ := hf + exact DecidableInTimeO.of_computableInTimeO_polyBounded (fun _ => by positivity) hf hlen htest + /-- Subexponential function computation with polynomially bounded output length transfers to subexponential decision for any polynomial-time output predicate. -/ theorem DecidableInSubexpTime.of_computableInSubexpTime_polyBounded {μ : α → ℕ} diff --git a/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean b/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean index ec27b6dbc0..b5e6cfba74 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean @@ -369,38 +369,9 @@ theorem ComputableInSingleSubexpTime.ite_polyTime {f g : α → β} {p : α → (hf : ComputableInSingleSubexpTime f encIn encMid μ) (hg : ComputableInPolyTime g encIn encMid) : ComputableInSingleSubexpTime (fun a => if p a then f a else g a) encIn encMid μ := by - obtain ⟨t, sp, e, hcomp, hbound⟩ := computableInSingleSubexpTime_iff_exists_machine.mp hf - have hl : ∀ a, (encMid (f a)).length ≤ t a := hcomp.length_le - obtain ⟨k, hf'⟩ := ComputableInTimeAndSpace.exists_space_linear hcomp - have hfO : ComputableInO f encIn encMid t t := ComputableInO.of_bounds hf' (k + 1) - (fun a => by nlinarith) (fun a => by nlinarith) (fun a => by nlinarith [hl a]) - obtain ⟨dp, _, hp'⟩ := hp.exists_degree - obtain ⟨dg, _, hg'⟩ := hg.exists_degree - obtain ⟨c_comb, hcomb_ts, -⟩ := hp'.inO.ite hfO hg'.inO - refine computableInSingleSubexpTime_iff_exists_machine.mpr - ⟨_, _, dp + dg + e, hcomb_ts, fun δ hδ => ?_⟩ - obtain ⟨c, hc⟩ := hbound δ hδ - refine ⟨c_comb * (2 * c + 4), fun a => ?_⟩ - have hx : 0 ≤ δ * μ a := by positivity - have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := dp + dg + e) hx - have ht := le_two_mul_mul_of_le_mul_add (hc a) - (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega : e ≤ dp + dg + e)) hX - have hdp := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dp) (e := dp + dg + e) hx - (by omega) - have hdg := pow_le_two_rpow_mul_pow (L := (encIn a).length) (d := dg) (e := dp + dg + e) hx - (by omega) - have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) - -- the guarded runtime is at most `(2 * c + 4)` envelopes, in either branch - have hsum : ((((encIn a).length + 1) ^ dp + - if p a then t a else ((encIn a).length + 1) ^ dg) + 1 : ℕ) ≤ - (2 * c + 4) * (2 ^ (δ * μ a) * (((encIn a).length : ℝ) + 1) ^ (dp + dg + e)) := by - split_ifs <;> push_cast <;> linarith - have hmul := mul_le_mul_of_nonneg_left hsum (Nat.cast_nonneg c_comb : (0 : ℝ) ≤ c_comb) - have hpos : (0 : ℝ) ≤ (c_comb * (2 * c + 4) : ℕ) := Nat.cast_nonneg _ - change ((c_comb * ((((encIn a).length + 1) ^ dp + - if p a then t a else ((encIn a).length + 1) ^ dg) + 1) : ℕ) : ℝ) ≤ _ - push_cast at hmul hpos ⊢ - linarith + obtain ⟨s, e, hnn, hs_o, hf⟩ := hf + obtain ⟨e', h⟩ := hf.ite_polyTime_of_le hp hg (fun a => hnn (μ a)) fun _ _ => le_rfl + exact ⟨s, e', hnn, hs_o, h⟩ /-- **Single-machine decision from function computation.** Composing a single-machine subexponential function of polynomially bounded output length with a polynomial-time test yields a @@ -411,33 +382,10 @@ theorem DecidableInSingleSubexpTime.of_computableInSingleSubexpTime_polyBounded (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (encMid (f a)).length)) {test : β → Bool} (htest : ComputableInPolyTime test encMid encBool) : DecidableInSingleSubexpTime {a | test (f a) = true} encIn μ := by - obtain ⟨s, e, hnn, hs_o, hfO_time⟩ := hf - obtain ⟨t, c, hfO, ht⟩ := hfO_time.exists_computableInO - obtain ⟨d, _, htest'⟩ := htest.exists_degree - obtain ⟨p, q, hp⟩ := hlen.exists_le - obtain ⟨c_comp, hcomp_ts, -⟩ := htest'.inO.comp hfO - refine ⟨s, e + q * d, hnn, hs_o, c_comp * (2 * c + 2 + (p + 1) ^ d), _, _, fun a => ?_, - decidableInTimeAndSpace_iff.mpr ⟨test ∘ f, hcomp_ts, fun _ => Iff.rfl⟩⟩ - have hx : 0 ≤ s (μ a) := hnn (μ a) - have hX := one_le_two_rpow_mul_pow (L := (encIn a).length) (e := e + q * d) hx - have ht' : (t a : ℝ) ≤ 2 * c * (2 ^ s (μ a) * (((encIn a).length : ℝ) + 1) ^ (e + q * d)) := - le_two_mul_mul_of_le_mul_add (ht a) (two_rpow_mul_pow_le_two_rpow_mul_pow le_rfl (by omega)) hX - have hout : (((encMid (f a)).length : ℝ) + 1) ^ d ≤ - ((p + 1) ^ d : ℕ) * (((encIn a).length : ℝ) + 1) ^ (q * d) := by - exact_mod_cast Nat.add_one_pow_le_of_le_mul_pow (Nat.le_add_left 1 _) (hp a) d - have hq := mul_le_mul_of_nonneg_left (pow_le_two_rpow_mul_pow (L := (encIn a).length) - (d := q * d) (e := e + q * d) hx (by omega)) (Nat.cast_nonneg ((p + 1) ^ d) : (0 : ℝ) ≤ _) - -- the composed runtime is at most `2 * c + 2 + (p + 1) ^ d` envelopes - have hsum : ((t a + ((encMid (f a)).length + 1) ^ d + 1 : ℕ) : ℝ) ≤ - (2 * c + 2 + (p + 1) ^ d : ℕ) * - (2 ^ s (μ a) * (((encIn a).length : ℝ) + 1) ^ (e + q * d)) := by - push_cast at hout hq ⊢ - linarith - have hmul := mul_le_mul_of_nonneg_left hsum (Nat.cast_nonneg c_comp : (0 : ℝ) ≤ c_comp) - have hpos : (0 : ℝ) ≤ (c_comp * (2 * c + 2 + (p + 1) ^ d) : ℕ) := Nat.cast_nonneg _ - change ((c_comp * ((t a + ((encMid (f a)).length + 1) ^ d) + 1) : ℕ) : ℝ) ≤ _ - push_cast at hmul hpos ⊢ - linarith + obtain ⟨s, e, hnn, hs_o, hf⟩ := hf + obtain ⟨e', h⟩ := + DecidableInTimeO.of_computableInTimeO_polyBounded (fun a => hnn (μ a)) hf hlen htest + exact ⟨s, e', hnn, hs_o, h⟩ /-- **Transfer along linear-parameter parsimonious reductions (`SingleSubexp`).** -/ theorem ComputableInSingleSubexpTime.of_reduction {μA : α → ℕ} {μB : β → ℕ} @@ -698,37 +646,12 @@ theorem ComputableInSingleSubexpTime.SharpKSAT_length_of_numVars {k : ℕ} ComputableInSingleSubexpTime (SharpKSAT k) encCNF encNat List.length := by obtain ⟨s, e, hnn, hs_o, htime⟩ := h obtain ⟨sBar, hmono, hnnBar, hle, hsBar_o⟩ := exists_monotone_isLittleO_ge hnn hs_o - obtain ⟨t, c, hO, ht⟩ := htime.exists_computableInO - obtain ⟨dw, _, hw⟩ := (computableInPolyTime_all_length_le k).exists_degree - obtain ⟨dc, _, hc0⟩ := (ComputableInPolyTime.const (encIn := encCNF) (0 : ℕ)).exists_degree - have hite := (hw.inO.ite hO hc0.inO).of_enc_eq (g := SharpKSAT k) fun φ => congrArg encNat <| by - split_ifs with hφ - · simp only [SharpKSAT, hφ, ↓reduceIte] - · simp only [SharpKSAT, hφ, Bool.false_eq_true, ↓reduceIte] - let s' (m : ℕ) : ℝ := sBar (k * m + 0) - refine ⟨s', dw + dc + e, fun m => hnnBar _, - isLittleO_comp_linear_of_nonneg hnnBar hsBar_o k 0, - (ComputableInTimeO.of_computableInO hite fun _ => le_rfl).mono (2 * c + 3) - (fun φ => ?_) fun _ => by positivity⟩ - have hx : 0 ≤ s' φ.length := hnnBar _ - have hX := one_le_two_rpow_mul_pow (L := (encCNF φ).length) (e := dw + dc + e) hx - have hcX := mul_nonneg (Nat.cast_nonneg c : (0 : ℝ) ≤ c) (zero_le_one.trans hX) - have hdw := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dw) (e := dw + dc + e) hx - (by omega) - have hdc := pow_le_two_rpow_mul_pow (L := (encCNF φ).length) (d := dc) (e := dw + dc + e) hx - (by omega) - change ((((encCNF φ).length + 1) ^ dw + - if φ.all (fun cl => decide (cl.length ≤ k)) then t φ - else ((encCNF φ).length + 1) ^ dc : ℕ) : ℝ) ≤ _ - split_ifs with hφ - · simp only [List.all_eq_true, decide_eq_true_eq] at hφ - have hexp : s φ.numVars ≤ s' φ.length := - (hle _).trans (hmono (by simpa only [Nat.add_zero] using CNF.numVars_le_mul_length hφ)) - have ht' := le_two_mul_mul_of_le_mul_add (ht φ) - (two_rpow_mul_pow_le_two_rpow_mul_pow hexp (by omega)) hX - push_cast - linarith - · push_cast - linarith + obtain ⟨e', hite⟩ := htime.ite_polyTime_of_le (computableInPolyTime_all_length_le k) + (ComputableInPolyTime.const 0) (y := fun φ => sBar (k * φ.length + 0)) (fun _ => hnnBar _) + fun φ hφ => (hle _).trans (hmono (Nat.le_add_right_of_le (CNF.numVars_le_mul_length + (by simpa only [List.all_eq_true, decide_eq_true_eq] using hφ)))) + refine ⟨fun m => sBar (k * m + 0), e', fun _ => hnnBar _, + isLittleO_comp_linear_of_nonneg hnnBar hsBar_o k 0, ?_⟩ + simpa only [ite_all_length_le_SharpKSAT le_rfl] using hite end Cslib.Complexity From ffe6fef29be4108ef22e2c58c64e89dc877e623f Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 20:56:42 +0000 Subject: [PATCH 6/6] refactor(Complexity/FineGrained): derive single-machine decision results from their computation counterparts Add decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime (decision as single-machine computation of a Boolean indicator) and derive decidableInSingleSubexpTime_iff_exists_machine, DecidableInSingleSubexpTime.mono_measure, .of_reduction and .of_uniformFamily from their ComputableInSingleSubexpTime counterparts. This removes the duplicated quantifier-exchange proof that proof_copies flagged (survey item F2(b), #4737). decidableInTimeO_iff_exists_computableInTimeO moves from the Type section to the Type* FunctionBounds section of FunctionRates (its statement is unchanged apart from the universe generalization) so the SingleBounds lemmas can use it. No existing statement changes. --- .../Complexity/FineGrained/FunctionRates.lean | 22 ++-- .../Complexity/FineGrained/SingleSubexp.lean | 106 +++++++++--------- 2 files changed, 61 insertions(+), 67 deletions(-) diff --git a/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean index 76b4385c24..128a38f108 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/FunctionRates.lean @@ -116,6 +116,17 @@ theorem ComputableInSubexpTime.mono_measure {μ μ' : α → ℕ} {c : ℕ} (hμ ((h (δ / (c + 1)) (by positivity)).mono_measure hμ (by positivity)).mono (natCast_mul_div_add_one_le hδ.le c) +/-- `DecidableInTimeO` is `ComputableInTimeO` of a Boolean indicator function. -/ +theorem decidableInTimeO_iff_exists_computableInTimeO {A : Set α} : + DecidableInTimeO A encIn T ↔ + ∃ g : α → Bool, (∀ a, a ∈ A ↔ g a = true) ∧ ComputableInTimeO g encIn encBool T := by + constructor + · rintro ⟨c, t, s, ht, h⟩ + obtain ⟨g, hg, hA⟩ := decidableInTimeAndSpace_iff.mp h + exact ⟨g, hA, c, t, s, ht, hg⟩ + · rintro ⟨g, hA, c, t, s, ht, hg⟩ + exact ⟨c, t, s, ht, decidableInTimeAndSpace_iff.mpr ⟨g, hg, hA⟩⟩ + end FunctionBounds section FunctionMachines @@ -165,17 +176,6 @@ theorem ComputableInTimeO.of_computableInO {t S : α → ℕ} push_cast nlinarith [hT a, (Nat.cast_nonneg c : (0 : ℝ) ≤ c)] -/-- `DecidableInTimeO` is `ComputableInTimeO` of a Boolean indicator function. -/ -theorem decidableInTimeO_iff_exists_computableInTimeO {A : Set α} : - DecidableInTimeO A encIn T ↔ - ∃ g : α → Bool, (∀ a, a ∈ A ↔ g a = true) ∧ ComputableInTimeO g encIn encBool T := by - constructor - · rintro ⟨c, t, s, ht, h⟩ - obtain ⟨g, hg, hA⟩ := decidableInTimeAndSpace_iff.mp h - exact ⟨g, hA, c, t, s, ht, hg⟩ - · rintro ⟨g, hA, c, t, s, ht, hg⟩ - exact ⟨c, t, s, ht, decidableInTimeAndSpace_iff.mpr ⟨g, hg, hA⟩⟩ - /-- A `ComputableInO` certificate within `c * (2 ^ (δ * μ a) * (L + 1) ^ e)` gives `ComputableInExpTime`. -/ theorem ComputableInExpTime.of_computableInO {μ : α → ℕ} {δ : ℝ} {t S : α → ℕ} diff --git a/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean b/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean index b5e6cfba74..5323ca2b5f 100644 --- a/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean +++ b/CslibFrontier/Computability/Complexity/FineGrained/SingleSubexp.lean @@ -70,6 +70,9 @@ their exact relationship to the family notions: ## Main results +* `Cslib.Complexity.decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime`: decision + as single-machine computation of a Boolean indicator. The `Decidable…` transfers are derived from + their `Computable…` counterparts through it. * `Cslib.Complexity.decidableInSingleSubexpTime_iff_exists_machine`, `Cslib.Complexity.computableInSingleSubexpTime_iff_exists_machine`: equivalence with exchanging `∃ (M, e)` and `∀ δ > 0`. @@ -157,6 +160,20 @@ scale `s =o[atTop] id`. -/ ∃ (s : ℕ → ℝ) (e : ℕ), (∀ n, 0 ≤ s n) ∧ (s =o[atTop] fun n : ℕ => (n : ℝ)) ∧ ComputableInTimeO f encIn encOut fun a => 2 ^ s (μ a) * ((encIn a).length + 1) ^ e +/-- `DecidableInSingleSubexpTime` is `ComputableInSingleSubexpTime` of a Boolean indicator +function. -/ +theorem decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime {A : Set α} + {enc : α ↪ List Bool} {μ : α → ℕ} : + DecidableInSingleSubexpTime A enc μ ↔ + ∃ g : α → Bool, (∀ a, a ∈ A ↔ g a = true) ∧ + ComputableInSingleSubexpTime g enc encBool μ := by + constructor + · rintro ⟨s, e, hnn, hs_o, h⟩ + obtain ⟨g, hA, hg⟩ := decidableInTimeO_iff_exists_computableInTimeO.mp h + exact ⟨g, hA, s, e, hnn, hs_o, hg⟩ + · rintro ⟨g, hA, s, e, hnn, hs_o, hg⟩ + exact ⟨s, e, hnn, hs_o, decidableInTimeO_iff_exists_computableInTimeO.mpr ⟨g, hA, hg⟩⟩ + /-- **Single-machine implies family subexponential decision.** -/ theorem DecidableInSingleSubexpTime.decidableInSubexpTime {A : Set α} {enc : α ↪ List Bool} {μ : α → ℕ} (h : DecidableInSingleSubexpTime A enc μ) : @@ -252,33 +269,6 @@ private theorem exists_isLittleO_of_forall_exp_bound {t : α → ℕ} {enc : α rw [Real.norm_of_nonneg (hnn n), Real.norm_of_nonneg (Nat.cast_nonneg n)] linarith [hs_le n] -/-- **Machine-quantifier characterization of `DecidableInSingleSubexpTime`.** Single-machine -`2 ^ o(μ)` decision is equivalent to having *one* machine (`DecidableInTimeAndSpace A enc t sp`) -and *one* polynomial degree `e` that satisfy the `2 ^ (δ * μ a) * (L + 1) ^ e` runtime bound for -every `δ > 0` (with only the constant `c` depending on `δ`). -/ -theorem decidableInSingleSubexpTime_iff_exists_machine {A : Set α} {enc : α ↪ List Bool} - {μ : α → ℕ} : - DecidableInSingleSubexpTime A enc μ ↔ - ∃ (t sp : α → ℕ) (e : ℕ), DecidableInTimeAndSpace A enc t sp ∧ - ∀ δ : ℝ, 0 < δ → ∃ c : ℕ, - ∀ a, (t a : ℝ) ≤ c * (2 ^ (δ * μ a) * ((enc a).length + 1) ^ e) + c := by - constructor - · rintro ⟨s, e, _, hs_o, c₀, t, sp, ht, hdec⟩ - refine ⟨t, sp, e, hdec, fun δ hδ => ?_⟩ - obtain ⟨K, _, hK⟩ := exists_two_pow_le_of_isLittleO hs_o hδ - refine ⟨c₀ * ⌈K⌉₊ + c₀, fun a => (ht a).trans ?_⟩ - have h := mul_le_mul_of_nonneg_left (two_rpow_mul_pow_le_natCeil_mul_add_of_le - (L := (enc a).length) (e := e) (hK (μ a))) (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) - have hpos := mul_nonneg (Nat.cast_nonneg c₀ : (0 : ℝ) ≤ c₀) - (by positivity : (0 : ℝ) ≤ 2 ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e) - push_cast - linarith - · rintro ⟨t, sp, e, hdec, h⟩ - obtain ⟨s, hnn, hs_o, hbound⟩ := exists_isLittleO_of_forall_exp_bound h - refine ⟨s, e, hnn, hs_o, 1, t, sp, fun a => ?_, hdec⟩ - push_cast - linarith [hbound a] - /-- **Machine-quantifier characterization of `ComputableInSingleSubexpTime`.** Single-machine `2 ^ o(μ)` function computation is equivalent to having *one* machine (`ComputableInTimeAndSpace f encIn encOut t sp`) and *one* polynomial degree `e` that satisfy the @@ -306,22 +296,26 @@ theorem computableInSingleSubexpTime_iff_exists_machine {f : α → β} {encIn : push_cast linarith [hbound a] -/-! ### Measure rescaling and reduction transfers -/ +/-- **Machine-quantifier characterization of `DecidableInSingleSubexpTime`.** Single-machine +`2 ^ o(μ)` decision is equivalent to having *one* machine (`DecidableInTimeAndSpace A enc t sp`) +and *one* polynomial degree `e` that satisfy the `2 ^ (δ * μ a) * (L + 1) ^ e` runtime bound for +every `δ > 0` (with only the constant `c` depending on `δ`). -/ +theorem decidableInSingleSubexpTime_iff_exists_machine {A : Set α} {enc : α ↪ List Bool} + {μ : α → ℕ} : + DecidableInSingleSubexpTime A enc μ ↔ + ∃ (t sp : α → ℕ) (e : ℕ), DecidableInTimeAndSpace A enc t sp ∧ + ∀ δ : ℝ, 0 < δ → ∃ c : ℕ, + ∀ a, (t a : ℝ) ≤ c * (2 ^ (δ * μ a) * ((enc a).length + 1) ^ e) + c := by + rw [decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime] + constructor + · rintro ⟨g, hA, hg⟩ + obtain ⟨t, sp, e, hcomp, h⟩ := computableInSingleSubexpTime_iff_exists_machine.mp hg + exact ⟨t, sp, e, decidableInTimeAndSpace_iff.mpr ⟨g, hcomp, hA⟩, h⟩ + · rintro ⟨t, sp, e, hdec, h⟩ + obtain ⟨g, hcomp, hA⟩ := decidableInTimeAndSpace_iff.mp hdec + exact ⟨g, hA, computableInSingleSubexpTime_iff_exists_machine.mpr ⟨t, sp, e, hcomp, h⟩⟩ -/-- Single-machine subexponential decision transfers to any parameter at least linear in `μ`. -/ -theorem DecidableInSingleSubexpTime.mono_measure {A : Set α} {enc : α ↪ List Bool} - {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) - (h : DecidableInSingleSubexpTime A enc μ) : - DecidableInSingleSubexpTime A enc μ' := by - obtain ⟨s, e, hnn, hs_o, hO⟩ := h - obtain ⟨sBar, hmono, hnnBar, hle, hsBar_o⟩ := exists_monotone_isLittleO_ge hnn hs_o - refine ⟨fun n => sBar (c * n + c), e, fun n => hnnBar _, - isLittleO_comp_linear_of_nonneg hnnBar hsBar_o c c, - hO.mono 1 (fun a => ?_) fun _ => by positivity⟩ - have h := two_rpow_mul_pow_le_two_rpow_mul_pow (L := (enc a).length) (d := e) (e := e) - ((hle (μ a)).trans (hmono (hμ a))) le_rfl - push_cast - linarith +/-! ### Measure rescaling and reduction transfers -/ /-- Single-machine subexponential function computation transfers to any parameter at least linear in `μ`. -/ @@ -339,6 +333,14 @@ theorem ComputableInSingleSubexpTime.mono_measure {f : α → β} {encIn : α push_cast linarith +/-- Single-machine subexponential decision transfers to any parameter at least linear in `μ`. -/ +theorem DecidableInSingleSubexpTime.mono_measure {A : Set α} {enc : α ↪ List Bool} + {μ μ' : α → ℕ} {c : ℕ} (hμ : ∀ a, μ a ≤ c * μ' a + c) + (h : DecidableInSingleSubexpTime A enc μ) : + DecidableInSingleSubexpTime A enc μ' := by + rw [decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime] at h ⊢ + exact h.imp fun g ⟨hA, hg⟩ => ⟨hA, hg.mono_measure hμ⟩ + end SingleBounds section SingleMachines @@ -431,14 +433,9 @@ theorem DecidableInSingleSubexpTime.of_reduction {A : Set α} {B : Set β} {c : ℕ} (hμ : ∀ a, μB (r a) ≤ c * μA a + c) (hB : DecidableInSingleSubexpTime B encMid μB) : DecidableInSingleSubexpTime A encIn μA := by - obtain ⟨s, e, hnn, hs_o, hB_time⟩ := hB - obtain ⟨g, hgB, hg_time⟩ := decidableInTimeO_iff_exists_computableInTimeO.mp hB_time - have hg_single : ComputableInSingleSubexpTime g encMid encBool μB := - ⟨s, e, hnn, hs_o, hg_time⟩ - obtain ⟨s', e', hnn', hs'_o, hgr_time⟩ := hg_single.of_reduction hr hμ - exact ⟨s', e', hnn', hs'_o, - decidableInTimeO_iff_exists_computableInTimeO.mpr ⟨g ∘ r, fun a => (hAB a).trans (hgB (r a)), - hgr_time⟩⟩ + rw [decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime] at hB ⊢ + obtain ⟨g, hgB, hg⟩ := hB + exact ⟨g ∘ r, fun a => (hAB a).trans (hgB (r a)), hg.of_reduction hr hμ⟩ end SingleMachines @@ -589,13 +586,10 @@ theorem DecidableInSingleSubexpTime.of_uniformFamily {A : Set α} {μ : α → (htend : ∀ M : ℕ, ∃ N : ℕ, ∀ a, N ≤ μ a → M ≤ sched a) : DecidableInSingleSubexpTime A encIn μ := by let g (a : α) : Bool := decideAt { precision := 0, input := a } - have hg_single : ComputableInSingleSubexpTime g encIn encBool μ := - .of_uniformFamily hdec + exact decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime.mpr ⟨g, + fun a => hcorrect 0 a, .of_uniformFamily hdec (fun m a => Bool.eq_iff_iff.mpr ((hcorrect m a).symm.trans (hcorrect 0 a))) - htime hsched htend - obtain ⟨s, e', hnn, hs_o, hg_time⟩ := hg_single - exact ⟨s, e', hnn, hs_o, - decidableInTimeO_iff_exists_computableInTimeO.mpr ⟨g, fun a => hcorrect 0 a, hg_time⟩⟩ + htime hsched htend⟩ end UniformFamily