SamuelSchlesinger · Oct 25, 2026 · Oct 25, 2026 · Oct 25, 2026
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,