Romanov's theorem (p + 2^k has positive density) in Lean: proof layout that compiled

This takes about 1200 lines on top of an existing Selberg twin/Goldbach sieve and Mertens' second theorem. (1) Generalise the twin sieve to n(n+h), sifting primes p ∤ 2h. In the CRT disjointness step, a common divisor of n and n+h divides h. This gives #{p ≤ x : p, p+h prime} ≪ (2h/φ(2h))² x/log² z + error. (2) For h = 2^k − 2^l, 2h/φ(2h) = 2(2^j−1)/φ(2^j−1) with j = k − l; use Nat.totient_mul and Nat.totient_prime_pow. (3) Average ∑_{m≤M} ((2^m−1)/φ)² ≪ M: write (n/φ(n))² = ∏_{p|n}(1+w(p)), expand with Finset.prod_one_add, and swap sums. A prime set t counts the m with orderOf (2 : ZMod (∏ t)) ∣ m, via orderOf_dvd_iff_pow_eq_one and ZMod.natCast_eq_zero_iff on 2^m − 1. Use the identity 1/e = 1/(M+1) + ∑_{Y=e}^{M} 1/(Y(Y+1)) with Finset.sum_comm' (dependent ranges). Then ∑_{e(t)≤Y} W(t) ≤ ∏_{p | 2^e−1, e≤Y}(1+w(p)) ≪ (log Y)⁴. To get it, note #primes ≤ Y² (from 2^{#pf} ≤ ∏ p ≤ ∏(2^e−1) < 2^{Y²}), so primes > Y² contribute ≤ 1 to ∑1/p, and Mertens handles the rest. (4) Let r(y) = #{k : y − 2^k prime}. Then ∑r² = ∑_{k,l} #{y : k,l ∈ r(y)}; the diagonal equals ∑r exactly, which avoids needing an upper bound for π(x). Cauchy–Schwarz runs over the support of r. Finish with t ≥ x/2, t² ≤ N(t + Dx) ⇒ N ≥ x/(2+4D), using (t − x/2)((2+4D)t + 2Dx) ≥ 0 as an nlinarith hint.