SamuelSchlesinger · Oct 24, 2026 · Oct 23, 2026
diff --git a/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean b/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean
@@ -34,14 +34,11 @@ is `Cslib.Complexity.mem_RP_iff_forall_decidesWithOneSidedErrorExponent`.
 ## Main definitions
 
 * `Cslib.Complexity.DecidesWithErrorExponent`: error at most `2 ^ (-q(n))`.
-* `Cslib.Complexity.repeatMajority`: the strict majority of `2 r(n)` independent runs.
 
 ## Main results
 
 * `Cslib.Complexity.DecidesWithBoundedError.repeatMajority`: `12 q(n)` majority votes reduce the
   error to `2 ^ (-q(n))`.
-* `Cslib.Complexity.computableTidilyInPolyTime_repeatMajority`: majority votes take polynomial
-  time.
 * `Cslib.Complexity.DecidesWithErrorExponent.decidesWithBoundedError`: error at most
   `2 ^ (-q(n)) ≤ 1 / 4` is bounded error.
 * `Cslib.Complexity.mem_BPP_iff_forall_decidesWithErrorExponent`: error reduction for `BPP`.

diff --git a/Complexity/Computability/Complexity/Classes/Oracle.lean b/Complexity/Computability/Complexity/Classes/Oracle.lean
@@ -36,7 +36,7 @@ machine's clock also bounds their number and length
 
 The classes relativize `P` and `NP` by this one substitution: `PWithOracle A enc` and
 `NPWithOracle A enc` are `Cslib.Complexity.P` and `Cslib.Complexity.NP` with
-`ComputableTidilyInPolyTime` replaced by `ComputableInPolyTimeWithOracle A`. Hence `NPWithOracle`
+`ComputableInPolyTime` replaced by `ComputableInPolyTimeWithOracle A`. Hence `NPWithOracle`
 uses verifiers with an oracle and certificates of exactly polynomial length.
 
 For a deterministic program and an answer function, `OracleComp.queriesWith` lists the requests

diff --git a/Complexity/Computability/Complexity/Classes/RP.lean b/Complexity/Computability/Complexity/Classes/RP.lean
@@ -41,7 +41,6 @@ Two runs reject a member with probability at most `1 / 4`, so `RP ⊆ BPP`.
 * `Cslib.Complexity.DecidesWithOneSidedError`: the one-sided error condition.
 * `Cslib.Complexity.RP`, `Cslib.Complexity.coRP`.
 * `Cslib.Complexity.DecidesWithOneSidedErrorExponent`: one-sided error at most `2 ^ (-q(n))`.
-* `Cslib.Complexity.repeatAny`: the disjunction of `q(n)` independent runs.
 
 ## Main results
 

diff --git a/Complexity/Computability/Complexity/Classes/Toda/Counting.lean b/Complexity/Computability/Complexity/Classes/Toda/Counting.lean
@@ -61,7 +61,6 @@ odd number of accepted witnesses (`Cslib.Complexity.Toda.testBit_card_filter_sha
 ## Main definitions
 
 * `Cslib.Complexity.Toda.parityCoeff`: the coefficients of the amplification.
-* `Cslib.BitString.wordLt`: the lexicographic order on words of equal length.
 * `Cslib.Complexity.Toda.countingTest`, `Cslib.Complexity.Toda.sharpTest`: the word tests of the
   counting functions.
 

diff --git a/Complexity/Computability/Complexity/Classes/ValiantVazirani.lean b/Complexity/Computability/Complexity/Classes/ValiantVazirani.lean
@@ -30,7 +30,7 @@ The randomized isolation reduction `ValiantVazirani.reduce` and its amplificatio
 ## The class form
 
 `RPWithOracle A enc` is `RP` relative to the oracle language `A`: `Cslib.Complexity.RP` with
-`ComputableTidilyInPolyTime` replaced by `Cslib.Complexity.ComputableInPolyTimeWithOracle A`, as
+`ComputableInPolyTime` replaced by `Cslib.Complexity.ComputableInPolyTimeWithOracle A`, as
 `PWithOracle` relativizes `P`. For an oracle that is a promise problem, `RPWithPromiseOracle Q encQ
 enc` asks for one algorithm that is correct against every language solving `Q`, whose answers
 outside the promise are arbitrary. Every problem in `NP` lies in `RP` relative to `PromiseUSAT`
@@ -75,8 +75,8 @@ variable {α β : Type}
 /-! ### Randomized polynomial time relative to an oracle -/
 
 /-- The problems decided with one-sided error by polynomial-time machines with oracle `A` reading
-polynomially long random strings: `Cslib.Complexity.RP` with `ComputableTidilyInPolyTime`
-replaced by `ComputableInPolyTimeWithOracle A`, as `PWithOracle` relativizes `P`. -/
+polynomially long random strings: `Cslib.Complexity.RP` with `ComputableInPolyTime` replaced by
+`ComputableInPolyTimeWithOracle A`, as `PWithOracle` relativizes `P`. -/
 def RPWithOracle (A : Set (List Bool)) (enc : α ↪ List Bool) : Set (Set α) :=
   {L | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTimeWithOracle A V (encPair enc encBits) encBool ∧

diff --git a/Complexity/Computability/Complexity/Fagin/Converse.lean b/Complexity/Computability/Complexity/Fagin/Converse.lean
@@ -65,7 +65,6 @@ sentence over `L`.
 * `Cslib.Logic.ESO.Definable.of_queryLanguage_mem_NP`: every isomorphism-closed class `K` whose
   query language is in `NP` is existential second-order definable.
 * `Cslib.Logic.ESO.definable_iff_queryLanguage_mem_NP`,
-  `Cslib.Logic.Vocabulary.definable_iff_queryLanguage_mem_NP`,
   `Cslib.Logic.ESO.definable_iff_isoClosed_and_queryLanguage_mem_NP`: **Fagin's theorem**
   (`Definable K ↔ v.queryLanguage K ∈ NP encStructure` for isomorphism-closed `K`, and
   `Definable K ↔ IsoClosed K ∧ v.queryLanguage K ∈ NP encStructure` in general).

diff --git a/Complexity/Computability/PCP/Amplification.lean b/Complexity/Computability/PCP/Amplification.lean
@@ -42,7 +42,9 @@ the round maps `Σ₀` to itself and **doubles the value up to the threshold** `
 `min (2 UNSAT(G)) γ ≤ UNSAT(G.amplify T q)` (`Cslib.PCP.Dinur.min_le_unsatVal_amplify`). This is
 Dinur's main theorem, in a non-explicit form: the expanders of preprocessing are chosen
 non-constructively (`Cslib.RotationMap.expanderFamily`), and the round is a noncomputable
-definition; its realization in polynomial time is not addressed here. The construction remains
+definition. Its polynomial-time realization, with explicit expanders and a larger killing rate, is
+`Cslib.PCP.Encoded.Graph.arithmeticAmplify`, in
+`Complexity.Computability.PCP.Encoded.Amplification.Arithmetic`. The construction remains
 asymptotic: despite the smaller answer alphabet, the size factors are triply exponential in `T`.
 
 ## Main definitions

diff --git a/Complexity/Computability/PCP/Amplifier.lean b/Complexity/Computability/PCP/Amplifier.lean
@@ -35,7 +35,9 @@ map the satisfiable constraint graphs to one without edges and the others to a s
 edge. The interest of an amplifier lies in its construction: Dinur's round
 (`Cslib.PCP.Dinur.amplifier`) transforms a constraint graph locally, and can be carried out in
 polynomial time given explicit expanders [Dinur, Theorem 4.1][Dinur2005]. This file is only about
-the consequences of the interface; running times are not formalized here.
+the consequences of the interface. Running times are formalized for the executable pipeline
+`Cslib.PCP.Encoded.gapGraph`, whose rounds are iterated in
+`Complexity.Computability.PCP.Encoded.Amplification.Iteration`.
 
 ## Main definitions
 

diff --git a/Complexity/Computability/PCP/Encoded/Composition/Enumeration.lean b/Complexity/Computability/PCP/Encoded/Composition/Enumeration.lean
@@ -22,8 +22,8 @@ not a claim of practical runtime at arbitrary fixed alphabets.
 
 ## Main definitions
 
-* `Cslib.PCP.HadamardTester.Rand.finEnum`, `Cslib.PCP.Encoded.Graph.ComposeSlot.finEnum`:
-  reusable constructive coin enumeration and slot numbering.
+* `Cslib.PCP.Encoded.Graph.ComposeSlot.finEnum`: constructive slot numbering, used with the coin
+  enumeration of `Complexity.Computability.PCP.Encoded.AssignmentTester.Enumeration`.
 * `Cslib.PCP.Encoded.Graph.composeEnumerated`: tabulated composition with complete enumerations.
 
 ## Main results

diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Residue.lean b/Complexity/Computability/TreeEval/Reader/Cert/Residue.lean
@@ -19,7 +19,8 @@ in the lengths of their encoded arguments.
 ## Main results
 
 * `Cslib.TreeEval.Reader.addMod_inSpace`, `.mulMod_inSpace`, `.negMod_inSpace`,
-  `.powMod_inSpace`, `.chi_inSpace`: the residue operations.
+  `.chi_inSpace`, `.unitInv_inSpace`: the residue operations; `unitInv p j` computes
+  `(j + 1) ^ (p - 2)` modulo `p` by repeated multiplication.
 -/
 
 @[expose] public section