Supporting material for Edgar Dobriban, The Benjamini–Hochberg Procedure Can Fail to Control the
FDR for Correlated Two-Sided Gaussian Tests (July 2026; arXiv:2607.12208). The paper constructs a
correlated two-sided Gaussian factor model for which, at level α = 0.01, the false discovery rate
is provably above 0.0104 for all sufficiently large numbers of hypotheses — disproving a
conjecture believed for two decades.
This repository holds three 8000 independent pieces of evidence for that claim:
- A rigorous interval-arithmetic certificate (
bh_two_sided_gaussian_counterexample_*.py), an outward-rounded Arb computation provingliminf FDR > 0.010416829070473713… > 0.01for the stated factor-model sequence. - A seeded stratified Monte Carlo experiment applying ordinary BH directly at
N = 50, 100, 200, consistent with the theoretical result. - A complete Lean 4 formalization in
BHFormalization/— an independent, kernel-checked re-derivation of the paper's main theorem,∀ᶠ N, 0.0104 < gaussianBHFDR N, resting only on Mathlib's three standard axioms. Start withBHFormalization/README.md, or the pairedChallenge.lean(the statement) andFinal.lean(the proof).
The theorem relies on neither the Monte Carlo experiment nor the Lean layer — the certificate is
self-sufficient. Layer 3, the Lean formalization in BHFormalization/, is the
original contribution of this repository and the only part covered by this repo's license and
verification claims. Layers 1–2 (every Python script, reproducibility_manifest.json, and the
CSV JSON/ data at the repository root) are the author's reproducibility bundle, reproduced from
dobriban/BH and included only for convenience.
Note on the Python bundle. These upstream files are not maintained here and are not part of this repository's reproducibility guarantees. In particular,
verify_reproducibility.pyandreproducibility_manifest.jsonreference manuscript and experiment artifacts (e.g.main.tex, pooled result files) that live in the upstream repository, so the root verifier is not expected to pass from a clone of this repo. For the authoritative Python bundle and manuscript, use dobriban/BH. The section below is retained verbatim from upstream and documents that bundle in its original context.
Python reproducibility bundle (upstream — see dobriban/BH)
- Python 3.12.3 (also recorded in
.python-version) - NumPy 1.26.4
- SciPy 1.14.1
- python-flint 0.8.0
- latexmk 4.87 with pdfTeX 3.141592653-2.6-1.40.27 (MiKTeX 25.4)
Create a clean environment and install the exact direct dependencies:
py -3.12 -m venv .venv
.\.venv\Scripts\python.exe -m pip install --upgrade pip
.\.venv\Scripts\python.exe -m pip install -r requirements.txtOn POSIX systems, activate .venv/bin/python instead. The canonical artifact
files intentionally omit elapsed time because timing is not reproducible.
This checks the environment lock, every SHA-256 manifest entry, all seven experiment chunks, all 300 macro-replications, the pooled results, the generated LaTeX values, the embedded certificate source, and a fresh Arb certificate run:
python verify_reproducibility.py --jobs 4Use --skip-certificate-rerun only for a quicker structural check.
The cross-platform Python runner is the run-plan authority. It regenerates all
seven chunks, recombines them, reruns the Arb certificate, rebuilds main.pdf,
refreshes reproducibility_manifest.json, and finally runs the read-only
verifier:
python run_published_fdr_experiment.py --certificate-jobs 4Thin wrappers are also supplied:
.\run_published_fdr_experiment.ps1 -CertificateJobs 4./run_published_fdr_experiment.sh --certificate-jobs 4The experiment is intentionally substantial: it generates and sorts complete Gaussian vectors for 300 macro-replications, each containing 1,000 strata.
published_fdr_plan.json is the single machine-readable plan. It fixes the
model, stratification, batching policy, RNG, seed construction, environment,
and these independent chunks:
| Prefix | N | Macro-replications | Master seed |
|---|---|---|---|
fdr_N50 |
50 | 100 | 20260711 |
fdr_N100_a |
100 | 50 | 20260712 |
fdr_N100_b |
100 | 50 | 20260713 |
fdr_N200_a |
200 | 25 | 20260720 |
fdr_N200_b |
200 | 25 | 20260721 |
fdr_N200_c |
200 | 25 | 20260722 |
fdr_N200_d |
200 | 25 | 20260723 |
Each command uses SeedSequence(master_seed).spawn(1)[0]; the child spawn key
is recorded and validated. The target_entries=1,500,000 batching policy is
also fixed because changing batching changes how a deterministic RNG stream is
assigned to simulated coordinates.
Every chunk retains:
PREFIX.json: validated configuration, provenance, and scientific summary;PREFIX.csv: the same one-row summary in CSV form;PREFIX_macro.csv: every macro-level FDP estimate, mean rejection count, and rejection probability.
The pooled canonical outputs are:
fdr_experiment_results.jsonfdr_experiment_results.csvfdr_experiment_macro_estimates.csvfdr_experiment_results.tex(generated values consumed bymain.tex)
The strict combiner can be run independently after the chunk files exist:
python combine_fdr_experiment_results.pyIt validates all source files before atomically overwriting any pooled output.
| N | m | FDR estimate | MCSE | t-based 95% MC interval | One-sided p-value vs. 0.01 |
|---|---|---|---|---|---|
| 50 | 5,000 | 0.00993617 | 0.00011333 | [0.00971129, 0.01016104] | 0.7127 |
| 100 | 10,000 | 0.01012922 | 0.00009590 | [0.00993893, 0.01031951] | 0.09046 |
| 200 | 20,000 | 0.01035891 | 0.00010270 | [0.01015514, 0.01056269] | 0.0003555 |
These Student-t quantities are conventional Monte Carlo summaries. They quantify simulation error and are not the rigorous disproof.
Rerun only the certificate and replace its canonical output with:
python bh_two_sided_gaussian_counterexample_parallel_verify.py `
--jobs 4 `
--output bh_two_sided_gaussian_counterexample_certificate_output.txtreproducibility_manifest.json hashes all authoritative source files, all 21
chunk files, the pooled outputs, the certificate output.
The Lean formalization in BHFormalization/ — the original contribution of this
repository — is released under the Apache License 2.0; see NOTICE for scope
and CITATION.cff for citation metadata. The Python reproducibility bundle above is
reproduced from dobriban/BH and remains subject to that project's
terms.