Math and TheorySharp universal Rényi threshold for iid sums on finite Sidon sets
Problem and result
- Problem
- Rényi entropy of iid sums on Sidon sets: for which orders is uniform input optimal?
- Status
- Determined exactly
- Result
- For Rényi order α > 1, the uniform law maximizes H_α(X+X') for iid X, X' on every nonempty finite strong Sidon (B₂) set exactly when 2^(α−1) ≤ 2α − 1, i.e. α ≤ α_c ≈ 3.65986.
Abstract
A sharp universal Renyi-order threshold for iid sums supported on finite strong-B2 sets.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Additive combinatorics and entropy
- Subject
- Discrete analysis, tilings, probability and entropy
- Result type
- Standalone theorem and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
sidon-renyi- Keywords
- Sidon sets, Rényi entropy, sums of independent random variables, additive combinatorics, B2 sets, entropy inequalities
Statement and scope
Formal scope. The finite-support iid theorem, zero probabilities and critical endpoint are formalized. Comparison with unverified source definitions is conditional.
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.pdf323 KB- PDF on GitHub
papers/mathematics/ sidon-renyi/ manuscript.pdf - LaTeX source
papers/mathematics/ sidon-renyi/ manuscript.tex - Bibliography
papers/mathematics/ sidon-renyi/ references.bib
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/ sidon-renyi/ - Lean project
papers/12 Lean filesmathematics/ sidon-renyi/ formalization/ - Lakefile
papers/mathematics/ sidon-renyi/ formalization/ lakefile.toml - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Build the manuscript
mkdir -p .build
latexmk -pdf -interaction=nonstopmode -halt-on-error -outdir=.build manuscript.tex
cp .build/manuscript.pdf manuscript.pdfReproduce the formal proof
cd formalization
lake exe cache get
bash verify.shReproduce the formal proof
cd formalization
PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover -s tests -v- README
papers/mathematics/ sidon-renyi/ README.md - Formalization notes
papers/mathematics/ sidon-renyi/ FORMALIZATION.md - Source provenance
papers/mathematics/ sidon-renyi/ SOURCE_PROVENANCE.md - Authorship
papers/mathematics/ sidon-renyi/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Questions and answers
For which Rényi orders is uniform input optimal for iid sums on Sidon sets?
For α > 1, uniform input maximizes H_α(X+X') for two iid draws on every nonempty finite strong-B₂ Sidon set if and only if 2^(α−1) ≤ 2α − 1, i.e. 1 < α ≤ α_c with α_c ≈ 3.65986 strictly between 3 and 4. Above α_c a nonuniform law on {0,1} beats uniform input; the result does not classify optimizers for larger fixed supports, and makes no Shannon-entropy or different-input-law claim.
Was this threshold known before?
Partly. Gu (arXiv:1809.07364) is credited, in the supplied source context, with an earlier sufficient bound, the threshold equation and a binary obstruction, and Hillion and Johnson with related methods. These attributions and the source definitions have not been verified against the primary texts, so the theorem is presented as a self-contained classification with no priority or gap-closing claim.
Is the proof formally verified?
Yes. The finite-support iid classification, including zero probabilities and the critical endpoint, is formalized in Lean 4 with twelve axiom-audited declarations; its correspondence with the unverified source definitions is conditional.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@unpublished{Goyal2026SidonRenyi,
author = {Dev D. Goyal},
title = {Sharp universal {R\'enyi} threshold for iid sums on finite {Sidon} sets},
year = {2026},
note = {Unpublished manuscript. Historical novelty of the matching universal sufficient bound remains provisional}
}