From eb6a8da7ee7e14d2f57b55f08926127ce79b0273 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 09:31:00 +0000 Subject: [PATCH 1/2] refactor(MCSP,Kolmogorov): unify gap convention for GapMCSP and GapMINKT (#884) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Unify promise problem gap conventions across MCSP and MINKT under #884 Item 5: - In `MCSP/Basic.lean`: - Re-implement `GapMCSP` over `List Bool` (truth tables of all lengths) using raw `yesSet (s₁ : ℕ → ℕ) : Language Bool` and `noSet (s₂ : ℕ → ℕ) : Language Bool` rather than single-length parameterization. - Dedup `truthTableLanguage` and `ofFn_mem_truthTableLanguage` into `Circuits.Boolean` in `MCSP/Basic.lean` and remove duplicate in `NaturalProof.lean`. - Provide `ofFn_mem_yesSet_iff_mem_MCSP`, `ofFn_mem_noSet_iff_not_mem_MCSP`, `disjoint_yesSet_noSet`, `yesSet_mono`, and `noSet_anti`. - In `Kolmogorov/MINKT.lean`: - Rename raw sets to `GapMINKT.yesSet` and `GapMINKT.noSet` to avoid shadowing `PromiseProblem.yes` and `PromiseProblem.no`. - Define `GapMINKT` cleanly as `{ yes := yesSet, no := noSet, disjoint := ... }` without artificial set subtraction `\ yes`. - Update `disjoint_yesSet_noSet`, `no_eq`, `id_eq`. - Update tests and axiom guards in `Axioms.lean`, `Kannan.lean`, `KarpLipton.lean`, and `KolmogorovTimeBounded.lean`. --- .../Circuit/Boolean/NaturalProof.lean | 21 +-- .../Computability/Kolmogorov/MINKT.lean | 69 ++++---- Complexity/Computability/MCSP/Basic.lean | 156 ++++++++++++------ ComplexityTests/Kannan.lean | 6 +- ComplexityTests/KarpLipton.lean | 10 +- ComplexityTests/KolmogorovTimeBounded.lean | 8 +- 6 files changed, 153 insertions(+), 117 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/NaturalProof.lean b/Complexity/Computability/Circuit/Boolean/NaturalProof.lean index beb6323c3f..62db92761e 100644 --- a/Complexity/Computability/Circuit/Boolean/NaturalProof.lean +++ b/Complexity/Computability/Circuit/Boolean/NaturalProof.lean @@ -132,25 +132,6 @@ theorem card_filter_truthTableTest (C : Set (BooleanFunction n)) : truthTableTest_truthTable_eq_true_iff, (truthTable n).injective.mem_set_image] rw [← Set.ncard_coe_finset, h, Set.ncard_image_of_injective _ (truthTable n).injective] -/-- The truth tables of a property, as a language [RazborovRudich1997]: a word of length `2 ^ n` -belongs to it when it is the truth table of a function in `C n`. Words whose length is not a power -of two do not belong to it. -/ -def truthTableLanguage (C : ∀ n, Set (BooleanFunction n)) : Language Bool := - {w | ∃ n, ∃ h : w.length = 2 ^ n, - (truthTable n).symm (fun i => w[(i : ℕ)]'(i.isLt.trans_eq h.symm)) ∈ C n} - -/-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `truthTableLanguage C` -if and only if its corresponding Boolean function lies in `C n`. -/ -theorem ofFn_mem_truthTableLanguage {C : ∀ n, Set (BooleanFunction n)} {T : BitString (2 ^ n)} : - List.ofFn T ∈ truthTableLanguage C ↔ (truthTable n).symm T ∈ C n := by - constructor - · rintro ⟨m, h, hm⟩ - obtain rfl : m = n := - Nat.pow_right_injective le_rfl (h.symm.trans (List.length_ofFn (f := T))) - simpa only [List.getElem_ofFn] using hm - · intro h - exact ⟨n, List.length_ofFn, by simpa only [List.getElem_ofFn] using h⟩ - /-- At length `2 ^ n`, the truth-table language of `C` is decided by the test for `C n`. -/ @[simp] theorem slice_truthTableLanguage (C : ∀ n, Set (BooleanFunction n)) (n : ℕ) : (truthTableLanguage C).slice (2 ^ n) = truthTableTest (C n) := by @@ -398,7 +379,7 @@ theorem isUseful_PPoly_setOf_lt_complexity : /-- Under the hypothesis of `not_isUseful_PPoly_of_isNatural`, the truth tables of the functions on `n` inputs that need more than `2 ^ n / (5 n)` gates, that is the no-instances -`GapMCSP.no (fun n => 2 ^ n / (5 * n)) n`, do not form a language in `P/poly` +`GapMCSP.noSet (fun n => 2 ^ n / (5 * n))`, do not form a language in `P/poly` [RazborovRudich1997], [KabanetsCai2000]. The property is large and useful against `P/poly`, so it is not `P/poly`-constructive. -/ theorem truthTableLanguage_setOf_lt_complexity_notMem_PPoly {F : ∀ n, Key n → BooleanFunction n} diff --git a/Complexity/Computability/Kolmogorov/MINKT.lean b/Complexity/Computability/Kolmogorov/MINKT.lean index 827b1a1dea..06647ba6ac 100644 --- a/Complexity/Computability/Kolmogorov/MINKT.lean +++ b/Complexity/Computability/Kolmogorov/MINKT.lean @@ -49,8 +49,8 @@ and bridged: * `Cslib.Kolmogorov.MINKT.check`: polynomial-time witness check for `MINKT`. * `Cslib.Kolmogorov.MINKTAt`, `Cslib.Kolmogorov.MINKTAt.toInstance`: fixed-threshold language `{x | timeBounded t x ≤ s x.length}` and its canonical embedding into `MINKT.Instance`. -* `Cslib.Kolmogorov.GapMINKT`, `Cslib.Kolmogorov.GapMINKT.yes`, `Cslib.Kolmogorov.GapMINKT.no`: - Hirahara's promise problem `GapMINKT[σ, τ]` and its yes/no sets +* `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]). ## Main results @@ -69,7 +69,7 @@ and bridged: * `Cslib.Kolmogorov.MINKTAt.mem_NP`, `Cslib.Kolmogorov.MINKTAt.mem_NP_polynomial`, `Cslib.Kolmogorov.MINKTAt.mem_NP_polynomial₂`: `MINKTAt t s ∈ NP encBits` for polynomial-time unary thresholds and for polynomial time bounds `t = p.eval`. -* `Cslib.Kolmogorov.GapMINKT.disjoint_yes_no`, `Cslib.Kolmogorov.GapMINKT.no_eq`, +* `Cslib.Kolmogorov.GapMINKT.disjoint_yesSet_noSet`, `Cslib.Kolmogorov.GapMINKT.no_eq`, `Cslib.Kolmogorov.GapMINKT.id_eq`: consistency and specialization of `GapMINKT`. ## References @@ -351,32 +351,33 @@ namespace GapMINKT /-- The yes-instances of `GapMINKT`: instances `(x, t, s)` with $K^t(x) \le s$ ([Hirahara, Definition II.6][Hirahara2018]). -/ -def yes : Set MINKT.Instance := +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]). -/ -def no (σ τ : ℕ → ℕ → ℕ) : Set MINKT.Instance := +def noSet (σ τ : ℕ → ℕ → ℕ) : Set MINKT.Instance := {i | (σ i.string.length i.size : ℕ∞) < timeBoundedAt (τ i.string.length i.time) i.string} -/-- `i ∈ GapMINKT.yes` iff `i ∈ MINKT`. -/ -theorem mem_yes_iff {i : MINKT.Instance} : i ∈ yes ↔ i ∈ MINKT := +/-- `i ∈ GapMINKT.yesSet` iff `i ∈ MINKT`. -/ +theorem mem_yesSet_iff {i : MINKT.Instance} : i ∈ yesSet ↔ i ∈ MINKT := Iff.rfl -/-- `i ∈ GapMINKT.no σ τ` iff +/-- `i ∈ GapMINKT.noSet σ τ` iff `σ |i.string| i.size < timeBoundedAt (τ |i.string| i.time) i.string`. -/ -theorem mem_no_iff {σ τ : ℕ → ℕ → ℕ} {i : MINKT.Instance} : - i ∈ no σ τ ↔ +theorem mem_noSet_iff {σ τ : ℕ → ℕ → ℕ} {i : MINKT.Instance} : + i ∈ noSet σ τ ↔ (σ i.string.length i.size : ℕ∞) < timeBoundedAt (τ i.string.length i.time) i.string := Iff.rfl /-- When $\sigma(n, s) \ge s$ and $\tau(n, t) \ge t$ (as required in -[Hirahara, Definition II.6][Hirahara2018]), `GapMINKT.yes` and `GapMINKT.no σ τ` are disjoint. -/ -theorem disjoint_yes_no {σ τ : ℕ → ℕ → ℕ} +[Hirahara, Definition II.6][Hirahara2018]), `GapMINKT.yesSet` and `GapMINKT.noSet σ τ` +are disjoint. -/ +theorem disjoint_yesSet_noSet {σ τ : ℕ → ℕ → ℕ} (hσ : ∀ n s, s ≤ σ n s) (hτ : ∀ n t, t ≤ τ n t) : - Disjoint yes (no σ τ) := by + Disjoint yesSet (noSet σ τ) := by refine Set.disjoint_left.mpr fun i hyes hno => ?_ have h1 : timeBoundedAt (τ i.string.length i.time) i.string ≤ timeBoundedAt i.time i.string := @@ -386,42 +387,48 @@ theorem disjoint_yes_no {σ τ : ℕ → ℕ → ℕ} (h1.trans hyes).trans (Nat.cast_le.mpr (hσ i.string.length i.size)) exact not_lt_of_ge h2 hno -/-- With trivial gap functions `σ n s = s` and `τ n t = t`, `GapMINKT.no` is the complement of +/-- With trivial gap functions `σ n s = s` and `τ n t = t`, `GapMINKT.noSet` is the complement of `MINKT`. -/ -theorem no_id_eq_compl : no (fun _ s => s) (fun _ t => t) = MINKTᶜ := by +theorem noSet_id_eq_compl : noSet (fun _ s => s) (fun _ t => t) = MINKTᶜ := by ext i - simp [no, MINKT] + simp [noSet, MINKT] end GapMINKT /-- **Hirahara's `GapMINKT` promise problem** ([Hirahara, Definition II.6][Hirahara2018]): -yes-instances are `MINKT`, and no-instances are those in `GapMINKT.no σ τ \ MINKT` (which equals -`GapMINKT.no σ τ` whenever `s ≤ σ n s` and `t ≤ τ n t`, see `GapMINKT.no_eq`). -/ -def GapMINKT (σ τ : ℕ → ℕ → ℕ) : PromiseProblem MINKT.Instance where - yes := GapMINKT.yes - no := GapMINKT.no σ τ \ GapMINKT.yes - disjoint := disjoint_sdiff_self_right +the promise problem whose yes-instances are `MINKT`, and whose no-instances are +`GapMINKT.noSet σ τ`, when `s ≤ σ n s` and `t ≤ τ n t`. -/ +def GapMINKT (σ τ : ℕ → ℕ → ℕ) + (hσ : ∀ n s, s ≤ σ n s) (hτ : ∀ n t, t ≤ τ n t) : + PromiseProblem MINKT.Instance where + yes := GapMINKT.yesSet + no := GapMINKT.noSet σ τ + disjoint := GapMINKT.disjoint_yesSet_noSet hσ hτ namespace GapMINKT -/-- The yes-set of `GapMINKT σ τ` is `MINKT`. -/ +variable {σ τ : ℕ → ℕ → ℕ} +variable (hσ : ∀ n s, s ≤ σ n s) (hτ : ∀ n t, t ≤ τ n t) + +/-- The yes-set of `GapMINKT σ τ hσ hτ` is `MINKT`. -/ @[simp] -theorem yes_eq (σ τ : ℕ → ℕ → ℕ) : (GapMINKT σ τ).yes = MINKT := +theorem yes_eq : (GapMINKT σ τ hσ hτ).yes = MINKT := rfl -/-- Whenever $\sigma(n, s) \ge s$ and $\tau(n, t) \ge t$, `(GapMINKT σ τ).no = GapMINKT.no σ τ`. -/ -theorem no_eq {σ τ : ℕ → ℕ → ℕ} - (hσ : ∀ n s, s ≤ σ n s) (hτ : ∀ n t, t ≤ τ n t) : - (GapMINKT σ τ).no = no σ τ := - sdiff_eq_left.mpr (disjoint_yes_no hσ hτ).symm +/-- The no-instances of `GapMINKT σ τ hσ hτ` are `GapMINKT.noSet σ τ`. -/ +@[simp] +theorem no_eq : (GapMINKT σ τ hσ hτ).no = noSet σ τ := + rfl /-- With no gap (`σ n s = s` and `τ n t = t`), `GapMINKT` is the decision problem `MINKT` viewed as a promise problem (`PromiseProblem.ofSet MINKT`). -/ @[simp] -theorem id_eq : GapMINKT (fun _ s => s) (fun _ t => t) = PromiseProblem.ofSet MINKT := by +theorem id_eq : + GapMINKT (fun _ s => s) (fun _ t => t) (fun _ _ => le_rfl) (fun _ _ => le_rfl) = + PromiseProblem.ofSet MINKT := by ext i · rfl - · rw [no_eq (fun _ _ => le_rfl) (fun _ _ => le_rfl), no_id_eq_compl] + · rw [no_eq, noSet_id_eq_compl] rfl end GapMINKT diff --git a/Complexity/Computability/MCSP/Basic.lean b/Complexity/Computability/MCSP/Basic.lean index 6fd97754cd..44cb83b75e 100644 --- a/Complexity/Computability/MCSP/Basic.lean +++ b/Complexity/Computability/MCSP/Basic.lean @@ -13,6 +13,7 @@ public import Complexity.Computability.Complexity.Classes.Promise.Basic public import Complexity.Foundations.Data.BitString.Basic public import Cslib.Computability.Circuit.Boolean.Complexity public import Cslib.Computability.Circuit.Boolean.Counting +public import Mathlib.Computability.Language public import Mathlib.Data.Set.Card /-! @@ -37,18 +38,20 @@ cslib's `computableFunctions n s`, so there are as many of them as such function ## Main definitions * `Cslib.MCSP.truthTable`: truth tables of Boolean functions. +* `Cslib.Circuits.Boolean.truthTableLanguage`: the truth tables of a property, as a language. * `Cslib.MCSP.Instance`, `Cslib.MCSP`: the instances and the yes-instances of MCSP. -* `Cslib.GapMCSP`: `GapMCSP[s₁, s₂]` as a `PromiseProblem`, with sides `Cslib.GapMCSP.yes` and - `Cslib.GapMCSP.no`. +* `Cslib.GapMCSP`: `GapMCSP[s₁, s₂]` as a `PromiseProblem (List Bool)`, with sides + `Cslib.GapMCSP.yesSet` and `Cslib.GapMCSP.noSet`. ## Main results +* `Cslib.Circuits.Boolean.ofFn_mem_truthTableLanguage`: membership of an `ofFn`-vector in + `truthTableLanguage`. * `Cslib.MCSP.mem_iff_exists_circuit`, `Cslib.MCSP.mem_iff_mem_computableFunctions`: the yes- instances of MCSP, as circuits and as computable functions. * `Cslib.MCSP.ncard_setOf_mem`: the number of yes-instances of a given arity and threshold. -* `Cslib.GapMCSP.disjoint_yes_no`: the promise of `GapMCSP[s₁, s₂]` is consistent when - `s₁ ≤ s₂`, and `Cslib.GapMCSP.no_eq_compl_yes`, `Cslib.GapMCSP.eq_ofSet`: `GapMCSP[s, s]` is - MCSP at threshold `s`. +* `Cslib.GapMCSP.disjoint_yesSet_noSet`: the promise of `GapMCSP[s₁, s₂]` is consistent when + `s₁ n ≤ s₂ n` for all `n`. ## References @@ -158,70 +161,113 @@ theorem ncard_setOf_mem (n s : ℕ) : end MCSP -namespace GapMCSP - -open MCSP - -variable {s₁ s₂ : ℕ → ℕ} {n : ℕ} - -/-- The yes-instances of `GapMCSP[s₁, s₂]` on functions of `n` inputs: the truth tables of -functions with circuits of at most `s₁ n` gates [OliveiraPichSanthanam2019, Definition 2.4]. -/ -def yes (s₁ : ℕ → ℕ) (n : ℕ) : Set (BitString (2 ^ n)) := - {T | complexity interpretation (single ((truthTable n).symm T)) ≤ s₁ n} +namespace Circuits.Boolean + +/-- The truth tables of a property, as a language [RazborovRudich1997]: a word of length `2 ^ n` +belongs to it when it is the truth table of a function in `C n`. Words whose length is not a power +of two do not belong to it. -/ +def truthTableLanguage (C : ∀ n, Set (BooleanFunction n)) : Language Bool := + {w | ∃ n, ∃ h : w.length = 2 ^ n, + (MCSP.truthTable n).symm (fun i => w[(i : ℕ)]'(i.isLt.trans_eq h.symm)) ∈ C n} + +/-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `truthTableLanguage C` +if and only if its corresponding Boolean function lies in `C n`. -/ +theorem ofFn_mem_truthTableLanguage {C : ∀ n, Set (BooleanFunction n)} {n : ℕ} + {T : BitString (2 ^ n)} : + List.ofFn T ∈ truthTableLanguage C ↔ (MCSP.truthTable n).symm T ∈ C n := by + constructor + · rintro ⟨m, h, hm⟩ + obtain rfl : m = n := + Nat.pow_right_injective le_rfl (h.symm.trans (List.length_ofFn (f := T))) + simpa only [List.getElem_ofFn] using hm + · intro h + exact ⟨n, List.length_ofFn, by simpa only [List.getElem_ofFn] using h⟩ + +end Circuits.Boolean -/-- The no-instances of `GapMCSP[s₁, s₂]` on functions of `n` inputs: the truth tables of -functions that need more than `s₂ n` gates [OliveiraPichSanthanam2019, Definition 2.4]. -/ -def no (s₂ : ℕ → ℕ) (n : ℕ) : Set (BitString (2 ^ n)) := - {T | s₂ n < complexity interpretation (single ((truthTable n).symm T))} - -/-- The yes-instances of `GapMCSP[s₁, s₂]` are those of MCSP at threshold `s₁ n`. -/ -theorem mem_yes_iff {T : BitString (2 ^ n)} : T ∈ yes s₁ n ↔ ⟨n, T, s₁ n⟩ ∈ MCSP := - Iff.rfl - -/-- The no-instances of `GapMCSP[s₁, s₂]` are the truth tables that are not yes-instances of -MCSP at threshold `s₂ n`. -/ -theorem no_eq_compl_yes (s₂ : ℕ → ℕ) (n : ℕ) : no s₂ n = (yes s₂ n)ᶜ := by - ext T - simp [yes, no] +namespace GapMCSP -/-- The promise of `GapMCSP[s₁, s₂]` is consistent: when `s₁ n ≤ s₂ n`, no truth table is both a -yes-instance and a no-instance. -/ -theorem disjoint_yes_no (h : s₁ n ≤ s₂ n) : Disjoint (yes s₁ n) (no s₂ n) := - Set.disjoint_left.mpr fun _ hyes hno => (lt_irrefl _) ((hyes.trans h).trans_lt hno) +open MCSP Circuits.Boolean + +variable {s₁ s₂ : ℕ → ℕ} + +/-- The yes-instances of `GapMCSP[s₁, s₂]` across all lengths [OliveiraPichSanthanam2019, +Definition 2.4]: the truth tables of Boolean functions with circuit complexity at most +`s₁ n`. -/ +def yesSet (s₁ : ℕ → ℕ) : Language Bool := + truthTableLanguage fun n => {f | complexity interpretation (single f) ≤ s₁ n} + +/-- The no-instances of `GapMCSP[s₁, s₂]` across all lengths [OliveiraPichSanthanam2019, +Definition 2.4]: the truth tables of Boolean functions with circuit complexity greater than +`s₂ n`. -/ +def noSet (s₂ : ℕ → ℕ) : Language Bool := + truthTableLanguage fun n => {f | s₂ n < complexity interpretation (single f)} + +/-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `yesSet s₁` +if and only if its circuit complexity is at most `s₁ n`. -/ +@[simp] theorem ofFn_mem_yesSet_iff {n : ℕ} {T : BitString (2 ^ n)} : + List.ofFn T ∈ yesSet s₁ ↔ complexity interpretation (single ((truthTable n).symm T)) ≤ s₁ n := + ofFn_mem_truthTableLanguage + +/-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `yesSet s₁` +if and only if `⟨n, T, s₁ n⟩ ∈ MCSP`. -/ +theorem ofFn_mem_yesSet_iff_mem_MCSP {n : ℕ} {T : BitString (2 ^ n)} : + List.ofFn T ∈ yesSet s₁ ↔ (⟨n, T, s₁ n⟩ : MCSP.Instance) ∈ MCSP := + ofFn_mem_yesSet_iff + +/-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `noSet s₂` +if and only if its circuit complexity is strictly greater than `s₂ n`. -/ +@[simp] theorem ofFn_mem_noSet_iff {n : ℕ} {T : BitString (2 ^ n)} : + List.ofFn T ∈ noSet s₂ ↔ s₂ n < complexity interpretation (single ((truthTable n).symm T)) := + ofFn_mem_truthTableLanguage + +/-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `noSet s₂` +if and only if `⟨n, T, s₂ n⟩ ∉ MCSP`. -/ +theorem ofFn_mem_noSet_iff_not_mem_MCSP {n : ℕ} {T : BitString (2 ^ n)} : + List.ofFn T ∈ noSet s₂ ↔ (⟨n, T, s₂ n⟩ : MCSP.Instance) ∉ MCSP := by + rw [ofFn_mem_noSet_iff] + exact not_le.symm + +/-- When `s₁ n ≤ s₂ n` for all `n`, no truth table is both a yes-instance and a no-instance. -/ +theorem disjoint_yesSet_noSet (h : ∀ n, s₁ n ≤ s₂ n) : Disjoint (yesSet s₁) (noSet s₂) := by + refine Set.disjoint_left.mpr fun w hyes hno => ?_ + obtain ⟨n₁, hn₁, hf₁⟩ := hyes + obtain ⟨n₂, hn₂, hf₂⟩ := hno + obtain rfl : n₁ = n₂ := + Nat.pow_right_injective le_rfl (hn₁.symm.trans hn₂) + have h_eq : (truthTable n₁).symm (fun i => w[(i : ℕ)]'(i.isLt.trans_eq hn₁.symm)) = + (truthTable n₁).symm (fun i => w[(i : ℕ)]'(i.isLt.trans_eq hn₂.symm)) := rfl + rw [h_eq] at hf₁ + exact (lt_irrefl _) ((hf₁.trans (h n₁)).trans_lt hf₂) /-- Raising the yes-threshold adds yes-instances. -/ -theorem yes_mono {s₁' : ℕ → ℕ} (h : s₁ n ≤ s₁' n) : yes s₁ n ⊆ yes s₁' n := - fun _ hT => le_trans hT h +theorem yesSet_mono {s₁' : ℕ → ℕ} (h : ∀ n, s₁ n ≤ s₁' n) : yesSet s₁ ≤ yesSet s₁' := + fun _ ⟨n, hn, hf⟩ => ⟨n, hn, le_trans hf (h n)⟩ /-- Raising the no-threshold removes no-instances. -/ -theorem no_anti {s₂' : ℕ → ℕ} (h : s₂ n ≤ s₂' n) : no s₂' n ⊆ no s₂ n := - fun _ hT => lt_of_le_of_lt h hT +theorem noSet_anti {s₂' : ℕ → ℕ} (h : ∀ n, s₂ n ≤ s₂' n) : noSet s₂' ≤ noSet s₂ := + fun _ ⟨n, hn, hf⟩ => ⟨n, hn, lt_of_le_of_lt (h n) hf⟩ end GapMCSP -/-- **`GapMCSP[s₁, s₂]` on functions of `n` inputs** [OliveiraPichSanthanam2019, Definition 2.4]: -the promise problem whose yes-instances are the truth tables of functions with circuits of at most -`s₁ n` gates and whose no-instances are those of functions that need more than `s₂ n` gates, when -`s₁ n ≤ s₂ n`. -/ -def GapMCSP (s₁ s₂ : ℕ → ℕ) (n : ℕ) (h : s₁ n ≤ s₂ n) : - Complexity.PromiseProblem (BitString (2 ^ n)) where - yes := GapMCSP.yes s₁ n - no := GapMCSP.no s₂ n - disjoint := GapMCSP.disjoint_yes_no h +/-- **`GapMCSP[s₁, s₂]`** [OliveiraPichSanthanam2019, Definition 2.4]: the promise problem whose +yes-instances are truth tables of functions with circuits of at most `s₁ n` gates and whose +no-instances are truth tables of functions that need more than `s₂ n` gates, when `s₁ n ≤ s₂ n` +for all `n`. -/ +def GapMCSP (s₁ s₂ : ℕ → ℕ) (h : ∀ n, s₁ n ≤ s₂ n) : + Complexity.PromiseProblem (List Bool) where + yes := GapMCSP.yesSet s₁ + no := GapMCSP.noSet s₂ + disjoint := GapMCSP.disjoint_yesSet_noSet h namespace GapMCSP -variable {s₁ s₂ : ℕ → ℕ} {n : ℕ} - -@[simp] theorem yes_eq (h : s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ n h).yes = yes s₁ n := rfl +variable {s₁ s₂ : ℕ → ℕ} +variable (h : ∀ n, s₁ n ≤ s₂ n) -@[simp] theorem no_eq (h : s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ n h).no = no s₂ n := rfl +@[simp] theorem yes_eq : (GapMCSP s₁ s₂ h).yes = yesSet s₁ := rfl -/-- At equal thresholds `s`, `GapMCSP[s, s]` is the decision problem `GapMCSP.yes s n`, MCSP on -`n` inputs at threshold `s`. -/ -@[simp] theorem eq_ofSet (s : ℕ → ℕ) (n : ℕ) : - GapMCSP s s n le_rfl = Complexity.PromiseProblem.ofSet (yes s n) := - Complexity.PromiseProblem.ext rfl (no_eq_compl_yes s n) +@[simp] theorem no_eq : (GapMCSP s₁ s₂ h).no = noSet s₂ := rfl end GapMCSP diff --git a/ComplexityTests/Kannan.lean b/ComplexityTests/Kannan.lean index d610847b64..5f8c54ff64 100644 --- a/ComplexityTests/Kannan.lean +++ b/ComplexityTests/Kannan.lean @@ -37,9 +37,9 @@ example : MCSP.tableFunction 2 [false, true, true, false] ![true, false] = true example : MCSP.tableFunction 2 [false, true, true, false] ![true, true] = false := by decide example : Kannan.table 0 0 (List.replicate 10 true) = List.replicate 8 true := by decide --- GapMCSP bundles `GapMCSP.yes`, `GapMCSP.no`, and `GapMCSP.disjoint_yes_no` as a `PromiseProblem`. -example (s : ℕ → ℕ) (n : ℕ) : - GapMCSP s s n le_rfl = PromiseProblem.ofSet (GapMCSP.yes s n) := by simp +-- GapMCSP bundles `GapMCSP.yesSet`, `GapMCSP.noSet`, and `GapMCSP.disjoint_yesSet_noSet`. +example (s : ℕ → ℕ) : + (GapMCSP s s fun _ => le_rfl).yes = GapMCSP.yesSet s := rfl example : BitString.binaryValue [true, false, true] = 5 := by decide example {u v : List Bool} (hlen : u.length = v.length) diff --git a/ComplexityTests/KarpLipton.lean b/ComplexityTests/KarpLipton.lean index adda998619..dd0041cc16 100644 --- a/ComplexityTests/KarpLipton.lean +++ b/ComplexityTests/KarpLipton.lean @@ -155,11 +155,13 @@ example : (⟨1, ![true, false], 0⟩ : MCSP.Instance) ∉ MCSP := by · have := hV []; revert this; cases b <;> decide · simp [certLength, MCSP.budget] at hu -example : ![false, true] ∈ (GapMCSP (fun _ => 0) (fun _ => 0) 1 le_rfl).yes := - MCSP.mem_of_verifier_eq_true (x := ⟨1, ![false, true], 0⟩) (w := certificate 1 0 [] 0) (by decide) +example : [false, true] ∈ (GapMCSP (fun _ => 0) (fun _ => 0) fun _ => le_rfl).yes := + (GapMCSP.ofFn_mem_yesSet_iff_mem_MCSP (n := 1) (T := ![false, true])).mpr + (MCSP.mem_of_verifier_eq_true (x := ⟨1, ![false, true], 0⟩) (w := certificate 1 0 [] 0) + (by decide)) -example : ![true, false] ∈ (GapMCSP (fun _ => 0) (fun _ => 0) 1 le_rfl).no := by - rw [GapMCSP.no_eq, GapMCSP.no_eq_compl_yes, Set.mem_compl_iff, GapMCSP.mem_yes_iff] +example : [true, false] ∈ (GapMCSP (fun _ => 0) (fun _ => 0) fun _ => le_rfl).no := by + refine (GapMCSP.ofFn_mem_noSet_iff_not_mem_MCSP (n := 1) (T := ![true, false])).mpr ?_ intro hx obtain ⟨_ | ⟨b, _ | _⟩, hu, hV⟩ := MCSP.exists_verifier_append hx · revert hu; decide diff --git a/ComplexityTests/KolmogorovTimeBounded.lean b/ComplexityTests/KolmogorovTimeBounded.lean index a03eb5c22c..a4fe521501 100644 --- a/ComplexityTests/KolmogorovTimeBounded.lean +++ b/ComplexityTests/KolmogorovTimeBounded.lean @@ -110,16 +110,15 @@ example (t s : ℕ) : -- exhibits both a concrete yes-instance and a no-instance of length `2 * s + 2`. example : let P := GapMINKT (fun _ s => 2 * s + 1) (fun _ t => 2 * t + 2) + (fun _ s => by omega) (fun _ t => by omega) (⟨[true, false], 3, 2 + copyOverhead⟩ : MINKT.Instance) ∈ P.yes ∧ ∀ t s : ℕ, ∃ x : List Bool, x.length = 2 * s + 2 ∧ (⟨x, t, s⟩ : MINKT.Instance) ∈ P.no := by intro P - have hno_eq : P.no = GapMINKT.no (fun _ s => 2 * s + 1) (fun _ t => 2 * t + 2) := - GapMINKT.no_eq (fun _ s => by omega) (fun _ t => by omega) refine ⟨MINKT.mk_mem_iff.mpr (timeBoundedAt_le_length_add le_rfl), fun t s => ?_⟩ obtain ⟨x, hx, hall⟩ := exists_length_eq_forall_le_timeBounded (2 * s + 2) refine ⟨x, hx, ?_⟩ - rw [hno_eq, GapMINKT.mem_no_iff] + rw [GapMINKT.no_eq, GapMINKT.mem_noSet_iff] dsimp only have hle : ((2 * s + 2 : ℕ) : ℕ∞) ≤ timeBoundedAt (2 * t + 2) x := hall (fun _ => 2 * t + 2) @@ -131,7 +130,8 @@ example : MINKT ∈ NP MINKT.enc := example (p q : Polynomial ℕ) : MINKTAt p.eval q.eval ∈ NP encBits := MINKTAt.mem_NP_polynomial₂ p q -example : GapMINKT (fun _ s => s) (fun _ t => t) = PromiseProblem.ofSet MINKT := +example : GapMINKT (fun _ s => s) (fun _ t => t) (fun _ _ => le_rfl) (fun _ _ => le_rfl) = + PromiseProblem.ofSet MINKT := GapMINKT.id_eq end ComplexityTests.KolmogorovTimeBounded From 3deddaae2431f32ef2d0839078d261154b0a5db9 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 10:06:59 +0000 Subject: [PATCH 2/2] refactor(MCSP,Kolmogorov): address reviewer feedback on gap convention (#884) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit • MCSP/Basic.lean: add ofFn_mem_yesSet_iff_mem_MCSP and ofFn_mem_noSet_iff_notMem_MCSP to Main results. Document that GapMCSP bundles the threshold ordering hypothesis per OPS19 Def 2.4 to ensure disjointness by construction. • MCSP/Basic.lean, KarpLipton.lean: rename ofFn_mem_noSet_iff_not_mem_MCSP to ofFn_mem_noSet_iff_notMem_MCSP following Mathlib naming convention. • NaturalProof.lean: remove moved truthTableLanguage from Main definitions. • MINKT.lean: document that GapMINKT bundles the gap hypotheses per Hirahara Def II.6 to ensure disjointness by construction. • Kannan.lean: replace signature restatement with concrete tests verifying that a word of length 3 (not a power of two) belongs to neither side of GapMCSP. --- .../Circuit/Boolean/NaturalProof.lean | 1 - .../Computability/Kolmogorov/MINKT.lean | 3 ++- Complexity/Computability/MCSP/Basic.lean | 8 ++++-- ComplexityTests/Kannan.lean | 27 ++++++++++++++++--- ComplexityTests/KarpLipton.lean | 2 +- 5 files changed, 33 insertions(+), 8 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/NaturalProof.lean b/Complexity/Computability/Circuit/Boolean/NaturalProof.lean index 62db92761e..1bb2df068d 100644 --- a/Complexity/Computability/Circuit/Boolean/NaturalProof.lean +++ b/Complexity/Computability/Circuit/Boolean/NaturalProof.lean @@ -62,7 +62,6 @@ in `P/poly` (`truthTableLanguage_setOf_lt_complexity_notMem_PPoly`) [KabanetsCai ## Main definitions * `Cslib.Circuits.Boolean.truthTableTest`: the test deciding a property from truth tables. -* `Cslib.Circuits.Boolean.truthTableLanguage`: the truth tables of a property, as a language. * `Cslib.Circuits.Boolean.NaturalProof.IsLarge`, `Cslib.Circuits.Boolean.NaturalProof.IsNatural`, `Cslib.Circuits.Boolean.NaturalProof.IsUseful`: large, natural and useful properties. diff --git a/Complexity/Computability/Kolmogorov/MINKT.lean b/Complexity/Computability/Kolmogorov/MINKT.lean index 06647ba6ac..cb1697412c 100644 --- a/Complexity/Computability/Kolmogorov/MINKT.lean +++ b/Complexity/Computability/Kolmogorov/MINKT.lean @@ -397,7 +397,8 @@ end GapMINKT /-- **Hirahara's `GapMINKT` promise problem** ([Hirahara, Definition II.6][Hirahara2018]): the promise problem whose yes-instances are `MINKT`, and whose no-instances are -`GapMINKT.noSet σ τ`, when `s ≤ σ n s` and `t ≤ τ n t`. -/ +`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. -/ def GapMINKT (σ τ : ℕ → ℕ → ℕ) (hσ : ∀ n s, s ≤ σ n s) (hτ : ∀ n t, t ≤ τ n t) : PromiseProblem MINKT.Instance where diff --git a/Complexity/Computability/MCSP/Basic.lean b/Complexity/Computability/MCSP/Basic.lean index 44cb83b75e..338ecca9df 100644 --- a/Complexity/Computability/MCSP/Basic.lean +++ b/Complexity/Computability/MCSP/Basic.lean @@ -50,6 +50,9 @@ cslib's `computableFunctions n s`, so there are as many of them as such function * `Cslib.MCSP.mem_iff_exists_circuit`, `Cslib.MCSP.mem_iff_mem_computableFunctions`: the yes- instances of MCSP, as circuits and as computable functions. * `Cslib.MCSP.ncard_setOf_mem`: the number of yes-instances of a given arity and threshold. +* `Cslib.GapMCSP.ofFn_mem_yesSet_iff_mem_MCSP`, + `Cslib.GapMCSP.ofFn_mem_noSet_iff_notMem_MCSP`: characterization of truth tables of length `2^n` + in the yes and no sets. * `Cslib.GapMCSP.disjoint_yesSet_noSet`: the promise of `GapMCSP[s₁, s₂]` is consistent when `s₁ n ≤ s₂ n` for all `n`. @@ -223,7 +226,7 @@ if and only if its circuit complexity is strictly greater than `s₂ n`. -/ /-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `noSet s₂` if and only if `⟨n, T, s₂ n⟩ ∉ MCSP`. -/ -theorem ofFn_mem_noSet_iff_not_mem_MCSP {n : ℕ} {T : BitString (2 ^ n)} : +theorem ofFn_mem_noSet_iff_notMem_MCSP {n : ℕ} {T : BitString (2 ^ n)} : List.ofFn T ∈ noSet s₂ ↔ (⟨n, T, s₂ n⟩ : MCSP.Instance) ∉ MCSP := by rw [ofFn_mem_noSet_iff] exact not_le.symm @@ -253,7 +256,8 @@ end GapMCSP /-- **`GapMCSP[s₁, s₂]`** [OliveiraPichSanthanam2019, Definition 2.4]: the promise problem whose yes-instances are truth tables of functions with circuits of at most `s₁ n` gates and whose no-instances are truth tables of functions that need more than `s₂ n` gates, when `s₁ n ≤ s₂ n` -for all `n`. -/ +for all `n`. Following OPS19, the hypothesis `∀ n, s₁ n ≤ s₂ n` is bundled to guarantee +disjointness of the promise problem by construction. -/ def GapMCSP (s₁ s₂ : ℕ → ℕ) (h : ∀ n, s₁ n ≤ s₂ n) : Complexity.PromiseProblem (List Bool) where yes := GapMCSP.yesSet s₁ diff --git a/ComplexityTests/Kannan.lean b/ComplexityTests/Kannan.lean index 5f8c54ff64..db332ee9c5 100644 --- a/ComplexityTests/Kannan.lean +++ b/ComplexityTests/Kannan.lean @@ -37,9 +37,30 @@ example : MCSP.tableFunction 2 [false, true, true, false] ![true, false] = true example : MCSP.tableFunction 2 [false, true, true, false] ![true, true] = false := by decide example : Kannan.table 0 0 (List.replicate 10 true) = List.replicate 8 true := by decide --- GapMCSP bundles `GapMCSP.yesSet`, `GapMCSP.noSet`, and `GapMCSP.disjoint_yesSet_noSet`. -example (s : ℕ → ℕ) : - (GapMCSP s s fun _ => le_rfl).yes = GapMCSP.yesSet s := rfl +-- Words whose length is not a power of two belong to neither side of GapMCSP. +example (s : ℕ → ℕ) : [true, false, true] ∉ (GapMCSP s s fun _ => le_rfl).yes := by + rintro ⟨n, hn, -⟩ + match n with + | 0 => revert hn; decide + | 1 => revert hn; decide + | k + 2 => + have h : 3 < 2 ^ (k + 2) := + calc 3 < 2 ^ 2 := by decide + _ ≤ 2 ^ (k + 2) := Nat.pow_le_pow_right (by omega) (by omega) + revert hn + exact ne_of_lt (by simpa using h) + +example (s : ℕ → ℕ) : [true, false, true] ∉ (GapMCSP s s fun _ => le_rfl).no := by + rintro ⟨n, hn, -⟩ + match n with + | 0 => revert hn; decide + | 1 => revert hn; decide + | k + 2 => + have h : 3 < 2 ^ (k + 2) := + calc 3 < 2 ^ 2 := by decide + _ ≤ 2 ^ (k + 2) := Nat.pow_le_pow_right (by omega) (by omega) + revert hn + exact ne_of_lt (by simpa using h) example : BitString.binaryValue [true, false, true] = 5 := by decide example {u v : List Bool} (hlen : u.length = v.length) diff --git a/ComplexityTests/KarpLipton.lean b/ComplexityTests/KarpLipton.lean index dd0041cc16..1e6dc7774e 100644 --- a/ComplexityTests/KarpLipton.lean +++ b/ComplexityTests/KarpLipton.lean @@ -161,7 +161,7 @@ example : [false, true] ∈ (GapMCSP (fun _ => 0) (fun _ => 0) fun _ => le_rfl). (by decide)) example : [true, false] ∈ (GapMCSP (fun _ => 0) (fun _ => 0) fun _ => le_rfl).no := by - refine (GapMCSP.ofFn_mem_noSet_iff_not_mem_MCSP (n := 1) (T := ![true, false])).mpr ?_ + refine (GapMCSP.ofFn_mem_noSet_iff_notMem_MCSP (n := 1) (T := ![true, false])).mpr ?_ intro hx obtain ⟨_ | ⟨b, _ | _⟩, hu, hV⟩ := MCSP.exists_verifier_append hx · revert hu; decide