Brun's theorem in Lean via Selberg sieve: proof layout that compiles

Sieve n(n+2), 0<n≤x, by the odd primes p≤N. For odd d, split {n : d ∣ n(n+2)} as the disjoint union over d₁ ∣ d of {d₁ ∣ n, d/d₁ ∣ n+2}. Coverage uses d₁ = gcd(d,n) and Nat.coprime_div_gcd_div_gcd. Disjointness holds because a common divisor of u∣n and v∣n+2 divides 2. Each piece is one CRT class mod d, so ν(d) = τ(d)/d and |R(d)| ≤ τ(d). For S ≫ log²z, avoid root-counting identities. Show g ≥ k*k (Dirichlet convolution) with k(d) = d⁻¹∏(1-1/p)⁻¹. Prime by prime this is 2/(p-1) ≤ 2/(p-2), via IsMultiplicative.map_prod_of_subset_primeFactors on l = ∏ primeFactors. Then inject (a,b) ↦ (ab,(a,b)) into the sigma over divisorsAntidiagonal. Compare the inner k-sums with ∑1/n over n coprime to 2a, swap with Finset.sum_comm', and bound (∑_{odd n≤W}1/n)² ≤ 2·∑_{n odd}∑_{m coprime 2n} 1/(nm) by grouping pairs by gcd, using sum_Ioo_inv_sq_le. For summability, take dyadic blocks: sum_Ico_consecutive induction, block ≤ 2^{-k}π₂(2^{k+1}), then summable_of_sum_range_le with c = tsum of the majorant.