Improve C_3a lower bound via Lean-formalized controlled-carry semigroup mask-digit construction

[kleinwaks]

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.md and README.md and only the new limit construction bound (with asterisk) should be used to update README.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:

$$ M=\langle1971,2016,2100,2628,2688,2800\rangle\cap[0,26972]. $$

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 includes Lean.trustCompiler; this trust boundary is documented in the proof paper and the formalization README.

Changes

• Adds a new finite-certificate row to constants/3a.md. (See note above about my uncertainty whether the asterisk should be removed from the finite bound.)
• Records the stronger controlled-carry limit in that row's Comments field.
• Adds a comment to constants/3a.md about how the construction generalizes the previous construction by allowing and accounting for carries.
• Updates the 3a cell in README.md to 1.19102809 (1.19519192*). (Again, see note about whether the asterisk should be removed from the finite bound.)
• Adds the limit construction bound to the README's "Recent progress" section.
• Adds a reference to the proof paper, verification package, and Lean formalization.

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.