From 773e92220d628f5ff63e4b0e1e5eb76b27ffa521 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 19:35:15 -0400 Subject: [PATCH] doc(classes): fix stale module docs in the classes area - `PCP/Amplification` and `PCP/Amplifier` said the polynomial-time realization of Dinur's round was "not addressed". They now point to the executable pipeline (`Encoded.Graph.arithmeticAmplify`, `Encoded.gapGraph`). #623 makes the same correction in `PCP/GapTheorem`. - `ValiantVazirani.lean` and `Oracle.lean` still described `RP`, `P` and `NP` as defined with `ComputableTidilyInPolyTime`; they are plain since #559. - `Fagin/Converse.lean` listed the dot-notation alias `Vocabulary.definable_iff_queryLanguage_mem_NP` as a main result beside the theorem it repeats, and `TreeEval/Reader/Cert/Residue.lean` listed a nonexistent `powMod_inSpace`; the latter now names `unitInv_inSpace`, which computes `(j + 1) ^ (p - 2)` modulo `p`. - Main lists no longer present declarations of other modules as their own (`repeatMajority`, `repeatAny`, `BitString.wordLt`, `HadamardTester.Rand.finEnum`). Refs #610 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Computability/Complexity/Classes/BPP/Amplification.lean | 3 --- Complexity/Computability/Complexity/Classes/Oracle.lean | 2 +- Complexity/Computability/Complexity/Classes/RP.lean | 1 - .../Computability/Complexity/Classes/Toda/Counting.lean | 1 - .../Computability/Complexity/Classes/ValiantVazirani.lean | 6 +++--- Complexity/Computability/Complexity/Fagin/Converse.lean | 1 - Complexity/Computability/PCP/Amplification.lean | 4 +++- Complexity/Computability/PCP/Amplifier.lean | 4 +++- .../Computability/PCP/Encoded/Composition/Enumeration.lean | 4 ++-- Complexity/Computability/TreeEval/Reader/Cert/Residue.lean | 3 ++- 10 files changed, 14 insertions(+), 15 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean b/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean index 73f00caf98..da8d86ff34 100644 --- 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 index b7d8e1d978..838a72216c 100644 --- 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 index 75499fd0d3..d80de9b785 100644 --- 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 index db04336cd0..1c410645de 100644 --- 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 index 117a47f1e7..3c78d65027 100644 --- 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 index fc85926b40..88daa31a35 100644 --- 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 index 20f595d909..5d6e8d27a0 100644 --- 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 index 2d392aa835..a45ee5b727 100644 --- 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 index 92ff92f998..297bc0c275 100644 --- 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 index ae6d6b1f47..a85c048a3c 100644 --- 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