This repository contains a companion Lean 4 formalization of the Gaussian stochastic-domination theorem and its application to the Weak Simplex Conjecture in Stochastic Domination of Gaussian Maxima: A Resolution of the Weak Simplex Conjecture by Abhijeet Mulgund. The development also certifies strictness and the equality cases needed for uniqueness of the regular-simplex Gram matrix. It uses mathlib and is pinned to Lean 4.31.0.
For R be an m × m correlation matrix satisfying
If
or equivalently, for every
The comparison is for equal-threshold lower orthants; it does not assert an analogous inequality for arbitrary threshold vectors.
The Lean development proves a pointwise rigidity statement stronger than equality in distribution: when R ≠ I, the lower-orthant inequality is strict at every finite threshold, and equality at any one finite threshold holds if and only if R = I. It also proves the corresponding strict upper-tail comparison for the coordinate maximum. Consequently, every positive exponential moment of that maximum is strictly smaller away from independence.
| Result | Lean declaration | Source |
|---|---|---|
| Theorem 2.1, lowe 7440 r-orthant and stochastic-order forms | lowerOrthant_ge_iid, coordinateMax_tail_le_iid |
Orthant/Singular.lean, Maxima/StochasticOrder.lean |
| Strict lower-orthant, strict maximum-tail, and equality characterization | lowerOrthant_gt_iid_of_ne_one, coordinateMax_tail_lt_iid_of_ne_one, lowerOrthant_eq_iid_iff |
Orthant/Strict.lean, Maxima/StrictStochasticOrder.lean |
Strict Gaussian-maximum MGF comparison and equality characterization for mu > 0 |
gaussianMax_mgf_lt_regularSimplex, gaussianMax_mgf_eq_regularSimplex_iff |
Maxima/StrictExponentialMoments.lean |
| Corollary 2.3, Gaussian-maximum MGF comparison | gramGaussianMax_mgf_le_regularSimplex |
Coding/RegularSimplex.lean |
Strict Gram-level MGF comparison and equality characterization for lam > 0 |
gramGaussianMax_mgf_lt_regularSimplex, gramGaussianMax_mgf_eq_regularSimplex_iff |
Coding/RegularSimplex.lean |
| Corollary 2.4, Weak Simplex Conjecture | weak_simplex, weak_simplex_of_scoreMaximizingDecoders |
Coding/WeakSimplex.lean |
Operational strictness and equality characterization for lam > 0 |
weak_simplex_strict, weak_simplex_eq_iff_codeGram_eq, weak_simplex_strict_of_scoreMaximizingDecoders, weak_simplex_eq_iff_codeGram_eq_of_scoreMaximizingDecoders |
Coding/WeakSimplex.lean |
The final coding theorems cover arbitrary measurable pointwise score-maximizing tie-breaking rules. The more general identity decoderSuccessOf_eq_bayesValue shows that every measurable likelihood-maximizing decoder has the same success probability, without assuming distinct codewords or null tie sets. The non-strict comparison permits zero signal strength. Strictness and uniqueness require lam > 0; uniqueness is false at lam = 0 because every codebook has the same value there.
A regular simplex is supplied to the final theorem through the exact Gram-matrix condition codeGram simplex = regularSimplexGram (n + 1). At positive signal strength, equality in Bayes/ML success is equivalent to codeGram code = regularSimplexGram (n + 1), both for the deterministic tie-safe ML decoder and for arbitrary measurable score-maximizing decoders. This is uniqueness at the Gram-matrix level. A separate theorem identifying equal-Gram realizations up to orthogonal congruence is optional and is not part of the certified core result; the repository also does not separately construct a coordinate realization of the regular-simplex Gram matrix.
The operational declarations are phrased in terms of correct-decoding probability. Since block error rate is one minus correct-decoding probability, weak_simplex_strict and weak_simplex_eq_iff_codeGram_eq equivalently certify that, for lam > 0, the regular-simplex Gram matrix is the unique BLER minimizer among the equal-energy codes in scope. BLER complementation is not duplicated as a separate Lean declaration.
For the Simplex Mean Width Conjecture, the strict stochastic-order theorem supplies the decisive rigidity input used by the current paper: a non-simplex normalized covariance has a strictly smaller expected maximum. The repository does not yet formalize that expectation corollary or the subsequent variance-completion, support-function, and Euclidean-congruence reductions. Thus the Lean proof supports the paper's mean-width uniqueness deduction, but the complete geometric corollary is not an end-to-end Lean theorem here.
The formalization includes the proof chain for the equal-threshold stochastic comparison, its strict and equality cases, its Gaussian-maximum MGF consequences, the Bayes/maximum-likelihood identity, and the Weak Simplex Conjecture with Gram-level uniqueness. It includes adaptive tilting, the centered log-concave product inequality needed by the proof, positive-definite and singular covariance arguments, and measurable treatment of decoder ties.
The paper's general monotone-function corollary, variance-completion lemma, Simplex Mean Width corollary, and unrestricted finite-energy AWGN formula are not formalized here as standalone Lean theorems. The general centered product inequality remains restricted to positive-definite covariance. The uniqueness branch makes exactly two narrow departures from handling singular covariance only at the outer lower-orthant theorem: centered_product_of_continuous supplies a non-strict singular limit for continuous factors after the strict sum-difference step, yielding a strict theorem only for the specialized adaptive centered half-lines; and exists_adaptiveWitnesses_of_weakSimplexCov constructs singular adaptive witnesses as compact limits of positive-definite witnesses. These results do not constitute a generic singular centered-product strictness or equality theory.
Install Lean using the official instructions, then clone the repository:
git clone https://github.com/abhmul/weak-simplex-conjecture-lean.git
cd weak-simplex-conjecture-leanThe repository pins Lean and all Lake dependencies. Downloading the mathlib cache is optional but substantially reduces build time:
lake exe cache get
lake build --wfailThe project-owned production source builds without sorry, admit, project-defined axioms, unsafe declarations, or native_decide. The permanent audit file prints the transitive axioms of the public results:
python3 scripts/check_axiom_audit.pyEvery audited declaration uses exactly Lean's standard propext, Classical.choice, and Quot.sound axioms. Continuous integration also builds the public root, checks the production import graph, runs the trusted-source scanner, and verifies the provenance ledger.
Deterministic floating-point sanity checks for the strict and equality cases are available separately:
python3 scripts/check_uniqueness_sanity.pyThese diagnostics are not proof dependencies and are outside the trusted Lean development.
WeakSimplexConjectureLean/contains the formalization. The principal proof branches are underTilt/,Product/,Orthant/,Maxima/, andCoding/.WeakSimplexConjectureLean.leanis the public umbrella import.WeakSimplexConjectureLean/Audit/Axioms.leanis the permanent axiom audit.WeakSimplexConjectureLean/Vendor/contains the minimal vendored StatLean source used by the proof;PROVENANCE.mdrecords exact revisions, changes, licenses, and audit results.Scratch/preserves research experiments and upstream snapshots. It is not imported by the production library.docs/theorem-dependencies.mdgives the principal theorem dependency graph;docs/andnotes/also contain development records, architecture notes, and historical mathematical source material.
If you use this formalization, please cite the accompanying paper. Machine-readable software and preferred-paper citation metadata are provided in CITATION.cff.
@misc{mulgund2026stochastic,
title = {Stochastic Domination of Gaussian Maxima: A Resolution of the Weak Simplex Conjecture},
author = {Abhijeet Mulgund},
year = {2026},
eprint = {2607.14087},
archivePrefix = {arXiv},
primaryClass = {math.PR},
doi = {10.48550/arXiv.2607.14087},
url = {https://arxiv.org/abs/2607.14087}
}Questions, corrections, and reproducibility reports are welcome through GitHub issues.
The accompanying paper acknowledges support from the National Science Foundation under awards 2240532 and 2217023. This formalization relies on mathlib and on a small audited source closure from StatLean.
Project-authored code is released under the MIT License. Vendored StatLean code and copied research artifacts retain their upstream Apache-2.0 licenses; see PROVENANCE.md and the Scratch/WP01 provenance ledger.