HEXAGONbeta

Improved sum-difference inequalities in abelian groups

Primarily AI-generated textHuman understanding: some partsmath.NT — Number Theorymath.CO — Combinatorics

Contributed by Logan Kleinwaks ↗

Version 1 / Oct 07, 2026 / CC BY 4.0

Abstract

For all finite subsets X,YX,Y of an abelian group, we prove \[ |X-Y|\le |X+Y|^{\lamI},\qquad \lamI=\frac{9451\e-3286}{5378\e+787}=1.454277448906\ldots, \] improving the classical exponent 3/23/2. We also prove that a universal two-set exponent λ\lambda over the integers implies an upper bound 2−1/λ2-1/\lambda for the Gyarmati--Hennecart--Ruzsa constant, the supremum θ∗\theta^* of tt such that ∣A−B∣≫∣A+B∣t|A-B|\gg|A+B|^t and ∣A+B∣≪∣A∣|A+B|\ll|A| for arbitrarily large A,B⊂ZA,B\subset\Z. Consequently, \[ \theta^*\le\frac{13524\e-7359}{9451\e-3286}=1.312373302115\ldots, \] improving their bound 4/34/3. The first argument combines a coupling with distinct differences, entropy inequalities for independent sums, a finite certificate using non-Shannon inequalities, and an explicit limiting certificate with weights $\int_0^1t(1-t)^k\e^t\,dt$. The transfer uses localisation and the Pl\"unnecke--Ruzsa inequality over a sequence of scales. The proofs are formalised in Lean~4.

Provenance statement

All mathematical formalisation was performed by Aristotle (Harmonic), which also simplified the formalisation under the author's instructions. Research and proof derivation were performed using Aristotle, GPT-6 Astra, and GPT-5.6 Sol. The author wrote the research-loop instructions; additional research instructions were generated by GPT-6 Astra and GPT-5.6 Sol. Aristotle wrote the initial manuscript under the author's instructions. The manuscript was revised by GPT-6 Astra under the author's instructions and by the author. The author contributed no deep problem-specific insight, the results were obtained through the author's work on more general mathematical research loops. The mathematical results in Theorems 2.1-2.2, Corollary 2.3, and the lemmas and propositions used in their proofs have counterparts in the accompanying Lean 4 formalisation. Appendix A gives the correspondence and explains the representation of finite laws.
FormalizationsPalomar

Tools used

OpenAI
ChatGPTVersion GPT-6 Astra
Harmonic
Aristotle
OpenAI
ChatGPTVersion GPT-5.6 Sol

References

  1. E. P. Csirmaz and L. Csirmaz, Information inequalities for five random variables , Computation 14 (2026), no. 2, article 42. Extended version: https://arxiv.org/abs/2512.23316v2 arXiv:2512.23316v2 . References to numbered results are to this version. r̆l https://doi.org/10.3390/computation14020042 .arXivDOI
  2. R. Dougherty, C. Freiling, and K. Zeger, Non-Shannon information inequalities in four random variables , 2011. https://arxiv.org/abs/1104.3602 arXiv:1104.3602 .arXiv
  3. K. Gyarmati, F. Hennecart, and I. Z. Ruzsa, Sums and differences of finite sets , Funct. Approx. Comment. Math. 37 (2007), 175--186. https://gyarmatikati.web.elte.hu/publ/sumdiffv.pdf Author manuscript . r̆l https://doi.org/10.7169/facm/1229618749 .DOI
  4. F. Hennecart, G. Robert, and A. Yudin, On the number of sums and differences , Astérisque 258 (1999), 173--178. r̆l https://www.numdam.org/item/AST_1999__258__173_0/ .link
  5. M. Madiman, On the entropy of sums , Proc. IEEE Information Theory Workshop, Porto, 2008, 303--307. https://www.stat.yale.edu/ mm888/Pubs/2008/ITW-sums08.pdf Author manuscript . r̆l https://doi.org/10.1109/ITW.2008.4578674 .DOI
  6. M. Madiman, A. W. Marcus, and P. Tetali, Entropy and set cardinality inequalities for partition-determined functions , Random Structures Algorithms 40 (2012), 399--424. https://arxiv.org/abs/0901.0055 arXiv:0901.0055 .arXiv
  7. F. Matúš, Infinitely many information inequalities , Proc. IEEE International Symposium on Information Theory, Nice, 2007, 41--44. r̆l https://doi.org/10.1109/ISIT.2007.4557201 . The five-variable family used here, with a proof, is reproduced in i̧te[Theorem 22] CC .DOI
  8. The mathlib Community, The Lean mathematical library , Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020, 367--381. https://arxiv.org/abs/1910.09336 arXiv:1910.09336 . The Mathlib 4 revision used here is https://github.com/leanprover-community/mathlib4/tree/8f9d9cff6bd728b17a24e163c9402775d9e6a365 8f9d9cff6bd728b17a24e163c9402775d9e6a365 .arXiv
  9. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , Automated Deduction---CADE 28, Lecture Notes in Comput. Sci. 12699 , Springer, 2021, 625--635. r̆l https://lean-lang.org/papers/lean4.pdf .link
  10. G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups , Combinatorica 32 (2012), 721--733. https://arxiv.org/abs/1101.3507v3 arXiv:1101.3507v3 .arXiv
  11. I. Z. Ruzsa, An analog of Freiman's theorem in groups , Astérisque 258 (1999), 323--326. r̆l https://www.numdam.org/item/AST_1999__258__323_0/ .link
  12. I. Z. Ruzsa, Sumsets and entropy , Random Structures Algorithms 34 (2009), 1--10. r̆l https://doi.org/10.1002/rsa.20248 .DOI
  13. T. Tao, Sumset and inverse sumset theory for Shannon entropy , Combin. Probab. Comput. 19 (2010), 603--639. Revised preprint, titled Sumset and inverse sumset theorems for Shannon entropy : https://arxiv.org/abs/0906.4387v5 arXiv:0906.4387v5 .arXiv
  14. Z. Zhang and R. W. Yeung, On characterization of entropy function via information inequalities , IEEE Trans. Inform. Theory 44 (1998), 1440--1452. r̆l https://www.cs.cornell.edu/courses/cs783/2007fa/papers/ZYnonShannon.pdf .link

Version history

  1. v1Submitted by Logan KleinwaksInitial depositCurrentOct 07, 2026