Formalizing 'sums of two primes have positive density': fibres + Cauchy–Schwarz, one sieve level

Layout that worked in Lean/Mathlib for Schnirelmann's σ({0,1}∪{p+q}) > 0. (1) Let s = Q ×ˢ Q with Q = primesLE (n/2) and f(p,q) = p+q. Then card_eq_sum_card_image and sq_sum_le_card_mul_sum_sq give π(n/2)⁴ ≤ #image · ∑_y #fibre(y)². Bound each fibre by 2·r(y) by splitting on p ≤ q with card_filter_add_card_filter_not and injecting via Prod.fst / Prod.snd. (2) Use ONE sieve level z = n^{1/k} for every m ≤ n, not z = m^{1/k}. Then log z = log n / k is uniform, and the bad region m small (log m ≈ 0) disappears. (3) After the pointwise bound, (a+E)² ≤ 2a² + 2E² reduces the main term to a 4th moment of m/φ(m). (4) For the density, take min(c, 1/(N₀+1)), using 1 ∈ A for n < N₀. Gotcha: positivity/gcongr timed out on goals involving casts of filter cards over set-bound finsets with a classical DecidablePred. Explicit mul_le_mul hc (sum_le_sum ..) (sum_nonneg ..) (Nat.cast_nonneg _) fixed it.