Skip to content

feat(Computability/Kolmogorov): formalize MKtP ∈ EXP and MINcKT ∈ NP (#798) #1087

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 3 commits into from
Oct 25, 2026
Merged

feat(Computability/Kolmogorov): formalize MKtP ∈ EXP and MINcKT ∈ NP (#798) #1087

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
458c139
feat(Computability/Kolmogorov): formalize MKtP ∈ EXP and MINcKT ∈ NP …
SamuelSchlesinger Oct 25, 2026
293253f
fix(Kolmogorov): extract Conditional.lean, move PolyTimeReducible.mem…
SamuelSchlesinger Oct 25, 2026
eebc9f3
docs(Kolmogorov): unify Hirahara2018 ECCC numbering and fix Ko1991/OS…
SamuelSchlesinger Oct 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions Complexity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -856,10 +856,13 @@ public import Complexity.Computability.Interactive.Sumcheck
public import Complexity.Computability.Kolmogorov.AverageCase
public import Complexity.Computability.Kolmogorov.Basic
public import Complexity.Computability.Kolmogorov.ChainRule
public import Complexity.Computability.Kolmogorov.Conditional
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
Expand Down
40 changes: 40 additions & 0 deletions Complexity/Computability/Complexity/Classes/EXP.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ module

public import Complexity.Computability.Complexity.Classes.Hierarchy
public import Complexity.Computability.Complexity.Classes.Time
public import Complexity.Computability.Complexity.Reduction
import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
Expand Down Expand Up @@ -54,6 +55,8 @@ in exponential time and applying the timed-reduction API.
* `Cslib.Complexity.P_ssubset_EXP`: polynomial time is strictly within exponential time.
* `Cslib.Complexity.setOf_mem_E_of_computableInPolyTime_pad`: polynomial time on inputs
padded to length `2 ^ n` gives `E`.
* `Cslib.Complexity.PolyTimeReducible.mem_EXP`: `EXP` is closed under polynomial-time many-one
reductions.

## References

Expand Down Expand Up @@ -222,4 +225,41 @@ theorem setOf_mem_E_of_computableInPolyTime_pad {Ψ : List Bool × ℕ → Bool}
_ = (c * 4 ^ d + 3) * 2 ^ ((d + 2) * n) := by ring
_ ≤ _ := Nat.le_add_right _ _

/-- **`EXP` is closed under polynomial-time many-one reductions.** -/
theorem PolyTimeReducible.mem_EXP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool}
{A : Set α} {B : Set β} (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
568 changes: 568 additions & 0 deletions Complexity/Computability/Kolmogorov/Conditional.lean
View file
Open in desktop

Large diffs are not rendered by default.

18 changes: 9 additions & 9 deletions Complexity/Computability/Kolmogorov/MINKT.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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 :=
Expand All @@ -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
Expand Down Expand Up @@ -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}
Expand All @@ -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) :
Expand All @@ -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. -/
Expand Down
Loading
Loading