New lower bounds for Romanoff's constant

Let d be the lower density of the set of integers of the form p + 2a with p prime and a ≥ 1. We prove that d ≥ 0.109406, and, assuming a bound that Johnston and Trudgian deduce from Lichtman’s Theorems 1.2 and 1.7, that d ≥ 0.117953. The best lower bound in the literature was 0.10788, from the method of Elsholtz and Schlage-Puchta. That method splits the integers into residue classes modulo a fixed integer l and bounds, in each class, the number of pairs of representations of the same integer by a sieve bound with the constant 8. We use the modulus l = 3·5·7·11·13·17·31·41·241 and bound the singular series with the prime factors of 2t − 1 for t ≤ 1200, which gives the first bound. The bound of Johnston and Trudgian gives the constant 6.7814 for the total over all classes, but their argument does not give it for a single class. For the second bound we use both constants. A linear program finds the distribution of the pairs over the classes that minimizes the resulting bound for d, and an exact Lagrangian certificate bounds its minimum from below. We also prove both bounds in the Lean proof assistant, with the analytic inputs from the literature as hypotheses; there the checks of the certificates run as compiled code. Version 2 adds the formal proof in Lean (Section 7). The programs, the data and the Lean files are archived at doi:10.5281/zenodo.23548710 and available at github.com/tejasvi/romanoff-constant-v2.