diff --git a/Complexity.lean b/Complexity.lean index 64c0717af6..4ea64f53bc 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -743,6 +743,7 @@ public import Complexity.Computability.Complexity.Fagin.Verifier public import Complexity.Computability.Complexity.FineGrained public import Complexity.Computability.Complexity.FineGrained.Assignment public import Complexity.Computability.Complexity.FineGrained.BruteForce +public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch public import Complexity.Computability.Complexity.FineGrained.Exponents public import Complexity.Computability.Complexity.FineGrained.GraphProblems public import Complexity.Computability.Complexity.FineGrained.OrthogonalVectors diff --git a/Complexity/Computability/Complexity/FineGrained/BruteForce.lean b/Complexity/Computability/Complexity/FineGrained/BruteForce.lean index 6b0be76383..f8c162021a 100644 --- a/Complexity/Computability/Complexity/FineGrained/BruteForce.lean +++ b/Complexity/Computability/Complexity/FineGrained/BruteForce.lean @@ -8,25 +8,20 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.FineGrained.Assignment +public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch import Complexity.Computability.Complexity.Problems.SAT.PolyTime -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Binary -import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain /-! # Exhaustive search for satisfiability Exhaustive search decides `SAT` by trying the `2 ^ n` numbered assignments of the `n` distinct -variables of a formula (`Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment`). It iterates a -polynomial-time step `2 ^ n` times with a binary counter -(`Turing.MultiTapeTM.ComputableTidilyInO.iterate`), so it runs within time `2 ^ n` times a -polynomial in the length of the encoded formula -(`Cslib.Complexity.BruteForce.exists_computableInO_search`). Hence `SAT`, and every -`k`-SAT, is decidable within time `2 ^ n` times a polynomial +variables of a formula (`Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment`). By +`Cslib.Complexity.DecidableInExpTime.of_exhaustiveSearch`, iterating the polynomial-time evaluation +step (`Cslib.Complexity.computableInPolyTime_eval_bitsAssignment`) `2 ^ n` times decides `SAT`, and +every `k`-SAT, within time `2 ^ n` times a polynomial in the length of the encoded formula (`Cslib.Complexity.SAT_decidableInExpTime_one`, `Cslib.Complexity.KSAT_decidableInExpTime_one`). ## Main definitions @@ -35,8 +30,9 @@ polynomial in the length of the encoded formula ## Main results +* `Cslib.Complexity.exists_le_mul_two_pow_of_polyBounded`: combining `2 ^ μ a + 1` rounds of a + polynomial with a polynomial into `2 ^ μ a` times a polynomial. * `Cslib.Complexity.BruteForce.search_eq_true_iff`: exhaustive search decides `SAT`. -* `Cslib.Complexity.BruteForce.exists_computableInO_search`: its running time. * `Cslib.Complexity.SAT_decidableInExpTime_one`, `Cslib.Complexity.KSAT_decidableInExpTime_one`: `SAT` and `k`-SAT are decidable within time `2 ^ n` times a polynomial. @@ -81,164 +77,47 @@ namespace BruteForce /-! ### The search -/ -/-- The state of exhaustive search: the formula, its distinct variables, the number of the next -assignment to try, and whether a satisfying assignment was found. -/ -abbrev State : Type := (CNF ℕ × List ℕ) × (ℕ × Bool) - -/-- States encoded as framed tuples. -/ -private abbrev encState : State ↪ List Bool := - encPair (encPair encCNF (encList encNat)) (encPair encNat encBool) - -/-- Try the next numbered assignment. -/ -def step (s : State) : State := - (s.1, (s.2.1 + 1, s.2.2 || s.1.1.eval (bitsAssignment s.1.2 s.2.1))) - -/-- The initial state: no assignment tried yet. -/ -def init (φ : CNF ℕ) : State := ((φ, φ.distinctVars), (0, false)) - /-- **Exhaustive search**: try the `2 ^ n` assignments numbered by `i < 2 ^ n` on the `n` distinct variables of the formula. -/ -def search (φ : CNF ℕ) : Bool := (step^[2 ^ φ.distinctVars.length] (init φ)).2.2 - -private theorem iterate_step_init (φ : CNF ℕ) (k : ℕ) : - step^[k] (init φ) = ((φ, φ.distinctVars), - (k, (List.range k).any fun i => φ.eval (bitsAssignment φ.distinctVars i))) := by - induction k with - | zero => rfl - | succ k ih => - rw [Function.iterate_succ_apply', ih, step, List.range_succ, List.any_append] - simp +def search (φ : CNF ℕ) : Bool := + (List.range (2 ^ φ.distinctVars.length)).any fun i => φ.eval (bitsAssignment φ.distinctVars i) /-- **Exhaustive search decides `SAT`.** -/ theorem search_eq_true_iff (φ : CNF ℕ) : search φ = true ↔ φ ∈ SAT := by - rw [search, iterate_step_init, mem_SAT, + rw [search, mem_SAT, CNF.satisfiable_iff_exists_bitsAssignment fun v hv => CNF.mem_distinctVars.mpr hv] simp -/-! ### Running time -/ - -open ComputableTidilyInPolyTime in -/-- A step of exhaustive search is polynomial-time. -/ -private theorem computableTidilyInPolyTime_step - : ComputableTidilyInPolyTime step encState encState := by - have h : ComputableTidilyInPolyTime (fun s : State => s.1.1.eval (bitsAssignment s.1.2 s.2.1)) - encState encBool := - computableInPolyTime_eval_bitsAssignment.tidy.comp - (show ComputableTidilyInPolyTime (fun s : State => (s.1, s.2.1)) encState - (encPair (encPair encCNF (encList encNat)) encNat) by fun_prop) - unfold step - fun_prop - -attribute [local fun_prop] ComputableInPolyTime.tidy in -open ComputableTidilyInPolyTime in -/-- The initial state is computed in polynomial time. -/ -private theorem computableTidilyInPolyTime_init - : ComputableTidilyInPolyTime init encCNF encState := by - have hvars := SAT.computableInPolyTime_distinctVars.tidy - unfold init - fun_prop - -attribute [local fun_prop] ComputableInPolyTime.tidy in -open ComputableTidilyInPolyTime in -/-- The number `2 ^ n` of rounds is computed in binary in polynomial time. -/ -private theorem computableTidilyInPolyTime_count : - ComputableTidilyInPolyTime (fun φ => 2 ^ φ.distinctVars.length) encCNF encNat := by - fun_prop - -/-- **The running time of exhaustive search**: within time `2 ^ n` times a polynomial in the -length of the encoded formula, on formulas with `n` variables. -/ -theorem exists_computableInO_search : ∃ e, ComputableInO search encCNF encBool - (fun φ => 2 ^ φ.numVars * ((encCNF φ).length + 1) ^ e) - fun φ => 2 ^ φ.numVars * ((encCNF φ).length + 1) ^ e := by - have this : ∃ e, ComputableTidilyInO search encCNF encBool - (fun φ => 2 ^ φ.numVars * ((encCNF φ).length + 1) ^ e) fun φ => 2 ^ φ.numVars * - ((encCNF φ).length + 1) ^ e := by - obtain ⟨d, _, hstep⟩ := computableTidilyInPolyTime_step.exists_degree - obtain ⟨d₀, _, hinit⟩ := computableTidilyInPolyTime_init.exists_degree - obtain ⟨d₁, _, hcount⟩ := computableTidilyInPolyTime_count.exists_degree - obtain ⟨d₂, _, hans⟩ := - (show ComputableTidilyInPolyTime (fun s : State => s.2.2) encState encBool - by fun_prop).exists_degree - obtain ⟨cv, dv, hvs⟩ := - SAT.computableInPolyTime_distinctVars.tidy.polyBounded_length.exists_le - set size : CNF ℕ → ℕ := fun φ => (encCNF φ).length - set B : CNF ℕ → ℕ := fun φ => (2 * cv + 13) * (size φ + 1) ^ (dv + 1) - have hn (φ : CNF ℕ) : φ.distinctVars.length ≤ size φ := by - rw [CNF.length_distinctVars] - exact φ.numVars_le_length_vars.trans (SAT.length_vars_le φ) - have hstate : ∀ φ, ∀ k ≤ 2 ^ φ.distinctVars.length, - (encState (step^[k] (init φ))).length ≤ B φ := by - intro φ k hk - have hK := ComputableTidilyInO.length_encNat_mono hk - rw [encNat_two_pow] at hK - have hV := hvs φ - have h₁ : size φ + 1 ≤ (size φ + 1) ^ (dv + 1) := by - simpa using Nat.pow_le_pow_right (Nat.succ_pos (size φ)) (Nat.le_add_left 1 dv) - have h₂ : (size φ + 1) ^ dv ≤ (size φ + 1) ^ (dv + 1) := - Nat.pow_le_pow_right (Nat.succ_pos _) (Nat.le_succ dv) - have h₃ := Nat.mul_le_mul_left cv h₂ - have h₄ := hn φ - rw [iterate_step_init] - simp only [List.length_append, List.length_replicate, List.length_singleton] at hK - simp only [encState, length_encPair, encBool_apply, List.length_singleton, B, size] - at hV h₁ h₃ h₄ ⊢ - nlinarith - have hiter := ComputableTidilyInO.iterate hcount.inO hinit.inO hstep.inO - (R := fun φ => (B φ + 1) ^ d) (Q := fun φ => (B φ + 1) ^ d) (B := B) - (fun φ k hk => Nat.pow_le_pow_left (Nat.add_le_add_right (hstate φ k hk) 1) d) - (fun φ k hk => Nat.pow_le_pow_left (Nat.add_le_add_right (hstate φ k hk) 1) d) hstate - have h := hans.inO.comp hiter - have hB : PolyBounded size B := .of_forall_le (2 * cv + 13) (dv + 1) fun φ => le_rfl - have hpow (j : ℕ) : PolyBounded size fun φ => (B φ + 1) ^ j := - ((PolyBounded.of_polynomiallyBounded id (bound := fun x => (x + 1) ^ j) (by fun_prop)).comp - hB).mono fun φ => le_rfl - have hL (j : ℕ) : PolyBounded size fun φ => (size φ + 1) ^ j := - .of_forall_le 1 j fun φ => by simp - obtain ⟨c, e, hT⟩ := exists_le_mul_two_pow_of_polyBounded (size := size) (μ := CNF.numVars) - ((hpow d).add (hB.add (.of_forall_le 4 2 fun φ => le_rfl))) - ((hL d₁).add ((hL d₀).add (hpow d₂))) - (T := fun φ => ((encCNF φ).length + 1) ^ d₁ + ((encCNF φ).length + 1) ^ d₀ + - (2 ^ φ.distinctVars.length + 1) * ((B φ + 1) ^ d + B φ + - ((encNat (2 ^ φ.distinctVars.length)).length + 1) ^ 2) + - ((encState (step^[2 ^ φ.distinctVars.length] (init φ))).length + 1) ^ d₂) - (fun φ => by - have hK : ((encNat (2 ^ φ.distinctVars.length)).length + 1) ^ 2 ≤ - 4 * (size φ + 1) ^ 2 := by - rw [encNat_two_pow] - simp only [List.length_append, List.length_replicate, List.length_singleton] - calc (φ.distinctVars.length + 1 + 1) ^ 2 ≤ (2 * (size φ + 1)) ^ 2 := - Nat.pow_le_pow_left (by have := hn φ; omega) 2 - _ = 4 * (size φ + 1) ^ 2 := by ring - have hS := Nat.pow_le_pow_left (Nat.add_le_add_right (hstate φ _ le_rfl) 1) d₂ - rw [CNF.length_distinctVars] at hK hS ⊢ - have := Nat.mul_le_mul_left (2 ^ φ.numVars + 1) - (Nat.add_le_add_left hK ((B φ + 1) ^ d + B φ)) - simp only [size] at this hS ⊢ - nlinarith) - refine ⟨e, (h.mono c (fun φ => ?_) fun φ => ?_).of_enc_eq fun φ => rfl⟩ - all_goals - have h₁ := hT φ - simp only [size] at h₁ - generalize 2 ^ φ.distinctVars.length = N at h₁ ⊢ - generalize (encNat N).length = K at h₁ ⊢ - obtain ⟨X, hX⟩ : ∃ X, (B φ + 1) ^ d + B φ = X := ⟨_, rfl⟩ - rw [hX] at h₁ - have h₂ : K ≤ (K + 1) ^ 2 := by nlinarith - have h₃ : X + (K + 1) ^ 2 ≤ (N + 1) * (X + (K + 1) ^ 2) := Nat.le_mul_of_pos_left _ (by omega) - nlinarith - simpa only [computableInO_iff_computableTidilyInO] using this - end BruteForce +open ComputableTidilyInPolyTime in /-- **`SAT` by exhaustive search**: `SAT` is decidable within time `2 ^ n` times a polynomial in the length of the encoded formula, on formulas with `n` variables. -/ theorem SAT_decidableInExpTime_one : DecidableInExpTime SAT encCNF CNF.numVars 1 := by - obtain ⟨e, h⟩ := BruteForce.exists_computableInO_search - refine DecidableInExpTime.of_computableInO h (fun φ => (BruteForce.search_eq_true_iff φ).symm) 1 e - fun φ => ?_ - rw [one_mul, Real.rpow_natCast] - push_cast - rw [one_mul] + have hB : DecidableInExpTime + {p : (CNF ℕ × List ℕ) × ℕ | p.1.1.eval (bitsAssignment p.1.2 p.2) = true} + (encPair (encPair encCNF (encList encNat)) encNat) (fun _ => 0) 0 := + .of_computableInPolyTime computableInPolyTime_eval_bitsAssignment (fun _ => Iff.rfl) + have hf : ComputableInPolyTime + (fun q : CNF ℕ × ℕ => ((q.1, q.1.distinctVars), q.2)) + (encPair encCNF encNat) (encPair (encPair encCNF (encList encNat)) encNat) := by + have := SAT.computableInPolyTime_distinctVars.tidy + exact .of_tidy (by fun_prop) + have hν : ComputableInPolyTime CNF.numVars encCNF encUnary := by + have := SAT.computableInPolyTime_distinctVars.tidy + refine .of_tidy ?_ + have heq : (CNF.numVars : CNF ℕ → ℕ) = fun φ => φ.distinctVars.length := by + funext φ; exact φ.length_distinctVars.symm + rw [heq] + fun_prop + have hfA (φ : CNF ℕ) : φ ∈ SAT ↔ ∃ r < 2 ^ φ.numVars, + ((φ, φ.distinctVars), r) ∈ + {p : (CNF ℕ × List ℕ) × ℕ | p.1.1.eval (bitsAssignment p.1.2 p.2) = true} := by + rw [mem_SAT, ← φ.length_distinctVars, + CNF.satisfiable_iff_exists_bitsAssignment fun v hv => CNF.mem_distinctVars.mpr hv] + rfl + simpa using hB.of_exhaustiveSearch hf hν hfA (c := 0) (fun _ _ => Nat.zero_le _) + (M := 1) (K := 0) (fun φ => by simp) le_rfl open ComputableTidilyInPolyTime in /-- Checking that every clause has at most `k` literals is polynomial-time. -/ diff --git a/Complexity/Computability/Complexity/FineGrained/ExhaustiveSearch.lean b/Complexity/Computability/Complexity/FineGrained/ExhaustiveSearch.lean new file mode 100644 index 0000000000..4601192455 --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/ExhaustiveSearch.lean @@ -0,0 +1,459 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.FineGrained +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower + +/-! +# Exhaustive-search reductions + +Exponential and subexponential time bounds transfer along Turing reductions that branch over +$2^{\nu(a)}$ polynomial-time subinstances $f(a, r)$ (`r < 2 ^ ν a`), implemented by iterating a +polynomial-time step with a binary counter (`Turing.MultiTapeTM.ComputableTidilyInO.iterate`): +* `Cslib.Complexity.DecidableInExpTime.of_computableInPolyTime`: a set decided in polynomial time is + decidable within exponential time with exponent `0`. +* `Cslib.Complexity.DecidableInExpTime.of_exhaustiveSearch`: if + $a \in A \iff \exists r < 2^{\nu(a)}, f(a, r) \in B$, $\mu_B(f(a, r)) \le c \cdot \mu_A(a) + c$, + and $\nu(a) \le \mu_A(a) / M + K$, then a decider for $B$ within time + $2^{\delta \mu_B(b)} \cdot \mathrm{poly}(|b|)$ gives a decider for $A$ within time + $2^{(1 / M + c \delta) \mu_A(a)} \cdot \mathrm{poly}(|a|)$. +* `Cslib.Complexity.DecidableInSubexpTime.of_exhaustiveSearch`: when $\nu(a) \le \mu_A(a) / M + K_M$ + for every $M \ge 1$, subexponential time for $B$ in $\mu_B$ gives subexponential time for $A$ in + $\mu_A$. + +## Main results + +* `Cslib.Complexity.DecidableInExpTime.of_computableInPolyTime`: polynomial-time predicates have + exponential-time exponent `0`. +* `Cslib.Complexity.DecidableInExpTime.of_exhaustiveSearch`, + `Cslib.Complexity.DecidableInSubexpTime.of_exhaustiveSearch`: exponential and subexponential time + transfer along exhaustive-search reductions. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, Section 2.3][AroraBarak09] +* [R. Impagliazzo, R. Paturi, *On the complexity of k-SAT*][ImpagliazzoPaturi2001] +-/ + +public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +variable {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} + {A : Set α} {B : Set β} {μA : α → ℕ} {μB : β → ℕ} + +/-- A set decided by a polynomial-time predicate is decidable within exponential time with exponent +`0` for any parameter `μ`. -/ +theorem DecidableInExpTime.of_computableInPolyTime {μ : α → ℕ} {p : α → Bool} + (hp : ComputableInPolyTime p encA encBool) (hA : ∀ a, a ∈ A ↔ p a = true) : + DecidableInExpTime A encA μ 0 := by + obtain ⟨d, _, hp'⟩ := hp.tidy.exists_degree + refine DecidableInExpTime.of_computableInO (.of_tidy hp'.inO) hA 1 d fun a => ?_ + simp + +namespace ExhaustiveSearch + +private abbrev State (α : Type) : Type := (α × ℕ) × Bool + +private def encState (encA : α ↪ List Bool) : State α ↪ List Bool := + encPair (encPair encA encNat) encBool + +private def init (a : α) : State α := ((a, 0), false) + +private def step (f : α × ℕ → β) (g : β → Bool) (s : State α) : State α := + ((s.1.1, s.1.2 + 1), s.2 || g (f s.1)) + +private def rounds (ν : α → ℕ) (a : α) : ℕ := 2 ^ ν a + +private def search (f : α × ℕ → β) (ν : α → ℕ) (g : β → Bool) (a : α) : Bool := + ((step f g)^[rounds ν a] (init a)).2 + +private theorem iterate_step_init (f : α × ℕ → β) (g : β → Bool) (a : α) (k : ℕ) : + (step f g)^[k] (init a) = + ((a, k), (List.range k).any fun r => g (f (a, r))) := by + induction k with + | zero => rfl + | succ k ih => + rw [Function.iterate_succ_apply', ih, step, List.range_succ, List.any_append, + List.any_cons, List.any_nil, Bool.or_false] + +private theorem search_eq_true_iff {f : α × ℕ → β} {ν : α → ℕ} {g : β → Bool} + (hfA : ∀ a, a ∈ A ↔ ∃ r < 2 ^ ν a, f (a, r) ∈ B) + (hg : ∀ b, g b = true ↔ b ∈ B) (a : α) : + search f ν g a = true ↔ a ∈ A := by + rw [search, iterate_step_init, List.any_eq_true, hfA] + simp only [List.mem_range, hg, rounds] + +open ComputableTidilyInPolyTime in +private theorem computableTidilyInPolyTime_init : + ComputableTidilyInPolyTime init encA (encState encA) := by + unfold init encState + fun_prop + +open ComputableTidilyInPolyTime in +private theorem computableTidilyInPolyTime_rounds {ν : α → ℕ} + (hν : ComputableTidilyInPolyTime ν encA encUnary) : + ComputableTidilyInPolyTime (rounds ν) encA encNat := + binary_two_pow.comp hν + +open ComputableTidilyInPolyTime in +private theorem exists_computableTidilyInO_step {f : α × ℕ → β} + (hf : ComputableTidilyInPolyTime f (encPair encA encNat) encB) + {g : β → Bool} {t : β → ℕ} + (hg : ComputableTidilyInO g encB encBool t t) : + ∃ d, ComputableTidilyInO (step f g) (encState encA) (encState encA) + (fun s => ((encState encA s).length + 1) ^ d + t (f s.1)) + (fun s => ((encState encA s).length + 1) ^ d + t (f s.1)) := by + obtain ⟨dN, eN, hN⟩ := (show ComputableTidilyInPolyTime (fun s : State α => (s.1.1, s.1.2 + 1)) + (encState encA) (encPair encA encNat) by unfold encState; fun_prop).exists_degree + obtain ⟨dB, eB, hB⟩ := (show ComputableTidilyInPolyTime (fun s : State α => s.2) + (encState encA) encBool by unfold encState; fun_prop).exists_degree + obtain ⟨dR, eR, hR⟩ := (hf.comp (show ComputableTidilyInPolyTime (fun s : State α => s.1) + (encState encA) (encPair encA encNat) by unfold encState; fun_prop)).exists_degree + obtain ⟨dO, eO, hO⟩ := bool_or.exists_degree + set D := dN + dB + dR + have hN' := (hN.mono (d' := D) (e' := eN) (by omega) le_rfl).inO + have hB' := (hB.mono (d' := D) (e' := eB) (by omega) le_rfl).inO + have hR' := (hR.mono (d' := D) (e' := eR) (by omega) le_rfl).inO + have h := hN'.prod (hO.inO.comp (hB'.prod (hg.comp hR'))) + have h4 (p : Bool × Bool) : (encPair encBool encBool p).length = 4 := by simp + refine ⟨D, (h.mono (5 ^ dO + 4) (fun s => ?_) (fun s => ?_)).of_enc_eq fun _ => rfl⟩ <;> + · simp only [Function.comp_apply, h4] + generalize ((encState encA s).length + 1) ^ D = P + generalize t (f s.1) = T + have hF : 1 ≤ (4 + 1) ^ dO := Nat.one_le_pow _ _ (by norm_num) + generalize (4 + 1) ^ dO = F at hF ⊢ + nlinarith + +private theorem exists_state_and_node_bounds {f : α × ℕ → β} {ν : α → ℕ} + (hf : ComputableTidilyInPolyTime f (encPair encA encNat) encB) + (hν : ComputableTidilyInPolyTime ν encA encUnary) : + ∃ (c_st d_st c_nd d_nd : ℕ), + (∀ (g : β → Bool) (a : α) (k : ℕ), + k ≤ rounds ν a → + (encState encA ((step f g)^[k] (init a))).length ≤ c_st * ((encA a).length + 1) ^ d_st) ∧ + (∀ (a : α), + (encNat (rounds ν a)).length + 1 ≤ c_st * ((encA a).length + 1) ^ d_st) ∧ + (∀ (a : α) (k : ℕ), + k ≤ rounds ν a → + (encB (f (a, k))).length ≤ c_nd * ((encA a).length + 1) ^ d_nd) := by + obtain ⟨c_ν, d_ν, hν_len⟩ := hν.polyBounded_length.exists_le + obtain ⟨cb, db, hf_len⟩ := hf.polyBounded_length.exists_le + set d_st := d_ν + 1 + set c_p := 2 * c_ν + 4 + set c_st := 2 * c_p + 4 + have hpair_le (a : α) {k : ℕ} (hk : k ≤ rounds ν a) : + (encPair encA encNat (a, k)).length ≤ c_p * ((encA a).length + 1) ^ d_st := by + set L := (encA a).length + have hK := ComputableTidilyInO.length_encNat_mono hk + rw [rounds, encNat_two_pow, List.length_append, List.length_replicate, + List.length_singleton] at hK + have hνa : ν a ≤ c_ν * (L + 1) ^ d_ν := by + simpa only [encUnary_apply, List.length_replicate] using hν_len a + have hd1 : (L + 1) ^ d_ν ≤ (L + 1) ^ d_st := + Nat.pow_le_pow_right (Nat.succ_pos L) (Nat.le_succ d_ν) + have hd2 : L + 1 ≤ (L + 1) ^ d_st := by + simpa only [pow_one] using Nat.pow_le_pow_right (Nat.succ_pos L) (Nat.succ_pos d_ν) + have hνa' : ν a ≤ c_ν * (L + 1) ^ d_st := hνa.trans (Nat.mul_le_mul_left c_ν hd1) + simp only [length_encPair, L, c_p] + nlinarith + refine ⟨c_st, d_st, cb * (c_p + 1) ^ db, d_st * db, + fun g a k hk => ?_, fun a => ?_, fun a k hk => ?_⟩ + · rw [iterate_step_init, encState, length_encPair] + have hp := hpair_le a hk + have h1 : 1 ≤ ((encA a).length + 1) ^ d_st := Nat.one_le_pow _ _ (Nat.succ_pos _) + simp only [encBool_apply, List.length_singleton, c_st] + nlinarith + · set L := (encA a).length + rw [rounds, encNat_two_pow, List.length_append, List.length_replicate, List.length_singleton] + have hνa : ν a ≤ c_ν * (L + 1) ^ d_ν := by + simpa only [encUnary_apply, List.length_replicate] using hν_len a + have hd1 : (L + 1) ^ d_ν ≤ (L + 1) ^ d_st := + Nat.pow_le_pow_right (Nat.succ_pos L) (Nat.le_succ d_ν) + have h1 : 1 ≤ (L + 1) ^ d_st := Nat.one_le_pow _ _ (Nat.succ_pos L) + have hνa' : ν a ≤ c_ν * (L + 1) ^ d_st := hνa.trans (Nat.mul_le_mul_left c_ν hd1) + simp only [c_st, c_p, L] + nlinarith + · have h1 := hf_len (a, k) + have h2 := hpair_le a hk + have h3 : (encPair encA encNat (a, k)).length + 1 ≤ + (c_p + 1) * ((encA a).length + 1) ^ d_st := by + have : 1 ≤ ((encA a).length + 1) ^ d_st := Nat.one_le_pow _ _ (Nat.succ_pos _) + nlinarith + calc (encB (f (a, k))).length + ≤ cb * ((encPair encA encNat (a, k)).length + 1) ^ db := h1 + _ ≤ cb * ((c_p + 1) * ((encA a).length + 1) ^ d_st) ^ db := + Nat.mul_le_mul_left cb (Nat.pow_le_pow_left h3 db) + _ = cb * (c_p + 1) ^ db * ((encA a).length + 1) ^ (d_st * db) := by + rw [mul_pow, ← pow_mul, ← mul_assoc] + +private noncomputable def leafTime (encA : α ↪ List Bool) (μA : α → ℕ) + (c_mu c_nd d_nd : ℕ) (δ : ℝ) (c e : ℕ) (a : α) : ℕ := + ⌈(c : ℝ) * (2 ^ (δ * ((c_mu * μA a + c_mu : ℕ) : ℝ)) * + ((c_nd * ((encA a).length + 1) ^ d_nd : ℕ) + 1 : ℝ) ^ e) + c⌉₊ + +end ExhaustiveSearch + +open ExhaustiveSearch in +/-- **Exponential-time transfer along an exhaustive search.** If +$f : \alpha \times \mathbb{N} \to \beta$ and $\nu : \alpha \to \mathbb{N}$ are computable in +polynomial time (with $\nu$ in unary), $a \in A \iff \exists r < 2^{\nu(a)},\, f(a, r) \in B$, +$\mu_B(f(a, r)) \le c \cdot \mu_A(a) + c$, and $\nu(a) \le \mu_A(a) / M + K$, then a decider for $B$ +within time $2^{\delta \mu_B(b)} \cdot \mathrm{poly}(|b|)$ yields a decider for $A$ within time +$2^{(1 / M + c \delta) \mu_A(a)} \cdot \mathrm{poly}(|a|)$. -/ +theorem DecidableInExpTime.of_exhaustiveSearch {f : α × ℕ → β} {ν : α → ℕ} + (hf : ComputableInPolyTime f (encPair encA encNat) encB) + (hν : ComputableInPolyTime ν encA encUnary) + (hfA : ∀ a, a ∈ A ↔ ∃ r < 2 ^ ν a, f (a, r) ∈ B) {c : ℕ} + (hμ : ∀ a r, μB (f (a, r)) ≤ c * μA a + c) {M K : ℕ} + (hνM : ∀ a, ν a ≤ μA a / M + K) {δ : ℝ} (hδ : 0 ≤ δ) + (h : DecidableInExpTime B encB μB δ) : + DecidableInExpTime A encA μA (1 / M + c * δ) := by + rcases isEmpty_or_nonempty α with hα | hα + · exact DecidableInExpTime.of_computableInO (.of_tidy (.const false)) + (fun a => hα.elim a) 1 0 (fun a => hα.elim a) + obtain ⟨a₀⟩ := hα + have : Inhabited α := ⟨a₀⟩ + have hf_tidy := hf.tidy + have hν_tidy := hν.tidy + obtain ⟨e, h⟩ := h + obtain ⟨g, t, k_dec, hg, hgB, ht⟩ := h.exists_computableInO + have hg := hg.tidy + obtain ⟨d, hstep⟩ := exists_computableTidilyInO_step hf_tidy hg + obtain ⟨dn, _, hn⟩ := (computableTidilyInPolyTime_rounds hν_tidy).exists_degree + obtain ⟨di, _, hi⟩ := (computableTidilyInPolyTime_init (encA := encA)).exists_degree + obtain ⟨da, _, ha⟩ := (show ComputableTidilyInPolyTime (fun s : State α => s.2) + (encState encA) encBool by unfold encState; fun_prop).exists_degree + obtain ⟨c_st, d_st, c_nd, d_nd, hst_bound, hrounds_len, hnd_bound⟩ := + exists_state_and_node_bounds hf_tidy hν_tidy + set stBound : α → ℕ := fun a => c_st * ((encA a).length + 1) ^ d_st + set ndBound : α → ℕ := fun a => c_nd * ((encA a).length + 1) ^ d_nd + have hround (a : α) (k : ℕ) (hk : k ≤ rounds ν a) : + ((encState encA ((step f g)^[k] (init a))).length + 1) ^ d + + t (f ((step f g)^[k] (init a)).1) ≤ + (stBound a + 1) ^ d + leafTime encA μA c c_nd d_nd δ k_dec e a := by + have hS : (encState encA ((step f g)^[k] (init a))).length ≤ stBound a := + hst_bound g a k hk + refine Nat.add_le_add (Nat.pow_le_pow_left (by omega) d) ?_ + rw [iterate_step_init] + dsimp only + set b := f (a, k) + have hb_mu : μB b ≤ c * μA a + c := hμ a k + have hb_enc : (encB b).length ≤ ndBound a := hnd_bound a k hk + have h₁ : (2 : ℝ) ^ (δ * μB b) ≤ 2 ^ (δ * ((c * μA a + c : ℕ) : ℝ)) := + Real.rpow_le_rpow_of_exponent_le (by norm_num) + (mul_le_mul_of_nonneg_left (by exact_mod_cast hb_mu) hδ) + have h₂ : (((encB b).length : ℝ) + 1) ^ e ≤ ((ndBound a : ℝ) + 1) ^ e := + pow_le_pow_left₀ (by positivity) (by exact_mod_cast Nat.add_le_add_right hb_enc 1) e + have h₃ := mul_le_mul h₁ h₂ (by positivity) (by positivity) + have h₄ := mul_le_mul_of_nonneg_left h₃ (Nat.cast_nonneg k_dec : (0 : ℝ) ≤ k_dec) + have h₅ := (ht b).trans (add_le_add h₄ le_rfl) + exact Nat.cast_le.mp (h₅.trans (Nat.le_ceil _)) + have hstate (a : α) (k : ℕ) (hk : k ≤ rounds ν a) : + (encState encA ((step f g)^[k] (init a))).length ≤ stBound a := + hst_bound g a k hk + have hiter := ComputableTidilyInO.iterate hn.inO hi.inO hstep hround hround hstate + have hsearch := ha.inO.comp hiter + set C₁ := (c_st + 1) ^ d + c_st + c_st ^ 2 + set C₃ := (c_st + 1) ^ da + set E := dn + di + d_st * d + d_st * da + d_nd * e + 2 * d_st + set C₂ : ℝ := k_dec * 2 ^ (c * δ) * ((c_nd : ℝ) + 1) ^ e + k_dec + 1 + set C₀ : ℝ := 3 + C₃ + (2 ^ K + 1 : ℝ) * (C₁ + C₂) + refine DecidableInExpTime.of_computableInO (.of_tidy hsearch) + (fun a => (search_eq_true_iff hfA (fun b => (hgB b).symm) a).symm) ⌈C₀⌉₊ E fun a => ?_ + set L := (encA a).length + set N := μA a + set P := (L + 1) ^ E + have hP (m : ℕ) (hm : m ≤ E) : (L + 1) ^ m ≤ P := Nat.pow_le_pow_right (Nat.succ_pos L) hm + have hsb : stBound a = c_st * (L + 1) ^ d_st := rfl + have hr : rounds ν a + 1 ≤ (2 ^ K + 1) * 2 ^ (N / M) := by + have h1 := hνM a + have h2 : rounds ν a ≤ 2 ^ K * 2 ^ (N / M) := by + calc rounds ν a = 2 ^ ν a := rfl + _ ≤ 2 ^ (N / M + K) := Nat.pow_le_pow_right two_pos h1 + _ = 2 ^ K * 2 ^ (N / M) := by rw [pow_add, Nat.mul_comm] + have h3 : 1 ≤ 2 ^ (N / M) := Nat.one_le_two_pow + nlinarith + have hpoly : (L + 1) ^ dn + (L + 1) ^ di ≤ 2 * P := by + have := hP dn (by omega) + have := hP di (by omega) + omega + have hans_le : + ((encState encA ((step f g)^[rounds ν a] (init a))).length + 1) ^ da ≤ C₃ * P := by + have h1 := hstate a (rounds ν a) le_rfl + have h2 : stBound a + 1 ≤ (c_st + 1) * (L + 1) ^ d_st := by + have : 1 ≤ (L + 1) ^ d_st := Nat.one_le_pow _ _ (Nat.succ_pos L) + rw [hsb] + nlinarith + calc ((encState encA ((step f g)^[rounds ν a] (init a))).length + 1) ^ da + ≤ (stBound a + 1) ^ da := Nat.pow_le_pow_left (by omega) da + _ ≤ ((c_st + 1) * (L + 1) ^ d_st) ^ da := Nat.pow_le_pow_left h2 da + _ = C₃ * (L + 1) ^ (d_st * da) := by simp only [C₃, mul_pow, ← pow_mul] + _ ≤ C₃ * P := Nat.mul_le_mul_left C₃ (hP (d_st * da) (by omega)) + have hrnd : (stBound a + 1) ^ d + stBound a + + ((encNat (rounds ν a)).length + 1) ^ 2 ≤ C₁ * P := by + have h1 : (stBound a + 1) ^ d ≤ (c_st + 1) ^ d * (L + 1) ^ (d_st * d) := by + have hst1 : stBound a + 1 ≤ (c_st + 1) * (L + 1) ^ d_st := by + have : 1 ≤ (L + 1) ^ d_st := Nat.one_le_pow _ _ (Nat.succ_pos L) + rw [hsb] + nlinarith + calc (stBound a + 1) ^ d ≤ ((c_st + 1) * (L + 1) ^ d_st) ^ d := Nat.pow_le_pow_left hst1 d + _ = (c_st + 1) ^ d * (L + 1) ^ (d_st * d) := by rw [mul_pow, ← pow_mul] + have h2 : ((encNat (rounds ν a)).length + 1) ^ 2 ≤ c_st ^ 2 * (L + 1) ^ (d_st * 2) := by + have hr_len := hrounds_len a + calc ((encNat (rounds ν a)).length + 1) ^ 2 + ≤ (c_st * (L + 1) ^ d_st) ^ 2 := Nat.pow_le_pow_left hr_len 2 + _ = c_st ^ 2 * (L + 1) ^ (d_st * 2) := by rw [mul_pow, ← pow_mul] + have h3 := hP (d_st * d) (by omega) + have h4 := hP d_st (by omega) + have h5 := hP (d_st * 2) (by omega) + calc (stBound a + 1) ^ d + stBound a + ((encNat (rounds ν a)).length + 1) ^ 2 + ≤ (c_st + 1) ^ d * P + c_st * P + c_st ^ 2 * P := by + have := h1.trans (Nat.mul_le_mul_left ((c_st + 1) ^ d) h3) + have := (le_of_eq hsb).trans (Nat.mul_le_mul_left c_st h4) + have := h2.trans (Nat.mul_le_mul_left (c_st ^ 2) h5) + omega + _ = C₁ * P := by simp only [C₁]; ring + set Y : ℝ := 2 ^ ((c * δ) * N) + have hY : 1 ≤ Y := Real.one_le_rpow (by norm_num) (by positivity) + have hP1 : (1 : ℝ) ≤ P := by exact_mod_cast Nat.one_le_pow _ _ (Nat.succ_pos L) + have hleaf : (leafTime encA μA c c_nd d_nd δ k_dec e a : ℝ) ≤ C₂ * Y * P := by + have h₁ : (2 : ℝ) ^ (δ * ((c * N + c : ℕ) : ℝ)) = 2 ^ (c * δ) * Y := by + rw [← Real.rpow_add (by norm_num)] + congr 1 + push_cast + ring + have h₂ : ((ndBound a : ℝ) + 1) ^ e ≤ ((c_nd : ℝ) + 1) ^ e * P := by + have hnb_le : (ndBound a : ℝ) + 1 ≤ ((c_nd : ℝ) + 1) * ((L : ℝ) + 1) ^ d_nd := by + have hnb_eq : (ndBound a : ℝ) = c_nd * ((L : ℝ) + 1) ^ d_nd := by + simp only [ndBound] + push_cast + ring + have hpow1 : (1 : ℝ) ≤ ((L : ℝ) + 1) ^ d_nd := + one_le_pow₀ (by linarith [(L.cast_nonneg : (0 : ℝ) ≤ L)]) + nlinarith + calc ((ndBound a : ℝ) + 1) ^ e ≤ (((c_nd : ℝ) + 1) * ((L : ℝ) + 1) ^ d_nd) ^ e := + pow_le_pow_left₀ (by positivity) hnb_le e + _ = ((c_nd : ℝ) + 1) ^ e * ((L : ℝ) + 1) ^ (d_nd * e) := by rw [mul_pow, ← pow_mul] + _ ≤ ((c_nd : ℝ) + 1) ^ e * P := by + refine mul_le_mul_of_nonneg_left ?_ (by positivity) + exact_mod_cast hP (d_nd * e) (by omega) + have h₃ := Nat.ceil_lt_add_one (show (0 : ℝ) ≤ (k_dec : ℝ) * (2 ^ (δ * ((c * N + c : ℕ) : ℝ)) * + ((ndBound a : ℝ) + 1) ^ e) + k_dec by positivity) + unfold leafTime + change (⌈(k_dec : ℝ) * (2 ^ (δ * ((c * N + c : ℕ) : ℝ)) * + ((ndBound a : ℝ) + 1) ^ e) + k_dec⌉₊ : ℝ) ≤ _ + rw [h₁] at h₃ ⊢ + have h₄ : (k_dec : ℝ) * (2 ^ (c * δ) * Y * ((ndBound a : ℝ) + 1) ^ e) ≤ + k_dec * 2 ^ (c * δ) * ((c_nd : ℝ) + 1) ^ e * Y * P := by + have := mul_le_mul_of_nonneg_left h₂ (by positivity : (0 : ℝ) ≤ k_dec * 2 ^ (c * δ) * Y) + nlinarith + have h₅ : (k_dec : ℝ) + 1 ≤ ((k_dec : ℝ) + 1) * Y * P := by + have : (1 : ℝ) ≤ Y * P := one_le_mul_of_one_le_of_one_le hY hP1 + nlinarith + calc (⌈(k_dec : ℝ) * (2 ^ (c * δ) * Y * ((ndBound a : ℝ) + 1) ^ e) + k_dec⌉₊ : ℝ) + ≤ (k_dec : ℝ) * (2 ^ (c * δ) * Y * ((ndBound a : ℝ) + 1) ^ e) + k_dec + 1 := h₃.le + _ ≤ C₂ * Y * P := by simp only [C₂]; nlinarith + set X : ℝ := 2 ^ ((1 / M : ℝ) * N) + have hX : ((2 ^ (N / M) : ℕ) : ℝ) ≤ X := by + rw [Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_natCast] + refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ + rw [one_div_mul_eq_div] + exact Nat.cast_div_le + have hX1 : 1 ≤ X := Real.one_le_rpow (by norm_num) (by positivity) + have hXY : X * Y = 2 ^ ((1 / M + c * δ) * N) := by + rw [← Real.rpow_add (by norm_num)] + ring_nf + have hT : ((L + 1) ^ dn + (L + 1) ^ di + + (rounds ν a + 1) * ((stBound a + 1) ^ d + leafTime encA μA c c_nd d_nd δ k_dec e a + + stBound a + ((encNat (rounds ν a)).length + 1) ^ 2) + + ((encState encA ((step f g)^[rounds ν a] (init a))).length + 1) ^ da : ℝ) ≤ + (2 + C₃ : ℝ) * P + (2 ^ K + 1 : ℝ) * X * (C₁ * P + C₂ * Y * P) := by + have h₁ : ((L + 1) ^ dn + (L + 1) ^ di : ℝ) ≤ 2 * P := by exact_mod_cast hpoly + have h₁' : + (((encState encA ((step f g)^[rounds ν a] (init a))).length + 1) ^ da : ℝ) ≤ C₃ * P := by + exact_mod_cast hans_le + have h₂ : ((rounds ν a + 1 : ℕ) : ℝ) ≤ (2 ^ K + 1 : ℝ) * X := by + have : ((rounds ν a + 1 : ℕ) : ℝ) ≤ (((2 ^ K + 1) * 2 ^ (N / M) : ℕ) : ℝ) := by + exact_mod_cast hr + rw [Nat.cast_mul] at this + have hKM : (0 : ℝ) ≤ (2 ^ K + 1 : ℕ) := Nat.cast_nonneg _ + have hmul := mul_le_mul_of_nonneg_left hX hKM + push_cast at this hmul ⊢ + linarith + have h₃ : (((stBound a + 1) ^ d + stBound a + + ((encNat (rounds ν a)).length + 1) ^ 2 : ℕ) : ℝ) ≤ C₁ * P := by exact_mod_cast hrnd + have h₄ : (((stBound a + 1) ^ d + leafTime encA μA c c_nd d_nd δ k_dec e a + stBound a + + ((encNat (rounds ν a)).length + 1) ^ 2 : ℕ) : ℝ) ≤ C₁ * P + C₂ * Y * P := by + push_cast at h₃ ⊢ + linarith + have h₅ := mul_le_mul h₂ h₄ (by positivity) (by positivity) + push_cast at h₁ h₁' h₅ ⊢ + linarith + calc _ ≤ (2 + C₃ : ℝ) * P + (2 ^ K + 1 : ℝ) * X * (C₁ * P + C₂ * Y * P) := by + exact_mod_cast hT + _ ≤ C₀ * (X * Y * P) := by + have hXY1 : 1 ≤ X * Y := one_le_mul_of_one_le_of_one_le hX1 hY + have hC₂ : 0 ≤ C₂ := by positivity + have hC₁ : (0 : ℝ) ≤ C₁ := by positivity + have hC₃ : (0 : ℝ) ≤ C₃ := by positivity + have hKM : (0 : ℝ) ≤ 2 ^ K + 1 := by positivity + have hP0 : (0 : ℝ) ≤ P := by positivity + have a₁ : (P : ℝ) ≤ X * Y * P := le_mul_of_one_le_left hP0 hXY1 + have a₂ : X * P ≤ X * Y * P := by + have := mul_le_mul_of_nonneg_left hY (by positivity : (0 : ℝ) ≤ X * P) + linarith [show X * P * Y = X * Y * P by ring] + have a₃ := mul_le_mul_of_nonneg_left a₂ (mul_nonneg hKM hC₁) + have a₄ := mul_le_mul_of_nonneg_left a₁ hC₃ + simp only [C₀] + nlinarith + _ ≤ ⌈C₀⌉₊ * (2 ^ ((1 / M + c * δ) * N) * ((L : ℝ) + 1) ^ E) := by + rw [← hXY] + push_cast [P] + exact mul_le_mul_of_nonneg_right (Nat.le_ceil C₀) (by positivity) + +/-- **Subexponential-time transfer along an exhaustive search with sublinear branch exponent.** If +$f : \alpha \times \mathbb{N} \to \beta$ and $\nu : \alpha \to \mathbb{N}$ are computable in +polynomial time (with $\nu$ in unary), $a \in A \iff \exists r < 2^{\nu(a)},\, f(a, r) \in B$, +$\mu_B(f(a, r)) \le c \cdot \mu_A(a) + c$, and for every $M \ge 1$ there is a constant $K$ with +$\nu(a) \le \mu_A(a) / M + K$, then subexponential time for $B$ in $\mu_B$ gives subexponential time +for $A$ in $\mu_A$. -/ +theorem DecidableInSubexpTime.of_exhaustiveSearch {f : α × ℕ → β} {ν : α → ℕ} + (hf : ComputableInPolyTime f (encPair encA encNat) encB) + (hν : ComputableInPolyTime ν encA encUnary) + (hfA : ∀ a, a ∈ A ↔ ∃ r < 2 ^ ν a, f (a, r) ∈ B) {c : ℕ} + (hμ : ∀ a r, μB (f (a, r)) ≤ c * μA a + c) + (hνM : ∀ M > 0, ∃ K, ∀ a, ν a ≤ μA a / M + K) + (h : DecidableInSubexpTime B encB μB) : + DecidableInSubexpTime A encA μA := by + intro ε hε + obtain ⟨M, hM⟩ := exists_nat_gt (2 / ε) + have hMpos : (0 : ℝ) < M := lt_trans (by positivity) hM + have hM_nat : 0 < M := Nat.cast_pos.mp hMpos + obtain ⟨K, hK⟩ := hνM M hM_nat + have hMε : 1 / (M : ℝ) < ε / 2 := by + rw [div_lt_iff₀ hMpos] + rw [div_lt_iff₀ hε] at hM + linarith + set δ : ℝ := ε / (2 * (c + 1)) + 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 + linarith + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean b/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean index a1baaac301..cdd8f1e3ea 100644 --- a/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean +++ b/Complexity/Computability/Complexity/FineGrained/PermutationIndependentSet.lean @@ -8,17 +8,15 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.FineGrained.GraphProblems -public import Complexity.Foundations.Data.BitString.List -public import Complexity.Foundations.Data.BitString.List.Binary -public import Mathlib.Data.Fin.Tuple.Sort -import Complexity.Computability.Complexity.FineGrained.Assignment -import Complexity.Computability.Complexity.FineGrained.BruteForce -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch +import Complexity.Foundations.Data.BitString.List +import Complexity.Foundations.Data.BitString.List.Binary import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log +import Mathlib.Data.Fin.Tuple.Sort import Mathlib.Data.List.GetD import Mathlib.Data.Nat.Bitwise @@ -59,12 +57,13 @@ To prove [LokshtanovMarxSaurabh2018, Theorem 2.11], this library gives a direct from `ThreeColoring` on $N$-vertex graphs (which has no $2^{o(N)}$-time algorithm under `ETH` by `ETH.not_decidableInSubexpTime_ThreeColoring_vertices`) to subexponentially many instances of `BipartitePermutationIndependentSet` of parameter $n = \Theta(N / \log N)$, for which -$n \log_2 n \le 10 N + 5$ (`numBlocks_mul_log_le`), using a library proof based on monotone -threshold enumeration (`Tuple.sort` and `Tuple.lt_card_le_iff_apply_le_of_monotone`): +$n \log_2 n \le 10 N + 5$ (`BipartitePermutationIndependentSet.fst_bpisOfColoring_mul_log_le`), +using a library proof based on monotone threshold enumeration (`Tuple.sort` and +`Tuple.lt_card_le_iff_apply_le_of_monotone`): * Partition the $N$ vertices into $n = \lfloor N / b \rfloor + 1$ blocks of size $b = \lfloor (\log_2 N) / 4 \rfloor + 1$, so that $n \log_2 n \le 10 N + 5$ - (`numBlocks_mul_log_le`). + (`BipartitePermutationIndependentSet.fst_bpisOfColoring_mul_log_le`). * A 3-coloring of a block is encoded by $2b$ bits as a number below $B = 2^{2b} = 4^b$, so a 3-coloring of the graph induces a tuple $a : \mathrm{Fin}\, n \to \mathrm{Fin}\, B$. * By `Tuple.sort`, any tuple $a : \mathrm{Fin}\, n \to \mathrm{Fin}\, B$ factors as @@ -89,6 +88,9 @@ threshold enumeration (`Tuple.sort` and `Tuple.lt_card_le_iff_apply_le_of_monoto `Cslib.Complexity.BipartitePermutationGraph.SatisfiesUndirected`: Lokshtanov–Marx–Saurabh's block-preserving single-permutation predicate on $\mathrm{Fin}\,(2n)$. * `Cslib.Complexity.BipartitePermutationIndependentSet`: the language of satisfiable instances. +* `Cslib.Complexity.BipartitePermutationIndependentSet.searchBits`, + `Cslib.Complexity.BipartitePermutationIndependentSet.bpisOfColoring`: threshold-table bit length + and the block-sorting reduction from `ThreeColoring`. ## Main results @@ -97,6 +99,9 @@ threshold enumeration (`Tuple.sort` and `Tuple.lt_card_le_iff_apply_le_of_monoto equivalence of Ilango's and Lokshtanov–Marx–Saurabh's formulations. * `Cslib.Complexity.ETH.not_decidableInSubexpTime_ThreeColoring_vertices`: under `ETH`, `ThreeColoring` is not decidable in time $2^{o(|V|)}$. +* `Cslib.Complexity.BipartitePermutationIndependentSet.mem_ThreeColoring_iff_exists_bpisOfColoring`: + correctness of the block-sorting reduction from `ThreeColoring` to + `BipartitePermutationIndependentSet`. * `Cslib.Complexity.ETH.not_decidableInSubexpTime_BipartitePermutationIndependentSet`: under `ETH`, `BipartitePermutationIndependentSet` is not decidable in time $2^{o(n \log n)}$ ([LokshtanovMarxSaurabh2018, Theorem 2.11]; [Ilango2020FOCS, Section III.B, p. 427; ECCC @@ -117,12 +122,12 @@ threshold enumeration (`Tuple.sort` and `Tuple.lt_card_le_iff_apply_le_of_monoto Problems*][LokshtanovMarxSaurabh2018] -/ -@[expose] public section - namespace Cslib.Complexity open Cslib.Logic.PL Turing.MultiTapeTM ComputableTidilyInPolyTime +public section + /-! ### Problem definitions and equivalence of formulations -/ /-- An instance of `$2n \times 2n$ Bipartite Permutation Independent Set` @@ -134,11 +139,11 @@ abbrev BipartitePermutationGraph : Type := ℕ × List ((ℕ × ℕ) × (ℕ × /-- Unary encoding of a `BipartitePermutationGraph`, matching Ilango's presentation in which the graph has $O(n^2)$ vertices and coordinates are bounded by $n$ [Ilango2020FOCS, Section III.B, p. 427; ECCC TR20-183, Section 3, p. 20]. -/ -def encBipartitePermutationGraph : BipartitePermutationGraph ↪ List Bool := +@[expose] def encBipartitePermutationGraph : BipartitePermutationGraph ↪ List Bool := encPair encUnary (encList (encPair (encPair encUnary encUnary) (encPair encUnary encUnary))) /-- Binary encoding of a `BipartitePermutationGraph`. -/ -def encBipartitePermutationGraphBinary : BipartitePermutationGraph ↪ List Bool := +@[expose] def encBipartitePermutationGraphBinary : BipartitePermutationGraph ↪ List Bool := encPair encNat (encList (encPair (encPair encNat encNat) (encPair encNat encNat))) namespace BipartitePermutationGraph @@ -147,14 +152,14 @@ namespace BipartitePermutationGraph TR20-183, Section 3, Theorem 10, p. 20]: two permutations $\pi_1, \pi_2 \in S_n$ satisfy $G$ when for no edge $((u_1, u_2), (v_1, v_2)) \in G.2$ with coordinates below $n = G.1$ do we have both $\pi_1(u_1) = u_2$ and $\pi_2(v_1) = v_2$. -/ -def Satisfies (G : BipartitePermutationGraph) (π₁ π₂ : Equiv.Perm (Fin G.1)) : Prop := +@[expose] def Satisfies (G : BipartitePermutationGraph) (π₁ π₂ : Equiv.Perm (Fin G.1)) : Prop := ∀ e ∈ G.2, ∀ (hu₁ : e.1.1 < G.1) (hu₂ : e.1.2 < G.1) (hv₁ : e.2.1 < G.1) (hv₂ : e.2.2 < G.1), π₁ ⟨e.1.1, hu₁⟩ = ⟨e.1.2, hu₂⟩ → π₂ ⟨e.2.1, hv₁⟩ ≠ ⟨e.2.2, hv₂⟩ /-- A permutation of $\mathrm{Fin}\,(2n)$ is **block-preserving** when it maps the first half $[0, n)$ to $[0, n)$ (and hence the second half $[n, 2n)$ to $[n, 2n)$) [LokshtanovMarxSaurabh2018, Theorem 2.11]. -/ -def IsBlockPreserving {n : ℕ} (π : Equiv.Perm (Fin (2 * n))) : Prop := +@[expose] def IsBlockPreserving {n : ℕ} (π : Equiv.Perm (Fin (2 * n))) : Prop := ∀ i : Fin (2 * n), i.val < n ↔ (π i).val < n /-- **Lokshtanov–Marx–Saurabh's undirected bipartite satisfaction predicate** @@ -162,7 +167,8 @@ def IsBlockPreserving {n : ℕ} (π : Equiv.Perm (Fin (2 * n))) : Prop := $\pi \in S_{2n}$ preserves the two blocks $[0, n)$ and $[n, 2n)$ and for no conflict edge $((u_1, u_2), (v_1, v_2)) \in G.2$ between the two blocks do we have both $\pi(u_1) = u_2$ and $\pi(n + v_1) = n + v_2$. -/ -def SatisfiesUndirected (G : BipartitePermutationGraph) (π : Equiv.Perm (Fin (2 * G.1))) : Prop := +@[expose] def SatisfiesUndirected (G : BipartitePermutationGraph) + (π : Equiv.Perm (Fin (2 * G.1))) : Prop := IsBlockPreserving π ∧ ∀ e ∈ G.2, ∀ (hu₁ : e.1.1 < G.1) (_hu₂ : e.1.2 < G.1) (hv₁ : e.2.1 < G.1) (_hv₂ : e.2.2 < G.1), (π ⟨e.1.1, by omega⟩).val = e.1.2 → (π ⟨G.1 + e.2.1, by omega⟩).val ≠ G.1 + e.2.2 @@ -172,59 +178,42 @@ theorem IsBlockPreserving.symm {n : ℕ} {π : Equiv.Perm (Fin (2 * n))} intro i simpa only [π.apply_symm_apply] using (hπ (π.symm i)).symm +/-- The block-splitting equivalence $\mathrm{Fin}\, n \oplus \mathrm{Fin}\, n \simeq +\mathrm{Fin}\,(2n)$. -/ +private def blockEquiv (n : ℕ) : Fin n ⊕ Fin n ≃ Fin (2 * n) := + finSumFinEquiv.trans (finCongr (two_mul n).symm) + /-- Combining two permutations $\pi_1, \pi_2 \in S_n$ on the two halves of $\mathrm{Fin}\,(2n)$. -/ -def combinePerm {n : ℕ} (π₁ π₂ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (2 * n)) where - toFun i := - if h : i.val < n then - ⟨(π₁ ⟨i.val, h⟩).val, by have := (π₁ ⟨i.val, h⟩).isLt; omega⟩ - else - ⟨n + (π₂ ⟨i.val - n, by omega⟩).val, by have := (π₂ ⟨i.val - n, by omega⟩).isLt; omega⟩ - invFun i := - if h : i.val < n then - ⟨(π₁.symm ⟨i.val, h⟩).val, by have := (π₁.symm ⟨i.val, h⟩).isLt; omega⟩ - else - ⟨n + (π₂.symm ⟨i.val - n, by omega⟩).val, - by have := (π₂.symm ⟨i.val - n, by omega⟩).isLt; omega⟩ - left_inv i := by - ext - dsimp only - split_ifs with h₁ h₂ h₃ - · simp [Fin.eta] - · exfalso - dsimp only at h₂ - exact h₂ (π₁ ⟨i.val, h₁⟩).isLt - · exfalso - dsimp only at h₃ - omega - · have hsub : n + (π₂ ⟨i.val - n, by omega⟩).val - n = (π₂ ⟨i.val - n, by omega⟩).val := by - omega - simp only [hsub, Fin.eta, Equiv.symm_apply_apply] - omega - right_inv i := by - ext - dsimp only - split_ifs with h₁ h₂ h₃ - · simp [Fin.eta] - · exfalso - dsimp only at h₂ - exact h₂ (π₁.symm ⟨i.val, h₁⟩).isLt - · exfalso - dsimp only at h₃ - omega - · have hsub : n + (π₂.symm ⟨i.val - n, by omega⟩).val - n = - (π₂.symm ⟨i.val - n, by omega⟩).val := by - omega - simp only [hsub, Fin.eta, Equiv.apply_symm_apply] - omega +def combinePerm {n : ℕ} (π₁ π₂ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (2 * n)) := + (blockEquiv n).permCongr (Equiv.Perm.sumCongr π₁ π₂) + +@[simp] theorem combinePerm_inl {n : ℕ} (π₁ π₂ : Equiv.Perm (Fin n)) (i : Fin n) : + (combinePerm π₁ π₂ ⟨i.val, by omega⟩).val = (π₁ i).val := by + have h : (⟨i.val, by omega⟩ : Fin (2 * n)) = blockEquiv n (Sum.inl i) := by + ext; simp [blockEquiv] + rw [h, combinePerm, Equiv.permCongr_apply, Equiv.symm_apply_apply] + simp [blockEquiv] + +@[simp] theorem combinePerm_inr {n : ℕ} (π₁ π₂ : Equiv.Perm (Fin n)) (i : Fin n) : + (combinePerm π₁ π₂ ⟨n + i.val, by omega⟩).val = n + (π₂ i).val := by + have h : (⟨n + i.val, by omega⟩ : Fin (2 * n)) = blockEquiv n (Sum.inr i) := by + ext; simp only [blockEquiv, Equiv.trans_apply, finCongr_apply, Fin.val_cast, + finSumFinEquiv_apply_right, Fin.val_natAdd] + rw [h, combinePerm, Equiv.permCongr_apply, Equiv.symm_apply_apply] + simp only [Equiv.Perm.sumCongr_apply, Sum.map_inr, blockEquiv, Equiv.trans_apply, + finCongr_apply, Fin.val_cast, finSumFinEquiv_apply_right, Fin.val_natAdd] theorem isBlockPreserving_combinePerm {n : ℕ} (π₁ π₂ : Equiv.Perm (Fin n)) : IsBlockPreserving (combinePerm π₁ π₂) := by intro i - simp only [combinePerm, Equiv.coe_fn_mk] - split_ifs with h - · have := (π₁ ⟨i.val, h⟩).isLt - simp [h, this] - · simp [h, show ¬n + (π₂ ⟨i.val - n, by omega⟩).val < n by omega] + by_cases h : i.val < n + · have hi : i = ⟨(⟨i.val, h⟩ : Fin n).val, by omega⟩ := rfl + rw [hi, combinePerm_inl] + exact ⟨fun _ => (π₁ ⟨i.val, h⟩).isLt, fun _ => h⟩ + · let j : Fin n := ⟨i.val - n, by omega⟩ + have hi : i = ⟨n + j.val, by omega⟩ := by ext; dsimp only [j]; omega + rw [hi, combinePerm_inr] + exact ⟨fun hlt => absurd (hi ▸ hlt) h, fun hlt => by omega⟩ /-- Extracting the first-half permutation on $\mathrm{Fin}\, n$ from a block-preserving permutation of $\mathrm{Fin}\,(2n)$. -/ @@ -232,57 +221,37 @@ def fstPerm {n : ℕ} (π : Equiv.Perm (Fin (2 * n))) (hπ : IsBlockPreserving Equiv.Perm (Fin n) where toFun i := ⟨(π ⟨i.val, by omega⟩).val, (hπ ⟨i.val, by omega⟩).mp i.isLt⟩ invFun i := ⟨(π.symm ⟨i.val, by omega⟩).val, (hπ.symm ⟨i.val, by omega⟩).mp i.isLt⟩ - left_inv i := by - ext - simp [Fin.eta] - right_inv i := by - ext - simp [Fin.eta] + left_inv i := by ext; simp [Fin.eta] + right_inv i := by ext; simp [Fin.eta] + +private def sndPermFun {n : ℕ} (π : Equiv.Perm (Fin (2 * n))) (hπ : IsBlockPreserving π) + (i : Fin n) : Fin n := + ⟨(π ⟨n + i.val, by omega⟩).val - n, by + have := mt (hπ ⟨n + i.val, by omega⟩).mpr (by simp) + have := (π ⟨n + i.val, by omega⟩).isLt + omega⟩ + +private theorem sndPermFun_left_inv {n : ℕ} {π : Equiv.Perm (Fin (2 * n))} + (hπ : IsBlockPreserving π) (i : Fin n) : + sndPermFun π.symm hπ.symm (sndPermFun π hπ i) = i := by + ext + dsimp only [sndPermFun] + have hge : n ≤ (π ⟨n + i.val, by omega⟩).val := + Nat.le_of_not_lt (mt (hπ ⟨n + i.val, by omega⟩).mpr (by simp)) + have heq : (⟨n + ((π ⟨n + i.val, by omega⟩).val - n), by omega⟩ : Fin (2 * n)) = + π ⟨n + i.val, by omega⟩ := by ext; dsimp only; omega + rw [heq, π.symm_apply_apply] + dsimp only + omega /-- Extracting the second-half permutation on $\mathrm{Fin}\, n$ from a block-preserving permutation of $\mathrm{Fin}\,(2n)$. -/ def sndPerm {n : ℕ} (π : Equiv.Perm (Fin (2 * n))) (hπ : IsBlockPreserving π) : Equiv.Perm (Fin n) where - toFun i := - ⟨(π ⟨n + i.val, by omega⟩).val - n, by - have h1 : ¬(⟨n + i.val, by omega⟩ : Fin (2 * n)).val < n := by simp - have h2 := mt (hπ ⟨n + i.val, by omega⟩).mpr h1 - have h3 := (π ⟨n + i.val, by omega⟩).isLt - omega⟩ - invFun i := - ⟨(π.symm ⟨n + i.val, by omega⟩).val - n, by - have h1 : ¬(⟨n + i.val, by omega⟩ : Fin (2 * n)).val < n := by simp - have h2 := mt (hπ.symm ⟨n + i.val, by omega⟩).mpr h1 - have h3 := (π.symm ⟨n + i.val, by omega⟩).isLt - omega⟩ - left_inv i := by - ext - dsimp only - have h1 : ¬(⟨n + i.val, by omega⟩ : Fin (2 * n)).val < n := by simp - have h2 : n ≤ (π ⟨n + i.val, by omega⟩).val := - Nat.le_of_not_lt (mt (hπ ⟨n + i.val, by omega⟩).mpr h1) - have h3 : (⟨n + ((π ⟨n + i.val, by omega⟩).val - n), by omega⟩ : Fin (2 * n)) = - π ⟨n + i.val, by omega⟩ := by - ext - dsimp only - omega - rw [h3, π.symm_apply_apply] - dsimp only - omega - right_inv i := by - ext - dsimp only - have h1 : ¬(⟨n + i.val, by omega⟩ : Fin (2 * n)).val < n := by simp - have h2 : n ≤ (π.symm ⟨n + i.val, by omega⟩).val := - Nat.le_of_not_lt (mt (hπ.symm ⟨n + i.val, by omega⟩).mpr h1) - have h3 : (⟨n + ((π.symm ⟨n + i.val, by omega⟩).val - n), by omega⟩ : Fin (2 * n)) = - π.symm ⟨n + i.val, by omega⟩ := by - ext - dsimp only - omega - rw [h3, π.apply_symm_apply] - dsimp only - omega + toFun := sndPermFun π hπ + invFun := sndPermFun π.symm hπ.symm + left_inv := sndPermFun_left_inv hπ + right_inv := sndPermFun_left_inv hπ.symm /-- **Equivalence of Ilango's and Lokshtanov–Marx–Saurabh's formulations**: an instance $G$ is satisfied by a pair of permutations $\pi_1, \pi_2 \in S_n$ if and only if it is satisfied by a @@ -294,16 +263,9 @@ theorem exists_satisfies_iff_exists_satisfiesUndirected (G : BipartitePermutatio · rintro ⟨π₁, π₂, hG⟩ refine ⟨combinePerm π₁ π₂, isBlockPreserving_combinePerm π₁ π₂, fun e he hu₁ hu₂ hv₁ hv₂ h1 h2 => ?_⟩ - simp only [combinePerm, Equiv.coe_fn_mk, hu₁, ↓reduceDIte] at h1 - have hnot : ¬G.1 + e.2.1 < G.1 := by omega - simp only [combinePerm, Equiv.coe_fn_mk, hnot, ↓reduceDIte] at h2 - have hsub : G.1 + e.2.1 - G.1 = e.2.1 := by omega - have hπ₁ : π₁ ⟨e.1.1, hu₁⟩ = ⟨e.1.2, hu₂⟩ := Fin.ext h1 - have hπ₂ : π₂ ⟨e.2.1, hv₁⟩ = ⟨e.2.2, hv₂⟩ := by - ext - have h2' : (π₂ ⟨G.1 + e.2.1 - G.1, by omega⟩).val = e.2.2 := by omega - simpa only [hsub] using h2' - exact hG e he hu₁ hu₂ hv₁ hv₂ hπ₁ hπ₂ + rw [combinePerm_inl π₁ π₂ ⟨e.1.1, hu₁⟩] at h1 + rw [combinePerm_inr π₁ π₂ ⟨e.2.1, hv₁⟩] at h2 + exact hG e he hu₁ hu₂ hv₁ hv₂ (Fin.ext h1) (Fin.ext (Nat.add_left_cancel h2)) · rintro ⟨π, hblock, hG⟩ refine ⟨fstPerm π hblock, sndPerm π hblock, fun e he hu₁ hu₂ hv₁ hv₂ h1 h2 => ?_⟩ have h1' : (π ⟨e.1.1, by omega⟩).val = e.1.2 := congrArg Fin.val h1 @@ -320,7 +282,7 @@ end BipartitePermutationGraph [LokshtanovMarxSaurabh2018, Section 2.2, Theorem 2.11]: the set of instances $G = (n, E)$ admitting permutations $\pi_1, \pi_2 \in S_n$ that avoid all conflict edges in $E$. -/ -def BipartitePermutationIndependentSet : Set BipartitePermutationGraph := +@[expose] def BipartitePermutationIndependentSet : Set BipartitePermutationGraph := {G | ∃ π₁ π₂ : Equiv.Perm (Fin G.1), G.Satisfies π₁ π₂} /-- Equivalence between the two-permutation bipartite formulation of the Bipartite Permutation @@ -378,44 +340,44 @@ theorem ETH.not_decidableInSubexpTime_ThreeColoring_vertices (h : ETH) : namespace BipartitePermutationIndependentSet /-- Block size $b = \lfloor (\log_2 N) / 4 \rfloor + 1$ for grouping $N$ vertices. -/ -def blockSize (N : ℕ) : ℕ := Nat.log 2 N / 4 + 1 +private def blockSize (N : ℕ) : ℕ := Nat.log 2 N / 4 + 1 /-- Number of $2b$-bit block-coloring assignments $B = 2^{2b} = 4^b$. -/ -def numAssignments (N : ℕ) : ℕ := 2 ^ (2 * blockSize N) +private def numAssignments (N : ℕ) : ℕ := 2 ^ (2 * blockSize N) /-- Number of vertex blocks $n = \lfloor N / b \rfloor + 1$. -/ -def numBlocks (N : ℕ) : ℕ := N / blockSize N + 1 +private def numBlocks (N : ℕ) : ℕ := N / blockSize N + 1 /-- Bit-width $L = \lfloor \log_2 n \rfloor + 1$ of each threshold count in $\{0, \ldots, n\}$. -/ -def wordLen (N : ℕ) : ℕ := Nat.log 2 (numBlocks N) + 1 +private def wordLen (N : ℕ) : ℕ := Nat.log 2 (numBlocks N) + 1 /-- Total number of bits $K = B \cdot L$ in a threshold table. -/ def searchBits (N : ℕ) : ℕ := numAssignments N * wordLen N -theorem blockSize_pos (N : ℕ) : 0 < blockSize N := Nat.succ_pos _ +private theorem blockSize_pos (N : ℕ) : 0 < blockSize N := Nat.succ_pos _ -theorem numBlocks_pos (N : ℕ) : 0 < numBlocks N := Nat.succ_pos _ +private theorem numBlocks_pos (N : ℕ) : 0 < numBlocks N := Nat.succ_pos _ -theorem div_blockSize_lt_numBlocks {N p : ℕ} (hp : p < N) : +private theorem div_blockSize_lt_numBlocks {N p : ℕ} (hp : p < N) : p / blockSize N < numBlocks N := by have := Nat.div_le_div_right hp.le (c := blockSize N) unfold numBlocks omega -theorem numBlocks_lt_two_pow_wordLen (N : ℕ) : numBlocks N < 2 ^ wordLen N := +private theorem numBlocks_lt_two_pow_wordLen (N : ℕ) : numBlocks N < 2 ^ wordLen N := Nat.lt_pow_succ_log_self Nat.one_lt_two (numBlocks N) -theorem blockSize_le (N : ℕ) : blockSize N ≤ N + 1 := by +private theorem blockSize_le (N : ℕ) : blockSize N ≤ N + 1 := by have := Nat.log_le_self 2 N unfold blockSize omega -theorem numBlocks_le (N : ℕ) : numBlocks N ≤ N + 1 := by +private theorem numBlocks_le (N : ℕ) : numBlocks N ≤ N + 1 := by have := Nat.div_le_self N (blockSize N) unfold numBlocks omega -theorem log_numBlocks_le (N : ℕ) : Nat.log 2 (numBlocks N) ≤ 5 * blockSize N := by +private theorem log_numBlocks_le (N : ℕ) : Nat.log 2 (numBlocks N) ≤ 5 * blockSize N := by have hlog : Nat.log 2 N + 1 ≤ 4 * blockSize N := by unfold blockSize omega @@ -429,9 +391,7 @@ theorem log_numBlocks_le (N : ℕ) : Nat.log 2 (numBlocks N) ≤ 5 * blockSize N omega exact (Nat.log_lt_of_lt_pow (numBlocks_pos N).ne' hnb).le -/-- **Parameter bound**: the output parameter $n = \mathrm{numBlocks}\, N$ satisfies -$n \log_2 n \le 10 N + 5$. -/ -theorem numBlocks_mul_log_le (N : ℕ) : +private theorem numBlocks_mul_log_le (N : ℕ) : numBlocks N * Nat.log 2 (numBlocks N) ≤ 10 * N + 5 := by have hlog := log_numBlocks_le N have hdiv : N / blockSize N * blockSize N ≤ N := Nat.div_mul_le_self N (blockSize N) @@ -442,7 +402,7 @@ theorem numBlocks_mul_log_le (N : ℕ) : _ ≤ 5 * N + 5 * (N + 1) := by omega _ = 10 * N + 5 := by ring -theorem numAssignments_le (N : ℕ) : numAssignments N ≤ 4 * N + 4 := by +private theorem numAssignments_le (N : ℕ) : numAssignments N ≤ 4 * N + 4 := by set k := Nat.log 2 N / 4 have h2k : 2 * k ≤ Nat.log 2 N := by omega have hpow : 2 ^ (2 * k) ≤ N + 1 := by @@ -456,25 +416,12 @@ theorem numAssignments_le (N : ℕ) : numAssignments N ≤ 4 * N + 4 := by ring omega -theorem wordLen_le (N : ℕ) : wordLen N ≤ 6 * blockSize N := by +private theorem wordLen_le (N : ℕ) : wordLen N ≤ 6 * blockSize N := by have hlog := log_numBlocks_le N have hbs := blockSize_pos N unfold wordLen omega -theorem wordLen_le_two_mul (N : ℕ) : wordLen N ≤ 2 * (N + 1) := by - have h1 : Nat.log 2 (numBlocks N) ≤ numBlocks N := Nat.log_le_self 2 (numBlocks N) - have h2 := numBlocks_le N - unfold wordLen - omega - -theorem searchBits_le_quad (N : ℕ) : searchBits N ≤ 8 * (N + 1) ^ 2 := by - have hA := numAssignments_le N - have hW := wordLen_le_two_mul N - calc searchBits N = numAssignments N * wordLen N := rfl - _ ≤ (4 * N + 4) * (2 * (N + 1)) := Nat.mul_le_mul hA hW - _ = 8 * (N + 1) ^ 2 := by ring - /-- **Sublinear search-exponent bound**: for every $M \ge 1$, the number of threshold bits is at most $N / M + 48 \cdot (48 M)^3$. -/ theorem searchBits_le_div_add (N : ℕ) {M : ℕ} (hM : 0 < M) : @@ -519,37 +466,37 @@ theorem searchBits_le_div_add (N : ℕ) {M : ℕ} (hM : 0 < M) : /-- Extract the 2-bit color in $\{0, 1, 2, 3\}$ of local vertex offset $u$ from a block assignment number $c$. -/ -def extractColor (c u : ℕ) : ℕ := +private def extractColor (c u : ℕ) : ℕ := (c.testBit (2 * u)).toNat + 2 * (c.testBit (2 * u + 1)).toNat /-- Check whether a block assignment number $c$ assigns a valid color in $\{0, 1, 2\}$ to every offset $u < b$. -/ -def validAssignment (b c : ℕ) : Bool := +private def validAssignment (b c : ℕ) : Bool := (List.range b).all fun u => decide (extractColor c u < 3) /-- Decode the $v$-th threshold count from the binary digits of $r$, as an $L$-bit word capped at $n$. -/ -def thresholdOf (n L r v : ℕ) : ℕ := +private def thresholdOf (n L r v : ℕ) : ℕ := Cslib.BitString.boundedBinaryValue n (Cslib.BitString.listRow L v r.bits) /-- Reconstruct the sorted block assignment $\beta(j) \in \{0, \ldots, B - 1\}$ at sorted position $j$ from the decoded thresholds: $\beta(j)$ is the number of values $v < B - 1$ whose threshold $t_v = |\{k < n \mid \beta(k) \le v\}|$ is at most $j$. -/ -def bucketOf (B n L r j : ℕ) : ℕ := +private def bucketOf (B n L r j : ℕ) : ℕ := (List.range (B - 1)).countP fun v => decide (thresholdOf n L r v ≤ j) /-- The color assigned to local offset $u$ by the $j$-th sorted bucket under threshold table $r$. -/ -def colorAt (N r j u : ℕ) : ℕ := +private def colorAt (N r j u : ℕ) : ℕ := extractColor (bucketOf (numAssignments N) (numBlocks N) (wordLen N) r j) u /-- Edges enforcing $\pi_1(i) = \pi_2(i)$ for all $i < n$. -/ -def consistencyEdges (n : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := +private def consistencyEdges (n : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := (List.range n).flatMap fun i => (List.range n).flatMap fun j₁ => ((List.range n).filter fun j₂ => !decide (j₁ = j₂)).map fun j₂ => ((i, j₁), (i, j₂)) /-- Self-edges forbidding $\pi_1(i) = j$ when bucket $j$ is not a valid 3-coloring of a block. -/ -def invalidBucketEdges (N r : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := +private def invalidBucketEdges (N r : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := let b := blockSize N let B := numAssignments N let n := numBlocks N @@ -559,7 +506,7 @@ def invalidBucketEdges (N r : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := ((i, j), (i, j)) /-- Test whether bucket pair $(j_1, j_2)$ creates a color conflict for vertex pair $(p, q)$. -/ -def innerConflictTest (N r p q j₁ j₂ : ℕ) : Bool := +private def innerConflictTest (N r p q j₁ j₂ : ℕ) : Bool := let b := blockSize N let i₁ := p / b let u₁ := p % b @@ -569,11 +516,11 @@ def innerConflictTest (N r p q j₁ j₂ : ℕ) : Bool := decide (colorAt N r j₁ u₁ = colorAt N r j₂ u₂) /-- Filtered second-bucket indices $j_2 < n$ that conflict with $(p, q, j_1)$. -/ -def innerConflictBuckets (N r p q j₁ : ℕ) : List ℕ := +private def innerConflictBuckets (N r p q j₁ : ℕ) : List ℕ := (List.range (numBlocks N)).filter (innerConflictTest N r p q j₁) /-- Conflict edges for a fixed vertex pair $(p, q)$ and first bucket index $j_1$. -/ -def innerConflictEdges (N r p q j₁ : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := +private def innerConflictEdges (N r p q j₁ : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := let b := blockSize N let i₁ := p / b let i₂ := q / b @@ -581,18 +528,18 @@ def innerConflictEdges (N r p q j₁ : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ) ((i₁, j₁), (i₂, j₂)) /-- Conflict edges for a fixed vertex pair $(p, q)$ across all bucket pairs $(j_1, j_2)$. -/ -def pairConflictEdges (N r p q : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := +private def pairConflictEdges (N r p q : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := (List.range (numBlocks N)).flatMap fun j₁ => innerConflictEdges N r p q j₁ /-- Conflict edges incident to vertex position $p$ across all adjacent vertex positions $q$. -/ -def vertexConflictEdges (H : Graph) (r p : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := +private def vertexConflictEdges (H : Graph) (r p : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := let N := H.1.length ((List.range N).filter fun q => H.adjBool (H.1.getD p 0) (H.1.getD q 0)).flatMap fun q => pairConflictEdges N r p q /-- Edges forbidding adjacent vertices $p, q < N$ of $H$ from receiving the same color under the block assignments selected by $\pi_1(p / b) = j_1$ and $\pi_2(q / b) = j_2$. -/ -def conflictEdges (H : Graph) (r : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := +private def conflictEdges (H : Graph) (r : ℕ) : List ((ℕ × ℕ) × (ℕ × ℕ)) := (List.range H.1.length).flatMap fun p => vertexConflictEdges H r p /-- The instance of `BipartitePermutationIndependentSet` corresponding to a graph $H$ and a @@ -601,6 +548,16 @@ def bpisOfColoring (x : Graph × ℕ) : BipartitePermutationGraph := let N := x.1.1.length (numBlocks N, consistencyEdges (numBlocks N) ++ invalidBucketEdges N x.2 ++ conflictEdges x.1 x.2) +/-- **Parameter bound**: the output parameter $n = (\mathrm{bpisOfColoring}\,(H, r)).1$ satisfies +$n \log_2 n \le 10 |V| + 5$. -/ +theorem fst_bpisOfColoring_mul_log_le (H : Graph) (r : ℕ) : + (bpisOfColoring (H, r)).1 * Nat.log 2 (bpisOfColoring (H, r)).1 ≤ 10 * H.1.length + 5 := + numBlocks_mul_log_le H.1.length + +@[simp] theorem bpisOfColoring_empty_zero : + bpisOfColoring (([], []), 0) = (1, [((0, 0), (0, 0))]) := by + decide + /-! ### Correctness of the reduction -/ private theorem countP_range_lt {m k : ℕ} (hk : k ≤ m) : @@ -619,7 +576,8 @@ open Finset in /-- Every tuple $a : \mathrm{Fin}\, n \to \mathrm{Fin}\, B$ has a threshold number $r < 2^{\mathrm{searchBits}\, N}$ from which `bucketOf` recovers the sorted tuple $a \circ \mathrm{Tuple.sort}\, a$. -/ -theorem exists_bucketOf_eq_sort (N : ℕ) (a : Fin (numBlocks N) → Fin (numAssignments N)) : +private theorem exists_bucketOf_eq_sort (N : ℕ) + (a : Fin (numBlocks N) → Fin (numAssignments N)) : ∃ r < 2 ^ searchBits N, ∀ j : Fin (numBlocks N), bucketOf (numAssignments N) (numBlocks N) (wordLen N) r j.val = (a (Tuple.sort a j)).val := by @@ -676,7 +634,7 @@ theorem exists_bucketOf_eq_sort (N : ℕ) (a : Fin (numBlocks N) → Fin (numAss /-- Packing a vertex coloring $f : \mathrm{Fin}\, N \to \mathrm{Fin}\, 3$ into block assignment numbers below $\mathrm{numAssignments}\, N$. -/ -theorem exists_block_assignments_of_coloring {N : ℕ} (f : Fin N → Fin 3) : +private theorem exists_block_assignments_of_coloring {N : ℕ} (f : Fin N → Fin 3) : ∃ a : Fin (numBlocks N) → Fin (numAssignments N), (∀ i : Fin (numBlocks N), validAssignment (blockSize N) (a i).val = true) ∧ ∀ p : Fin N, @@ -703,11 +661,11 @@ theorem exists_block_assignments_of_coloring {N : ℕ} (f : Fin N → Fin 3) : have hextract (i : Fin n) (u : ℕ) (hu : u < b) : extractColor (a i).val u = col i.val u := by have h0 : (a i).val.testBit (2 * u) = decide (col i.val u % 2 = 1) := by rw [BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE, List.getD_eq_getElem?_getD, - List.getElem?_eq_getElem (by simp [word]; omega)] + List.getElem?_eq_getElem (by simp only [word, List.length_map, List.length_range]; omega)] simp [word, bitFn, Nat.mul_div_right _ two_pos] have h1 : (a i).val.testBit (2 * u + 1) = decide (col i.val u / 2 = 1) := by rw [BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE, List.getD_eq_getElem?_getD, - List.getElem?_eq_getElem (by simp [word]; omega)] + List.getElem?_eq_getElem (by simp only [word, List.length_map, List.length_range]; omega)] have hdiv : (2 * u + 1) / 2 = u := by omega have hmod : (2 * u + 1) % 2 = 1 := by omega simp [word, bitFn, hdiv, hmod] @@ -1124,131 +1082,22 @@ theorem computableInPolyTime_bpisOfColoring_binary : encBipartitePermutationGraphBinary := .of_tidy (computableTidilyInPolyTime_toBinary.comp computableTidilyInPolyTime_bpisOfColoring) -/-! ### Exhaustive search over threshold tables and the ETH lower bound -/ - -private abbrev State : Type := (Graph × ℕ) × Bool - -private def encState : State ↪ List Bool := - encPair (encPair encGraph encNat) encBool - -private def init (H : Graph) : State := ((H, 0), false) - -private def step (g : BipartitePermutationGraph → Bool) (s : State) : State := - ((s.1.1, s.1.2 + 1), s.2 || g (bpisOfColoring s.1)) - -private def rounds (H : Graph) : ℕ := 2 ^ searchBits H.1.length - -private def search (g : BipartitePermutationGraph → Bool) (H : Graph) : Bool := - ((step g)^[rounds H] (init H)).2 - -private theorem iterate_step_init (g : BipartitePermutationGraph → Bool) (H : Graph) (k : ℕ) : - (step g)^[k] (init H) = - ((H, k), (List.range k).any fun r => g (bpisOfColoring (H, r))) := by - induction k with - | zero => rfl - | succ k ih => - rw [Function.iterate_succ_apply', ih, step, List.range_succ, List.any_append, - List.any_cons, List.any_nil, Bool.or_false] - -private theorem search_eq_true_iff {g : BipartitePermutationGraph → Bool} - (hg : ∀ G, g G = true ↔ G ∈ BipartitePermutationIndependentSet) (H : Graph) : - search g H = true ↔ H ∈ ThreeColoring := by - rw [search, iterate_step_init, List.any_eq_true, mem_ThreeColoring_iff_exists_bpisOfColoring] - simp only [List.mem_range, hg, rounds] - -private theorem computableTidilyInPolyTime_init : - ComputableTidilyInPolyTime init encGraph encState := by - unfold init encState - fun_prop +/-- Computing `searchBits` is polynomial-time in the plain machine model. -/ +@[fun_prop] +theorem computableInPolyTime_searchBits : + ComputableInPolyTime searchBits encUnary encUnary := + .of_tidy computableTidilyInPolyTime_searchBits -private theorem computableTidilyInPolyTime_rounds : - ComputableTidilyInPolyTime rounds encGraph encNat := by - have hlen : ComputableTidilyInPolyTime (fun H : Graph => H.1.length) encGraph encUnary := by - unfold encGraph - fun_prop - unfold rounds +/-- Computing `searchBits H.1.length` from a graph `H` is polynomial-time in the plain machine +model. -/ +@[fun_prop] +theorem computableInPolyTime_searchBits_length : + ComputableInPolyTime (fun H : Graph => searchBits H.1.length) encGraph encUnary := by + refine .of_tidy (computableTidilyInPolyTime_searchBits.comp ?_) + unfold encGraph fun_prop -private theorem exists_computableTidilyInO_step {g : BipartitePermutationGraph → Bool} - {t : BipartitePermutationGraph → ℕ} - (hg : ComputableTidilyInO g encBipartitePermutationGraph encBool t t) : - ∃ d, ComputableTidilyInO (step g) encState encState - (fun s => ((encState s).length + 1) ^ d + t (bpisOfColoring s.1)) - (fun s => ((encState s).length + 1) ^ d + t (bpisOfColoring s.1)) := by - obtain ⟨dN, eN, hN⟩ := (show ComputableTidilyInPolyTime (fun s : State => (s.1.1, s.1.2 + 1)) - encState (encPair encGraph encNat) by unfold encState; fun_prop).exists_degree - obtain ⟨dB, eB, hB⟩ := (show ComputableTidilyInPolyTime (fun s : State => s.2) - encState encBool by unfold encState; fun_prop).exists_degree - obtain ⟨dR, eR, hR⟩ := (show ComputableTidilyInPolyTime (fun s : State => bpisOfColoring s.1) - encState encBipartitePermutationGraph by unfold encState; fun_prop).exists_degree - obtain ⟨dO, eO, hO⟩ := bool_or.exists_degree - set D := dN + dB + dR - have hN' := (hN.mono (d' := D) (e' := eN) (by omega) le_rfl).inO - have hB' := (hB.mono (d' := D) (e' := eB) (by omega) le_rfl).inO - have hR' := (hR.mono (d' := D) (e' := eR) (by omega) le_rfl).inO - have h := hN'.prod (hO.inO.comp (hB'.prod (hg.comp hR'))) - have h4 (p : Bool × Bool) : (encPair encBool encBool p).length = 4 := by simp - refine ⟨D, (h.mono (5 ^ dO + 4) (fun s => ?_) (fun s => ?_)).of_enc_eq fun _ => rfl⟩ <;> - · simp only [Function.comp_apply, h4] - generalize ((encState s).length + 1) ^ D = P - generalize t (bpisOfColoring s.1) = T - have hF : 1 ≤ (4 + 1) ^ dO := Nat.one_le_pow _ _ (by norm_num) - generalize (4 + 1) ^ dO = F at hF ⊢ - nlinarith - -private theorem length_encPair_le_of_le_rounds (H : Graph) {k : ℕ} (hk : k ≤ rounds H) : - (encPair encGraph encNat (H, k)).length ≤ 11 * ((encGraph H).length + 1) ^ 2 := by - have hK := ComputableTidilyInO.length_encNat_mono hk - rw [rounds, encNat_two_pow] at hK - simp only [List.length_append, List.length_replicate, List.length_singleton] at hK - have hSB := searchBits_le_quad H.1.length - have hNL := H.length_vertices_le_encGraph - have hsq : (H.1.length + 1) ^ 2 ≤ ((encGraph H).length + 1) ^ 2 := - Nat.pow_le_pow_left (by omega) 2 - simp only [length_encPair] - nlinarith - -private theorem exists_state_and_node_bounds : - ∃ (c_st c_nd d_nd : ℕ), - (∀ (g : BipartitePermutationGraph → Bool) (H : Graph) (k : ℕ), - k ≤ rounds H → - (encState ((step g)^[k] (init H))).length ≤ c_st * ((encGraph H).length + 1) ^ 2) ∧ - (∀ (H : Graph), - (encNat (rounds H)).length + 1 ≤ c_st * ((encGraph H).length + 1) ^ 2) ∧ - (∀ (H : Graph) (k : ℕ), - k ≤ rounds H → - (encBipartitePermutationGraph (bpisOfColoring (H, k))).length ≤ - c_nd * ((encGraph H).length + 1) ^ d_nd) := by - obtain ⟨cb, db, hbpis⟩ := computableTidilyInPolyTime_bpisOfColoring.polyBounded_length.exists_le - refine ⟨24, cb * 12 ^ db, 2 * db, fun g H k hk => ?_, fun H => ?_, fun H k hk => ?_⟩ - · rw [iterate_step_init, encState, length_encPair] - have hp := length_encPair_le_of_le_rounds H hk - have h1 : 1 ≤ ((encGraph H).length + 1) ^ 2 := Nat.one_le_pow _ _ (Nat.succ_pos _) - simp only [encBool_apply, List.length_singleton] - omega - · rw [rounds, encNat_two_pow, List.length_append, List.length_replicate, List.length_singleton] - have hSB := searchBits_le_quad H.1.length - have hNL := H.length_vertices_le_encGraph - have hsq : (H.1.length + 1) ^ 2 ≤ ((encGraph H).length + 1) ^ 2 := - Nat.pow_le_pow_left (by omega) 2 - have h1 : 1 ≤ ((encGraph H).length + 1) ^ 2 := Nat.one_le_pow _ _ (Nat.succ_pos _) - omega - · have h1 := hbpis (H, k) - have h2 := length_encPair_le_of_le_rounds H hk - have h3 : (encPair encGraph encNat (H, k)).length + 1 ≤ - 12 * ((encGraph H).length + 1) ^ 2 := by - have : 1 ≤ ((encGraph H).length + 1) ^ 2 := Nat.one_le_pow _ _ (Nat.succ_pos _) - omega - calc (encBipartitePermutationGraph (bpisOfColoring (H, k))).length - ≤ cb * ((encPair encGraph encNat (H, k)).length + 1) ^ db := h1 - _ ≤ cb * (12 * ((encGraph H).length + 1) ^ 2) ^ db := - Nat.mul_le_mul_left cb (Nat.pow_le_pow_left h3 db) - _ = cb * 12 ^ db * ((encGraph H).length + 1) ^ (2 * db) := by - rw [mul_pow, ← pow_mul, ← mul_assoc] - -private noncomputable def leafTime (c_nd d_nd : ℕ) (δ : ℝ) (c e : ℕ) (H : Graph) : ℕ := - ⌈(c : ℝ) * (2 ^ (δ * ((10 * H.1.length + 5 : ℕ) : ℝ)) * - ((c_nd * ((encGraph H).length + 1) ^ d_nd : ℕ) + 1 : ℝ) ^ e) + c⌉₊ +/-! ### Exhaustive search over threshold tables and the ETH lower bound -/ /-- **Transfer of exponential-time deciders along the block-sorting reduction**: for every $M \ge 1$ and $\delta \ge 0$, a decider for `BipartitePermutationIndependentSet` within time @@ -1258,202 +1107,10 @@ theorem decidableInExpTime_ThreeColoring_of_bpis {M : ℕ} (hM : 0 < M) {δ : (h : DecidableInExpTime BipartitePermutationIndependentSet encBipartitePermutationGraph (fun G => G.1 * Nat.log 2 G.1) δ) : DecidableInExpTime ThreeColoring encGraph (fun H => H.1.length) (1 / M + 10 * δ) := by - obtain ⟨e, h⟩ := h - obtain ⟨g, t, c, hg, hgB, ht⟩ := h.exists_computableInO - have hg := hg.tidy - obtain ⟨d, hstep⟩ := exists_computableTidilyInO_step hg - obtain ⟨dn, _, hn⟩ := computableTidilyInPolyTime_rounds.exists_degree - obtain ⟨di, _, hi⟩ := computableTidilyInPolyTime_init.exists_degree - obtain ⟨da, _, ha⟩ := (show ComputableTidilyInPolyTime (fun s : State => s.2) encState encBool - by unfold encState; fun_prop).exists_degree - obtain ⟨c_st, c_nd, d_nd, hst_bound, hrounds_len, hnd_bound⟩ := exists_state_and_node_bounds - obtain ⟨K_M, hK_M⟩ : ∃ K_M : ℕ, ∀ N, searchBits N ≤ N / M + K_M := - ⟨48 * (48 * M) ^ 3, fun N => searchBits_le_div_add N hM⟩ - set stBound : Graph → ℕ := fun H => c_st * ((encGraph H).length + 1) ^ 2 - set ndBound : Graph → ℕ := fun H => c_nd * ((encGraph H).length + 1) ^ d_nd - have hround (H : Graph) (k : ℕ) (hk : k ≤ rounds H) : - ((encState ((step g)^[k] (init H))).length + 1) ^ d + - t (bpisOfColoring ((step g)^[k] (init H)).1) ≤ - (stBound H + 1) ^ d + leafTime c_nd d_nd δ c e H := by - have hS : (encState ((step g)^[k] (init H))).length ≤ stBound H := hst_bound g H k hk - refine Nat.add_le_add (Nat.pow_le_pow_left (by omega) d) ?_ - rw [iterate_step_init] - dsimp only - set G := bpisOfColoring (H, k) - have hG1 : G.1 * Nat.log 2 G.1 ≤ 10 * H.1.length + 5 := - numBlocks_mul_log_le H.1.length - have hGenc : (encBipartitePermutationGraph G).length ≤ ndBound H := hnd_bound H k hk - have h₁ : (2 : ℝ) ^ (δ * (G.1 * Nat.log 2 G.1 : ℕ)) ≤ - 2 ^ (δ * ((10 * H.1.length + 5 : ℕ) : ℝ)) := - Real.rpow_le_rpow_of_exponent_le (by norm_num) - (mul_le_mul_of_nonneg_left (by exact_mod_cast hG1) hδ) - have h₂ : (((encBipartitePermutationGraph G).length : ℝ) + 1) ^ e ≤ - ((ndBound H : ℝ) + 1) ^ e := - pow_le_pow_left₀ (by positivity) (by exact_mod_cast Nat.add_le_add_right hGenc 1) e - have h₃ := mul_le_mul h₁ h₂ (by positivity) (by positivity) - have h₄ := mul_le_mul_of_nonneg_left h₃ (Nat.cast_nonneg c : (0 : ℝ) ≤ c) - have h₅ := (ht G).trans (add_le_add h₄ le_rfl) - exact Nat.cast_le.mp (h₅.trans (Nat.le_ceil _)) - have hstate (H : Graph) (k : ℕ) (hk : k ≤ rounds H) : - (encState ((step g)^[k] (init H))).length ≤ stBound H := - hst_bound g H k hk - have hiter := ComputableTidilyInO.iterate hn.inO hi.inO hstep hround hround hstate - have hsearch := ha.inO.comp hiter - set C₁ := (c_st + 1) ^ d + c_st + c_st ^ 2 - set C₃ := (c_st + 1) ^ da - set E := dn + di + 2 * d + 2 * da + d_nd * e + 4 - set C₂ : ℝ := c * 2 ^ (5 * δ) * ((c_nd : ℝ) + 1) ^ e + c + 1 - set C₀ : ℝ := 3 + C₃ + (2 ^ K_M + 1 : ℝ) * (C₁ + C₂) - refine DecidableInExpTime.of_computableInO (.of_tidy hsearch) - (fun H => (search_eq_true_iff (fun G => (hgB G).symm) H).symm) ⌈C₀⌉₊ E fun H => ?_ - set L := (encGraph H).length - set N := H.1.length - set P := (L + 1) ^ E - have hP (a : ℕ) (ha : a ≤ E) : (L + 1) ^ a ≤ P := Nat.pow_le_pow_right (Nat.succ_pos L) ha - have hsb : stBound H = c_st * (L + 1) ^ 2 := rfl - have hr : rounds H + 1 ≤ (2 ^ K_M + 1) * 2 ^ (N / M) := by - have h1 := hK_M N - have h2 : rounds H ≤ 2 ^ K_M * 2 ^ (N / M) := by - calc rounds H = 2 ^ searchBits N := rfl - _ ≤ 2 ^ (N / M + K_M) := Nat.pow_le_pow_right two_pos h1 - _ = 2 ^ K_M * 2 ^ (N / M) := by rw [pow_add, Nat.mul_comm] - have h3 : 1 ≤ 2 ^ (N / M) := Nat.one_le_two_pow - nlinarith - have hpoly : (L + 1) ^ dn + (L + 1) ^ di ≤ 2 * P := by - have := hP dn (by omega) - have := hP di (by omega) - omega - have hans_le : ((encState ((step g)^[rounds H] (init H))).length + 1) ^ da ≤ C₃ * P := by - have h1 := hstate H (rounds H) le_rfl - have h2 : stBound H + 1 ≤ (c_st + 1) * (L + 1) ^ 2 := by - have : 1 ≤ (L + 1) ^ 2 := Nat.one_le_pow _ _ (Nat.succ_pos L) - rw [hsb] - nlinarith - calc ((encState ((step g)^[rounds H] (init H))).length + 1) ^ da - ≤ (stBound H + 1) ^ da := Nat.pow_le_pow_left (by omega) da - _ ≤ ((c_st + 1) * (L + 1) ^ 2) ^ da := Nat.pow_le_pow_left h2 da - _ = C₃ * (L + 1) ^ (2 * da) := by simp only [C₃, mul_pow, ← pow_mul] - _ ≤ C₃ * P := Nat.mul_le_mul_left C₃ (hP (2 * da) (by omega)) - have hrnd : (stBound H + 1) ^ d + stBound H + - ((encNat (rounds H)).length + 1) ^ 2 ≤ C₁ * P := by - have h1 : (stBound H + 1) ^ d ≤ (c_st + 1) ^ d * (L + 1) ^ (2 * d) := by - have hst1 : stBound H + 1 ≤ (c_st + 1) * (L + 1) ^ 2 := by - have : 1 ≤ (L + 1) ^ 2 := Nat.one_le_pow _ _ (Nat.succ_pos L) - rw [hsb] - nlinarith - calc (stBound H + 1) ^ d ≤ ((c_st + 1) * (L + 1) ^ 2) ^ d := Nat.pow_le_pow_left hst1 d - _ = (c_st + 1) ^ d * (L + 1) ^ (2 * d) := by rw [mul_pow, ← pow_mul] - have h2 : ((encNat (rounds H)).length + 1) ^ 2 ≤ c_st ^ 2 * (L + 1) ^ 4 := by - have hr_len := hrounds_len H - calc ((encNat (rounds H)).length + 1) ^ 2 - ≤ (c_st * (L + 1) ^ 2) ^ 2 := Nat.pow_le_pow_left hr_len 2 - _ = c_st ^ 2 * (L + 1) ^ 4 := by rw [mul_pow, ← pow_mul] - have h3 := hP (2 * d) (by omega) - have h4 := hP 2 (by omega) - have h5 := hP 4 (by omega) - calc (stBound H + 1) ^ d + stBound H + ((encNat (rounds H)).length + 1) ^ 2 - ≤ (c_st + 1) ^ d * P + c_st * P + c_st ^ 2 * P := by - have := h1.trans (Nat.mul_le_mul_left ((c_st + 1) ^ d) h3) - have := (le_of_eq hsb).trans (Nat.mul_le_mul_left c_st h4) - have := h2.trans (Nat.mul_le_mul_left (c_st ^ 2) h5) - omega - _ = C₁ * P := by simp only [C₁]; ring - set Y : ℝ := 2 ^ ((10 * δ) * N) - have hY : 1 ≤ Y := Real.one_le_rpow (by norm_num) (by positivity) - have hP1 : (1 : ℝ) ≤ P := by exact_mod_cast Nat.one_le_pow _ _ (Nat.succ_pos L) - have hleaf : (leafTime c_nd d_nd δ c e H : ℝ) ≤ C₂ * Y * P := by - have h₁ : (2 : ℝ) ^ (δ * ((10 * N + 5 : ℕ) : ℝ)) = 2 ^ (5 * δ) * Y := by - rw [← Real.rpow_add (by norm_num)] - congr 1 - push_cast - ring - have h₂ : ((ndBound H : ℝ) + 1) ^ e ≤ ((c_nd : ℝ) + 1) ^ e * P := by - have hnb_le : (ndBound H : ℝ) + 1 ≤ ((c_nd : ℝ) + 1) * ((L : ℝ) + 1) ^ d_nd := by - have hnb_eq : (ndBound H : ℝ) = c_nd * ((L : ℝ) + 1) ^ d_nd := by - simp only [ndBound] - push_cast - ring - have hpow1 : (1 : ℝ) ≤ ((L : ℝ) + 1) ^ d_nd := - one_le_pow₀ (by linarith [(L.cast_nonneg : (0 : ℝ) ≤ L)]) - nlinarith - calc ((ndBound H : ℝ) + 1) ^ e ≤ (((c_nd : ℝ) + 1) * ((L : ℝ) + 1) ^ d_nd) ^ e := - pow_le_pow_left₀ (by positivity) hnb_le e - _ = ((c_nd : ℝ) + 1) ^ e * ((L : ℝ) + 1) ^ (d_nd * e) := by rw [mul_pow, ← pow_mul] - _ ≤ ((c_nd : ℝ) + 1) ^ e * P := by - refine mul_le_mul_of_nonneg_left ?_ (by positivity) - exact_mod_cast hP (d_nd * e) (by omega) - have h₃ := Nat.ceil_lt_add_one (show (0 : ℝ) ≤ (c : ℝ) * (2 ^ (δ * ((10 * N + 5 : ℕ) : ℝ)) * - ((ndBound H : ℝ) + 1) ^ e) + c by positivity) - unfold leafTime - change (⌈(c : ℝ) * (2 ^ (δ * ((10 * N + 5 : ℕ) : ℝ)) * - ((ndBound H : ℝ) + 1) ^ e) + c⌉₊ : ℝ) ≤ _ - rw [h₁] at h₃ ⊢ - have h₄ : (c : ℝ) * (2 ^ (5 * δ) * Y * ((ndBound H : ℝ) + 1) ^ e) ≤ - c * 2 ^ (5 * δ) * ((c_nd : ℝ) + 1) ^ e * Y * P := by - have := mul_le_mul_of_nonneg_left h₂ (by positivity : (0 : ℝ) ≤ c * 2 ^ (5 * δ) * Y) - nlinarith - have h₅ : (c : ℝ) + 1 ≤ ((c : ℝ) + 1) * Y * P := by - have : (1 : ℝ) ≤ Y * P := one_le_mul_of_one_le_of_one_le hY hP1 - nlinarith - calc (⌈(c : ℝ) * (2 ^ (5 * δ) * Y * ((ndBound H : ℝ) + 1) ^ e) + c⌉₊ : ℝ) - ≤ (c : ℝ) * (2 ^ (5 * δ) * Y * ((ndBound H : ℝ) + 1) ^ e) + c + 1 := h₃.le - _ ≤ C₂ * Y * P := by simp only [C₂]; nlinarith - set X : ℝ := 2 ^ ((1 / M : ℝ) * N) - have hX : ((2 ^ (N / M) : ℕ) : ℝ) ≤ X := by - rw [Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_natCast] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - rw [one_div_mul_eq_div] - exact Nat.cast_div_le - have hX1 : 1 ≤ X := Real.one_le_rpow (by norm_num) (by positivity) - have hXY : X * Y = 2 ^ ((1 / M + 10 * δ) * N) := by - rw [← Real.rpow_add (by norm_num)] - ring_nf - have hT : ((L + 1) ^ dn + (L + 1) ^ di + - (rounds H + 1) * ((stBound H + 1) ^ d + leafTime c_nd d_nd δ c e H + - stBound H + ((encNat (rounds H)).length + 1) ^ 2) + - ((encState ((step g)^[rounds H] (init H))).length + 1) ^ da : ℝ) ≤ - (2 + C₃ : ℝ) * P + (2 ^ K_M + 1 : ℝ) * X * (C₁ * P + C₂ * Y * P) := by - have h₁ : ((L + 1) ^ dn + (L + 1) ^ di : ℝ) ≤ 2 * P := by exact_mod_cast hpoly - have h₁' : (((encState ((step g)^[rounds H] (init H))).length + 1) ^ da : ℝ) ≤ C₃ * P := by - exact_mod_cast hans_le - have h₂ : ((rounds H + 1 : ℕ) : ℝ) ≤ (2 ^ K_M + 1 : ℝ) * X := by - have : ((rounds H + 1 : ℕ) : ℝ) ≤ (((2 ^ K_M + 1) * 2 ^ (N / M) : ℕ) : ℝ) := by - exact_mod_cast hr - rw [Nat.cast_mul] at this - have hKM : (0 : ℝ) ≤ (2 ^ K_M + 1 : ℕ) := Nat.cast_nonneg _ - have hmul := mul_le_mul_of_nonneg_left hX hKM - push_cast at this hmul ⊢ - linarith - have h₃ : (((stBound H + 1) ^ d + stBound H + - ((encNat (rounds H)).length + 1) ^ 2 : ℕ) : ℝ) ≤ C₁ * P := by exact_mod_cast hrnd - have h₄ : (((stBound H + 1) ^ d + leafTime c_nd d_nd δ c e H + stBound H + - ((encNat (rounds H)).length + 1) ^ 2 : ℕ) : ℝ) ≤ C₁ * P + C₂ * Y * P := by - push_cast at h₃ ⊢ - linarith - have h₅ := mul_le_mul h₂ h₄ (by positivity) (by positivity) - push_cast at h₁ h₁' h₅ ⊢ - linarith - calc _ ≤ (2 + C₃ : ℝ) * P + (2 ^ K_M + 1 : ℝ) * X * (C₁ * P + C₂ * Y * P) := by - exact_mod_cast hT - _ ≤ C₀ * (X * Y * P) := by - have hXY1 : 1 ≤ X * Y := one_le_mul_of_one_le_of_one_le hX1 hY - have hC₂ : 0 ≤ C₂ := by positivity - have hC₁ : (0 : ℝ) ≤ C₁ := by positivity - have hC₃ : (0 : ℝ) ≤ C₃ := by positivity - have hKM : (0 : ℝ) ≤ 2 ^ K_M + 1 := by positivity - have hP0 : (0 : ℝ) ≤ P := by positivity - have a₁ : (P : ℝ) ≤ X * Y * P := le_mul_of_one_le_left hP0 hXY1 - have a₂ : X * P ≤ X * Y * P := by - have := mul_le_mul_of_nonneg_left hY (by positivity : (0 : ℝ) ≤ X * P) - linarith [show X * P * Y = X * Y * P by ring] - have a₃ := mul_le_mul_of_nonneg_left a₂ (mul_nonneg hKM hC₁) - have a₄ := mul_le_mul_of_nonneg_left a₁ hC₃ - simp only [C₀] - nlinarith - _ ≤ ⌈C₀⌉₊ * (2 ^ ((1 / M + 10 * δ) * N) * ((L : ℝ) + 1) ^ E) := by - rw [← hXY] - push_cast [P] - exact mul_le_mul_of_nonneg_right (Nat.le_ceil C₀) (by positivity) + simpa using h.of_exhaustiveSearch computableInPolyTime_bpisOfColoring + computableInPolyTime_searchBits_length mem_ThreeColoring_iff_exists_bpisOfColoring (c := 10) + (fun H r => by have := fst_bpisOfColoring_mul_log_le H r; omega) + (fun H => searchBits_le_div_add H.1.length hM) hδ end BipartitePermutationIndependentSet @@ -1464,20 +1121,11 @@ if `BipartitePermutationIndependentSet` is decidable in time $2^{o(n \log n)}$, theorem DecidableInSubexpTime.threeColoring_of_bipartitePermutationIndependentSet (h : DecidableInSubexpTime BipartitePermutationIndependentSet encBipartitePermutationGraph fun G => G.1 * Nat.log 2 G.1) : - DecidableInSubexpTime ThreeColoring encGraph fun H => H.1.length := by - intro ε hε - obtain ⟨M, hM⟩ := exists_nat_gt (2 / ε) - have hMpos : (0 : ℝ) < M := lt_trans (by positivity) hM - have hM_nat : 0 < M := Nat.cast_pos.mp hMpos - have hMε : 1 / (M : ℝ) < ε / 2 := by - rw [div_lt_iff₀ hMpos] - rw [div_lt_iff₀ hε] at hM - linarith - set δ := ε / 20 - have hδ : 0 < δ := by positivity - refine (decidableInExpTime_ThreeColoring_of_bpis hM_nat hδ.le (h δ hδ)).mono ?_ - simp only [δ] - linarith + DecidableInSubexpTime ThreeColoring encGraph fun H => H.1.length := + h.of_exhaustiveSearch computableInPolyTime_bpisOfColoring computableInPolyTime_searchBits_length + mem_ThreeColoring_iff_exists_bpisOfColoring (c := 10) + (fun H r => by have := fst_bpisOfColoring_mul_log_le H r; omega) + (fun M hM => ⟨48 * (48 * M) ^ 3, fun H => searchBits_le_div_add H.1.length hM⟩) /-- **Lokshtanov–Marx–Saurabh ETH Lower Bound for $2n \times 2n$ Bipartite Permutation Independent Set** [LokshtanovMarxSaurabh2018, Theorem 2.11] [Ilango2020FOCS, Section III.B, p. 427; ECCC @@ -1546,4 +1194,5 @@ theorem ETH.not_decidableInSubexpTime_BipartitePermutationIndependentSet_two_mul ≤ (2 * G.1) * (2 * Nat.log 2 G.1) := Nat.mul_le_mul_left _ hlog _ ≤ 4 * (G.1 * Nat.log 2 G.1) + 4 := by ring_nf; omega +end end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/FineGrained/Reduction.lean b/Complexity/Computability/Complexity/FineGrained/Reduction.lean index 82b0f0e707..64935ff8eb 100644 --- a/Complexity/Computability/Complexity/FineGrained/Reduction.lean +++ b/Complexity/Computability/Complexity/FineGrained/Reduction.lean @@ -8,8 +8,8 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.FineGrained.Sparsification -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic /-! # Reductions of linear size @@ -23,6 +23,11 @@ decider. The polynomial absorbs the running time of the reduction and the length Hence subexponential time in `μB` gives subexponential time in `μA` (`Cslib.Complexity.DecidableInSubexpTime.of_reduction`). +More generally, subexponential time transfers along **$2^{O(m(a))}$-time reductions** +(`Cslib.Complexity.DecidableInSubexpTime.of_expReduction`), where the target measure is bounded +linearly in $m(a) \log_2 m(a)$ and the $2^{O(m(a))}$ runtime is absorbed into +$2^{(\varepsilon / 2) m(a) \log_2 m(a)}$. + Under the exponential time hypothesis, 3SAT is not decidable in subexponential time in the number of clauses (`Cslib.Complexity.ETH_iff_not_decidableInSubexpTime_length`, by the sparsification lemma). So a polynomial-time reduction from 3SAT whose output measure is linear in the number of @@ -39,6 +44,8 @@ stronger: a lower bound for a measure gives one for every measure at most linear * `Cslib.Complexity.DecidableInExpTime.of_reduction`, `Cslib.Complexity.DecidableInSubexpTime.of_reduction`: transfer along reductions of linear size. +* `Cslib.Complexity.DecidableInSubexpTime.of_expReduction`: subexponential-time transfer along + $2^{O(m)}$-time reductions into parameter $m \log_2 m$. * `Cslib.Complexity.ETH.not_decidableInSubexpTime_of_reduction`: lower bounds from the exponential time hypothesis through reductions of linear size from 3SAT. @@ -209,6 +216,163 @@ theorem ETH.not_decidableInSubexpTime_of_reduction (hETH : ETH) {f : CNF ℕ → simp only [List.length_singleton, mul_one] at this nlinarith +/-! ### Exponential-time reductions into $m \log_2 m$ -/ + +/-- For any constant $C \ge 0$ and $\varepsilon > 0$, $(C : \mathbb{R}) \cdot n$ is bounded by an +$\varepsilon$-dependent constant plus $(\varepsilon / 2) \cdot n \log_2 n$. -/ +private theorem mul_le_pow_add_mul_log (C : ℕ) {ε : ℝ} (hε : 0 < ε) (n : ℕ) : + (C : ℝ) * n ≤ C * ((2 ^ (⌈(2 * C : ℝ) / ε⌉₊ + 1) : ℕ) : ℝ) + + (ε / 2) * (n * Nat.log 2 n : ℝ) := by + set M : ℕ := ⌈(2 * C : ℝ) / ε⌉₊ + 1 + have hnonneg : 0 ≤ (ε / 2) * (n * Nat.log 2 n : ℝ) := by positivity + have hpow_nonneg : 0 ≤ (C : ℝ) * ((2 ^ M : ℕ) : ℝ) := by positivity + by_cases hn : n < 2 ^ M + · have hn_le : (n : ℝ) ≤ ((2 ^ M : ℕ) : ℝ) := by exact_mod_cast hn.le + have h1 : (C : ℝ) * n ≤ C * ((2 ^ M : ℕ) : ℝ) := + mul_le_mul_of_nonneg_left hn_le (Nat.cast_nonneg C) + linarith + · have hn' : 2 ^ M ≤ n := not_lt.mp hn + have hlog : M ≤ Nat.log 2 n := Nat.le_log_of_pow_le Nat.one_lt_two hn' + have hM_ge : (2 * C : ℝ) / ε ≤ M := + (Nat.le_ceil ((2 * C : ℝ) / ε)).trans (by simp [M]) + have hlog_ge : (2 * C : ℝ) / ε ≤ (Nat.log 2 n : ℝ) := + hM_ge.trans (by exact_mod_cast hlog) + have hC_le : (C : ℝ) ≤ (ε / 2) * (Nat.log 2 n : ℝ) := by + rw [div_le_iff₀ hε] at hlog_ge + linarith + have hmul := mul_le_mul_of_nonneg_right hC_le (Nat.cast_nonneg n) + linarith [show (ε / 2) * (Nat.log 2 n : ℝ) * n = (ε / 2) * (n * Nat.log 2 n : ℝ) by ring] + +/-- **Subexponential-time transfer along $2^{O(m(a))}$-time reductions.** If $f : \alpha \to \beta$ +is computable in time $O(2^{C m(a)} \cdot (|a| + 1)^D)$, reduces $A$ to $B$, and maps every +instance $a$ to one with parameter $\mu_B(f(a)) \le c \cdot m(a) \log_2 m(a) + c$, then a +$2^{o(\mu_B)}$-time decider for $B$ yields a $2^{o(m \log m)}$-time decider for $A$. -/ +theorem DecidableInSubexpTime.of_expReduction {f : α → β} {m : α → ℕ} + (hf : ∃ C D : ℕ, ComputableInO f encA encB + (fun a => 2 ^ (C * m a) * ((encA a).length + 1) ^ D) + (fun a => 2 ^ (C * m a) * ((encA a).length + 1) ^ D)) + (hfA : ∀ a, a ∈ A ↔ f a ∈ B) {c : ℕ} + (hμ : ∀ a, μB (f a) ≤ c * (m a * Nat.log 2 (m a)) + c) + (h : DecidableInSubexpTime B encB μB) : + DecidableInSubexpTime A encA (fun a => m a * Nat.log 2 (m a)) := by + intro ε hε + obtain ⟨C, D, hfO⟩ := hf + have hfO := hfO.tidy + obtain ⟨l, hl⟩ := hfO.length_le_time + set δ : ℝ := ε / (2 * (c + 1)) + have hδ : 0 < δ := by positivity + obtain ⟨e, hdec⟩ := h δ hδ + obtain ⟨g, t, k, hg, hgB, ht⟩ := hdec.exists_computableInO + have hg := hg.tidy + set C' : ℕ := C * (e + 1) + set E : ℕ := D * (e + 1) + set M : ℕ := ⌈(2 * C' : ℝ) / ε⌉₊ + 1 + set K₀ : ℝ := 2 ^ ((C' : ℝ) * ((2 ^ M : ℕ) : ℝ)) + set K₁ : ℝ := 1 + k * 2 ^ (δ * c) * (2 * l + 1) ^ e + k + set K : ℝ := K₁ * K₀ + refine DecidableInExpTime.of_computableInO (.of_tidy (hg.comp hfO)) + (fun a => (hfA a).trans (hgB (f a))) + ⌈K⌉₊ E fun a => ?_ + show _ ≤ _ + set L : ℕ := (encA a).length + set P_exp : ℝ := 2 ^ ((C : ℝ) * m a) + set P_poly : ℝ := ((L : ℝ) + 1) ^ D + set P : ℝ := P_exp * P_poly + set X₁ : ℝ := 2 ^ ((ε / 2) * (m a * Nat.log 2 (m a) : ℕ)) + set X : ℝ := 2 ^ (ε * (m a * Nat.log 2 (m a) : ℕ)) + have hP_exp1 : 1 ≤ P_exp := Real.one_le_rpow (by norm_num) (by positivity) + have hP_poly1 : 1 ≤ P_poly := + one_le_pow₀ (by linarith [(Nat.cast_nonneg L : (0 : ℝ) ≤ L)]) + have hP : 1 ≤ P := one_le_mul_of_one_le_of_one_le hP_exp1 hP_poly1 + have hX₁ : 1 ≤ X₁ := Real.one_le_rpow (by norm_num) (by positivity) + have hk : (0 : ℝ) ≤ k := Nat.cast_nonneg k + have hP_nat : ((2 ^ (C * m a) * (L + 1) ^ D : ℕ) : ℝ) = P := by + simp only [P, P_exp, P_poly] + rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_natCast] + push_cast + rfl + have hlen : ((encB (f a)).length : ℝ) + 1 ≤ (2 * l + 1) * P := by + have h1 : ((encB (f a)).length : ℝ) ≤ l * (P + 1) := by + have := hl a + rw [← hP_nat] + exact_mod_cast this + nlinarith + have hcδ : (c : ℝ) * δ ≤ ε / 2 := by + simp only [δ] + rw [mul_div_assoc', div_le_iff₀ (by positivity)] + nlinarith + have hexp : (2 : ℝ) ^ (δ * μB (f a)) ≤ 2 ^ (δ * c) * X₁ := by + 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 + exact_mod_cast hμ a + have hmul := mul_le_mul_of_nonneg_right hcδ (Nat.cast_nonneg (m a * Nat.log 2 (m a))) + nlinarith + have hpow : (((encB (f a)).length : ℝ) + 1) ^ e ≤ (2 * l + 1) ^ e * P ^ e := by + rw [← mul_pow] + exact pow_le_pow_left₀ (by positivity) hlen e + have ht' : (t (f a) : ℝ) ≤ + k * (2 ^ (δ * c) * (2 * l + 1) ^ e) * (X₁ * P ^ e) + k := by + refine (ht (f a)).trans ?_ + have := mul_le_mul hexp hpow (by positivity) (by positivity) + nlinarith + have hPe : P ^ e ≤ P ^ (e + 1) := pow_le_pow_right₀ hP (Nat.le_succ e) + have hP1 : P ≤ P ^ (e + 1) := le_self_pow₀ hP (Nat.succ_ne_zero e) + have hX₁P : 1 ≤ X₁ * P ^ (e + 1) := one_le_mul_of_one_le_of_one_le hX₁ (one_le_pow₀ hP) + have hstep1 : P + (t (f a) : ℝ) ≤ K₁ * (X₁ * P ^ (e + 1)) := by + have h₁ : P ≤ X₁ * P ^ (e + 1) := hP1.trans (le_mul_of_one_le_left (by positivity) hX₁) + have h₂ : X₁ * P ^ e ≤ X₁ * P ^ (e + 1) := mul_le_mul_of_nonneg_left hPe (by positivity) + have h₃ := mul_le_mul_of_nonneg_left h₂ + (by positivity : (0 : ℝ) ≤ k * (2 ^ (δ * c) * (2 * l + 1) ^ e)) + have h₄ := mul_le_mul_of_nonneg_left hX₁P hk + simp only [K₁] + nlinarith + have hP_exp_pow : P_exp ^ (e + 1) ≤ K₀ * X₁ := by + have hrpow : P_exp ^ (e + 1) = 2 ^ ((C' : ℝ) * m a) := by + simp only [P_exp, C', ← Real.rpow_natCast] + rw [← Real.rpow_mul (by norm_num)] + congr 1 + push_cast + ring + rw [hrpow] + have hK₀X₁ : K₀ * X₁ = + 2 ^ ((C' : ℝ) * ((2 ^ M : ℕ) : ℝ) + (ε / 2) * (m a * Nat.log 2 (m a) : ℕ)) := by + simp only [K₀, X₁] + rw [← Real.rpow_add (by norm_num)] + rw [hK₀X₁] + refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ + simpa only [Nat.cast_mul] using mul_le_pow_add_mul_log C' hε (m a) + have hP_poly_pow : P_poly ^ (e + 1) = ((L : ℝ) + 1) ^ E := by + simp only [P_poly, E, ← pow_mul] + have hX₁_sq : X₁ * X₁ = X := by + simp only [X₁, X] + rw [← Real.rpow_add (by norm_num)] + congr 1 + ring + have hstep2 : X₁ * P ^ (e + 1) ≤ K₀ * (X * ((L : ℝ) + 1) ^ E) := by + have hsplit : X₁ * P ^ (e + 1) = X₁ * P_exp ^ (e + 1) * P_poly ^ (e + 1) := by + simp only [P, mul_pow] + ring + rw [hsplit, hP_poly_pow] + have hmul1 := mul_le_mul_of_nonneg_left hP_exp_pow (by positivity : (0 : ℝ) ≤ X₁) + have hmul2 := mul_le_mul_of_nonneg_right hmul1 (by positivity : (0 : ℝ) ≤ ((L : ℝ) + 1) ^ E) + calc X₁ * P_exp ^ (e + 1) * ((L : ℝ) + 1) ^ E + ≤ X₁ * (K₀ * X₁) * ((L : ℝ) + 1) ^ E := hmul2 + _ = K₀ * ((X₁ * X₁) * ((L : ℝ) + 1) ^ E) := by ring + _ = K₀ * (X * ((L : ℝ) + 1) ^ E) := by rw [hX₁_sq] + have hK_ceil : K ≤ ⌈K⌉₊ := Nat.le_ceil K + have hLHS : (((2 ^ (C * m a) * (L + 1) ^ D + t (f a) : ℕ) : ℝ)) = + P + (t (f a) : ℝ) := by + rw [Nat.cast_add, hP_nat] + calc (((2 ^ (C * m a) * (L + 1) ^ D + t (f a) : ℕ) : ℝ)) + = P + (t (f a) : ℝ) := hLHS + _ ≤ K₁ * (X₁ * P ^ (e + 1)) := hstep1 + _ ≤ K₁ * (K₀ * (X * ((L : ℝ) + 1) ^ E)) := + mul_le_mul_of_nonneg_left hstep2 (by positivity) + _ = K * (X * ((L : ℝ) + 1) ^ E) := by simp only [K, mul_assoc] + _ ≤ ⌈K⌉₊ * (X * ((L : ℝ) + 1) ^ E) := + mul_le_mul_of_nonneg_right hK_ceil (by positivity) + end Reduction end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Parameterized/VertexCover.lean b/Complexity/Computability/Complexity/Parameterized/VertexCover.lean index 682251ba95..7c1d4762a5 100644 --- a/Complexity/Computability/Complexity/Parameterized/VertexCover.lean +++ b/Complexity/Computability/Complexity/Parameterized/VertexCover.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Complexity.Parameterized.Kernelization public import Complexity.Computability.Complexity.Problems.VertexCover +import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Binary import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic @@ -33,8 +34,8 @@ step `j` (`Cslib.Complexity.VertexCover.foldBranch`). To keep the path length bo of the graph even when the binary target `k` exceeds the number `n` of distinct declared vertices, the search caps the depth at `min n k` (`Cslib.Complexity.VertexCover.cap`) and checks `k ≤ n` separately (`Cslib.Complexity.mem_VertexCover_iff_exists_card_le`). Iterating over the -`2 ^ min n k` paths (`Cslib.Complexity.VertexCover.search`) runs within time `2 ^ k` times a -polynomial in the length of the encoded instance +`2 ^ min n k` paths (`Cslib.Complexity.DecidableInExpTime.of_exhaustiveSearch`) runs within time +`2 ^ k` times a polynomial in the length of the encoded instance (`Cslib.Complexity.VertexCover_decidableInExpTime_one`), so `VertexCover` is fixed-parameter tractable in the target size `k` (`Cslib.Complexity.VertexCover_mem_FPT`). @@ -49,7 +50,6 @@ tractable in the target size `k` (`Cslib.Complexity.VertexCover_mem_FPT`). * `Cslib.Complexity.VertexCover.exists_lt_two_pow_isCover_foldBranch`: if a graph has a vertex cover of at most `m` vertices, one of the `2 ^ m` paths of length `m` finds a cover. * `Cslib.Complexity.VertexCover.search_eq_true_iff`: `VertexCover.search` decides `VertexCover`. -* `Cslib.Complexity.VertexCover.exists_computableInO_search`: its running time. * `Cslib.Complexity.VertexCover_decidableInExpTime_one`: `VertexCover` is decidable within time `2 ^ k` times a polynomial in the length of the encoded instance. * `Cslib.Complexity.VertexCover_mem_FPT`, `Cslib.Complexity.VertexCover_hasKernel`: `VertexCover` @@ -234,51 +234,20 @@ def cap (x : Graph × ℕ) : ℕ := theorem cap_eq (x : Graph × ℕ) : cap x = min x.1.1.toFinset.card x.2 := by rw [cap, Graph.length_distinctVertices] -private theorem cap_le_length (x : Graph × ℕ) : cap x ≤ (encGraph x.1).length := - (Nat.min_le_left _ _).trans x.1.length_distinctVertices_le - theorem cap_le_snd (x : Graph × ℕ) : cap x ≤ x.2 := Nat.min_le_right _ _ -/-- The state of the bounded-search-tree iteration: the instance `(G, k)`, the capped depth `cap` -in unary, the number of the next root-to-leaf path to try, and whether a cover has been found. -/ -abbrev State : Type := ((Graph × ℕ) × ℕ) × (ℕ × Bool) - -/-- States encoded as framed tuples, with the capped depth in unary. -/ -private abbrev encState : State ↪ List Bool := - encPair (encPair (encPair encGraph encNat) encUnary) (encPair encNat encBool) - -/-- Try the next numbered path in the bounded search tree. -/ -def step (s : State) : State := - (s.1, (s.2.1 + 1, - s.2.2 || isCover s.1.1.1 (foldBranch s.1.1.1 ((List.range s.1.2).map s.2.1.testBit)))) - -/-- The initial state: no path tried yet. -/ -def init (x : Graph × ℕ) : State := ((x, cap x), (0, false)) - -/-- Check that the target `k` is at most `|V|` (`s.1.2 = s.1.1.2`) and that a cover was found. -/ -def finish (s : State) : Bool := - decide (s.1.2 = s.1.1.2) && s.2.2 - /-- **Bounded-search-tree decision procedure for `VertexCover`**: try all `2 ^ cap x` paths of length `cap x` and check that `k ≤ |V|` (`cap x = k`). -/ def search (x : Graph × ℕ) : Bool := - finish (step^[2 ^ cap x] (init x)) - -private theorem iterate_step_init (x : Graph × ℕ) (j : ℕ) : - step^[j] (init x) = ((x, cap x), - (j, (List.range j).any fun i => - isCover x.1 (foldBranch x.1 ((List.range (cap x)).map i.testBit)))) := by - induction j with - | zero => rfl - | succ j ih => - rw [Function.iterate_succ_apply', ih, step, List.range_succ, List.any_append] - simp + decide (cap x = x.2) && + (List.range (2 ^ cap x)).any fun i => + isCover x.1 (foldBranch x.1 ((List.range (cap x)).map i.testBit)) /-- **`VertexCover.search` decides `VertexCover`.** -/ theorem search_eq_true_iff (x : Graph × ℕ) : search x = true ↔ x ∈ VertexCover := by rcases x with ⟨G, k⟩ - rw [search, iterate_step_init, finish, mem_VertexCover_iff_exists_card_le] + rw [search, mem_VertexCover_iff_exists_card_le] simp only [Bool.and_eq_true, decide_eq_true_eq, List.any_eq_true, List.mem_range, cap_eq, min_eq_right_iff] refine and_congr_right fun hk => ?_ @@ -336,13 +305,19 @@ private theorem length_encList_branchStep_le (G : Graph) (C : List ℕ) (b : Boo · simp only [↓reduceIte] omega +/-- Candidate path tuples `((G, k), cap (G, k), i)`, with `cap (G, k)` in unary. -/ +private abbrev Cand : Type := ((Graph × ℕ) × ℕ) × ℕ + +private abbrev encCand : Cand ↪ List Bool := + encPair (encPair (encPair encGraph encNat) encUnary) encNat + open ComputableTidilyInPolyTime in /-- Computing the `m` branching bits of path `i` is polynomial-time. -/ private theorem computableTidilyInPolyTime_branchBits : - ComputableTidilyInPolyTime (fun s : State => (List.range s.1.2).map s.2.1.testBit) - encState (encList encBool) := by - have heq : (fun s : State => (List.range s.1.2).map s.2.1.testBit) = - fun s => (List.range s.1.2).map fun j => (encNat s.2.1).getD j false := by + ComputableTidilyInPolyTime (fun s : Cand => (List.range s.1.2).map s.2.testBit) + encCand (encList encBool) := by + have heq : (fun s : Cand => (List.range s.1.2).map s.2.testBit) = + fun s => (List.range s.1.2).map fun j => (encNat s.2).getD j false := by funext s congr 1 funext j @@ -350,150 +325,79 @@ private theorem computableTidilyInPolyTime_branchBits : rfl rw [heq] exact mapWithInput (range.comp ((snd _ _).comp (fst _ _))) - (bitsGetDWithInput ((encode encNat).comp ((fst _ _).comp ((snd _ _).comp (fst _ _)))) + (bitsGetDWithInput ((encode encNat).comp ((snd _ _).comp (fst _ _))) (snd _ _) false) open ComputableTidilyInPolyTime in /-- Following a root-to-leaf path in the bounded search tree is polynomial-time. -/ private theorem computableTidilyInPolyTime_foldBranch : ComputableTidilyInPolyTime - (fun s : State => foldBranch s.1.1.1 ((List.range s.1.2).map s.2.1.testBit)) - encState (encList encNat) := by - have hG : ComputableTidilyInPolyTime (fun s : State => s.1.1.1) encState encGraph := by fun_prop - have hgrowth_poly : PolyBounded (fun s : State => (encState s).length) - (fun s : State => 2 * (encGraph s.1.1.1).length + 2) := + (fun s : Cand => foldBranch s.1.1.1 ((List.range s.1.2).map s.2.testBit)) + encCand (encList encNat) := by + have hG : ComputableTidilyInPolyTime (fun s : Cand => s.1.1.1) encCand encGraph := by fun_prop + have hgrowth_poly : PolyBounded (fun s : Cand => (encCand s).length) + (fun s : Cand => 2 * (encGraph s.1.1.1).length + 2) := ((PolyBounded.const 2).mul hG.polyBounded_length).add (.const 2) exact foldlWith_of_bounded_growth hG computableTidilyInPolyTime_branchBits (const []) computableInPolyTime_branchStep.tidy hgrowth_poly fun s C b _ => length_encList_branchStep_le s.1.1.1 C b open ComputableTidilyInPolyTime in -/-- One step of the search iteration is polynomial-time. -/ -private theorem computableTidilyInPolyTime_step - : ComputableTidilyInPolyTime step encState encState := by +/-- Checking whether candidate path `i` yields a valid vertex cover of size `k ≤ |V|` is +polynomial-time. -/ +private theorem computableInPolyTime_checkCand : + ComputableInPolyTime + (fun s : Cand => + decide (s.1.2 = s.1.1.2) && + isCover s.1.1.1 (foldBranch s.1.1.1 ((List.range s.1.2).map s.2.testBit))) + encCand encBool := by + refine .of_tidy ?_ have hcov : ComputableTidilyInPolyTime - (fun s : State => isCover s.1.1.1 (foldBranch s.1.1.1 ((List.range s.1.2).map s.2.1.testBit))) - encState encBool := + (fun s : Cand => isCover s.1.1.1 (foldBranch s.1.1.1 ((List.range s.1.2).map s.2.testBit))) + encCand encBool := computableInPolyTime_isCover.tidy.comp - ((show ComputableTidilyInPolyTime (fun s : State => s.1.1.1) encState encGraph + ((show ComputableTidilyInPolyTime (fun s : Cand => s.1.1.1) encCand encGraph by fun_prop).prod computableTidilyInPolyTime_foldBranch) - have hor : ComputableTidilyInPolyTime - (fun s : State => - s.2.2 || isCover s.1.1.1 (foldBranch s.1.1.1 ((List.range s.1.2).map s.2.1.testBit))) - encState encBool := - bool_or.comp ((show ComputableTidilyInPolyTime (fun s : State => s.2.2) encState encBool - by fun_prop).prod hcov) - exact (fst _ _).prod ((computableTidilyInPolyTime_succ.comp (by fun_prop)).prod hor) - -open ComputableTidilyInPolyTime in -/-- The initial state of the search is computed in polynomial time. -/ -private theorem computableTidilyInPolyTime_init : - ComputableTidilyInPolyTime init (encPair encGraph encNat) encState := by - have hcap := computableInPolyTime_cap.tidy - unfold init - fun_prop - -open ComputableTidilyInPolyTime in -/-- The number `2 ^ cap x` of paths is computed in binary in polynomial time. -/ -private theorem computableTidilyInPolyTime_count : - ComputableTidilyInPolyTime (fun x => 2 ^ cap x) (encPair encGraph encNat) encNat := by - have hcap := computableInPolyTime_cap.tidy - fun_prop - -open ComputableTidilyInPolyTime in -/-- Extracting the final answer from the search state is polynomial-time. -/ -private theorem computableTidilyInPolyTime_finish : - ComputableTidilyInPolyTime finish encState encBool := by - unfold finish exact bool_and' ((unary_to_binary.comp ((snd _ _).comp (fst _ _))).decide_eq' (by fun_prop)) - (by fun_prop) - -/-- **Running time of the bounded search tree for `VertexCover`**: within time `2 ^ k` times a -polynomial in the length of the encoded instance. -/ -theorem exists_computableInO_search : ∃ e, ComputableInO search - (encPair encGraph encNat) encBool - (fun x => 2 ^ x.2 * ((encPair encGraph encNat x).length + 1) ^ e) - fun x => 2 ^ x.2 * ((encPair encGraph encNat x).length + 1) ^ e := by - have this : ∃ e, ComputableTidilyInO search (encPair encGraph encNat) encBool - (fun x => 2 ^ x.2 * ((encPair encGraph encNat x).length + 1) ^ e) fun x => 2 ^ x.2 * - ((encPair encGraph encNat x).length + 1) ^ e := by - obtain ⟨d, _, hstep⟩ := computableTidilyInPolyTime_step.exists_degree - obtain ⟨d₀, _, hinit⟩ := computableTidilyInPolyTime_init.exists_degree - obtain ⟨d₁, _, hcount⟩ := computableTidilyInPolyTime_count.exists_degree - obtain ⟨d₂, _, hans⟩ := computableTidilyInPolyTime_finish.exists_degree - set size : Graph × ℕ → ℕ := fun x => (encPair encGraph encNat x).length - set B : Graph × ℕ → ℕ := fun x => 16 * (size x + 1) - have hcap (x : Graph × ℕ) : cap x ≤ size x := - (cap_le_length x).trans (by simp only [size, length_encPair]; omega) - have hstate : ∀ x, ∀ j ≤ 2 ^ cap x, - (encState (step^[j] (init x))).length ≤ B x := by - intro x j hj - have hK := ComputableTidilyInO.length_encNat_mono hj - rw [encNat_two_pow] at hK - have h₁ := hcap x - rw [iterate_step_init] - simp only [List.length_append, List.length_replicate, List.length_singleton] at hK - simp only [encState, length_encPair, encUnary_apply, List.length_replicate, encBool_apply, - List.length_singleton, B, size] at h₁ ⊢ - omega - have hiter := ComputableTidilyInO.iterate hcount.inO hinit.inO hstep.inO - (R := fun x => (B x + 1) ^ d) (Q := fun x => (B x + 1) ^ d) (B := B) - (fun x j hj => Nat.pow_le_pow_left (Nat.add_le_add_right (hstate x j hj) 1) d) - (fun x j hj => Nat.pow_le_pow_left (Nat.add_le_add_right (hstate x j hj) 1) d) hstate - have h := hans.inO.comp hiter - have hB : PolyBounded size B := .of_forall_le 16 1 fun _ => by simp [B] - have hpow (j : ℕ) : PolyBounded size fun x => (B x + 1) ^ j := - ((PolyBounded.of_polynomiallyBounded id (bound := fun n => (n + 1) ^ j) (by fun_prop)).comp - hB).mono fun _ => le_rfl - have hL (j : ℕ) : PolyBounded size fun x => (size x + 1) ^ j := - .of_forall_le 1 j fun _ => by simp - obtain ⟨c, e, hT⟩ := exists_le_mul_two_pow_of_polyBounded (size := size) (μ := Prod.snd) - ((hpow d).add (hB.add (.of_forall_le 4 2 fun _ => le_rfl))) - ((hL d₁).add ((hL d₀).add (hpow d₂))) - (T := fun x => ((encPair encGraph encNat x).length + 1) ^ d₁ + - ((encPair encGraph encNat x).length + 1) ^ d₀ + - (2 ^ cap x + 1) * ((B x + 1) ^ d + B x + ((encNat (2 ^ cap x)).length + 1) ^ 2) + - ((encState (step^[2 ^ cap x] (init x))).length + 1) ^ d₂) - (fun x => by - have hK : ((encNat (2 ^ cap x)).length + 1) ^ 2 ≤ 4 * (size x + 1) ^ 2 := by - rw [encNat_two_pow] - simp only [List.length_append, List.length_replicate, List.length_singleton] - calc (cap x + 1 + 1) ^ 2 ≤ (2 * (size x + 1)) ^ 2 := - Nat.pow_le_pow_left (by have := hcap x; omega) 2 - _ = 4 * (size x + 1) ^ 2 := by ring - have hS := Nat.pow_le_pow_left (Nat.add_le_add_right (hstate x _ le_rfl) 1) d₂ - have h2 : 2 ^ cap x ≤ 2 ^ x.2 := Nat.pow_le_pow_right (by norm_num) (cap_le_snd x) - have h3 := Nat.mul_le_mul (Nat.add_le_add_right h2 1) - (Nat.add_le_add_left hK ((B x + 1) ^ d + B x)) - simp only [size] at h3 hS ⊢ - nlinarith) - refine ⟨e, (h.mono c (fun x => ?_) fun x => ?_).of_enc_eq fun x => rfl⟩ - all_goals - have h₁ := hT x - simp only [size] at h₁ - generalize 2 ^ cap x = N at h₁ ⊢ - generalize (encNat N).length = K at h₁ ⊢ - obtain ⟨X, hX⟩ : ∃ X, (B x + 1) ^ d + B x = X := ⟨_, rfl⟩ - rw [hX] at h₁ - have h₂ : K ≤ (K + 1) ^ 2 := by nlinarith - have h₃ : X + (K + 1) ^ 2 ≤ (N + 1) * (X + (K + 1) ^ 2) := Nat.le_mul_of_pos_left _ (by omega) - nlinarith - simpa only [computableInO_iff_computableTidilyInO] using this + hcov end VertexCover +open ComputableTidilyInPolyTime in /-- **`VertexCover` by bounded search tree**: `VertexCover` is decidable within time `2 ^ k` times a polynomial in the length of the encoded instance, for target cover size `k`. -/ theorem VertexCover_decidableInExpTime_one : DecidableInExpTime VertexCover (encPair encGraph encNat) Prod.snd 1 := by - obtain ⟨e, h⟩ := VertexCover.exists_computableInO_search - refine DecidableInExpTime.of_computableInO h (fun x => (VertexCover.search_eq_true_iff x).symm) 1 - e - fun x => ?_ - rw [one_mul, Real.rpow_natCast] - push_cast - rw [one_mul] + have hB : DecidableInExpTime + {s : VertexCover.Cand | + (decide (s.1.2 = s.1.1.2) && + VertexCover.isCover s.1.1.1 + (VertexCover.foldBranch s.1.1.1 ((List.range s.1.2).map s.2.testBit))) = true} + VertexCover.encCand (fun _ => 0) 0 := + .of_computableInPolyTime VertexCover.computableInPolyTime_checkCand (fun _ => Iff.rfl) + have hf : ComputableInPolyTime + (fun q : (Graph × ℕ) × ℕ => ((q.1, VertexCover.cap q.1), q.2)) + (encPair (encPair encGraph encNat) encNat) VertexCover.encCand := by + have := VertexCover.computableInPolyTime_cap.tidy + exact .of_tidy (by fun_prop) + have hfA (x : Graph × ℕ) : x ∈ VertexCover ↔ ∃ i < 2 ^ VertexCover.cap x, + ((x, VertexCover.cap x), i) ∈ + {s : VertexCover.Cand | + (decide (s.1.2 = s.1.1.2) && + VertexCover.isCover s.1.1.1 + (VertexCover.foldBranch s.1.1.1 ((List.range s.1.2).map s.2.testBit))) = true} := by + rw [← VertexCover.search_eq_true_iff, VertexCover.search] + simp only [Bool.and_eq_true, decide_eq_true_eq, List.any_eq_true, List.mem_range, + Set.mem_ofPred_eq] + constructor + · rintro ⟨hcap, i, hi, hcov⟩ + exact ⟨i, hi, hcap, hcov⟩ + · rintro ⟨i, hi, hcap, hcov⟩ + exact ⟨hcap, i, hi, hcov⟩ + simpa using hB.of_exhaustiveSearch hf VertexCover.computableInPolyTime_cap hfA + (c := 0) (fun _ _ => Nat.zero_le _) (M := 1) (K := 0) + (fun x => by simpa using VertexCover.cap_le_snd x) le_rfl /-- **`VertexCover` is fixed-parameter tractable** in the target cover size `k`. -/ theorem VertexCover_mem_FPT : VertexCover ∈ FPT (encPair encGraph encNat) Prod.snd := diff --git a/Complexity/Computability/MCSP/PartialETH.lean b/Complexity/Computability/MCSP/PartialETH.lean index 38a801c49c..6d51f6196f 100644 --- a/Complexity/Computability/MCSP/PartialETH.lean +++ b/Complexity/Computability/MCSP/PartialETH.lean @@ -2091,155 +2091,6 @@ theorem arity_mul_log_ilangoReduction_le (G : BipartitePermutationGraph) : ≤ 6 * G.1 * (4 * Nat.log 2 G.1) := Nat.mul_le_mul_left _ hlog_le _ ≤ 24 * (G.1 * Nat.log 2 G.1) + 2 := by ring_nf; omega -private theorem mul_le_pow_add_mul_log (C : ℕ) {ε : ℝ} (hε : 0 < ε) (n : ℕ) : - (C : ℝ) * n ≤ C * ((2 ^ (⌈(2 * C : ℝ) / ε⌉₊ + 1) : ℕ) : ℝ) + - (ε / 2) * (n * Nat.log 2 n : ℝ) := by - set M : ℕ := ⌈(2 * C : ℝ) / ε⌉₊ + 1 - have hnonneg : 0 ≤ (ε / 2) * (n * Nat.log 2 n : ℝ) := by positivity - have hpow_nonneg : 0 ≤ (C : ℝ) * ((2 ^ M : ℕ) : ℝ) := by positivity - by_cases hn : n < 2 ^ M - · have hn_le : (n : ℝ) ≤ ((2 ^ M : ℕ) : ℝ) := by exact_mod_cast hn.le - have h1 : (C : ℝ) * n ≤ C * ((2 ^ M : ℕ) : ℝ) := - mul_le_mul_of_nonneg_left hn_le (Nat.cast_nonneg C) - linarith - · have hn' : 2 ^ M ≤ n := not_lt.mp hn - have hlog : M ≤ Nat.log 2 n := Nat.le_log_of_pow_le Nat.one_lt_two hn' - have hM_ge : (2 * C : ℝ) / ε ≤ M := - (Nat.le_ceil ((2 * C : ℝ) / ε)).trans (by simp [M]) - have hlog_ge : (2 * C : ℝ) / ε ≤ (Nat.log 2 n : ℝ) := - hM_ge.trans (by exact_mod_cast hlog) - have hC_le : (C : ℝ) ≤ (ε / 2) * (Nat.log 2 n : ℝ) := by - rw [div_le_iff₀ hε] at hlog_ge - linarith - have hmul := mul_le_mul_of_nonneg_right hC_le (Nat.cast_nonneg n) - linarith [show (ε / 2) * (Nat.log 2 n : ℝ) * n = (ε / 2) * (n * Nat.log 2 n : ℝ) by ring] - -private theorem decidableInSubexpTime_bpis_of_ilangoReduction_aux - {B : Set Instance} {encB : Instance ↪ List Bool} - (hred : ∃ C D : ℕ, ComputableInO ilangoReduction - encBipartitePermutationGraph encB - (fun G => 2 ^ (C * G.1) * ((encBipartitePermutationGraph G).length + 1) ^ D) - (fun G => 2 ^ (C * G.1) * ((encBipartitePermutationGraph G).length + 1) ^ D)) - (hiff : ∀ G, G ∈ BipartitePermutationIndependentSet ↔ ilangoReduction G ∈ B) - (hsub : DecidableInSubexpTime B encB fun I => I.arity * Nat.log 2 I.arity) : - DecidableInSubexpTime BipartitePermutationIndependentSet encBipartitePermutationGraph - fun G => G.1 * Nat.log 2 G.1 := by - intro ε hε - obtain ⟨C, D, hfO⟩ := hred - have hfO := hfO.tidy - obtain ⟨l, hl⟩ := hfO.length_le_time - set δ : ℝ := ε / 48 - have hδ : 0 < δ := by positivity - obtain ⟨e, hdec⟩ := hsub δ hδ - obtain ⟨g, t, k, hg, hgB, ht⟩ := hdec.exists_computableInO - have hg := hg.tidy - set C' : ℕ := C * (e + 1) - set E : ℕ := D * (e + 1) - set M : ℕ := ⌈(2 * C' : ℝ) / ε⌉₊ + 1 - set K₀ : ℝ := 2 ^ ((C' : ℝ) * ((2 ^ M : ℕ) : ℝ)) - set K₁ : ℝ := 1 + k * 2 ^ (2 * δ) * (2 * l + 1) ^ e + k - set K : ℝ := K₁ * K₀ - refine DecidableInExpTime.of_computableInO (.of_tidy (hg.comp hfO)) - (fun G => (hiff G).trans (hgB (ilangoReduction G))) - ⌈K⌉₊ E fun G => ?_ - show _ ≤ _ - set L : ℕ := (encBipartitePermutationGraph G).length - set P_exp : ℝ := 2 ^ ((C : ℝ) * G.1) - set P_poly : ℝ := ((L : ℝ) + 1) ^ D - set P : ℝ := P_exp * P_poly - set X₁ : ℝ := 2 ^ ((ε / 2) * (G.1 * Nat.log 2 G.1 : ℕ)) - set X : ℝ := 2 ^ (ε * (G.1 * Nat.log 2 G.1 : ℕ)) - have hP_exp1 : 1 ≤ P_exp := Real.one_le_rpow (by norm_num) (by positivity) - have hP_poly1 : 1 ≤ P_poly := - one_le_pow₀ (by linarith [(Nat.cast_nonneg L : (0 : ℝ) ≤ L)]) - have hP : 1 ≤ P := one_le_mul_of_one_le_of_one_le hP_exp1 hP_poly1 - have hX₁ : 1 ≤ X₁ := Real.one_le_rpow (by norm_num) (by positivity) - have hk : (0 : ℝ) ≤ k := Nat.cast_nonneg k - have hP_nat : ((2 ^ (C * G.1) * (L + 1) ^ D : ℕ) : ℝ) = P := by - simp only [P, P_exp, P_poly] - rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_natCast] - push_cast - rfl - have hlen : ((encB (ilangoReduction G)).length : ℝ) + 1 ≤ (2 * l + 1) * P := by - have h1 : ((encB (ilangoReduction G)).length : ℝ) ≤ l * (P + 1) := by - have := hl G - rw [← hP_nat] - exact_mod_cast this - nlinarith - have hexp : (2 : ℝ) ^ (δ * ((ilangoReduction G).arity * - Nat.log 2 (ilangoReduction G).arity : ℕ)) ≤ 2 ^ (2 * δ) * X₁ := by - rw [← Real.rpow_add (by norm_num)] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - have hμ : (((ilangoReduction G).arity * Nat.log 2 (ilangoReduction G).arity : ℕ) : ℝ) ≤ - 24 * (G.1 * Nat.log 2 G.1 : ℕ) + 2 := by - exact_mod_cast arity_mul_log_ilangoReduction_le G - simp only [δ] at hμ ⊢ - nlinarith - have hpow : (((encB (ilangoReduction G)).length : ℝ) + 1) ^ e ≤ (2 * l + 1) ^ e * P ^ e := by - rw [← mul_pow] - exact pow_le_pow_left₀ (by positivity) hlen e - have ht' : (t (ilangoReduction G) : ℝ) ≤ - k * (2 ^ (2 * δ) * (2 * l + 1) ^ e) * (X₁ * P ^ e) + k := by - refine (ht (ilangoReduction G)).trans ?_ - have := mul_le_mul hexp hpow (by positivity) (by positivity) - nlinarith - have hPe : P ^ e ≤ P ^ (e + 1) := pow_le_pow_right₀ hP (Nat.le_succ e) - have hP1 : P ≤ P ^ (e + 1) := le_self_pow₀ hP (Nat.succ_ne_zero e) - have hX₁P : 1 ≤ X₁ * P ^ (e + 1) := one_le_mul_of_one_le_of_one_le hX₁ (one_le_pow₀ hP) - have hstep1 : P + (t (ilangoReduction G) : ℝ) ≤ K₁ * (X₁ * P ^ (e + 1)) := by - have h₁ : P ≤ X₁ * P ^ (e + 1) := hP1.trans (le_mul_of_one_le_left (by positivity) hX₁) - have h₂ : X₁ * P ^ e ≤ X₁ * P ^ (e + 1) := mul_le_mul_of_nonneg_left hPe (by positivity) - have h₃ := mul_le_mul_of_nonneg_left h₂ - (by positivity : (0 : ℝ) ≤ k * (2 ^ (2 * δ) * (2 * l + 1) ^ e)) - have h₄ := mul_le_mul_of_nonneg_left hX₁P hk - simp only [K₁] - nlinarith - have hP_exp_pow : P_exp ^ (e + 1) ≤ K₀ * X₁ := by - have hrpow : P_exp ^ (e + 1) = 2 ^ ((C' : ℝ) * G.1) := by - simp only [P_exp, C', ← Real.rpow_natCast] - rw [← Real.rpow_mul (by norm_num)] - congr 1 - push_cast - ring - rw [hrpow] - have hK₀X₁ : K₀ * X₁ = - 2 ^ ((C' : ℝ) * ((2 ^ M : ℕ) : ℝ) + (ε / 2) * (G.1 * Nat.log 2 G.1 : ℕ)) := by - simp only [K₀, X₁] - rw [← Real.rpow_add (by norm_num)] - rw [hK₀X₁] - refine Real.rpow_le_rpow_of_exponent_le (by norm_num) ?_ - simpa only [Nat.cast_mul] using mul_le_pow_add_mul_log C' hε G.1 - have hP_poly_pow : P_poly ^ (e + 1) = ((L : ℝ) + 1) ^ E := by - simp only [P_poly, E, ← pow_mul] - have hX₁_sq : X₁ * X₁ = X := by - simp only [X₁, X] - rw [← Real.rpow_add (by norm_num)] - congr 1 - ring - have hstep2 : X₁ * P ^ (e + 1) ≤ K₀ * (X * ((L : ℝ) + 1) ^ E) := by - have hsplit : X₁ * P ^ (e + 1) = X₁ * P_exp ^ (e + 1) * P_poly ^ (e + 1) := by - simp only [P, mul_pow] - ring - rw [hsplit, hP_poly_pow] - have hmul1 := mul_le_mul_of_nonneg_left hP_exp_pow (by positivity : (0 : ℝ) ≤ X₁) - have hmul2 := mul_le_mul_of_nonneg_right hmul1 (by positivity : (0 : ℝ) ≤ ((L : ℝ) + 1) ^ E) - calc X₁ * P_exp ^ (e + 1) * ((L : ℝ) + 1) ^ E - ≤ X₁ * (K₀ * X₁) * ((L : ℝ) + 1) ^ E := hmul2 - _ = K₀ * ((X₁ * X₁) * ((L : ℝ) + 1) ^ E) := by ring - _ = K₀ * (X * ((L : ℝ) + 1) ^ E) := by rw [hX₁_sq] - have hK_ceil : K ≤ ⌈K⌉₊ := Nat.le_ceil K - have hLHS : (((2 ^ (C * G.1) * (L + 1) ^ D + t (ilangoReduction G) : ℕ) : ℝ)) = - P + (t (ilangoReduction G) : ℝ) := by - rw [Nat.cast_add, hP_nat] - calc (((2 ^ (C * G.1) * (L + 1) ^ D + t (ilangoReduction G) : ℕ) : ℝ)) - = P + (t (ilangoReduction G) : ℝ) := hLHS - _ ≤ K₁ * (X₁ * P ^ (e + 1)) := hstep1 - _ ≤ K₁ * (K₀ * (X * ((L : ℝ) + 1) ^ E)) := - mul_le_mul_of_nonneg_left hstep2 (by positivity) - _ = K * (X * ((L : ℝ) + 1) ^ E) := by simp only [K, mul_assoc] - _ ≤ ⌈K⌉₊ * (X * ((L : ℝ) + 1) ^ E) := - mul_le_mul_of_nonneg_right hK_ceil (by positivity) - /-- **Subexponential-time transfer along Ilango's $2^{O(n)}$-time reduction** (unary threshold encoding `PartialMCSP.enc`): if a target problem `B` on `PartialMCSP.Instance` is decidable in time $2^{o(m \log m)}$ and `ilangoReduction` reduces `BipartitePermutationIndependentSet` to `B`, then @@ -2250,8 +2101,8 @@ theorem decidableInSubexpTime_bpis_of_ilangoReduction (hsub : DecidableInSubexpTime B PartialMCSP.enc fun I => I.arity * Nat.log 2 I.arity) : DecidableInSubexpTime BipartitePermutationIndependentSet encBipartitePermutationGraph fun G => G.1 * Nat.log 2 G.1 := - decidableInSubexpTime_bpis_of_ilangoReduction_aux - exists_computableInO_ilangoReduction hiff hsub + hsub.of_expReduction exists_computableInO_ilangoReduction hiff + (c := 24) fun G => (arity_mul_log_ilangoReduction_le G).trans (by omega) /-- **Subexponential-time transfer along Ilango's $2^{O(n)}$-time reduction** (binary threshold encoding `PartialMCSP.encBinary`): if a target problem `B` on `PartialMCSP.Instance` is decidable in @@ -2263,8 +2114,8 @@ theorem decidableInSubexpTime_bpis_of_ilangoReduction_encBinary (hsub : DecidableInSubexpTime B PartialMCSP.encBinary fun I => I.arity * Nat.log 2 I.arity) : DecidableInSubexpTime BipartitePermutationIndependentSet encBipartitePermutationGraph fun G => G.1 * Nat.log 2 G.1 := - decidableInSubexpTime_bpis_of_ilangoReduction_aux - exists_computableInO_ilangoReduction_encBinary hiff hsub + hsub.of_expReduction exists_computableInO_ilangoReduction_encBinary hiff + (c := 24) fun G => (arity_mul_log_ilangoReduction_le G).trans (by omega) end PartialMCSP