diff --git a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean
index 81af56815c..cc66943187 100644
--- a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean
+++ b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean
@@ -24,6 +24,18 @@ 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 = Σ₃ᴾ`.
 
+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
 
 To place a language `A ∈ Π₃ᴾ` in `Σ₃ᴾ`, peel off its first two quantifier blocks of lengths `p₁`
@@ -74,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]
 -/
 
@@ -854,7 +873,8 @@ theorem SigmaP_three_eq_PiP_three_of_coBH_subset_BH {k : ℕ}
   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 `Σ₃ᴾ`. -/
+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 :=
@@ -863,7 +883,8 @@ theorem PH_eq_SigmaP_three_of_coBH_subset_BH {k : ℕ}
       (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 `Σ₃ᴾ ∩ Π₃ᴾ`. -/
+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 6ea4c79b48..e73995aa23 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -196,6 +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.
+- **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
 
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},