diff --git a/Complexity/Computability/Complexity/AverageCase.lean b/Complexity/Computability/Complexity/AverageCase.lean index 913631fb80..c069bfaa35 100644 --- a/Complexity/Computability/Complexity/AverageCase.lean +++ b/Complexity/Computability/Complexity/AverageCase.lean @@ -61,6 +61,8 @@ theorem, lemma, and page locators follow the full version `arXiv:2009.11514v1` ( * `Cslib.Complexity.MildlyHardOnAverageToOneSidedApprox.mildlyHardOnAverageToApprox`: shift + gap-scaling bridge converting one-sided $(2 g)$-approximation hardness into symmetric $g$-approximation hardness whenever `fun x => g x.length` is computable in polynomial time. +* `Cslib.Complexity.MildlyHardOnAverageToOneSidedApproxDet.mildlyHardOnAverageToApproxDet`: the + same bridge for deterministic approximation. * `Cslib.Complexity.MildlyHardOnAverageToApprox.eventually_real_abs_sub_le`: upper-rounded integer log window `d * (Nat.log 2 n + 1)` implies the real-valued symmetric window $|(v : \mathbb{R}) - f(x)| \le d \log_2 |x|$ of Definition 2.5. diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Collapse.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Collapse.lean index b8fa4e83ce..49d05e6de7 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Collapse.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Collapse.lean @@ -37,6 +37,7 @@ The proof: ## Main results * `Cslib.Complexity.SigmaP_two_subset_AM_of_coNP_subset_AM`: `coNP ⊆ AM` gives `Σ₂ ⊆ AM`. +* `Cslib.Complexity.PiP_two_subset_SigmaP_two_of_coNP_subset_AM`: `coNP ⊆ AM` gives `Π₂ ⊆ Σ₂`. * `Cslib.Complexity.PH_eq_SigmaP_two_of_coNP_subset_AM`: **Boppana–Håstad–Zachos**. * `Cslib.Complexity.SigmaP_two_eq_AM_of_coNP_subset_AM`, `Cslib.Complexity.PiP_two_eq_SigmaP_two_of_coNP_subset_AM`: `Σ₂ = Π₂ = AM`. diff --git a/Complexity/Computability/Complexity/Classes/DP.lean b/Complexity/Computability/Complexity/Classes/DP.lean index 5804b11c13..6869bcbfbc 100644 --- a/Complexity/Computability/Complexity/Classes/DP.lean +++ b/Complexity/Computability/Complexity/Classes/DP.lean @@ -33,6 +33,7 @@ union and reduction closure are immediate duals of the DP results. ## Main results * `Cslib.Complexity.mem_DP_iff_diff`: differences of NP languages. +* `Cslib.Complexity.mem_coDP_iff_union`: coDP consists of unions of an NP and a coNP language. * `Cslib.Complexity.inter_mem_DP`, `Cslib.Complexity.PolyTimeReducible.mem_DP`. * `Cslib.Complexity.NPComplete.dpComplete_prod`: the product of any NP-complete language and any coNP-complete language is DP-complete. diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean index 779da1817d..9664834000 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean @@ -65,6 +65,8 @@ logarithmic overhead and is not claimed here. ## Main results +* `Cslib.Complexity.computableInO_timeDiagonal`: the clocked diagonal is computable within the + time of the universal machine. * `Cslib.Complexity.setOf_timeDiagonal_mem_DTIME`, `Cslib.Complexity.setOf_timeDiagonal_notMem_DTIME`: the clocked diagonal is decidable within the time of the universal machine, and not within time `O(f)` for clocks beyond every `O(f)`. diff --git a/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean b/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean index 3b0d3e77bc..3d68320a26 100644 --- a/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean +++ b/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean @@ -84,6 +84,9 @@ and the arithmetization of `NEXP` verification tableaux) is not formalized here ## Main results +* `Cslib.Complexity.MIP.exists_checkCert_of_detProver`, + `Cslib.Complexity.MIP.exists_detProver_of_checkCert`: completeness and soundness of `checkCert` + against families of deterministic provers. * `Cslib.Complexity.MIP_subset_NEXP`: `MIP ⊆ NEXP`. * `Cslib.Complexity.MIP₂_subset_NEXP`: `MIP₂ ⊆ NEXP`. @@ -783,9 +786,10 @@ theorem exists_detProver_of_checkCert {c d : ℕ} {x : List Bool} {cert : Cert} Finset.sum_le_univ_sum_of_nonneg fun _ => zero_le omit [Finite Control] in -/-- Upper bound on the encoded length of the canonical certificate built from -`D : Fin p → DetProver` for `M` on `x` with `t` coins: -`(encCert cert).length ≤ 32 * (p + x.length + t + 1) ^ 2 * 2 ^ t`. -/ +/-- **Completeness of `checkCert`**: if a family `D : Fin p → DetProver` of deterministic provers +makes `M` accept `x` on more than half of the `t = c * (x.length + 1) ^ d` coin strings, then +the canonical certificate built from `D` passes `checkCert`, and its encoded length is at most +`32 * (p + x.length + t + 1) ^ 2 * 2 ^ t`. -/ theorem exists_checkCert_of_detProver {c d : ℕ} (x : List Bool) (D : Fin p → DetProver) (hlt : 2 ^ (c * (x.length + 1) ^ d) < 2 * ((Finset.univ : Finset (Fin (c * (x.length + 1) ^ d) → Bool)).filter fun f => diff --git a/Complexity/Computability/Complexity/Classes/PCP/NP.lean b/Complexity/Computability/Complexity/Classes/PCP/NP.lean index 657220dfa1..2d5a76f00d 100644 --- a/Complexity/Computability/Complexity/Classes/PCP/NP.lean +++ b/Complexity/Computability/Complexity/Classes/PCP/NP.lean @@ -31,6 +31,8 @@ in the soundness argument, never by the polynomial-time verifier. ## Main results +* `PCPVerifier.isPolyTime_queryTable`: the complete address table is computable in polynomial + time under the logarithmic coin bound. * `PCPVerifier.isPolyTime_tableVerifier`: uniform efficiency, including malformed tables. * `PCPVerifier.tableVerifier_complete`, `PCPVerifier.tableVerifier_sound`: exact proof transfer. * `Cslib.Complexity.PCP_log_subset_NP`: logarithmic-randomness PCP is contained in NP. diff --git a/Complexity/Computability/Complexity/Classes/UP.lean b/Complexity/Computability/Complexity/Classes/UP.lean index d417ec59e2..fe37522778 100644 --- a/Complexity/Computability/Complexity/Classes/UP.lean +++ b/Complexity/Computability/Complexity/Classes/UP.lean @@ -30,7 +30,7 @@ elementary consequences of the corresponding UP results and complement closure o * `Cslib.Complexity.mem_UP`: the at-most-one-witness characterization. * `Cslib.Complexity.P_subset_UP`, `Cslib.Complexity.UP_subset_NP`, - `Cslib.Complexity.UP_subset_ParityP`. + `Cslib.Complexity.UP_subset_ParityP`, `Cslib.Complexity.coUP_subset_coNP`. * `Cslib.Complexity.PolyTimeReducible.mem_UP`: closure under polynomial-time reductions. ## References diff --git a/Complexity/Computability/Complexity/Fagin/Ordered.lean b/Complexity/Computability/Complexity/Fagin/Ordered.lean index 38caac2146..0949cd6b74 100644 --- a/Complexity/Computability/Complexity/Fagin/Ordered.lean +++ b/Complexity/Computability/Complexity/Fagin/Ordered.lean @@ -29,6 +29,8 @@ Consequently input relations need not be invariant under permutations of the uni * `Cslib.Logic.FO.Ordered.ESODefinable.of_queryLanguage_mem_NP`: every ordered query whose source-only encoding language is in NP is ESO-definable, without assuming invariance under permutations of the input relations. +* `Cslib.Logic.FO.Ordered.ESODefinable.of_powerLanguage`: the ordered version of the Fagin + power-structure bridge. ## References diff --git a/Complexity/Computability/Complexity/FineGrained/Sparsification.lean b/Complexity/Computability/Complexity/FineGrained/Sparsification.lean index 84a7d9b714..b547508812 100644 --- a/Complexity/Computability/Complexity/FineGrained/Sparsification.lean +++ b/Complexity/Computability/Complexity/FineGrained/Sparsification.lean @@ -55,6 +55,7 @@ runs a fixed number `2 ^ (n / M + 2)` of rounds, the last ones on the empty stac ## Main results * `Cslib.Complexity.Sparsify.search_eq_true_iff`: the search decides satisfiability. +* `Cslib.Complexity.Sparsify.decidableInExpTime_search`: the time of the search. * `Cslib.Complexity.exists_decidableInExpTime_numVars_of_length`: from clauses to variables. * `Cslib.Complexity.DecidableInSubexpTime.numVars_of_length`: subexponential time in the number of clauses gives subexponential time in the number of variables. diff --git a/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue/Completeness.lean b/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue/Completeness.lean index 92e1b57fb6..bd13cca934 100644 --- a/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue/Completeness.lean +++ b/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue/Completeness.lean @@ -42,6 +42,8 @@ its decider rather than by translating the given circuit directly. * `Cslib.Complexity.MonotoneCircuitValue.computableInLogSpace_dualTableauInstance`: the instances are computable in logarithmic space. +* `Cslib.Complexity.MonotoneCircuitValue.logSpaceReducible_of_mem_P`: every problem in `P` + reduces to monotone circuit value in logarithmic space. * `Cslib.Complexity.MonotoneCircuitValue.logSpaceHard`, `Cslib.Complexity.MonotoneCircuitValue.logSpaceComplete`: the monotone circuit value problem is `P`-hard and `P`-complete under logarithmic-space reductions. @@ -176,7 +178,7 @@ private theorem flatten_replicate_two_mul_add_one {β : Type*} (a : List β) (n simp only [List.append_assoc] /-- **The encoded dual-rail instance** is the word written by the writer. -/ -theorem encMonotoneCircuitValue_dualTableauInstance (w : List Bool) : +private theorem encMonotoneCircuitValue_dualTableauInstance (w : List Bool) : encMonotoneCircuitValue (dualTableauInstance tm C d w) = (dualSpec tm C d).output w := by rw [encMonotoneCircuitValue_apply, encCircuitValue_apply] simp only [toDeMorgan, dualTableauInstance, Circuit.code_mapOp, Monotone.code_dualRail,