Sharp stability and exact cap optima for Rademacher sums

Dev D. Goyal

Sharp stability and exact cap optima for Rademacher sums

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Exact Kolmogorov-distance cap optimum and support-gap stability for Rademacher sums
Status: Determined exactly
Result: A large support gap forces an odd flat core with the sharp distance bound 2 − 2√(1 − (a − x)²); support-gap near-optimizers are stable with optimal constant √(2+√2) at every cap; and, conditionally on the completed Keller–Klein comparison, the maximal Kolmogorov distance is exact for 1/√5 ≤ a ≤ 1/√3.

Abstract

For normalized Rademacher sums X = Σ bᵢεᵢ with |bᵢ| ≤ a, if every signed sum has magnitude at least x > a/2, the core {i : |bᵢ| ≥ x} is odd and the coefficients lie within squared distance 2 − 2√(1 − (a − x)²) of the flat vector on it, with equality exactly for a saturated core and one residual. At every cap, near-maximizers of the exact support-gap optimum lie within √(2+√2) times the deficit of an admissible vector of one of the two optimal shapes, with an optimal constant, and the exact nonlinear modulus on the saturated branch is determined. Conditionally on the completed Keller–Klein comparison, the maximal Kolmogorov distance K(a) is determined with all optimizers for 1/√5 ≤ a ≤ 1/√3, extending an earlier formula for a ≥ 1/√3.

Details

Year: 2026
Discipline: Mathematics
Area: Probability and normal approximation
Subject: Discrete analysis, tilings, probability and entropy
Result type: Sharp inverse and stability theorems, exact cap optima and reproducible proof package
Formal proof: Standalone Lean package
Family: keller-klein-sharp-stability
Keywords: Rademacher sums, support gap, minimum signed sum, stability, inverse theorem, Kolmogorov distance, Keller–Klein conjecture, Berry–Esseen, normal approximation, Hollom–Portier

Statement and scope

Formal scope. Lean 4.19.0 proves, for actual finite signed coefficient vectors and their actual minimum signed sum, the inverse theorem with its equality classification, stability at every cap with an explicit admissible comparison vector and its optimality, the exact saturated modulus with its equality cases and attainment, the fixed-flat inequalities and the sharpness witnesses: 67 audited statements in 15 new modules, replayed with nine inherited modules and the 62 earlier modules. A conditional Lean bridge derives the four-shift envelope with the analytic tail inputs as hypotheses. The probability optima have conventional proofs using the Keller–Klein, Hollom–Portier and Tomaszewski inputs and validated interval certificates on 27,972 rational boxes.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 455 KB
PDF on GitHub: papers/mathematics/keller-klein-sharp-stability/manuscript.pdf
LaTeX source: papers/mathematics/keller-klein-sharp-stability/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/keller-klein-sharp-stability/

Lean project

papers/mathematics/keller-klein-sharp-stability/lean/ 90 Lean files

Lakefile

papers/mathematics/keller-klein-sharp-stability/lean/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/keller-klein-sharp-stability/VERIFICATION.md, which gives their context and working directory.

Lean

lake exe cache get
python3 verify.py --lean "$(lean --print-prefix)/bin/lean" --mathlib .lake/packages/mathlib --trust 0 --output /tmp/keller-klein-sharp-stability-verification

Certificates

python3 certificates/check_two_core_upper.py
python3 certificates/check_four_core_upper.py
python3 -m venv /tmp/flint && /tmp/flint/bin/pip install -r certificates/requirements.txt
/tmp/flint/bin/python certificates/verify_lower_exact_gap_arb.py 128
/tmp/flint/bin/python certificates/verify_lower_five_flat_arb.py B 128
/tmp/flint/bin/python certificates/verify_lower_five_flat_arb.py C 128

README: papers/mathematics/keller-klein-sharp-stability/README.md
Verification guide: papers/mathematics/keller-klein-sharp-stability/verification/README.md
Verification record: papers/mathematics/keller-klein-sharp-stability/VERIFICATION.md
Authorship: papers/mathematics/keller-klein-sharp-stability/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Source. Keller and Klein (Adv. Math. 2022) posed the normal-approximation problem for Rademacher sums in their proof of Tomaszewski's conjecture. The probability results use the completed Keller–Klein comparison (the earlier keller-klein package together with Ivanisvili's computer-assisted results of 21 October 2026), the Hollom–Portier strict-tail profile and Tomaszewski's theorem. The support-gap optimum and the formula for a ≥ 1/√3 come from an unpublished preceding package. Stability results of De–Diakonikolas–Servedio, Fang–Wang and Xie are compared in the manuscript. Historical priority is not certified.

Questions and answers

What does the inverse theorem say?

If every coefficient of a normalized Rademacher sum is at most a in absolute value and every signed sum has magnitude at least x > a/2, the coefficients at least x form an odd core, and the squared distance to the flat vector on that core is at most 2 − 2√(1 − (a − x)²). Equality holds exactly for k coefficients a and one residual a − x.

Which parts are formally verified?

The inverse theorem, the all-cap stability theorem with its optimal constant √(2+√2), the exact saturated modulus with attainment, the fixed-flat inequalities and the sharpness examples are proved in Lean 4 for actual finite coefficient vectors. The probability optima are written proofs with interval-arithmetic certificates, and a Lean bridge checks their finite-law interface with the analytic inputs as hypotheses.

On what do the Kolmogorov-distance formulas depend?

They use the completed Keller–Klein comparison, which combines the earlier small-coefficient package with Ivanisvili's unrefereed computer-assisted results, the published Hollom–Portier tail profile and Tomaszewski's theorem. The work is an unrefereed preprint.

Cite

Citation file papers/mathematics/keller-klein-sharp-stability/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026kellerkleinstability,
  author = {Goyal, Dev D.},
  title = {Sharp Stability and Exact Cap Optima for {Rademacher} Sums},
  year = {2026},
  month = nov,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/keller-klein-sharp-stability}
}