Improve C_3a lower bound via Lean-formalized controlled-carry semigroup mask-digit construction - #146
Conversation
|
Great work - this looks very good. I independently cloned v3.2 and reran the certificate SHA checks, exact Python reconstruction, and exact controlled-exponent conversion; all passed, including the strict |
- README: add the missing Recent progress entry for the C_15a upper bound 2.371177 (arXiv:2608.16884, 17 Aug 2026), merged in #149. - 15a.md: join the split [DEKMRSZAWB2026] reference line and correct the author list (Mehrabian, Ruiz F. J. R., Vassilevska Williams). - 3a.md: show both the certified and limit values in the [K2026b] Bound cell, matching the README convention, and fix a missing cell space. - README rows 44 and 76: GitHub's inline-math extension does not open a "$" span when a word character precedes it, so "degree-$d$" rendered literally on github.com. Reword rather than insert spaces around the hyphen, which would render worse under MathJax on the Pages site. Reported in #143 by @andrew-yoo.
|
Merged, thanks — this is a very careful package, and the Lean formalization plus @carcango's independent replay of the certificates settles the question you raised. On the asterisk: I have dropped it from the finite construction. The asterisk marks values whose verification is minimal, and a Two cosmetic corrections in bc0e936: the Bound cell now reads |
3 participants
Summary
This PR includes new lower bounds for the Gyarmati-Hennecart-Ruzsa sum-difference constant, achieving$C_{3a}>1.19519192$ with a limit construction described in the proof paper and formalized in Lean. The formalization includes the relevant parts of [GHR2007], so it is self-contained.
Because the contribution guidelines recently changed and now distinguish (with an asterisk) between limit constructions and finite constructions, I have also included a finite construction achieving$C_{3a}>1.19102809$ .
I am unsure whether to apply the asterisk to the finite construction's bound or not and in this PR I have not. Although it is finite, it is very large, so it is proven by bounding sumset and difference set cardinalities rather than exactly counting them. It does not require any asymptotics and is formalized in Lean along with the limit construction. However, if only exact counting or peer-reviewed publication qualify for an asteriskless bound, then the asterisk should not be removed from the finite construction in
constants/3a.mdandREADME.mdand only the new limit construction bound (with asterisk) should be used to updateREADME.md.The new limit construction achieving$C_{3a}>1.19519192$ generalizes my previous carry-free masked-digit construction by allowing a lower base in which carries can occur and accounting for those carries rigorously. The previous construction in turn generalized Zheng's [Z2025] bounded-digit construction.
The new limit construction again uses a digit mask$M$ based on numerical semigroups:
The base in the construction is$q=27022$ , much lower than the carry-free base ($53945$ ), so there is carrying, which is accounted for rigorously in the proof paper (formalized in Lean). Note that this mask is different from the carry-free mask used in the finite construction, which remains the same as found previously. In other words, a different mask optimized the $C_{3a}$ bound when accounting for carrying than when using a carry-free base ("optimized" at least among the mask families I considered).
The proof paper provides rigorous carry-aware lower bounds for$C_{3a}$ based on the mask $M$ and base $q$ . Proposition 5 (Two-sided carry pressure) of the paper states the best bound.
The proof paper: https://github.com/kleinwaks/masked-digit-sum-difference-bound/blob/main/proof/masked_digit_bound.pdf (PDF), https://github.com/kleinwaks/masked-digit-sum-difference-bound/blob/main/proof/masked_digit_bound.tex (LaTeX).
Lean 4/Mathlib formalization: https://github.com/kleinwaks/masked-digit-sum-difference-bound/tree/main/formalization/lean
Everything including verifiers, certificates, etc.: https://github.com/kleinwaks/masked-digit-sum-difference-bound
Formalization
The Lean formalization was produced with Aristotle (Harmonic) (@Aristotle-Harmonic), guided jointly by the author and especially by this formalization blueprint generated by GPT-5.6 Sol: https://github.com/kleinwaks/masked-digit-sum-difference-bound/blob/main/formalization/LEAN_BLUEPRINT.txt.
It formalizes the [GHR2007] lower bound on$C_{3a}$ that uses a single finite set $U$ (which cannot achieve $C_{3a}$ greater than $1.25$ ), the carry-free and carry-aware bounds in the proof paper for masked-digit constructions, and the final numerical bounds on $C_{3a}$ claimed in this PR, among other things. The project contains no
sorry.The large exact Lean computations formalizing the numerical bounds in this PR use
native_decide, so their axiom report includesLean.trustCompiler; this trust boundary is documented in the proof paper and the formalization README.Changes
constants/3a.md. (See note above about my uncertainty whether the asterisk should be removed from the finite bound.)constants/3a.mdabout how the construction generalizes the previous construction by allowing and accounting for carries.3acell inREADME.mdto1.19102809 (1.19519192*). (Again, see note about whether the asterisk should be removed from the finite bound.)Verification
The finite MPFR verifier reconstructs the complete discrete data and finishes quickly. The full controlled-carry verifier takes much longer to run, reconstructing (as described in the paper) all eight difference frontiers, checking 351951 Collatz inequalities, and performing the 8192-step sum dynamic program. A short Python checker independently converts the rational pressure bounds to the displayed exponent using exact arithmetic only.
AI-use disclosure
During this work, the author used several large language models. OpenAI's GPT-5.6 Sol model was used extensively in software development, analysis of search results, drafting and revising the proof, and preparation of the verification package. Google's Gemini 3.1 Pro Preview was used in software development and analysis of search results; Google's Gemini 3.5 Flash and Gemini 3.6 Flash were used to review the proof; and Anthropic's Sonnet 5 was used in analysis of search results. Aristotle produced the Lean formalization, which was subsequently audited against the paper's mathematical statements. The author set the research goals, directed the computational work, selected which suggestions to pursue, ran the search and verification software, reviewed the mathematical arguments and outputs, and takes responsibility for all claims and references.
Even better bounds on the way?
In a comment on an earlier PR, @carcango mentioned that he has a candidate bound of 1.2060, greater than that claimed in this PR, using a different construction. Separately, I am working on an even greater bound using yet another kind of construction. Nevertheless, I think there is value in preserving the bound in this PR, and especially the link to the formalization, in case others can further improve this type of masked-digit bound.