From 458c13940c1a8593f71fc9b0a22d4adf3b80e9ae Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 18:01:58 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(Computability/Kolmogorov):=20formalize?= =?UTF-8?q?=20MKtP=20=E2=88=88=20EXP=20and=20MINcKT=20=E2=88=88=20NP=20(#7?= =?UTF-8?q?98)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Complexity.lean | 2 + .../Computability/Kolmogorov/MINcKT.lean | 853 ++++++++++++++++++ Complexity/Computability/Kolmogorov/MKtP.lean | 535 +++++++++++ ComplexityTests/MINcKT.lean | 108 +++ 4 files changed, 1498 insertions(+) create mode 100644 Complexity/Computability/Kolmogorov/MINcKT.lean create mode 100644 Complexity/Computability/Kolmogorov/MKtP.lean create mode 100644 ComplexityTests/MINcKT.lean diff --git a/Complexity.lean b/Complexity.lean index 11c32d9ffe..57d03178a8 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -859,6 +859,8 @@ public import Complexity.Computability.Kolmogorov.Depth public import Complexity.Computability.Kolmogorov.Incompressibility public import Complexity.Computability.Kolmogorov.Invariance public import Complexity.Computability.Kolmogorov.MINKT +public import Complexity.Computability.Kolmogorov.MINcKT +public import Complexity.Computability.Kolmogorov.MKtP public import Complexity.Computability.Kolmogorov.MultiTape public import Complexity.Computability.Kolmogorov.NisanWigderson public import Complexity.Computability.Kolmogorov.Partrec diff --git a/Complexity/Computability/Kolmogorov/MINcKT.lean b/Complexity/Computability/Kolmogorov/MINcKT.lean new file mode 100644 index 0000000000..ce960a2d52 --- /dev/null +++ b/Complexity/Computability/Kolmogorov/MINcKT.lean @@ -0,0 +1,853 @@ +/- +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.Kolmogorov.MINKT +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Foundations.Data.Nat.PolynomialBound.Closure + +/-! +# Conditional Time-Bounded Kolmogorov Complexity (`K^t(x | y)`) and `MINcKT` + +This module defines the conditional universal multi-tape Turing machine description method +`Cslib.Kolmogorov.DescriptionMethod.condUniversalTM`, the conditional plain, time-bounded, and +Levin Kolmogorov complexities `Cslib.Kolmogorov.condPlain` ($K(x \mid y)$), +`Cslib.Kolmogorov.condTimeBoundedAt` ($K^t(x \mid y)$), `Cslib.Kolmogorov.condTimeBounded`, and +`Cslib.Kolmogorov.condLevinKt` ($\mathrm{Kt}(x \mid y)$), and the decision and promise problems +`Cslib.Kolmogorov.MINcKT`, `Cslib.Kolmogorov.MINcKTAt`, and `Cslib.Kolmogorov.GapMINcKT`. + +## Modeling conventions + +* **Conditioning via `universalTM` on paired inputs:** + Given an auxiliary (condition) string `y : List Bool`, a binary program `p : List Bool` is parsed + into its machine description `unframe p` and program argument `dropFrame p`, and executed under + `universalTM` on the re-framed program + `frame (unframe p) ++ encPair encBits encBits (dropFrame p, y)`. + By `unframe_frame_append` and `dropFrame_frame_append`, at step budget `t` this runs the described + multi-tape machine `decodeDesc (unframe p)` on the paired input + `encPair encBits encBits (dropFrame p, y)` for `t` steps + ([Hirahara, Definition II.5][Hirahara2018]; [Liu and Pass, Section 2.1][LiuPass2021Crypto]). +* **Reuse of `universalTM` and `DescriptionMethod`:** + Because `condUniversalTM y` is defined directly in terms of `universalTM.run`, it inherits step + monotonicity from `universalTM`, polynomial-time evaluation from + `computableInPolyTime_universalTMRunFor`, and counting / incompressibility bounds for every fixed + condition `y` from `Cslib.Kolmogorov.DescriptionMethod` (`Incompressibility.lean`). + +## Main definitions + +* `Cslib.Kolmogorov.DescriptionMethod.condUniversalTMProgram`, + `Cslib.Kolmogorov.DescriptionMethod.condUniversalTMRunFor`, + `Cslib.Kolmogorov.DescriptionMethod.condUniversalTM`: the conditional universal multi-tape + description method for condition string `y`. +* `Cslib.Kolmogorov.condPlain`, `Cslib.Kolmogorov.condPlainNat`: conditional plain Kolmogorov + complexity $K(x \mid y)$ in `ℕ∞` and `ℕ`. +* `Cslib.Kolmogorov.condTimeBoundedAt`, `Cslib.Kolmogorov.condTimeBounded`, + `Cslib.Kolmogorov.condTimeBoundedNat`: step-indexed and function-indexed conditional time-bounded + Kolmogorov complexity $K^t(x \mid y)$ in `ℕ∞` and `ℕ`. +* `Cslib.Kolmogorov.condLevinKt`, `Cslib.Kolmogorov.condLevinKtNat`: conditional Levin complexity + $\mathrm{Kt}(x \mid y)$ in `ℕ∞` and `ℕ`. +* `Cslib.Kolmogorov.MINcKT.Instance`, `Cslib.Kolmogorov.MINcKT`, `Cslib.Kolmogorov.MINcKT.enc`, + `Cslib.Kolmogorov.MINcKT.check`: instances, decision problem, unary-threshold encoding, and + polynomial-time witness verifier for `MINcKT`. +* `Cslib.Kolmogorov.MINcKTAt`: fixed-threshold language + $\{(x, y) \mid K^{t(|x|)}(x \mid y) \le s(|x|)\}$. +* `Cslib.Kolmogorov.GapMINcKT`, `Cslib.Kolmogorov.GapMINcKT.yesSet`, + `Cslib.Kolmogorov.GapMINcKT.noSet`: the conditional promise problem `GapMINcKT[σ, τ]` + ([Hirahara, Definition II.6][Hirahara2018]). + +## Main results + +* `Cslib.Kolmogorov.DescriptionMethod.computableInPolyTime_condUniversalTMRunFor`: polynomial-time + evaluation of `condUniversalTMRunFor`. +* `Cslib.Kolmogorov.DescriptionMethod.exists_condTimeBoundedAt_le_of_multiTapeTM_pair`: + clock-preserving conditional simulation of every finite-state binary `MultiTapeTM` operating on + `encPair encBits encBits (w, y)`. +* `Cslib.Kolmogorov.exists_condTimeBoundedAt_le_of_computableInPolyTime`: for any polynomial-time + `F : List Bool × List Bool → List Bool`, $K^t(F(w, y) \mid y) \le |w| + O(1)$ at polynomial time. +* `Cslib.Kolmogorov.exists_condTimeBoundedAt_apply_le`, + `Cslib.Kolmogorov.exists_condTimeBoundedAt_self_le`: $K^t(f(y) \mid y) \le O(1)$ and + $K^t(y \mid y) \le O(1)$ for polynomial-time $f$. +* `Cslib.Kolmogorov.exists_condTimeBoundedAt_le_length_add`, + `Cslib.Kolmogorov.condPlain_ne_top`, `Cslib.Kolmogorov.condLevinKt_ne_top`: + $K^t(x \mid y) \le |x| + O(1)$ and finiteness of `condPlain` and `condLevinKt`. +* `Cslib.Kolmogorov.encard_setOf_condTimeBoundedAt_lt`, + `Cslib.Kolmogorov.exists_length_eq_forall_le_condTimeBoundedAt`: counting and incompressibility + for $K^t(\cdot \mid y)$ at any fixed condition $y$. +* `Cslib.Kolmogorov.MINcKT.mem_NP`, `Cslib.Kolmogorov.MINcKTAt.mem_NP`: `MINcKT ∈ NP MINcKT.enc` + and `MINcKTAt t s ∈ NP (encPair encBits encBits)`. + +## References + +* [S. Hirahara, *Non-Black-Box Worst-Case to Average-Case Reductions within NP*][Hirahara2018] +* [Y. Liu, R. Pass, *On One-way Functions and Kolmogorov Complexity*][LiuPass2020] +* [Y. Liu, R. Pass, *On the Possibility of Basing Cryptography on EXP ≠ BPP*][LiuPass2021Crypto] +* [E. Allender, H. Buhrman, M. Koucký, D. van Melkebeek, D. Ronneburger, + *Power from Random Strings*][AllenderBuhrmanKouckyVanMelkebeekRonneburger2006] +-/ + +@[expose] public section + +namespace Cslib.Kolmogorov + +open _root_.Turing _root_.Turing.MultiTapeTM _root_.Turing.MultiTapeTM.Universal +open Cslib.Complexity + +namespace DescriptionMethod + +/-! ### The conditional universal multi-tape description method (`condUniversalTM`) -/ + +/-- Re-frames a conditional program `p` with the auxiliary condition string `y` into a program for +`universalTM` whose machine description is `unframe p` and whose input is +`encPair encBits encBits (dropFrame p, y)`. -/ +def condUniversalTMProgram (p y : List Bool) : List Bool := + frame (unframe p) ++ encPair encBits encBits (dropFrame p, y) + +@[simp] +theorem unframe_condUniversalTMProgram (p y : List Bool) : + unframe (condUniversalTMProgram p y) = unframe p := by + simp [condUniversalTMProgram] + +@[simp] +theorem dropFrame_condUniversalTMProgram (p y : List Bool) : + dropFrame (condUniversalTMProgram p y) = encPair encBits encBits (dropFrame p, y) := by + simp [condUniversalTMProgram] + +/-- Clocked evaluation of a binary program `p` given condition string `y` for `t` steps of the +described multi-tape machine. -/ +def condUniversalTMRunFor (p y : List Bool) (t : ℕ) : Option (List Bool) := + universalTMRunFor (condUniversalTMProgram p y) t + +/-- The conditional universal multi-tape Turing machine description method for binary strings, +conditioned on `y : List Bool` ([Hirahara, Definition II.5][Hirahara2018]; +[Liu and Pass, Section 2.1][LiuPass2021Crypto]). -/ +def condUniversalTM (y : List Bool) : DescriptionMethod (List Bool) where + run p := universalTM.run (condUniversalTMProgram p y) + +/-- `((condUniversalTM y).run p).runFor t` is `condUniversalTMRunFor p y t`. -/ +@[simp] +theorem condUniversalTM_runFor (y p : List Bool) (t : ℕ) : + ((condUniversalTM y).run p).runFor t = condUniversalTMRunFor p y t := + rfl + +/-- Running `condUniversalTMRunFor` for `0` steps always returns `none`. -/ +@[simp] +theorem condUniversalTMRunFor_zero (p y : List Bool) : + condUniversalTMRunFor p y 0 = none := + universalTMRunFor_zero _ + +/-- Step monotonicity of `condUniversalTMRunFor`. -/ +theorem condUniversalTMRunFor_mono (p y : List Bool) {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) {x : List Bool} + (h : x ∈ condUniversalTMRunFor p y t₁) : + x ∈ condUniversalTMRunFor p y t₂ := + universalTMRunFor_mono _ ht h + +/-- At `0` steps, `(condUniversalTM y).etimeBoundedComplexity 0 x = ⊤`. -/ +@[simp] +theorem etimeBoundedComplexity_condUniversalTM_zero (y x : List Bool) : + (condUniversalTM y).etimeBoundedComplexity 0 x = ⊤ := by + rw [etimeBoundedComplexity_eq_top_iff] + intro p + simp + +/-- `condUniversalTMProgram` is computable in polynomial time. -/ +@[fun_prop] +theorem computableInPolyTime_condUniversalTMProgram : + ComputableInPolyTime (fun py : List Bool × List Bool => condUniversalTMProgram py.1 py.2) + (encPair encBits encBits) encBits := by + have heq : (fun py : List Bool × List Bool => condUniversalTMProgram py.1 py.2) = + fun py => frame (unframe py.1) ++ (frame (dropFrame py.1) ++ py.2) := by + funext ⟨p, y⟩ + simp [condUniversalTMProgram, encPair_apply] + rw [heq] + fun_prop + +/-- Evaluating `condUniversalTMRunFor` on `(p, (y, t))` is computable in polynomial time when `t` is +given in unary. -/ +@[fun_prop] +theorem computableInPolyTime_condUniversalTMRunFor : + ComputableInPolyTime + (fun pyt : List Bool × (List Bool × ℕ) => condUniversalTMRunFor pyt.1 pyt.2.1 pyt.2.2) + (encPair encBits (encPair encBits encUnary)) (encOption encBits) := by + unfold condUniversalTMRunFor + fun_prop + +/-! ### Clock-preserving conditional simulation of every binary `MultiTapeTM` -/ + +private noncomputable def condMachineHeader {k : ℕ} {State : Type} [Fintype State] + (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) : List Bool := + frame (eDesc (desc eS eBit tm)) + +private theorem condUniversalTM_runFor_condMachineHeader_append {k : ℕ} {State : Type} + [Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) + (w y : List Bool) (t : ℕ) : + ((condUniversalTM y).run (condMachineHeader eS tm ++ w)).runFor t = + ((ofMultiTapeTM tm).run (encPair encBits encBits (w, y))).runFor t := by + have hprog : condUniversalTMProgram (condMachineHeader eS tm ++ w) y = + condMachineHeader eS tm ++ encPair encBits encBits (w, y) := by + simp [condUniversalTMProgram, condMachineHeader] + rw [condUniversalTM_runFor, condUniversalTMRunFor, hprog, condMachineHeader, + universalTMRunFor, Desc.runFor, unframe_frame_append, decodeDesc_eDesc, + dropFrame_frame_append] + have hsim : ((ofMultiTapeTM tm).run (encPair encBits encBits (w, y))).runFor t = + let r := simulate (desc eS eBit tm) ((encPair encBits encBits (w, y)).map eBit) t + if r.2 then some (r.1.map (· != 0)) else none := + tm.runFor_eq_simulate eS (encPair encBits encBits (w, y)) t + rw [hsim] + dsimp only + rcases simulate (desc eS eBit tm) ((encPair encBits encBits (w, y)).map eBit) t with + ⟨out, _ | _⟩ <;> rfl + +/-- **Clock-preserving conditional simulation of `MultiTapeTM`:** for every finite-state binary +`MultiTapeTM`, there is a constant `c` such that whenever `tm` on input +`encPair encBits encBits (w, y)` halts within `t` steps and outputs `x`, `condUniversalTM y` +outputs `x` within `t` steps from a program of length at most `w.length + c`. -/ +theorem exists_etimeBoundedComplexity_condUniversalTM_le_ofMultiTapeTM {k : ℕ} {State : Type} + [Finite State] (tm : MultiTapeTM k Bool State) : + ∃ c : ℕ, ∀ (t : ℕ) (w y x : List Bool), + tm.RunsInTime (encPair encBits encBits (w, y)) t → + tm.Computes (encPair encBits encBits (w, y)) x → + (condUniversalTM y).etimeBoundedComplexity t x ≤ (w.length + c : ℕ) := by + have := Fintype.ofFinite State + let eS : State ↪ ℕ := (Fintype.equivFin State).toEmbedding.trans Fin.valEmbedding + refine ⟨(condMachineHeader eS tm).length, fun t w y x htime hcomp => ?_⟩ + have hmem : x ∈ ((ofMultiTapeTM tm).run (encPair encBits encBits (w, y))).runFor t := + mem_ofMultiTapeTM_runFor_iff.mpr ⟨htime, hcomp⟩ + rw [← condUniversalTM_runFor_condMachineHeader_append eS tm w y t] at hmem + refine (etimeBoundedComplexity_le_length hmem).trans ?_ + rw [List.length_append, Nat.add_comm] + +end DescriptionMethod + +open DescriptionMethod + +/-! ### Conditional Kolmogorov complexity measures (`condPlain`, `condTimeBoundedAt`, +`condTimeBounded`, `condLevinKt`) -/ + +/-- Conditional plain Kolmogorov complexity $K(x \mid y)$ under `condUniversalTM y`, in `ℕ∞`. -/ +noncomputable def condPlain (x y : List Bool) : ℕ∞ := + (condUniversalTM y).ecomplexity x + +/-- Conditional plain Kolmogorov complexity $K(x \mid y)$ as a natural number. -/ +noncomputable def condPlainNat (x y : List Bool) : ℕ := + (condUniversalTM y).complexity x + +/-- Step-indexed conditional time-bounded Kolmogorov complexity $K^t(x \mid y)$ at step budget +`t : ℕ` ([Hirahara, Definition II.5][Hirahara2018]; +[Liu and Pass, Section 2.1][LiuPass2021Crypto]), in `ℕ∞`. -/ +noncomputable def condTimeBoundedAt (t : ℕ) (x y : List Bool) : ℕ∞ := + (condUniversalTM y).etimeBoundedComplexity t x + +/-- Function-indexed conditional time-bounded Kolmogorov complexity $K^t(x \mid y)$ at step budget +`t x.length`, in `ℕ∞`. -/ +noncomputable def condTimeBounded (t : ℕ → ℕ) (x y : List Bool) : ℕ∞ := + condTimeBoundedAt (t x.length) x y + +/-- `condTimeBounded t x y` is `condTimeBoundedAt (t x.length) x y`. -/ +@[simp] +theorem condTimeBounded_eq_condTimeBoundedAt (t : ℕ → ℕ) (x y : List Bool) : + condTimeBounded t x y = condTimeBoundedAt (t x.length) x y := + rfl + +/-- Conditional time-bounded Kolmogorov complexity $K^t(x \mid y)$ as a natural number. -/ +noncomputable def condTimeBoundedNat (t : ℕ → ℕ) (x y : List Bool) : ℕ := + (condTimeBounded t x y).toNat + +/-- Conditional Levin time-bounded Kolmogorov complexity +$\mathrm{Kt}(x \mid y) = \inf_{s \in \mathbb{N}} \bigl(K^s(x \mid y) + \lceil \log_2 s \rceil\bigr)$ +([Allender et al.][AllenderBuhrmanKouckyVanMelkebeekRonneburger2006]; +[Liu and Pass, Section 2.2][LiuPass2021Crypto]), in `ℕ∞`. -/ +noncomputable def condLevinKt (x y : List Bool) : ℕ∞ := + ⨅ s : ℕ, condTimeBoundedAt s x y + Nat.clog 2 s + +/-- Conditional Levin complexity $\mathrm{Kt}(x \mid y)$ as a natural number. -/ +noncomputable def condLevinKtNat (x y : List Bool) : ℕ := + (condLevinKt x y).toNat + +/-! ### Basic properties and equivalence bridges -/ + +/-- At `0` steps, `condTimeBoundedAt 0 x y = ⊤`. -/ +@[simp] +theorem condTimeBoundedAt_zero (x y : List Bool) : condTimeBoundedAt 0 x y = ⊤ := + etimeBoundedComplexity_condUniversalTM_zero y x + +/-- `condTimeBoundedAt t x y ≤ k` iff some program of length at most `k` outputs `x` given `y` +within `t` steps. -/ +theorem condTimeBoundedAt_le_natCast_iff {t : ℕ} {x y : List Bool} {k : ℕ} : + condTimeBoundedAt t x y ≤ k ↔ + ∃ p : List Bool, p.length ≤ k ∧ x ∈ ((condUniversalTM y).run p).runFor t := + etimeBoundedComplexity_le_natCast_iff + +/-- `condTimeBoundedAt t x y < k` iff some program of length strictly less than `k` outputs `x` +given `y` within `t` steps. -/ +theorem condTimeBoundedAt_lt_natCast_iff {t : ℕ} {x y : List Bool} {k : ℕ} : + condTimeBoundedAt t x y < k ↔ + ∃ p : List Bool, p.length < k ∧ x ∈ ((condUniversalTM y).run p).runFor t := + etimeBoundedComplexity_lt_natCast_iff + +/-- `condTimeBounded t x y ≤ k` iff some program of length at most `k` outputs `x` given `y` +within `t |x|` steps. -/ +theorem condTimeBounded_le_natCast_iff {t : ℕ → ℕ} {x y : List Bool} {k : ℕ} : + condTimeBounded t x y ≤ k ↔ + ∃ p : List Bool, p.length ≤ k ∧ x ∈ ((condUniversalTM y).run p).runFor (t x.length) := + condTimeBoundedAt_le_natCast_iff + +/-- Whenever `condTimeBounded t x y ≠ ⊤`, `condTimeBoundedNat t x y` casts back to +`condTimeBounded t x y`. -/ +theorem natCast_condTimeBoundedNat {t : ℕ → ℕ} {x y : List Bool} + (h : condTimeBounded t x y ≠ ⊤) : + (condTimeBoundedNat t x y : ℕ∞) = condTimeBounded t x y := + ENat.natCast_toNat h + +/-- Antitonicity of `condTimeBoundedAt` in the step bound `t`. -/ +theorem condTimeBoundedAt_antitone (x y : List Bool) : + Antitone (condTimeBoundedAt · x y) := + (condUniversalTM y).etimeBoundedComplexity_antitone x + +/-- If `t₁ ≤ t₂`, then `condTimeBoundedAt t₂ x y ≤ condTimeBoundedAt t₁ x y`. -/ +theorem condTimeBoundedAt_anti {t₁ t₂ : ℕ} {x y : List Bool} (h : t₁ ≤ t₂) : + condTimeBoundedAt t₂ x y ≤ condTimeBoundedAt t₁ x y := + condTimeBoundedAt_antitone x y h + +/-- Antitonicity of `condTimeBounded` in the time function `t`. -/ +theorem condTimeBounded_antitone (x y : List Bool) : + Antitone (condTimeBounded · x y) := + fun _ _ h => condTimeBoundedAt_antitone x y (h x.length) + +/-- Dropping the step bound cannot increase conditional complexity (`K(x | y) ≤ K^t(x | y)`). -/ +theorem condPlain_le_condTimeBoundedAt (t : ℕ) (x y : List Bool) : + condPlain x y ≤ condTimeBoundedAt t x y := + (condUniversalTM y).ecomplexity_le_etimeBoundedComplexity t x + +/-- Dropping the time function cannot increase conditional complexity (`K(x | y) ≤ K^t(x | y)`). -/ +theorem condPlain_le_condTimeBounded (t : ℕ → ℕ) (x y : List Bool) : + condPlain x y ≤ condTimeBounded t x y := + condPlain_le_condTimeBoundedAt (t x.length) x y + +/-- `condPlain x y` is the infimum of `condTimeBoundedAt t x y` over `t : ℕ`. -/ +theorem iInf_condTimeBoundedAt (x y : List Bool) : + (⨅ t : ℕ, condTimeBoundedAt t x y) = condPlain x y := + (condUniversalTM y).iInf_etimeBoundedComplexity x + +/-- For every step count `s`, `condLevinKt x y ≤ condTimeBoundedAt s x y + Nat.clog 2 s`. -/ +theorem condLevinKt_le_condTimeBoundedAt_add (s : ℕ) (x y : List Bool) : + condLevinKt x y ≤ condTimeBoundedAt s x y + Nat.clog 2 s := + iInf_le _ s + +/-- Conditional plain complexity bounds conditional Levin complexity from below +(`K(x | y) ≤ Kt(x | y)`). -/ +theorem condPlain_le_condLevinKt (x y : List Bool) : + condPlain x y ≤ condLevinKt x y := + le_iInf fun s => (condPlain_le_condTimeBoundedAt s x y).trans le_self_add + +/-- Threshold characterization of `condLevinKt`: $\mathrm{Kt}(x \mid y) \le k$ iff some program $p$ +outputs $x$ given $y$ within $s$ steps with $|p| + \lceil \log_2 s \rceil \le k$. -/ +theorem condLevinKt_le_natCast_iff {x y : List Bool} {k : ℕ} : + condLevinKt x y ≤ k ↔ + ∃ (p : List Bool) (s : ℕ), + x ∈ ((condUniversalTM y).run p).runFor s ∧ p.length + Nat.clog 2 s ≤ k := by + rw [← ENat.lt_add_one_iff (ENat.natCast_ne_top k), condLevinKt, iInf_lt_iff] + constructor + · rintro ⟨s, hs⟩ + have hne : condTimeBoundedAt s x y ≠ ⊤ := by + intro htop + rw [htop, top_add] at hs + exact not_top_lt hs + obtain ⟨p, hp, hlen⟩ := exists_length_eq_etimeBoundedComplexity hne + rw [condTimeBoundedAt, ← hlen, ← Nat.cast_add, ← Nat.cast_add_one, ENat.natCast_lt_natCast, + Nat.lt_add_one_iff] at hs + exact ⟨p, s, hp, hs⟩ + · rintro ⟨p, s, hp, hle⟩ + refine ⟨s, ?_⟩ + have h1 : condTimeBoundedAt s x y + Nat.clog 2 s ≤ + (p.length + Nat.clog 2 s : ℕ) := by + rw [Nat.cast_add] + exact add_le_add_left (etimeBoundedComplexity_le_length hp) _ + exact h1.trans_lt (by exact_mod_cast Nat.lt_add_one_of_le hle) + +/-- Exponential-step characterization of `condLevinKt`: $\mathrm{Kt}(x \mid y) \le k$ iff some +program $p$ of length at most $k$ outputs $x$ given $y$ within $2^{k - |p|}$ steps. -/ +theorem condLevinKt_le_natCast_iff_exists_runFor_two_pow {x y : List Bool} {k : ℕ} : + condLevinKt x y ≤ k ↔ + ∃ p : List Bool, p.length ≤ k ∧ + x ∈ ((condUniversalTM y).run p).runFor (2 ^ (k - p.length)) := by + rw [condLevinKt_le_natCast_iff] + constructor + · rintro ⟨p, s, hp, hle⟩ + have hplen : p.length ≤ k := by omega + have hclog : Nat.clog 2 s ≤ k - p.length := by omega + have hs : s ≤ 2 ^ (k - p.length) := (Nat.clog_le_iff_le_pow one_lt_two).mp hclog + exact ⟨p, hplen, condUniversalTMRunFor_mono p y hs hp⟩ + · rintro ⟨p, hplen, hp⟩ + refine ⟨p, 2 ^ (k - p.length), hp, ?_⟩ + rw [Nat.clog_pow _ _ one_lt_two] + omega + +/-! ### Polynomial-time conditional upper bounds ($K^t(F(w, y) \mid y) \le |w| + O(1)$) -/ + +/-- **Polynomial-time conditional evaluation bound:** for any polynomial-time function +`F : List Bool × List Bool → List Bool`, there exist a monotone polynomial `pF` (with +`n + 1 ≤ pF.eval n`) and a constant `c` such that for all `w y : List Bool` and step budgets +`t ≥ pF.eval (encPair encBits encBits (w, y)).length`, +$$K^t(F(w, y) \mid y) \le |w| + c.$$ -/ +theorem exists_condTimeBoundedAt_le_of_computableInPolyTime + {F : List Bool × List Bool → List Bool} + (hF : ComputableInPolyTime F (encPair encBits encBits) encBits) : + ∃ (pF : Polynomial ℕ) (c : ℕ), + (∀ n, n + 1 ≤ pF.eval n) ∧ + Monotone pF.eval ∧ + ∀ {t : ℕ} (w y : List Bool), + pF.eval (encPair encBits encBits (w, y)).length ≤ t → + condTimeBoundedAt t (F (w, y)) y ≤ (w.length + c : ℕ) := by + obtain ⟨tF, sF, htF, _, k, State, hfin, tm, htm⟩ := hF + obtain ⟨c_tm, d_tm, hle⟩ := polynomiallyBounded_iff_le.mp htF + obtain ⟨c_sim, hsim⟩ := + exists_etimeBoundedComplexity_condUniversalTM_le_ofMultiTapeTM tm + let pF : Polynomial ℕ := Polynomial.C (c_tm + 1) * (Polynomial.X + 1) ^ (d_tm + 1) + have hpF_eval (n : ℕ) : pF.eval n = (c_tm + 1) * (n + 1) ^ (d_tm + 1) := by + simp [pF] + have hpF_ge (n : ℕ) : n + 1 ≤ pF.eval n := by + rw [hpF_eval, pow_succ'] + have hpow : 1 ≤ (n + 1) ^ d_tm := Nat.one_le_pow _ _ (by omega) + calc + n + 1 = 1 * ((n + 1) * 1) := by ring + _ ≤ (c_tm + 1) * ((n + 1) * (n + 1) ^ d_tm) := + Nat.mul_le_mul (by omega) (Nat.mul_le_mul_left _ hpow) + have hpF_mono : Monotone pF.eval := by + intro a b hab + dsimp only + rw [hpF_eval, hpF_eval] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have htF_le (n : ℕ) : tF n ≤ pF.eval n := by + rw [hpF_eval, pow_succ'] + have h1 := hle n + have h2 : c_tm * (n + 1) ^ d_tm ≤ (c_tm + 1) * (n + 1) ^ d_tm := + Nat.mul_le_mul_right _ (by omega) + have h3 : (c_tm + 1) * (n + 1) ^ d_tm ≤ (c_tm + 1) * ((n + 1) * (n + 1) ^ d_tm) := + Nat.mul_le_mul_left _ (Nat.le_mul_of_pos_left _ (by omega)) + omega + refine ⟨pF, c_sim, hpF_ge, hpF_mono, fun {t} w y ht => ?_⟩ + have hcomp := htm (w, y) + have hstep : tF (encPair encBits encBits (w, y)).length ≤ t := + (htF_le _).trans ht + exact (condTimeBoundedAt_anti hstep).trans + (hsim _ w y (F (w, y)) hcomp.2.1 hcomp.1) + +/-- **Conditional complexity of a polynomial-time function of the condition ($K^t(f(y) \mid y) \le +O(1)$):** for any `f : List Bool → List Bool` computable in polynomial time, there exist a monotone +polynomial `q` (with `n + 1 ≤ q.eval n`) and a constant `c` such that for all `y : List Bool` and +`t ≥ q.eval (y.length + 1)`, `condTimeBoundedAt t (f y) y ≤ c` and `condPlain (f y) y ≤ c`. -/ +theorem exists_condTimeBoundedAt_apply_le {f : List Bool → List Bool} + (hf : ComputableInPolyTime f encBits encBits) : + ∃ (q : Polynomial ℕ) (c : ℕ), + (∀ n, n + 1 ≤ q.eval n) ∧ + Monotone q.eval ∧ + (∀ {t : ℕ} (y : List Bool), q.eval (y.length + 1) ≤ t → + condTimeBoundedAt t (f y) y ≤ c) ∧ + ∀ y : List Bool, condPlain (f y) y ≤ c := by + have hF : ComputableInPolyTime (fun wy : List Bool × List Bool => f wy.2) + (encPair encBits encBits) encBits := + hf.comp (ComputableInPolyTime.snd encBits encBits) + obtain ⟨q, c, hq_ge, hq_mono, hbound⟩ := + exists_condTimeBoundedAt_le_of_computableInPolyTime hF + refine ⟨q, c, hq_ge, hq_mono, fun {t} y ht => ?_, fun y => ?_⟩ + · have hlen : (encPair encBits encBits ([], y)).length = y.length + 1 := by + simp + simpa using hbound [] y (hlen ▸ ht) + · have hlen : (encPair encBits encBits ([], y)).length = y.length + 1 := by + simp + exact (condPlain_le_condTimeBoundedAt (q.eval (y.length + 1)) (f y) y).trans + (by simpa using hbound [] y (hlen ▸ le_rfl)) + +/-- **Self-conditioning ($K^t(y \mid y) \le O(1)$):** there exist a monotone polynomial `q` and a +constant `c` such that `condTimeBoundedAt t y y ≤ c` whenever `q.eval (y.length + 1) ≤ t`, and +`condPlain y y ≤ c` for all `y`. -/ +theorem exists_condTimeBoundedAt_self_le : + ∃ (q : Polynomial ℕ) (c : ℕ), + (∀ n, n + 1 ≤ q.eval n) ∧ + Monotone q.eval ∧ + (∀ {t : ℕ} (y : List Bool), q.eval (y.length + 1) ≤ t → + condTimeBoundedAt t y y ≤ c) ∧ + ∀ y : List Bool, condPlain y y ≤ c := + exists_condTimeBoundedAt_apply_le ComputableInPolyTime.id' + +/-- **Trivial conditional upper bound ($K^t(x \mid y) \le |x| + O(1)$):** there exist a monotone +polynomial `q` (with `n + 1 ≤ q.eval n`) and a constant `c` such that for all `x y : List Bool` and +`t ≥ q.eval (2 * x.length + 1 + y.length)`, `condTimeBoundedAt t x y ≤ (x.length + c : ℕ)` and +`condPlain x y ≤ (x.length + c : ℕ)`. -/ +theorem exists_condTimeBoundedAt_le_length_add : + ∃ (q : Polynomial ℕ) (c : ℕ), + (∀ n, n + 1 ≤ q.eval n) ∧ + Monotone q.eval ∧ + (∀ {t : ℕ} (x y : List Bool), q.eval (2 * x.length + 1 + y.length) ≤ t → + condTimeBoundedAt t x y ≤ (x.length + c : ℕ)) ∧ + ∀ x y : List Bool, condPlain x y ≤ (x.length + c : ℕ) := by + obtain ⟨q, c, hq_ge, hq_mono, hbound⟩ := + exists_condTimeBoundedAt_le_of_computableInPolyTime + (ComputableInPolyTime.fst encBits encBits) + refine ⟨q, c, hq_ge, hq_mono, fun {t} x y ht => ?_, fun x y => ?_⟩ + · have hlen : (encPair encBits encBits (x, y)).length = 2 * x.length + 1 + y.length := by + simp + exact hbound x y (hlen ▸ ht) + · have hlen : (encPair encBits encBits (x, y)).length = 2 * x.length + 1 + y.length := by + simp + exact (condPlain_le_condTimeBoundedAt (q.eval (2 * x.length + 1 + y.length)) x y).trans + (hbound x y (hlen ▸ le_rfl)) + +/-- Conditional plain complexity `condPlain x y` is always finite. -/ +theorem condPlain_ne_top (x y : List Bool) : condPlain x y ≠ ⊤ := by + obtain ⟨_, c, _, _, _, hplain⟩ := exists_condTimeBoundedAt_le_length_add + exact ne_top_of_le_ne_top (ENat.natCast_ne_top _) (hplain x y) + +/-- Casting `condPlainNat x y` to `ℕ∞` yields `condPlain x y`. -/ +@[simp] +theorem natCast_condPlainNat (x y : List Bool) : + (condPlainNat x y : ℕ∞) = condPlain x y := + natCast_complexity (condPlain_ne_top x y) + +/-- Conditional Levin complexity `condLevinKt x y` is always finite. -/ +theorem condLevinKt_ne_top (x y : List Bool) : condLevinKt x y ≠ ⊤ := by + obtain ⟨q, c, _, _, hbound, _⟩ := exists_condTimeBoundedAt_le_length_add + set T := q.eval (2 * x.length + 1 + y.length) + have hle : condLevinKt x y ≤ ((x.length + c + Nat.clog 2 T : ℕ) : ℕ∞) := by + refine (condLevinKt_le_condTimeBoundedAt_add T x y).trans ?_ + rw [Nat.cast_add] + exact add_le_add_left (hbound x y le_rfl) _ + exact ne_top_of_le_ne_top (ENat.natCast_ne_top _) hle + +/-- Casting `condLevinKtNat x y` to `ℕ∞` yields `condLevinKt x y`. -/ +@[simp] +theorem natCast_condLevinKtNat (x y : List Bool) : + (condLevinKtNat x y : ℕ∞) = condLevinKt x y := + ENat.natCast_toNat (condLevinKt_ne_top x y) + +/-- `ℕ`-valued threshold characterization of `condLevinKtNat`. -/ +theorem condLevinKtNat_le_iff {x y : List Bool} {k : ℕ} : + condLevinKtNat x y ≤ k ↔ condLevinKt x y ≤ k := by + rw [← ENat.natCast_le_natCast, natCast_condLevinKtNat] + +/-! ### Counting and incompressibility for conditional complexity -/ + +/-- For every condition string `y`, step bound `t`, length `n`, and threshold `r`, fewer than +`2 ^ r` strings `x` of length `n` have `condTimeBoundedAt t x y < r`. -/ +theorem encard_setOf_condTimeBoundedAt_lt (y : List Bool) (t n r : ℕ) : + {x : List Bool | x.length = n ∧ condTimeBoundedAt t x y < r}.encard < 2 ^ r := by + refine (Set.encard_le_encard ?_).trans_lt + ((condUniversalTM y).encard_setOf_etimeBoundedComplexity_lt t r) + rintro x ⟨_, hx⟩ + exact hx + +/-- **Existence of conditionally incompressible strings:** for every condition string `y` and length +`n`, some string `x` of length `n` satisfies `n ≤ condPlain x y` (and hence +`n ≤ condTimeBoundedAt t x y` for all `t`). -/ +theorem exists_length_eq_forall_le_condTimeBoundedAt (y : List Bool) (n : ℕ) : + ∃ x : List Bool, x.length = n ∧ ∀ t : ℕ, (n : ℕ∞) ≤ condTimeBoundedAt t x y := + (condUniversalTM y).exists_length_eq_forall_le_etimeBoundedComplexity n + +/-- For every condition string `y`, time function `t`, and `n c : ℕ`, all but fewer than +`2 ^ (n - c)` of the `2 ^ n` strings `x` of length `n` satisfy +`(n - c : ℕ) ≤ condTimeBounded t x y`. -/ +theorem two_pow_lt_ncard_setOf_length_eq_le_condTimeBounded_add + (t : ℕ → ℕ) (y : List Bool) (n c : ℕ) : + 2 ^ n < {x : List Bool | x.length = n ∧ (n - c : ℕ) ≤ condTimeBounded t x y}.ncard + + 2 ^ (n - c) := by + have h := (condUniversalTM y).two_pow_lt_ncard_setOf_length_eq_le_ecomplexity_add n c + refine h.trans_le (Nat.add_le_add_right (Set.ncard_le_ncard ?_ ?_) _) + · rintro x ⟨hx, hplain⟩ + exact ⟨hx, hplain.trans (condPlain_le_condTimeBounded t x y)⟩ + · exact (Set.finite_of_encard_eq_coe (BitString.encard_setOf_length_eq n)).subset fun _ hx => hx.1 + +/-! ### The Minimum Conditional Time-Bounded Kolmogorov Complexity Problem (`MINcKT`) -/ + +namespace MINcKT + +/-- An instance of `MINcKT`: a target binary string `string`, a condition binary string `cond`, a +step bound `time`, and a program size threshold `size` ([Hirahara, Definition II.5][Hirahara2018]). +-/ +structure Instance where + /-- The target binary string `x`. -/ + string : List Bool + /-- The auxiliary condition binary string `y`. -/ + cond : List Bool + /-- The step bound `t` for the described multi-tape machine. -/ + time : ℕ + /-- The maximum allowed program length `s`. -/ + size : ℕ + deriving DecidableEq + +end MINcKT + +/-- **The Minimum Conditional Time-Bounded Kolmogorov Complexity Problem (`MINcKT`)** +([Hirahara, Definition II.5][Hirahara2018]; [Liu and Pass, Section 2.1][LiuPass2021Crypto]): +the set of instances `(x, y, t, s)` such that `condTimeBoundedAt t x y ≤ s`. -/ +def MINcKT : Set MINcKT.Instance := + {i | condTimeBoundedAt i.time i.string i.cond ≤ i.size} + +namespace MINcKT + +/-- Standard encoding of `MINcKT.Instance`: pairs `(i.string, i.cond)` with the unary thresholds +`(i.time, i.size)`. -/ +def enc : Instance ↪ List Bool := + (⟨fun i => ((i.string, i.cond), (i.time, i.size)), fun i j h => by + cases i; cases j + simp only [Prod.mk.injEq, Instance.mk.injEq] at h ⊢ + exact ⟨h.1.1, h.1.2, h.2.1, h.2.2⟩⟩ : + Instance ↪ (List Bool × List Bool) × (ℕ × ℕ)).trans + (encPair (encPair encBits encBits) (encPair encUnary encUnary)) + +/-- Applying `MINcKT.enc` encodes `((i.string, i.cond), (i.time, i.size))` via `encPair`. -/ +@[simp] +theorem enc_apply (i : Instance) : + enc i = encPair (encPair encBits encBits) (encPair encUnary encUnary) + ((i.string, i.cond), (i.time, i.size)) := + rfl + +/-- The unary size parameter `i.size` is at most `(enc i).length`. -/ +theorem size_le_length_enc (i : Instance) : i.size ≤ (enc i).length := by + simp only [enc_apply, length_encPair, encBits_apply, encUnary_apply, List.length_replicate] + omega + +/-- The unary time parameter `i.time` is at most `(enc i).length`. -/ +theorem time_le_length_enc (i : Instance) : i.time ≤ (enc i).length := by + simp only [enc_apply, length_encPair, encBits_apply, encUnary_apply, List.length_replicate] + omega + +/-- `i ∈ MINcKT` iff `condTimeBoundedAt i.time i.string i.cond ≤ i.size`. -/ +theorem mem_iff {i : Instance} : + i ∈ MINcKT ↔ condTimeBoundedAt i.time i.string i.cond ≤ i.size := + Iff.rfl + +/-- `⟨x, y, t, s⟩ ∈ MINcKT` iff `condTimeBoundedAt t x y ≤ s`. -/ +@[simp] +theorem mk_mem_iff {x y : List Bool} {t s : ℕ} : + (⟨x, y, t, s⟩ : Instance) ∈ MINcKT ↔ condTimeBoundedAt t x y ≤ s := + Iff.rfl + +/-- `i ∈ MINcKT` iff some program of length at most `i.size` outputs `i.string` given `i.cond` +within `i.time` steps. -/ +theorem mem_iff_exists_program {i : Instance} : + i ∈ MINcKT ↔ + ∃ p : List Bool, p.length ≤ i.size ∧ + i.string ∈ ((condUniversalTM i.cond).run p).runFor i.time := + condTimeBoundedAt_le_natCast_iff + +/-- Monotonicity of `MINcKT` in the size threshold `s`. -/ +theorem mem_of_size_le {x y : List Bool} {t s₁ s₂ : ℕ} + (h : (⟨x, y, t, s₁⟩ : Instance) ∈ MINcKT) (hs : s₁ ≤ s₂) : + (⟨x, y, t, s₂⟩ : Instance) ∈ MINcKT := + mk_mem_iff.mpr ((mk_mem_iff.mp h).trans (Nat.cast_le.mpr hs)) + +/-- Monotonicity of `MINcKT` in the step budget `t`. -/ +theorem mem_of_time_le {x y : List Bool} {t₁ t₂ s : ℕ} + (h : (⟨x, y, t₁, s⟩ : Instance) ∈ MINcKT) (ht : t₁ ≤ t₂) : + (⟨x, y, t₂, s⟩ : Instance) ∈ MINcKT := + mk_mem_iff.mpr ((condTimeBoundedAt_anti ht).trans (mk_mem_iff.mp h)) + +private theorem Instance.computableInPolyTime_toTuple : + ComputableInPolyTime (fun i : Instance => ((i.string, i.cond), (i.time, i.size))) enc + (encPair (encPair encBits encBits) (encPair encUnary encUnary)) := + ComputableInPolyTime.of_eq fun _ => rfl + +/-- Constructing a `MINcKT.Instance` from `((x, y), (t, s))` is computable in polynomial time. -/ +@[fun_prop] +theorem Instance.computableInPolyTime_mk : + ComputableInPolyTime + (fun q : (List Bool × List Bool) × (ℕ × ℕ) => Instance.mk q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encBits encBits) (encPair encUnary encUnary)) enc := + ComputableInPolyTime.of_eq fun _ => rfl + +/-- The witness check for `MINcKT`: given an instance `i` and a candidate program `p`, checks that +`p.length ≤ i.size` and that `condUniversalTMRunFor p i.cond i.time = some i.string`. -/ +def check (ip : Instance × List Bool) : Bool := + decide (ip.2.length ≤ ip.1.size) && + decide (condUniversalTMRunFor ip.2 ip.1.cond ip.1.time = some ip.1.string) + +/-- `check (i, p) = true` iff `p.length ≤ i.size` and `p` outputs `i.string` given `i.cond` within +`i.time` steps. -/ +theorem check_eq_true_iff {i : Instance} {p : List Bool} : + check (i, p) = true ↔ + p.length ≤ i.size ∧ i.string ∈ ((condUniversalTM i.cond).run p).runFor i.time := by + simp [check, condUniversalTM_runFor, Option.mem_def] + +/-- Checking a candidate program for `MINcKT` is computable in polynomial time. -/ +@[fun_prop] +theorem computableInPolyTime_check : + ComputableInPolyTime check (encPair enc encBits) encBool := by + open ComputableInPolyTime in + let encPairBits := encPair encBits encBits + let encPairUnary := encPair encUnary encUnary + have htuple := Instance.computableInPolyTime_toTuple.comp (fst enc encBits) + have hxy := (fst encPairBits encPairUnary).comp htuple + have hts := (snd encPairBits encPairUnary).comp htuple + have hstr := (fst encBits encBits).comp hxy + have hcond := (snd encBits encBits).comp hxy + have htime := (fst encUnary encUnary).comp hts + have hsize := (snd encUnary encUnary).comp hts + have hp := snd enc encBits + have hlen := (encoding_length encBits).comp hp + have hrun := computableInPolyTime_condUniversalTMRunFor.comp (hp.prod (hcond.prod htime)) + have hsome := (optionSome encBits).comp hstr + have hle : ComputableInPolyTime + (fun ip : Instance × List Bool => decide (ip.2.length ≤ ip.1.size)) + (encPair enc encBits) encBool := + (ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.unary_le).comp (hlen.prod hsize) + exact bool_and.comp (hle.prod (hrun.decide_eq' hsome)) + +/-- **`MINcKT` is in `NP`** ([Hirahara, Definition II.5][Hirahara2018]): a witness for +`(x, y, 1^t, 1^s)` is a binary program `p` of length at most `s ≤ |(x, y, 1^t, 1^s)|`, verified in +polynomial time by `MINcKT.check`. -/ +theorem mem_NP : MINcKT ∈ NP enc := by + have h := mem_NP_of_witness (enc := enc) (p := Polynomial.X) Decoder.bits + computableInPolyTime_check (fun i p => check_eq_true_iff) + fun i p hp => ⟨p, hp, by + simpa only [encBits_apply, Polynomial.eval_X] using hp.1.trans (size_le_length_enc i)⟩ + simpa only [← mem_iff_exists_program, Set.ofPred_mem_eq] using h + +end MINcKT + +/-! ### Fixed-threshold formulation (`MINcKTAt`) -/ + +/-- **Fixed-threshold `MINcKT`** (`MINcKTAt t s`, [Liu and Pass, Section 2.1][LiuPass2021Crypto]): +the language of string pairs `(x, y)` (encoded by `encPair encBits encBits`) such that +`condTimeBounded t x y ≤ s x.length`. -/ +def MINcKTAt (t s : ℕ → ℕ) : Set (List Bool × List Bool) := + {xy | condTimeBounded t xy.1 xy.2 ≤ s xy.1.length} + +/-- `(x, y) ∈ MINcKTAt t s` iff `⟨x, y, t x.length, s x.length⟩ ∈ MINcKT`. -/ +@[simp] +theorem mem_MINcKTAt_iff_mem_MINcKT {t s : ℕ → ℕ} {x y : List Bool} : + (x, y) ∈ MINcKTAt t s ↔ + (⟨x, y, t x.length, s x.length⟩ : MINcKT.Instance) ∈ MINcKT := + Iff.rfl + +namespace MINcKTAt + +/-- Embeds a pair `(x, y)` into `MINcKT.Instance` using threshold functions `t` and `s` at `|x|`. -/ +def toInstance (t s : ℕ → ℕ) (xy : List Bool × List Bool) : MINcKT.Instance := + ⟨xy.1, xy.2, t xy.1.length, s xy.1.length⟩ + +/-- `toInstance t s xy ∈ MINcKT` iff `xy ∈ MINcKTAt t s`. -/ +@[simp] +theorem toInstance_mem_MINcKT_iff {t s : ℕ → ℕ} {xy : List Bool × List Bool} : + toInstance t s xy ∈ MINcKT ↔ xy ∈ MINcKTAt t s := + Iff.rfl + +/-- If `t` and `s` are computable in polynomial time in unary, then `toInstance t s` is computable +in polynomial time. -/ +theorem computableInPolyTime_toInstance {t s : ℕ → ℕ} + (ht : ComputableInPolyTime t encUnary encUnary) + (hs : ComputableInPolyTime s encUnary encUnary) : + ComputableInPolyTime (toInstance t s) (encPair encBits encBits) MINcKT.enc := by + open ComputableInPolyTime in + have hx := fst encBits encBits + have hlen := length_bits_comp hx + have hid : ComputableInPolyTime (fun xy : List Bool × List Bool => xy) + (encPair encBits encBits) (encPair encBits encBits) := id' + have h := MINcKT.Instance.computableInPolyTime_mk.comp + (hid.prod ((ht.comp hlen).prod (hs.comp hlen))) + exact h + +/-- Whenever `t` and `s` are computable in polynomial time in unary, `MINcKTAt t s` is +polynomial-time many-one reducible to `MINcKT`. -/ +theorem polyTimeReducible_MINcKT {t s : ℕ → ℕ} + (ht : ComputableInPolyTime t encUnary encUnary) + (hs : ComputableInPolyTime s encUnary encUnary) : + PolyTimeReducible (encPair encBits encBits) MINcKT.enc (MINcKTAt t s) MINcKT := + ⟨toInstance t s, computableInPolyTime_toInstance ht hs, fun _ => Iff.rfl⟩ + +/-- **Fixed-threshold `MINcKTAt t s` is in `NP`** whenever `t` and `s` are computable in polynomial +time in unary. -/ +theorem mem_NP {t s : ℕ → ℕ} + (ht : ComputableInPolyTime t encUnary encUnary) + (hs : ComputableInPolyTime s encUnary encUnary) : + MINcKTAt t s ∈ NP (encPair encBits encBits) := + (polyTimeReducible_MINcKT ht hs).mem_NP MINcKT.mem_NP + +/-- When both `p.eval` and `q.eval` are polynomials, `MINcKTAt p.eval q.eval ∈ NP`. -/ +theorem mem_NP_polynomial₂ (p q : Polynomial ℕ) : + MINcKTAt p.eval q.eval ∈ NP (encPair encBits encBits) := + mem_NP (ComputableInPolyTime.unary_eval p) (ComputableInPolyTime.unary_eval q) + +end MINcKTAt + +/-! ### Hirahara's conditional promise problem `GapMINcKT` -/ + +namespace GapMINcKT + +/-- The yes-instances of `GapMINcKT`: instances `(x, y, t, s)` with $K^t(x \mid y) \le s$ +([Hirahara, Definition II.6][Hirahara2018]). -/ +def yesSet : Set MINcKT.Instance := + MINcKT + +/-- The no-instances of `GapMINcKT[σ, τ]`: instances `(x, y, t, s)` with +$K^{\tau(|x|, |y|, t)}(x \mid y) > \sigma(|x|, |y|, s)$ +([Hirahara, Definition II.6][Hirahara2018]). -/ +def noSet (σ τ : ℕ → ℕ → ℕ → ℕ) : Set MINcKT.Instance := + {i | (σ i.string.length i.cond.length i.size : ℕ∞) < + condTimeBoundedAt (τ i.string.length i.cond.length i.time) i.string i.cond} + +/-- When `s ≤ σ n m s` and `t ≤ τ n m t`, `GapMINcKT.yesSet` and `GapMINcKT.noSet σ τ` are +disjoint. -/ +theorem disjoint_yesSet_noSet {σ τ : ℕ → ℕ → ℕ → ℕ} + (hσ : ∀ n m s, s ≤ σ n m s) (hτ : ∀ n m t, t ≤ τ n m t) : + Disjoint yesSet (noSet σ τ) := by + refine Set.disjoint_left.mpr fun i hyes hno => ?_ + have h1 : condTimeBoundedAt (τ i.string.length i.cond.length i.time) i.string i.cond ≤ + condTimeBoundedAt i.time i.string i.cond := + condTimeBoundedAt_anti (hτ i.string.length i.cond.length i.time) + have h2 : condTimeBoundedAt (τ i.string.length i.cond.length i.time) i.string i.cond ≤ + (σ i.string.length i.cond.length i.size : ℕ∞) := + (h1.trans hyes).trans (Nat.cast_le.mpr (hσ i.string.length i.cond.length i.size)) + exact not_lt_of_ge h2 hno + +/-- With trivial gap functions `σ n m s = s` and `τ n m t = t`, `GapMINcKT.noSet` is `MINcKTᶜ`. -/ +theorem noSet_id_eq_compl : noSet (fun _ _ s => s) (fun _ _ t => t) = MINcKTᶜ := by + ext i + simp [noSet, MINcKT] + +end GapMINcKT + +/-- **Hirahara's `GapMINcKT` promise problem** ([Hirahara, Definition II.6][Hirahara2018]): +separates `MINcKT` from `GapMINcKT.noSet σ τ` when `s ≤ σ n m s` and `t ≤ τ n m t`. -/ +def GapMINcKT (σ τ : ℕ → ℕ → ℕ → ℕ) + (hσ : ∀ n m s, s ≤ σ n m s) (hτ : ∀ n m t, t ≤ τ n m t) : + PromiseProblem MINcKT.Instance where + yes := GapMINcKT.yesSet + no := GapMINcKT.noSet σ τ + disjoint := GapMINcKT.disjoint_yesSet_noSet hσ hτ + +namespace GapMINcKT + +variable {σ τ : ℕ → ℕ → ℕ → ℕ} +variable (hσ : ∀ n m s, s ≤ σ n m s) (hτ : ∀ n m t, t ≤ τ n m t) + +/-- The yes-set of `GapMINcKT σ τ hσ hτ` is `MINcKT`. -/ +@[simp] +theorem yes_eq : (GapMINcKT σ τ hσ hτ).yes = MINcKT := + rfl + +/-- The no-set of `GapMINcKT σ τ hσ hτ` is `GapMINcKT.noSet σ τ`. -/ +@[simp] +theorem no_eq : (GapMINcKT σ τ hσ hτ).no = noSet σ τ := + rfl + +/-- With no gap (`σ n m s = s` and `τ n m t = t`), `GapMINcKT` is `PromiseProblem.ofSet MINcKT`. -/ +@[simp] +theorem id_eq : + GapMINcKT (fun _ _ s => s) (fun _ _ t => t) (fun _ _ _ => le_rfl) (fun _ _ _ => le_rfl) = + PromiseProblem.ofSet MINcKT := by + ext i + · rfl + · rw [no_eq, noSet_id_eq_compl] + rfl + +end GapMINcKT + +end Cslib.Kolmogorov diff --git a/Complexity/Computability/Kolmogorov/MKtP.lean b/Complexity/Computability/Kolmogorov/MKtP.lean new file mode 100644 index 0000000000..267725dd42 --- /dev/null +++ b/Complexity/Computability/Kolmogorov/MKtP.lean @@ -0,0 +1,535 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.EXP +public import Complexity.Computability.Complexity.Classes.Ladner.PolyTime +public import Complexity.Computability.Complexity.Classes.Promise.Basic +public import Complexity.Computability.Complexity.Reduction +public import Complexity.Computability.Kolmogorov.TimeBounded +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Foundations.Data.Nat.PolynomialBound.Closure +import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential + +/-! +# The Minimum `Kt` Problem (`MKtP`) and `GapMKtP` + +This module develops the decision and promise problems associated with Levin's time-bounded +Kolmogorov complexity `Cslib.Kolmogorov.levinKt` ($\mathrm{Kt}$): + +* **Exponential-step witness characterization (`levinKt_le_natCast_iff_exists_runFor_two_pow`):** + $\mathrm{Kt}(x) \le k$ if and only if some binary program $p$ of length at most $k$ outputs $x$ + within $2^{k - |p|}$ steps under `universalTM`. +* **Optimal `Kt`-witnesses and running-time bound for random strings + (`exists_length_add_clog_eq_levinKtNat`, `encard_setOf_forall_optimal_levinKt_two_pow_lt`, + `two_pow_lt_ncard_setOf_exists_optimal_levinKt_le_two_pow`):** + Every string $x$ admits an optimal $\mathrm{Kt}$-witness $(p, s)$ with $s > 0$ and + $|p| + \lceil \log_2 s \rceil = \mathrm{Kt}(x)$. Following + [Liu and Pass, Section 3.1, Fact 3.1][LiuPass2021Crypto], if any witness $(p, s)$ satisfying + $|p| + \lceil \log_2 s \rceil \le \mathrm{Kt}(x)$ runs for more than + $2^{\mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil + m}$ steps, then $K(x) < |x| - m$; + consequently, all but fewer than $2^{n - m}$ strings of length $n$ have an optimal + $\mathrm{Kt}$-witness running in at most + $2^{\mathrm{copyOverhead} + \lceil \log_2(n + 1) \rceil + m}$ steps. +* **`MKtP ∈ E ⊆ EXP` (`MKtP.mem_E`, `MKtP.mem_EXP`, `MKtPAt.mem_EXP`):** + `Cslib.Kolmogorov.MKtP` is the set of pairs `(x, k) : List Bool × ℕ` (encoded by + `encPair encBits encUnary`) with `levinKt x ≤ k`, and `Cslib.Kolmogorov.MKtPAt s` is the + fixed-threshold language `{x | levinKt x ≤ s x.length}` + ([Allender et al., Definition 9][AllenderBuhrmanKouckyVanMelkebeekRonneburger2006]; + [Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]; + [Liu and Pass, Section 2.2][LiuPass2021Crypto]). Enumerating candidate programs `Ladner.word j` + of length at most `k` and running `universalTMRunFor` for $2^{k - |p|}$ steps places `MKtP` in + `E (encPair encBits encUnary)` and `EXP (encPair encBits encUnary)`, and places `MKtPAt s` in + `EXP encBits` whenever `s` is computable in polynomial time in unary. +* **Promise problem `GapMKtP` (`Cslib.Kolmogorov.GapMKtP`):** + The promise problem separating $\mathrm{Kt}(x) \le s_1(|x|)$ from $\mathrm{Kt}(x) > s_2(|x|)$ + for $s_1 \le s_2$ ([Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]). + +## Main definitions + +* `Cslib.Kolmogorov.MKtP`: the language $\{(x, k) \mid \mathrm{Kt}(x) \le k\}$. +* `Cslib.Kolmogorov.MKtP.boundedSearch`: polynomial-time bounded search for a `Kt`-witness up to + word-index and step cap `N`. +* `Cslib.Kolmogorov.MKtPAt`: the fixed-threshold language $\{x \mid \mathrm{Kt}(x) \le s(|x|)\}$. +* `Cslib.Kolmogorov.GapMKtP`, `Cslib.Kolmogorov.GapMKtP.yesSet`, + `Cslib.Kolmogorov.GapMKtP.noSet`: the promise problem `GapMKtP[s₁, s₂]`. + +## Main results + +* `Cslib.Kolmogorov.levinKt_le_natCast_iff_exists_runFor_two_pow`, + `Cslib.Kolmogorov.levinKtNat_le_iff_exists_runFor_two_pow`: exponential-step witness + characterization of $\mathrm{Kt}(x) \le k$. +* `Cslib.Kolmogorov.exists_length_add_clog_eq_levinKt`, + `Cslib.Kolmogorov.exists_length_add_clog_eq_levinKtNat`: existence of an optimal `Kt`-witness. +* `Cslib.Kolmogorov.plain_lt_of_levinKtNat_witness_two_pow_lt`, + `Cslib.Kolmogorov.encard_setOf_forall_optimal_levinKt_two_pow_lt`, + `Cslib.Kolmogorov.two_pow_lt_ncard_setOf_exists_optimal_levinKt_le_two_pow`: + running-time bound for optimal `Kt`-witnesses ([Liu and Pass, Section 3.1, + Fact 3.1][LiuPass2021Crypto]). +* `Cslib.Complexity.PolyTimeReducible.mem_EXP`: `EXP` is closed under polynomial-time many-one + reductions. +* `Cslib.Kolmogorov.MKtP.computableInPolyTime_boundedSearch`, + `Cslib.Kolmogorov.MKtP.boundedSearch_eq_true_iff_of_two_pow_le`: polynomial-time certificate and + exactness of `MKtP.boundedSearch`. +* `Cslib.Kolmogorov.MKtP.mem_E`, `Cslib.Kolmogorov.MKtP.mem_EXP`: `MKtP` is in `E` and `EXP`. +* `Cslib.Kolmogorov.MKtPAt.polyTimeReducible_MKtP`, `Cslib.Kolmogorov.MKtPAt.mem_EXP`, + `Cslib.Kolmogorov.MKtPAt.mem_EXP_polynomial`: `MKtPAt s ∈ EXP encBits` for polynomial-time unary + thresholds `s`. +* `Cslib.Kolmogorov.GapMKtP.disjoint_yesSet_noSet`, `Cslib.Kolmogorov.GapMKtP.id_eq`: consistency + and zero-gap specialization of `GapMKtP`. + +## References + +* [E. Allender, H. Buhrman, M. Koucký, D. van Melkebeek, D. Ronneburger, + *Power from Random Strings*][AllenderBuhrmanKouckyVanMelkebeekRonneburger2006] +* [L. A. Levin, *Universal Sequential Search Problems*][Levin1973] +* [L. A. Levin, *Randomness Conservation Inequalities; Information and Independence in + Mathematical Theories*][Levin1984] +* [Y. Liu, R. Pass, *On the Possibility of Basing Cryptography on EXP ≠ BPP*][LiuPass2021Crypto] +* [I. C. Oliveira, R. Santhanam, *Hardness Magnification for Natural + Problems*][OliveiraSanthanam2018] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM Filter + +variable {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} + +/-- **`EXP` is closed under polynomial-time many-one reductions.** -/ +theorem PolyTimeReducible.mem_EXP (hAB : PolyTimeReducible encA encB A B) (hB : B ∈ EXP encB) : + A ∈ EXP encA := by + obtain ⟨f, hf, hred⟩ := hAB + obtain ⟨k, hk⟩ := mem_EXP_iff.mp hB + obtain ⟨t, s, ht, hs, h⟩ := hf.tidy + obtain ⟨c, d, hcd⟩ := (ht.add hs).exists_le + have hfO : ComputableInO f encA encB (fun a => c * ((encA a).length + 1) ^ d) + (fun a => c * ((encA a).length + 1) ^ d) := + .of_tidy ((ComputableTidilyInO.of_bounds h 1 (fun _ => by omega) (fun _ => by omega) + fun a => (h.length_le a).trans (by omega)).mono_le (fun a => hcd _) (fun a => hcd _)) + have hlen (a : α) : (encB (f a)).length ≤ c * ((encA a).length + 1) ^ d := + (h.length_le a).trans ((Nat.le_add_right _ _).trans (hcd a)) + have hpre : f ⁻¹' B ∈ DTIME encA + (fun n => c * (n + 1) ^ d + 2 ^ (c * (n + 1) ^ d) ^ k) := by + refine preimage_mem_DTIME (C := 1) hk hfO fun a => ?_ + have hpow : 2 ^ (encB (f a)).length ^ k ≤ 2 ^ (c * ((encA a).length + 1) ^ d) ^ k := + Nat.pow_le_pow_right (by norm_num) (Nat.pow_le_pow_left (hlen a) k) + omega + have hA_eq : A = f ⁻¹' B := Set.ext hred + rw [hA_eq] + have hpoly : PolynomiallyBounded + (fun n => c * (n + 1) ^ d + (c * (n + 1) ^ d) ^ k + 1) := by fun_prop + obtain ⟨D, hD⟩ := hpoly + refine mem_EXP_iff.mpr ⟨D, DTIME_mono_of_eventually_le ?_ hpre⟩ + filter_upwards [hD] with n hn + set M := c * (n + 1) ^ d + (c * (n + 1) ^ d) ^ k + have h1 : c * (n + 1) ^ d ≤ 2 ^ M := + (Nat.le_add_right _ _).trans (Nat.lt_two_pow_self.le) + have h2 : 2 ^ (c * (n + 1) ^ d) ^ k ≤ 2 ^ M := + Nat.pow_le_pow_right (by norm_num) (Nat.le_add_left _ _) + calc + c * (n + 1) ^ d + 2 ^ (c * (n + 1) ^ d) ^ k ≤ 2 ^ M + 2 ^ M := Nat.add_le_add h1 h2 + _ = 2 ^ (M + 1) := by rw [← two_mul, pow_succ'] + _ ≤ 2 ^ n ^ D := Nat.pow_le_pow_right (by norm_num) hn + +end Cslib.Complexity + +namespace Cslib.Kolmogorov + +open _root_.Turing _root_.Turing.MultiTapeTM _root_.Turing.MultiTapeTM.Universal +open Cslib.Complexity DescriptionMethod + +/-! ### Exponential-step witness characterization and optimal witnesses for `levinKt` -/ + +/-- **Exponential-step characterization of `levinKt`.** $\mathrm{Kt}(x) \le k$ iff some binary +program $p$ of length at most $k$ outputs $x$ within $2^{k - |p|}$ steps under `universalTM`. -/ +theorem levinKt_le_natCast_iff_exists_runFor_two_pow {x : List Bool} {k : ℕ} : + levinKt x ≤ k ↔ + ∃ p : List Bool, p.length ≤ k ∧ x ∈ (universalTM.run p).runFor (2 ^ (k - p.length)) := by + rw [levinKt_le_natCast_iff] + constructor + · rintro ⟨p, s, hp, hle⟩ + have hplen : p.length ≤ k := by omega + have hclog : Nat.clog 2 s ≤ k - p.length := by omega + have hs : s ≤ 2 ^ (k - p.length) := (Nat.clog_le_iff_le_pow one_lt_two).mp hclog + exact ⟨p, hplen, universalTMRunFor_mono p hs hp⟩ + · rintro ⟨p, hplen, hp⟩ + refine ⟨p, 2 ^ (k - p.length), hp, ?_⟩ + rw [Nat.clog_pow _ _ one_lt_two] + omega + +/-- `ℕ`-valued exponential-step characterization of `levinKtNat`. -/ +theorem levinKtNat_le_iff_exists_runFor_two_pow {x : List Bool} {k : ℕ} : + levinKtNat x ≤ k ↔ + ∃ p : List Bool, p.length ≤ k ∧ x ∈ (universalTM.run p).runFor (2 ^ (k - p.length)) := by + rw [levinKtNat_le_iff, levinKt_le_natCast_iff_exists_runFor_two_pow] + +/-- Every string `x` admits an optimal `Kt`-witness `(p, s)` with `0 < s`, +`x ∈ (universalTM.run p).runFor s`, and `p.length + Nat.clog 2 s = levinKtNat x`. -/ +theorem exists_length_add_clog_eq_levinKtNat (x : List Bool) : + ∃ (p : List Bool) (s : ℕ), + 0 < s ∧ x ∈ (universalTM.run p).runFor s ∧ p.length + Nat.clog 2 s = levinKtNat x := by + obtain ⟨p, s, hp, hle⟩ := levinKt_le_natCast_iff.mp (natCast_levinKtNat x).symm.le + have hs : 0 < s := by + rcases Nat.eq_zero_or_pos s with rfl | hs + · simp [universalTM_runFor] at hp + · exact hs + have hge : levinKtNat x ≤ p.length + Nat.clog 2 s := by + rw [levinKtNat_le_iff] + refine (levinKt_le_timeBoundedAt_add s x).trans ?_ + rw [Nat.cast_add] + exact add_le_add_left (etimeBoundedComplexity_le_length hp) _ + exact ⟨p, s, hs, hp, le_antisymm hle hge⟩ + +/-- Every string `x` admits an optimal `Kt`-witness `(p, s)` in `ℕ∞` with `0 < s`, +`x ∈ (universalTM.run p).runFor s`, and `(p.length + Nat.clog 2 s : ℕ) = levinKt x`. -/ +theorem exists_length_add_clog_eq_levinKt (x : List Bool) : + ∃ (p : List Bool) (s : ℕ), + 0 < s ∧ x ∈ (universalTM.run p).runFor s ∧ + ((p.length + Nat.clog 2 s : ℕ) : ℕ∞) = levinKt x := by + obtain ⟨p, s, hs, hp, heq⟩ := exists_length_add_clog_eq_levinKtNat x + refine ⟨p, s, hs, hp, ?_⟩ + rw [heq, natCast_levinKtNat] + +/-- **[Liu and Pass, Section 3.1, Fact 3.1, p. 10][LiuPass2021Crypto]:** +If $(p, s)$ outputs $x$ within $s$ steps with $|p| + \lceil \log_2 s \rceil \le \mathrm{Kt}(x)$, and +$s > 2^{\mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil + m}$ (with $m \le |x|$), then the +plain Kolmogorov complexity of $x$ satisfies $K(x) < |x| - m$. -/ +theorem plain_lt_of_levinKtNat_witness_two_pow_lt {x p : List Bool} {s m : ℕ} + (hm : m ≤ x.length) + (hp : x ∈ (universalTM.run p).runFor s) + (hopt : p.length + Nat.clog 2 s ≤ levinKtNat x) + (hs : 2 ^ (copyOverhead + Nat.clog 2 (x.length + 1) + m) < s) : + plain x < (x.length - m : ℕ) := by + have hkt : levinKtNat x ≤ x.length + copyOverhead + Nat.clog 2 (x.length + 1) := + levinKtNat_le_iff.mpr (levinKt_le_length_add x) + have hclog : copyOverhead + Nat.clog 2 (x.length + 1) + m < Nat.clog 2 s := + (Nat.lt_clog_iff_pow_lt one_lt_two).mpr hs + have hplen : p.length < x.length - m := by omega + have hprod : universalTM.Produces p x := .of_mem_runFor hp + exact (ecomplexity_le_length hprod).trans_lt (by exact_mod_cast hplen) + +/-- **[Liu and Pass, Section 3.1, Fact 3.1, p. 10][LiuPass2021Crypto]:** +For $m \le n$, fewer than $2^{n - m}$ strings $x \in \{0, 1\}^n$ have the property that every +optimal $\mathrm{Kt}$-witness $(p, s)$ for $x$ runs for more than +$2^{\mathrm{copyOverhead} + \lceil \log_2(n + 1) \rceil + m}$ steps. -/ +theorem encard_setOf_forall_optimal_levinKt_two_pow_lt {n m : ℕ} (hm : m ≤ n) : + {x : List Bool | x.length = n ∧ + ∀ (p : List Bool) (s : ℕ), + x ∈ (universalTM.run p).runFor s → + p.length + Nat.clog 2 s ≤ levinKtNat x → + 2 ^ (copyOverhead + Nat.clog 2 (n + 1) + m) < s}.encard < 2 ^ (n - m) := by + refine (Set.encard_le_encard ?_).trans_lt + (universalTM.encard_setOf_ecomplexity_lt (n - m)) + rintro x ⟨rfl, hall⟩ + obtain ⟨p, s, _, hp, hopt⟩ := exists_length_add_clog_eq_levinKtNat x + exact plain_lt_of_levinKtNat_witness_two_pow_lt hm hp hopt.le (hall p s hp hopt.le) + +/-- **[Liu and Pass, Section 3.1, Fact 3.1, p. 10][LiuPass2021Crypto]:** +For $m \le n$, all but fewer than $2^{n - m}$ of the $2^n$ strings of length $n$ admit an optimal +$\mathrm{Kt}$-witness $(p, s)$ running in at most +$2^{\mathrm{copyOverhead} + \lceil \log_2(n + 1) \rceil + m}$ steps. -/ +theorem two_pow_lt_ncard_setOf_exists_optimal_levinKt_le_two_pow {n m : ℕ} (hm : m ≤ n) : + 2 ^ n < + {x : List Bool | x.length = n ∧ + ∃ (p : List Bool) (s : ℕ), + x ∈ (universalTM.run p).runFor s ∧ + p.length + Nat.clog 2 s ≤ levinKtNat x ∧ + s ≤ 2 ^ (copyOverhead + Nat.clog 2 (n + 1) + m)}.ncard + 2 ^ (n - m) := by + have hsub : {x : List Bool | x.length = n ∧ ((n - m : ℕ) : ℕ∞) ≤ plain x} ⊆ + {x : List Bool | x.length = n ∧ + ∃ (p : List Bool) (s : ℕ), + x ∈ (universalTM.run p).runFor s ∧ + p.length + Nat.clog 2 s ≤ levinKtNat x ∧ + s ≤ 2 ^ (copyOverhead + Nat.clog 2 (n + 1) + m)} := by + rintro x ⟨rfl, hplain⟩ + obtain ⟨p, s, _, hp, hopt⟩ := exists_length_add_clog_eq_levinKtNat x + refine ⟨rfl, p, s, hp, hopt.le, ?_⟩ + by_contra! hlt + exact not_lt_of_ge hplain (plain_lt_of_levinKtNat_witness_two_pow_lt hm hp hopt.le hlt) + have hfin : {x : List Bool | x.length = n ∧ + ∃ (p : List Bool) (s : ℕ), + x ∈ (universalTM.run p).runFor s ∧ + p.length + Nat.clog 2 s ≤ levinKtNat x ∧ + s ≤ 2 ^ (copyOverhead + Nat.clog 2 (n + 1) + m)}.Finite := + (Set.finite_of_encard_eq_coe (BitString.encard_setOf_length_eq n)).subset fun _ hx => hx.1 + exact (universalTM.two_pow_lt_ncard_setOf_length_eq_le_ecomplexity_add n m).trans_le + (Nat.add_le_add_right (Set.ncard_le_ncard hsub hfin) _) + +/-! ### The Minimum `Kt` Problem (`MKtP`) and `MKtP ∈ E ⊆ EXP` -/ + +/-- **The Minimum `Kt` Problem (`MKtP`)** +([Allender et al., Definition 9][AllenderBuhrmanKouckyVanMelkebeekRonneburger2006]; +[Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]; +[Liu and Pass, Section 2.2][LiuPass2021Crypto]): the set of pairs `(x, k) : List Bool × ℕ` +(encoded by `encPair encBits encUnary`) such that `levinKt x ≤ k`. -/ +def MKtP : Set (List Bool × ℕ) := + {xk | levinKt xk.1 ≤ xk.2} + +namespace MKtP + +/-- A pair `xk` belongs to `MKtP` iff `levinKt xk.1 ≤ xk.2`. -/ +theorem mem_iff {xk : List Bool × ℕ} : xk ∈ MKtP ↔ levinKt xk.1 ≤ xk.2 := + Iff.rfl + +/-- `(x, k) ∈ MKtP` iff `levinKt x ≤ k`. -/ +@[simp] +theorem pair_mem_iff {x : List Bool} {k : ℕ} : (x, k) ∈ MKtP ↔ levinKt x ≤ k := + Iff.rfl + +/-- `(x, k) ∈ MKtP` iff `levinKtNat x ≤ k`. -/ +theorem pair_mem_iff_levinKtNat_le {x : List Bool} {k : ℕ} : + (x, k) ∈ MKtP ↔ levinKtNat x ≤ k := + levinKtNat_le_iff.symm + +/-- `(x, k) ∈ MKtP` iff some program `p` of length at most `k` outputs `x` within `2 ^ (k - |p|)` +steps under `universalTM`. -/ +theorem pair_mem_iff_exists_runFor_two_pow {x : List Bool} {k : ℕ} : + (x, k) ∈ MKtP ↔ + ∃ p : List Bool, p.length ≤ k ∧ x ∈ (universalTM.run p).runFor (2 ^ (k - p.length)) := + levinKt_le_natCast_iff_exists_runFor_two_pow + +/-- Monotonicity of `MKtP` in the threshold `k`. -/ +theorem mem_of_le {x : List Bool} {k₁ k₂ : ℕ} (h : (x, k₁) ∈ MKtP) (hk : k₁ ≤ k₂) : + (x, k₂) ∈ MKtP := + pair_mem_iff.mpr ((pair_mem_iff.mp h).trans (Nat.cast_le.mpr hk)) + +/-- Bounded brute-force search for a `Kt`-witness of `(x, k)` up to word-index and step cap `N`: +checks whether some word `p = Ladner.word j` with `j < N` has `p.length ≤ k` and outputs `x` within +`min (2 ^ (k - p.length)) N` steps. -/ +def boundedSearch (x : List Bool) (k N : ℕ) : Bool := + (List.range N).any fun j => + decide ((Ladner.word j).length ≤ k) && + decide (universalTMRunFor (Ladner.word j) + (Ladner.capPow 2 (k - (Ladner.word j).length) N) = some x) + +/-- Whenever $2^{k + 1} \le N$, `boundedSearch x k N = true` iff `(x, k) ∈ MKtP`. -/ +theorem boundedSearch_eq_true_iff_of_two_pow_le {x : List Bool} {k N : ℕ} + (hN : 2 ^ (k + 1) ≤ N) : + boundedSearch x k N = true ↔ (x, k) ∈ MKtP := by + rw [boundedSearch, List.any_eq_true, pair_mem_iff_exists_runFor_two_pow] + constructor + · rintro ⟨j, _, hj⟩ + simp only [Bool.and_eq_true, decide_eq_true_eq] at hj + refine ⟨Ladner.word j, hj.1, ?_⟩ + rw [universalTM_runFor] + exact universalTMRunFor_mono _ (Nat.min_le_left _ _) hj.2 + · rintro ⟨p, hplen, hp⟩ + refine ⟨Ladner.index p, List.mem_range.mpr ?_, ?_⟩ + · have hind := Ladner.index_add_two_le p + have hpow : 2 ^ (p.length + 1) ≤ 2 ^ (k + 1) := + Nat.pow_le_pow_right (by norm_num) (by omega) + omega + · simp only [Ladner.word_index, Bool.and_eq_true, decide_eq_true_eq] + refine ⟨hplen, ?_⟩ + have hcap : Ladner.capPow 2 (k - p.length) N = 2 ^ (k - p.length) := + Nat.min_eq_left ((Nat.pow_le_pow_right (by norm_num) (by omega)).trans hN) + rw [hcap] + exact hp + +/-- `boundedSearch` is computable in polynomial time when `k` and `N` are encoded in unary. -/ +@[fun_prop] +theorem computableInPolyTime_boundedSearch : + ComputableInPolyTime (fun q : List Bool × (ℕ × ℕ) => boundedSearch q.1 q.2.1 q.2.2) + (encPair encBits (encPair encUnary encUnary)) encBool := by + unfold boundedSearch + fun_prop + +/-- **`MKtP` is in linear exponential time `E`** with respect to `encPair encBits encUnary`. -/ +theorem mem_E : MKtP ∈ E (encPair encBits encUnary) := by + let Ψ : List Bool × ℕ → Bool := fun yN => + boundedSearch (unframe yN.1) (dropFrame yN.1).length yN.2 + have hΨ : ComputableInPolyTime Ψ (encPair encBits encUnary) encBool := by + open ComputableInPolyTime in + have hy := fst encBits encUnary + have hN := snd encBits encUnary + have hunf : ComputableInPolyTime (fun yN : List Bool × ℕ => unframe yN.1) + (encPair encBits encUnary) encBits := + (ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.unframe).comp hy + have hdrop : ComputableInPolyTime (fun yN : List Bool × ℕ => (dropFrame yN.1).length) + (encPair encBits encUnary) encUnary := + (encoding_length encBits).comp + ((ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.dropFrame).comp hy) + exact computableInPolyTime_boundedSearch.comp (hunf.prod (hdrop.prod hN)) + obtain ⟨c, hc⟩ := mem_E_iff.mp (setOf_mem_E_of_computableInPolyTime_pad hΨ) + let g : List Bool × ℕ → List Bool := fun xk => encPair encBits encUnary xk + have hgO : ComputableInO g (encPair encBits encUnary) encBits + (fun xk => (encPair encBits encUnary xk).length) + (fun xk => (encPair encBits encUnary xk).length) := + .of_tidy (ComputableTidilyInO.of_linear + (.of_eq (f := g) (encIn := encPair encBits encUnary) (encMid := encBits) fun _ => rfl)) + have hpre : g ⁻¹' {y : List Bool | Ψ (y, 2 ^ y.length) = true} ∈ + DTIME (encPair encBits encUnary) (fun n => 2 ^ ((c + 1) * n)) := by + refine preimage_mem_DTIME (C := 2) hc hgO fun xk => ?_ + set n := (encPair encBits encUnary xk).length + have hlen : (encBits (g xk)).length = n := rfl + rw [hlen] + have h1 : n ≤ 2 ^ ((c + 1) * n) := by + have : n ≤ (c + 1) * n := Nat.le_mul_of_pos_left n (by omega) + exact this.trans (Nat.lt_two_pow_self.le) + have h2 : 2 ^ (c * n) ≤ 2 ^ ((c + 1) * n) := + Nat.pow_le_pow_right (by norm_num) (by nlinarith) + omega + have heq : MKtP = g ⁻¹' {y : List Bool | Ψ (y, 2 ^ y.length) = true} := by + ext ⟨x, k⟩ + simp only [Set.mem_preimage, Set.mem_ofPred_eq, Ψ, g] + have hunf : unframe (encPair encBits encUnary (x, k)) = x := by + simp [encPair_apply] + have hdrop : (dropFrame (encPair encBits encUnary (x, k))).length = k := by + simp [encPair_apply] + have hpow : 2 ^ (k + 1) ≤ 2 ^ (encPair encBits encUnary (x, k)).length := by + refine Nat.pow_le_pow_right (by norm_num) ?_ + simp only [length_encPair, encBits_apply, encUnary_apply, List.length_replicate] + omega + rw [hunf, hdrop, boundedSearch_eq_true_iff_of_two_pow_le hpow] + rw [heq] + exact mem_E_iff.mpr ⟨c + 1, hpre⟩ + +/-- **`MKtP` is in `EXP`** with respect to `encPair encBits encUnary` +([Allender et al.][AllenderBuhrmanKouckyVanMelkebeekRonneburger2006]; +[Liu and Pass, Section 2.2][LiuPass2021Crypto]). -/ +theorem mem_EXP : MKtP ∈ EXP (encPair encBits encUnary) := + E_subset_EXP mem_E + +end MKtP + +/-! ### Fixed-threshold formulation (`MKtPAt`) -/ + +/-- **Fixed-threshold `MKtP`** (`MKtPAt s`, +[Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]; +[Liu and Pass, Section 2.2][LiuPass2021Crypto]): the language of binary strings `x` with +`levinKt x ≤ s x.length`. -/ +def MKtPAt (s : ℕ → ℕ) : Set (List Bool) := + {x : List Bool | levinKt x ≤ s x.length} + +/-- `x ∈ MKtPAt s` iff `levinKt x ≤ s x.length`. -/ +theorem mem_MKtPAt_iff {s : ℕ → ℕ} {x : List Bool} : + x ∈ MKtPAt s ↔ levinKt x ≤ s x.length := + Iff.rfl + +/-- `x ∈ MKtPAt s` iff `(x, s x.length) ∈ MKtP`. -/ +@[simp] +theorem mem_MKtPAt_iff_mem_MKtP {s : ℕ → ℕ} {x : List Bool} : + x ∈ MKtPAt s ↔ (x, s x.length) ∈ MKtP := + Iff.rfl + +/-- `x ∈ MKtPAt s` iff `levinKtNat x ≤ s x.length`. -/ +theorem mem_MKtPAt_iff_levinKtNat_le {s : ℕ → ℕ} {x : List Bool} : + x ∈ MKtPAt s ↔ levinKtNat x ≤ s x.length := + levinKtNat_le_iff.symm + +namespace MKtPAt + +/-- Whenever `s` is computable in polynomial time in unary, `MKtPAt s` is polynomial-time +many-one reducible to `MKtP`. -/ +theorem polyTimeReducible_MKtP {s : ℕ → ℕ} + (hs : ComputableInPolyTime s encUnary encUnary) : + PolyTimeReducible encBits (encPair encBits encUnary) (MKtPAt s) MKtP := by + refine ⟨fun x => (x, s x.length), ?_, fun _ => Iff.rfl⟩ + open ComputableInPolyTime in + exact id'.prod (hs.comp (encoding_length encBits)) + +/-- **Fixed-threshold `MKtPAt s` is in `EXP`** whenever `s` is computable in polynomial time in +unary. -/ +theorem mem_EXP {s : ℕ → ℕ} (hs : ComputableInPolyTime s encUnary encUnary) : + MKtPAt s ∈ EXP encBits := + (polyTimeReducible_MKtP hs).mem_EXP MKtP.mem_EXP + +/-- For any polynomial threshold `q : Polynomial ℕ`, `MKtPAt q.eval ∈ EXP encBits`. -/ +theorem mem_EXP_polynomial (q : Polynomial ℕ) : + MKtPAt q.eval ∈ EXP encBits := + mem_EXP (ComputableInPolyTime.unary_eval q) + +end MKtPAt + +/-! ### The promise problem `GapMKtP` -/ + +namespace GapMKtP + +/-- The yes-instances of `GapMKtP[s₁, s₂]`: strings `x` with `levinKt x ≤ s₁ x.length` +([Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]). -/ +def yesSet (s₁ : ℕ → ℕ) : Set (List Bool) := + MKtPAt s₁ + +/-- The no-instances of `GapMKtP[s₁, s₂]`: strings `x` with `s₂ x.length < levinKt x` +([Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]). -/ +def noSet (s₂ : ℕ → ℕ) : Set (List Bool) := + {x : List Bool | (s₂ x.length : ℕ∞) < levinKt x} + +/-- `x ∈ GapMKtP.yesSet s₁` iff `x ∈ MKtPAt s₁`. -/ +theorem mem_yesSet_iff {s₁ : ℕ → ℕ} {x : List Bool} : + x ∈ yesSet s₁ ↔ x ∈ MKtPAt s₁ := + Iff.rfl + +/-- `x ∈ GapMKtP.noSet s₂` iff `(s₂ x.length : ℕ∞) < levinKt x`. -/ +theorem mem_noSet_iff {s₂ : ℕ → ℕ} {x : List Bool} : + x ∈ noSet s₂ ↔ (s₂ x.length : ℕ∞) < levinKt x := + Iff.rfl + +/-- `x ∈ GapMKtP.noSet s₂` iff `s₂ x.length < levinKtNat x`. -/ +theorem mem_noSet_iff_lt_levinKtNat {s₂ : ℕ → ℕ} {x : List Bool} : + x ∈ noSet s₂ ↔ s₂ x.length < levinKtNat x := by + rw [mem_noSet_iff, ← natCast_levinKtNat x, ENat.natCast_lt_natCast] + +/-- When `s₁ n ≤ s₂ n` for all `n`, `GapMKtP.yesSet s₁` and `GapMKtP.noSet s₂` are disjoint. -/ +theorem disjoint_yesSet_noSet {s₁ s₂ : ℕ → ℕ} (hs : ∀ n, s₁ n ≤ s₂ n) : + Disjoint (yesSet s₁) (noSet s₂) := by + refine Set.disjoint_left.mpr fun x hyes hno => ?_ + have hle : levinKt x ≤ (s₂ x.length : ℕ∞) := + hyes.trans (Nat.cast_le.mpr (hs x.length)) + exact not_lt_of_ge hle hno + +/-- When `s₁ = s₂`, `GapMKtP.noSet s` is the complement of `MKtPAt s`. -/ +theorem noSet_eq_compl (s : ℕ → ℕ) : noSet s = (MKtPAt s)ᶜ := by + ext x + simp [noSet, MKtPAt] + +end GapMKtP + +/-- **The `GapMKtP` promise problem** +([Oliveira and Santhanam, Section A, Definition 44, p. 34][OliveiraSanthanam2018]): +separates `MKtPAt s₁` (`levinKt x ≤ s₁ |x|`) from `GapMKtP.noSet s₂` (`levinKt x > s₂ |x|`) +whenever `s₁ n ≤ s₂ n`. -/ +def GapMKtP (s₁ s₂ : ℕ → ℕ) (hs : ∀ n, s₁ n ≤ s₂ n) : PromiseProblem (List Bool) where + yes := GapMKtP.yesSet s₁ + no := GapMKtP.noSet s₂ + disjoint := GapMKtP.disjoint_yesSet_noSet hs + +namespace GapMKtP + +variable {s₁ s₂ : ℕ → ℕ} (hs : ∀ n, s₁ n ≤ s₂ n) + +/-- The yes-instances of `GapMKtP s₁ s₂ hs` are `MKtPAt s₁`. -/ +@[simp] +theorem yes_eq : (GapMKtP s₁ s₂ hs).yes = MKtPAt s₁ := + rfl + +/-- The no-instances of `GapMKtP s₁ s₂ hs` are `GapMKtP.noSet s₂`. -/ +@[simp] +theorem no_eq : (GapMKtP s₁ s₂ hs).no = noSet s₂ := + rfl + +/-- With zero gap (`s₁ = s₂ = s`), `GapMKtP` is the decision problem `MKtPAt s` viewed as a promise +problem (`PromiseProblem.ofSet (MKtPAt s)`). -/ +@[simp] +theorem id_eq (s : ℕ → ℕ) : + GapMKtP s s (fun _ => le_rfl) = PromiseProblem.ofSet (MKtPAt s) := by + ext x + · rfl + · rw [no_eq, noSet_eq_compl] + rfl + +end GapMKtP + +end Cslib.Kolmogorov diff --git a/ComplexityTests/MINcKT.lean b/ComplexityTests/MINcKT.lean new file mode 100644 index 0000000000..b9cf54e70f --- /dev/null +++ b/ComplexityTests/MINcKT.lean @@ -0,0 +1,108 @@ +/- +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.Kolmogorov.MKtP +public import Complexity.Computability.Kolmogorov.MINcKT + +/-! +# Tests for `MKtP`, `GapMKtP`, `condUniversalTM`, and `MINcKT` + +Concrete non-vacuity checks and API tests for `Complexity.Computability.Kolmogorov.MKtP` and +`Complexity.Computability.Kolmogorov.MINcKT`. +-/ + +@[expose] public section + +namespace Cslib.Kolmogorov.Tests + +open Cslib.Complexity Cslib.Kolmogorov Cslib.Kolmogorov.DescriptionMethod +open _root_.Turing.MultiTapeTM + +/-! ### `MKtP` and `GapMKtP` checks -/ + +-- `MKtP` is in `E` and `EXP`, and polynomial-threshold `MKtPAt` is in `EXP`. +example : MKtP ∈ E (encPair encBits encUnary) := + MKtP.mem_E + +example : MKtP ∈ EXP (encPair encBits encUnary) := + MKtP.mem_EXP + +example : MKtPAt (Polynomial.X + 1).eval ∈ EXP encBits := + MKtPAt.mem_EXP_polynomial (Polynomial.X + 1) + +-- Concrete yes-instance of `MKtP` from the trivial upper bound `levinKt_le_length_add`. +example (x : List Bool) : + (x, x.length + copyOverhead + Nat.clog 2 (x.length + 1)) ∈ MKtP := + levinKt_le_length_add x + +-- Concrete check of `MKtP.boundedSearch` at `N = 0` (`List.range 0 = []`). +example (x : List Bool) (k : ℕ) : MKtP.boundedSearch x k 0 = false := + rfl + +-- `LiuPass2021Crypto, Fact 3.1`: at least one string of length `n` has an optimal `Kt`-witness +-- running in at most `2 ^ (copyOverhead + Nat.clog 2 (n + 1) + 1)` steps when `1 ≤ n`. +example (n : ℕ) (hn : 1 ≤ n) : + 0 < {x : List Bool | x.length = n ∧ + ∃ (p : List Bool) (s : ℕ), + x ∈ (universalTM.run p).runFor s ∧ + p.length + Nat.clog 2 s ≤ levinKtNat x ∧ + s ≤ 2 ^ (copyOverhead + Nat.clog 2 (n + 1) + 1)}.ncard := by + have h := two_pow_lt_ncard_setOf_exists_optimal_levinKt_le_two_pow hn + have hpow : 2 ^ (n - 1) < 2 ^ n := + Nat.pow_lt_pow_right (by norm_num) (by omega) + omega + +-- Zero-gap specialization of `GapMKtP`. +example (s : ℕ → ℕ) : + GapMKtP s s (fun _ => le_rfl) = PromiseProblem.ofSet (MKtPAt s) := + GapMKtP.id_eq s + +/-! ### `condUniversalTM` and `MINcKT` checks -/ + +-- `MINcKT` and polynomial-threshold `MINcKTAt` are in `NP`. +example : MINcKT ∈ NP MINcKT.enc := + MINcKT.mem_NP + +example : MINcKTAt (Polynomial.X + 1).eval (Polynomial.X + 1).eval ∈ + NP (encPair encBits encBits) := + MINcKTAt.mem_NP_polynomial₂ (Polynomial.X + 1) (Polynomial.X + 1) + +-- At 0 steps, no instance belongs to `MINcKT`, and `MINcKT.check` returns `false`. +example (x y : List Bool) (s : ℕ) : (⟨x, y, 0, s⟩ : MINcKT.Instance) ∉ MINcKT := by + simp [MINcKT.mk_mem_iff] + +example (x y p : List Bool) (s : ℕ) : + MINcKT.check (⟨x, y, 0, s⟩, p) = false := by + simp [MINcKT.check] + +-- Concrete yes-instances of `MINcKT` from self-conditioning (`exists_condTimeBoundedAt_self_le`). +example : ∃ (q : Polynomial ℕ) (c : ℕ), ∀ y : List Bool, + (⟨y, y, q.eval (y.length + 1), c⟩ : MINcKT.Instance) ∈ MINcKT := by + obtain ⟨q, c, _, _, hbound, _⟩ := exists_condTimeBoundedAt_self_le + exact ⟨q, c, fun y => MINcKT.mk_mem_iff.mpr (hbound y le_rfl)⟩ + +-- Concrete no-instances of `MINcKT` from conditional incompressibility +-- (`exists_length_eq_forall_le_condTimeBoundedAt`). +example (y : List Bool) (n t : ℕ) (hn : 1 ≤ n) : + ∃ x : List Bool, x.length = n ∧ (⟨x, y, t, n - 1⟩ : MINcKT.Instance) ∉ MINcKT := by + obtain ⟨x, hx, hall⟩ := exists_length_eq_forall_le_condTimeBoundedAt y n + refine ⟨x, hx, ?_⟩ + rw [MINcKT.mk_mem_iff] + intro hle + have h1 : (n : ℕ∞) ≤ ((n - 1 : ℕ) : ℕ∞) := (hall t).trans hle + have h2 : n ≤ n - 1 := ENat.natCast_le_natCast.mp h1 + omega + +-- Zero-gap specialization of `GapMINcKT`. +example : + GapMINcKT (fun _ _ s => s) (fun _ _ t => t) (fun _ _ _ => le_rfl) (fun _ _ _ => le_rfl) = + PromiseProblem.ofSet MINcKT := + GapMINcKT.id_eq + +end Cslib.Kolmogorov.Tests From eebc9f3a1d9fe362c4c326cda49fbb8900015112 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 19:16:30 +0000 Subject: [PATCH 2/2] docs(Kolmogorov): unify Hirahara2018 ECCC numbering and fix Ko1991/OS18 citations --- .../Computability/Kolmogorov/MINKT.lean | 18 ++++++++--------- .../Computability/Kolmogorov/MINcKT.lean | 2 +- Complexity/Computability/Kolmogorov/MKtP.lean | 20 ++++++++++--------- references.bib | 2 +- 4 files changed, 22 insertions(+), 20 deletions(-) diff --git a/Complexity/Computability/Kolmogorov/MINKT.lean b/Complexity/Computability/Kolmogorov/MINKT.lean index cb1697412c..ab360827b2 100644 --- a/Complexity/Computability/Kolmogorov/MINKT.lean +++ b/Complexity/Computability/Kolmogorov/MINKT.lean @@ -32,7 +32,7 @@ and bridged: * **Thresholds in the instance (`Cslib.Kolmogorov.MINKT`):** An instance `i : MINKT.Instance` consists of a binary string `i.string`, a time bound `i.time`, and a size threshold `i.size`, encoded by `MINKT.enc` as `x` followed by `1^time` and `1^size` in - unary ([Ko][Ko1991]; [Hirahara, Definition II.4][Hirahara2018]). The instance belongs to `MINKT` + unary ([Ko][Ko1991]; [Hirahara, Definition 9][Hirahara2018]). The instance belongs to `MINKT` when `timeBoundedAt i.time i.string ≤ i.size`. * **Fixed-function thresholds (`Cslib.Kolmogorov.MINKTAt t s`):** For time and size threshold functions `t s : ℕ → ℕ`, `MINKTAt t s : Set (List Bool)` is the @@ -51,7 +51,7 @@ and bridged: `{x | timeBounded t x ≤ s x.length}` and its canonical embedding into `MINKT.Instance`. * `Cslib.Kolmogorov.GapMINKT`, `Cslib.Kolmogorov.GapMINKT.yesSet`, `Cslib.Kolmogorov.GapMINKT.noSet`: Hirahara's promise problem `GapMINKT[σ, τ]` and its yes/no sets - ([Hirahara, Definition II.6][Hirahara2018]). + ([Hirahara, Definition 11][Hirahara2018]). ## Main results @@ -89,7 +89,7 @@ open Cslib.Complexity DescriptionMethod namespace MINKT /-- An instance of `MINKT`: a target binary string `string`, a step bound `time`, and a program size -threshold `size` ([Ko][Ko1991]; [Hirahara, Definition II.4][Hirahara2018]). -/ +threshold `size` ([Ko][Ko1991]; [Hirahara, Definition 9][Hirahara2018]). -/ structure Instance where /-- The target binary string `x`. -/ string : List Bool @@ -102,7 +102,7 @@ structure Instance where end MINKT /-- **The Minimum Time-Bounded Kolmogorov Complexity Problem (`MINKT`)** -([Ko][Ko1991]; [Hirahara, Definition II.4][Hirahara2018]): the set of instances +([Ko][Ko1991]; [Hirahara, Definition 9][Hirahara2018]): the set of instances `(x, t, s)` such that some binary program of length at most `s` outputs `x` within `t` steps under `universalTM`. -/ def MINKT : Set MINKT.Instance := @@ -111,7 +111,7 @@ def MINKT : Set MINKT.Instance := namespace MINKT /-- Standard encoding of `MINKT.Instance`: the string `x`, followed by `1^time` and `1^size` in -unary ([Ko][Ko1991]; [Hirahara, Definition II.4][Hirahara2018]). -/ +unary ([Ko][Ko1991]; [Hirahara, Definition 9][Hirahara2018]). -/ def enc : Instance ↪ List Bool := (⟨fun i => (i.string, (i.time, i.size)), fun i j h => by cases i; cases j; simpa using h⟩ : Instance ↪ List Bool × (ℕ × ℕ)).trans @@ -350,12 +350,12 @@ end MINKTAt namespace GapMINKT /-- The yes-instances of `GapMINKT`: instances `(x, t, s)` with $K^t(x) \le s$ -([Hirahara, Definition II.6][Hirahara2018]). -/ +([Hirahara, Definition 11][Hirahara2018]). -/ def yesSet : Set MINKT.Instance := MINKT /-- The raw no-instances of `GapMINKT[σ, τ]`: instances `(x, t, s)` with -$K^{\tau(|x|, t)}(x) > \sigma(|x|, s)$ ([Hirahara, Definition II.6][Hirahara2018]). -/ +$K^{\tau(|x|, t)}(x) > \sigma(|x|, s)$ ([Hirahara, Definition 11][Hirahara2018]). -/ def noSet (σ τ : ℕ → ℕ → ℕ) : Set MINKT.Instance := {i | (σ i.string.length i.size : ℕ∞) < timeBoundedAt (τ i.string.length i.time) i.string} @@ -373,7 +373,7 @@ theorem mem_noSet_iff {σ τ : ℕ → ℕ → ℕ} {i : MINKT.Instance} : Iff.rfl /-- When $\sigma(n, s) \ge s$ and $\tau(n, t) \ge t$ (as required in -[Hirahara, Definition II.6][Hirahara2018]), `GapMINKT.yesSet` and `GapMINKT.noSet σ τ` +[Hirahara, Definition 11][Hirahara2018]), `GapMINKT.yesSet` and `GapMINKT.noSet σ τ` are disjoint. -/ theorem disjoint_yesSet_noSet {σ τ : ℕ → ℕ → ℕ} (hσ : ∀ n s, s ≤ σ n s) (hτ : ∀ n t, t ≤ τ n t) : @@ -395,7 +395,7 @@ theorem noSet_id_eq_compl : noSet (fun _ s => s) (fun _ t => t) = MINKTᶜ := by end GapMINKT -/-- **Hirahara's `GapMINKT` promise problem** ([Hirahara, Definition II.6][Hirahara2018]): +/-- **Hirahara's `GapMINKT` promise problem** ([Hirahara, Definition 11][Hirahara2018]): the promise problem whose yes-instances are `MINKT`, and whose no-instances are `GapMINKT.noSet σ τ`, when `s ≤ σ n s` and `t ≤ τ n t`. Following Hirahara, the gap hypotheses `hσ` and `hτ` are bundled to ensure disjointness of yes- and no-instances by construction. -/ diff --git a/Complexity/Computability/Kolmogorov/MINcKT.lean b/Complexity/Computability/Kolmogorov/MINcKT.lean index 197696e7d5..a943a4bd4f 100644 --- a/Complexity/Computability/Kolmogorov/MINcKT.lean +++ b/Complexity/Computability/Kolmogorov/MINcKT.lean @@ -79,7 +79,7 @@ As with `MINKT` and `MINKTAt`, both threshold conventions are provided and bridg ## References * [S. Hirahara, *Non-Black-Box Worst-Case to Average-Case Reductions within NP*][Hirahara2018] -* [K.-I. Ko, *On the Notion of Infinite Pseudorandom Sequences*][Ko1991] +* [K.-I. Ko, *On the Complexity of Learning Minimum Time-Bounded Turing Machines*][Ko1991] -/ @[expose] public section diff --git a/Complexity/Computability/Kolmogorov/MKtP.lean b/Complexity/Computability/Kolmogorov/MKtP.lean index 708bc62686..5b7896cfe9 100644 --- a/Complexity/Computability/Kolmogorov/MKtP.lean +++ b/Complexity/Computability/Kolmogorov/MKtP.lean @@ -52,12 +52,14 @@ Kolmogorov complexity `Cslib.Kolmogorov.levinKt` ($\mathrm{Kt}$): `R_Kt ∈ E` in [Allender et al., Definitions 1 and 6][AllenderBuhrmanKouckyVanMelkebeekRonneburger2006]). While [Liu and Pass, Section 2.2][LiuPass2021Crypto] encode the threshold $k$ in binary as a - $\lceil \log_2 n \rceil$-bit integer (since $\mathrm{Kt}(x) \le |x| + O(\log |x|)$ makes larger - thresholds trivial), here `MKtP` is paired with the unary threshold encoding - `encPair encBits encUnary` so that $k + 1 \le |(x, 1^k)|$ holds unconditionally for arbitrary - $k \in \mathbb{N}$ without a syntactic $k < 2 |x|$ side condition; for nontrivial thresholds - $k \le O(|x|)$ and for every polynomial-time unary threshold $s$ in `MKtPAt s`, the unary - encoding has polynomial length and `EXP` membership transfers via `PolyTimeReducible.mem_EXP`. + $\lceil \log_2 n \rceil$-bit integer (in their model Fact 2.1 gives $\mathrm{Kt}(x) \le |x| + c$, + and in ours `levinKt_le_length_add` gives + $\mathrm{Kt}(x) \le |x| + \mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil$), here `MKtP` is + paired with the unary threshold encoding `encPair encBits encUnary` so that + $k + 1 \le |(x, 1^k)|$ holds unconditionally for arbitrary $k \in \mathbb{N}$ without a syntactic + $k < 2 |x|$ side condition; for nontrivial thresholds $k \le O(|x|)$ and for every + polynomial-time unary threshold $s$ in `MKtPAt s`, the unary encoding has polynomial length and + `EXP` membership transfers via `PolyTimeReducible.mem_EXP`. Enumerating candidate programs `Ladner.word j` of length at most `k` and running `universalTMRunFor` for $2^{k - |p|}$ steps places `MKtP` in `E (encPair encBits encUnary)` and `EXP (encPair encBits encUnary)`, and places `MKtPAt s` in `EXP encBits` whenever `s` is @@ -433,12 +435,12 @@ end MKtPAt namespace GapMKtP /-- The yes-instances of `GapMKtP[s₁, s₂]`: strings `x` with `levinKt x ≤ s₁ x.length` -([Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]). -/ +([Oliveira and Santhanam, Appendix A, Definition 44, p. 34][OliveiraSanthanam2018]). -/ def yesSet (s₁ : ℕ → ℕ) : Set (List Bool) := MKtPAt s₁ /-- The no-instances of `GapMKtP[s₁, s₂]`: strings `x` with `s₂ x.length < levinKt x` -([Oliveira and Santhanam, Section A, Definition 44][OliveiraSanthanam2018]). -/ +([Oliveira and Santhanam, Appendix A, Definition 44, p. 34][OliveiraSanthanam2018]). -/ def noSet (s₂ : ℕ → ℕ) : Set (List Bool) := {x : List Bool | (s₂ x.length : ℕ∞) < levinKt x} @@ -473,7 +475,7 @@ theorem noSet_eq_compl (s : ℕ → ℕ) : noSet s = (MKtPAt s)ᶜ := by end GapMKtP /-- **The `GapMKtP` promise problem** -([Oliveira and Santhanam, Section A, Definition 44, p. 34][OliveiraSanthanam2018]): +([Oliveira and Santhanam, Appendix A, Definition 44, p. 34][OliveiraSanthanam2018]): separates `MKtPAt s₁` (`levinKt x ≤ s₁ |x|`) from `GapMKtP.noSet s₂` (`levinKt x > s₂ |x|`) whenever `s₁ n ≤ s₂ n`. -/ def GapMKtP (s₁ s₂ : ℕ → ℕ) (hs : ∀ n, s₁ n ≤ s₂ n) : PromiseProblem (List Bool) where diff --git a/references.bib b/references.bib index 9bf77a068c..38701f709a 100644 --- a/references.bib +++ b/references.bib @@ -1922,7 +1922,7 @@ @inproceedings{Hirahara2018 year = {2018}, pages = {247--258}, doi = {10.1109/FOCS.2018.00032}, - note = {Full version in Electronic Colloquium on Computational Complexity (ECCC), TR18-138} + note = {Full version in Electronic Colloquium on Computational Complexity (ECCC), TR18-138; definition numbers follow ECCC TR18-138} } @inproceedings{Hirahara2022,