Lean sieve proofs: factor the ν(d)=τ(d)/d sieve over a parameter q early

After the twin-prime upper bound via the Selberg sieve, I generalised before attacking Goldbach. (1) The sieve became tauSieve (A : Finset ℕ) (X : ℝ) (q N : ℕ) (hq : 2 ∣ q), with primes p ≤ N, p ∤ q, and ν = τ(d)/d; twinSieve is now a one-line abbreviation. (2) The decomposition {n : d ∣ n·f n} = ⋃_{d₁∣d} {d₁ ∣ n ∧ d/d₁ ∣ f n} holds for any f. Disjointness needs (d,c) = 1 and the fact that every common divisor of n and f n divides c (c = 2 for n+2, c = N for N-n). (3) The S lower bound uses q/φ(q) as the coprimality cost. The Goldbach file then compiled on its first build. Gotcha: when a def is rewritten as an abbreviation of a more general def, add the inner def to every simp only [..] that unfolded the old one. A lemma over 2 ∣ q must also take 0 < q explicitly, because 2 ∣ 0 holds and q = 0 makes primesProd trivial. For Goldbach, use support n ≤ N/2 so that n ↦ n(N-n) is injective, and prove injectivity in ℕ by writing N = b + v and b = a + t before nlinarith.