From a3aeaf78146cd44e1086492caa8b7be00065144b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 07:28:25 -0400 Subject: [PATCH 1/3] =?UTF-8?q?doc(BooleanHierarchy):=20state=20that=20Kad?= =?UTF-8?q?in's=20published=20collapse=20is=20stronger=20than=20the=20?= =?UTF-8?q?=CE=A3=E2=82=83=E1=B4=BE=20form=20proved?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Kadin (SIAM J. Comput. 17(6), 1988, abstract) shows that a Boolean-hierarchy collapse gives a sparse S with coNP ⊆ NP^S and PH ⊆ P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ. Kadin.lean proves PH = Σ₃ᴾ ∩ Π₃ᴾ and called that "Kadin's theorem" without noting the weaker scope. Record the gap in the module and headline docstrings and in ROADMAP. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Classes/BooleanHierarchy/Kadin.lean | 15 +++++++++++---- ROADMAP.md | 3 +++ 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean index 81af56815c..07e2efc50d 100644 --- a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean @@ -24,6 +24,11 @@ equivalently `BH (k + 1) = BH k`), then the polynomial hierarchy collapses to it `Σ₃ᴾ ∩ Π₃ᴾ` (`PH = Σ₃ᴾ`) [Kadin][Kadin1988]. In particular, if `DP = coDP` (or `SATUNSAT ∈ coDP`), then `PH = Σ₃ᴾ`. +This is a weaker form of Kadin's result. Kadin shows that a Boolean-hierarchy collapse gives a +sparse set `S` with `coNP ⊆ NP^S`, and hence `PH ⊆ P^{NP^{NP}[O(log n)]}`, a subclass of `Δ₃ᴾ` +([Kadin][Kadin1988], abstract). Neither the sparse-set statement nor the `Δ₃ᴾ` collapse is +formalized here; the library has no class of bounded-query `Σ₂ᴾ`-oracle machines. + ## Proof overview To place a language `A ∈ Π₃ᴾ` in `Σ₃ᴾ`, peel off its first two quantifier blocks of lengths `p₁` @@ -853,8 +858,9 @@ theorem SigmaP_three_eq_PiP_three_of_coBH_subset_BH {k : ℕ} refine Set.Subset.antisymm (fun A hA => ?_) hsub simpa using compl_mem_PiP_of_mem_SigmaP (hsub (compl_mem_PiP_of_mem_SigmaP hA)) -/-- **Kadin's theorem** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, the polynomial -hierarchy collapses to `Σ₃ᴾ`. -/ +/-- **Kadin's theorem, `Σ₃ᴾ` form** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, the +polynomial hierarchy collapses to `Σ₃ᴾ`. Kadin proves the stronger collapse to +`P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`; see the module documentation. -/ theorem PH_eq_SigmaP_three_of_coBH_subset_BH {k : ℕ} (h : coBH encBits k ⊆ BH encBits k) : PH enc = SigmaP 3 enc := @@ -862,8 +868,9 @@ theorem PH_eq_SigmaP_three_of_coBH_subset_BH {k : ℕ} PiP_three_subset_SigmaP_three_of_coBH_subset_BH (coBH_subset_BH_of_coBH_encBits_subset_BH_encBits h) -/-- **Kadin's theorem** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, the polynomial -hierarchy collapses to `Σ₃ᴾ ∩ Π₃ᴾ`. -/ +/-- **Kadin's theorem, `Σ₃ᴾ ∩ Π₃ᴾ` form** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, +the polynomial hierarchy collapses to `Σ₃ᴾ ∩ Π₃ᴾ`. Kadin proves the stronger collapse to +`P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`; see the module documentation. -/ theorem PH_eq_SigmaP_three_inter_PiP_three_of_coBH_subset_BH {k : ℕ} (h : coBH encBits k ⊆ BH encBits k) : PH enc = SigmaP 3 enc ∩ PiP 3 enc := by diff --git a/ROADMAP.md b/ROADMAP.md index 6ea4c79b48..8d9197a2f1 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -196,6 +196,9 @@ index links to canonical definitions rather than keeping a second set. `O(ℓ + H log(ℓ + 2))` parameter bound. - Alternating time and space classes and bounded-alternation characterizations of PH; sharp bounds for sublinear space, distinct from polynomial-space simulation. +- **Kadin's full collapse:** a Boolean-hierarchy collapse gives a sparse `S` with `coNP ⊆ NP^S` + and `PH ⊆ P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`. `BooleanHierarchy/Kadin.lean` proves only + `PH = Σ₃ᴾ ∩ Π₃ᴾ`. ### Reducibilities and the structure of complete sets From 2644addea5420f78938fc342f7e08da1455bfbc8 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 09:44:40 -0400 Subject: [PATCH 2/3] doc(references): add Kadin's erratum and sources on the deeper BH collapse Add Kadin1991 (SIAM J. Comput. 20(2):404), ChangKadin1996, Yap1983 and the Hemaspaandra-Hemaspaandra-Hempel easy-hard survey (arXiv cs/9910002). The bibliographic data was checked against Crossref and arXiv. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- references.bib | 47 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/references.bib b/references.bib index 1b676dfaec..2609a96751 100644 --- a/references.bib +++ b/references.bib @@ -1051,6 +1051,17 @@ @article{ChandraStockmeyerVishkin1984 doi = {10.1137/0213028} } +@article{ChangKadin1996, + author = {Chang, Richard and Kadin, Jim}, + title = {The {Boolean} Hierarchy and the Polynomial Hierarchy: A Closer Connection}, + journal = {SIAM Journal on Computing}, + volume = {25}, + number = {2}, + pages = {340--354}, + year = {1996}, + doi = {10.1137/S0097539790178069} +} + @inproceedings{ChanHe2020, author = {Chan, Timothy M. and He, Qizheng}, title = {Reducing {3SUM} to {Convolution-3SUM}}, @@ -2337,6 +2348,20 @@ @inproceedings{HemaspaandraEtAl2018 doi = {10.4230/LIPIcs.MFCS.2018.51} } +@misc{HemaspaandraHemaspaandraHempel1999, + author = {Hemaspaandra, Edith and Hemaspaandra, Lane A. and Hempel, Harald}, + title = {What's Up with Downward Collapse: Using the Easy-Hard Technique to Link + {Boolean} and Polynomial Hierarchy Collapses}, + year = {1999}, + eprint = {cs/9910002}, + archivePrefix = {arXiv}, + primaryClass = {cs.CC}, + doi = {10.48550/arXiv.cs/9910002}, + url = {https://arxiv.org/abs/cs/9910002v1}, + note = {Technical Report UR-CS-TR-98-682, University of Rochester, 1998; extended + abstract in SIGACT News 29, 10--22, 1998} +} + @article{ Hennessy1985, author = {Matthew Hennessy and Robin Milner}, @@ -2737,6 +2762,17 @@ @article{Kadin1988 doi = {10.1137/0217080} } +@article{Kadin1991, + author = {Kadin, Jim}, + title = {Erratum: The Polynomial Time Hierarchy Collapses if the {Boolean} Hierarchy Collapses}, + journal = {SIAM Journal on Computing}, + volume = {20}, + number = {2}, + pages = {404}, + year = {1991}, + doi = {10.1137/0220025} +} + @article{Kahale1995, author = {Kahale, Nabil}, title = {Eigenvalues and Expansion of Regular Graphs}, @@ -5225,6 +5261,17 @@ @inproceedings{Yao1982 doi = {10.1109/SFCS.1982.45} } +@article{Yap1983, + author = {Yap, Chee K.}, + title = {Some Consequences of Non-Uniform Conditions on Uniform Classes}, + journal = {Theoretical Computer Science}, + volume = {26}, + number = {3}, + pages = {287--300}, + year = {1983}, + doi = {10.1016/0304-3975(83)90020-8} +} + @misc{Zhao2023, author = {Zhao, Yufei}, title = {Probabilistic Methods in Combinatorics}, From 9e902288c09ca226ffb94eee701337eed0735d1e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 09:44:40 -0400 Subject: [PATCH 3/3] doc(BooleanHierarchy): separate Kadin's corrected result from the deeper collapse MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Kadin's 1988 argument gives a sparse S with coNP ⊆ NP^S and, through Yap, PH ⊆ Σ₃ᴾ. The abstract's further claim PH ⊆ P^{NP^NP[O(log n)]} relied on an erroneous proof that S ∈ NP^NP, as recorded in his 1991 erratum and by Chang and Kadin. That deeper collapse holds by results of Wagner and of Chang and Kadin. Revise the module paragraph, the two headline docstrings and the ROADMAP bullet accordingly. No Lean statement changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Classes/BooleanHierarchy/Kadin.lean | 34 +++++++++++++------ ROADMAP.md | 7 ++-- 2 files changed, 28 insertions(+), 13 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean index 07e2efc50d..cc66943187 100644 --- a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean @@ -24,10 +24,17 @@ equivalently `BH (k + 1) = BH k`), then the polynomial hierarchy collapses to it `Σ₃ᴾ ∩ Π₃ᴾ` (`PH = Σ₃ᴾ`) [Kadin][Kadin1988]. In particular, if `DP = coDP` (or `SATUNSAT ∈ coDP`), then `PH = Σ₃ᴾ`. -This is a weaker form of Kadin's result. Kadin shows that a Boolean-hierarchy collapse gives a -sparse set `S` with `coNP ⊆ NP^S`, and hence `PH ⊆ P^{NP^{NP}[O(log n)]}`, a subclass of `Δ₃ᴾ` -([Kadin][Kadin1988], abstract). Neither the sparse-set statement nor the `Δ₃ᴾ` collapse is -formalized here; the library has no class of bounded-query `Σ₂ᴾ`-oracle machines. +Kadin's argument shows that a Boolean-hierarchy collapse gives a sparse set `S` with +`coNP ⊆ NP^S`, from which Yap's theorem [Yap][Yap1983] gives `PH ⊆ Σ₃ᴾ` [Kadin][Kadin1988]. The +1988 abstract also claims the stronger collapse `PH ⊆ P^{NP^{NP}[O(log n)]}`, a subclass of +`Δ₃ᴾ`, but that derivation rests on a proof that `S ∈ NP^{NP}` which contains an error, as +recorded in Kadin's erratum [Kadin][Kadin1991] and by [Chang and Kadin][ChangKadin1996]. The +stronger collapse holds by other arguments (survey: [Hemaspaandra, Hemaspaandra and +Hempel][HemaspaandraHemaspaandraHempel1999], Section 3). Wagner showed that `PH` then collapses +to the Boolean closure of `Σ₂ᴾ`, and Chang and Kadin to level `k` of the Boolean hierarchy over +`Σ₂ᴾ` [ChangKadin1996]; both classes lie in `P^{NP^{NP}[O(log n)]}`. Neither the sparse-set +statement nor these deeper collapses are formalized here; the library has no class of +bounded-query `Σ₂ᴾ`-oracle machines. ## Proof overview @@ -79,6 +86,13 @@ these `k` hard-prefix branches places `A` in `Σ₃ᴾ`. * [J. Kadin, *The Polynomial Time Hierarchy Collapses if the Boolean Hierarchy Collapses*][Kadin1988] +* [J. Kadin, *Erratum: The Polynomial Time Hierarchy Collapses if the Boolean Hierarchy + Collapses*][Kadin1991] +* [R. Chang and J. Kadin, *The Boolean Hierarchy and the Polynomial Hierarchy: A Closer + Connection*][ChangKadin1996] +* [E. Hemaspaandra, L. A. Hemaspaandra and H. Hempel, *What's Up with Downward Collapse: Using + the Easy-Hard Technique to Link Boolean and Polynomial Hierarchy + Collapses*][HemaspaandraHemaspaandraHempel1999] * [J.-Y. Cai et al., *The Boolean Hierarchy I: Structural Properties*][CaiEtAl1988] -/ @@ -858,9 +872,9 @@ theorem SigmaP_three_eq_PiP_three_of_coBH_subset_BH {k : ℕ} refine Set.Subset.antisymm (fun A hA => ?_) hsub simpa using compl_mem_PiP_of_mem_SigmaP (hsub (compl_mem_PiP_of_mem_SigmaP hA)) -/-- **Kadin's theorem, `Σ₃ᴾ` form** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, the -polynomial hierarchy collapses to `Σ₃ᴾ`. Kadin proves the stronger collapse to -`P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`; see the module documentation. -/ +/-- **Kadin's theorem** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, the polynomial +hierarchy collapses to `Σ₃ᴾ`. The deeper collapse into `P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`, due to later +work, is not formalized; see the module documentation. -/ theorem PH_eq_SigmaP_three_of_coBH_subset_BH {k : ℕ} (h : coBH encBits k ⊆ BH encBits k) : PH enc = SigmaP 3 enc := @@ -868,9 +882,9 @@ theorem PH_eq_SigmaP_three_of_coBH_subset_BH {k : ℕ} PiP_three_subset_SigmaP_three_of_coBH_subset_BH (coBH_subset_BH_of_coBH_encBits_subset_BH_encBits h) -/-- **Kadin's theorem, `Σ₃ᴾ ∩ Π₃ᴾ` form** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, -the polynomial hierarchy collapses to `Σ₃ᴾ ∩ Π₃ᴾ`. Kadin proves the stronger collapse to -`P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`; see the module documentation. -/ +/-- **Kadin's theorem** [Kadin][Kadin1988]: if `coBH encBits k ⊆ BH encBits k`, the polynomial +hierarchy collapses to `Σ₃ᴾ ∩ Π₃ᴾ`. The deeper collapse into `P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`, due to +later work, is not formalized; see the module documentation. -/ theorem PH_eq_SigmaP_three_inter_PiP_three_of_coBH_subset_BH {k : ℕ} (h : coBH encBits k ⊆ BH encBits k) : PH enc = SigmaP 3 enc ∩ PiP 3 enc := by diff --git a/ROADMAP.md b/ROADMAP.md index 8d9197a2f1..e73995aa23 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -196,9 +196,10 @@ index links to canonical definitions rather than keeping a second set. `O(ℓ + H log(ℓ + 2))` parameter bound. - Alternating time and space classes and bounded-alternation characterizations of PH; sharp bounds for sublinear space, distinct from polynomial-space simulation. -- **Kadin's full collapse:** a Boolean-hierarchy collapse gives a sparse `S` with `coNP ⊆ NP^S` - and `PH ⊆ P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`. `BooleanHierarchy/Kadin.lean` proves only - `PH = Σ₃ᴾ ∩ Π₃ᴾ`. +- **Deeper consequences of a Boolean-hierarchy collapse:** Kadin's sparse `S` with + `coNP ⊆ NP^S`, and the collapse of `PH` into `P^{NP^{NP}[O(log n)]} ⊆ Δ₃ᴾ`, which follows from + results of Wagner and of Chang and Kadin, not from Kadin's 1988 argument (see his erratum). + `BooleanHierarchy/Kadin.lean` proves only `PH = Σ₃ᴾ ∩ Π₃ᴾ`. ### Reducibilities and the structure of complete sets