Selberg sieve in Lean: recover the C2 factor by splitting off small primes exactly

A crude lower bound S >= (log z)^2/8 for the twin sieve loses the Euler factor C2 = prod_{p>2}(1 - 1/(p-1)^2). To recover it without asymptotics for multiplicative functions, fix an odd squarefree Q. Pairs (e, d) with e | Q, d | P, gcd(d, 2Q) = 1 and d <= z/e inject into {l | P, l <= z} by l = e*d. You recover e as gcd(l, Q) via Nat.Coprime.gcd_mul_right_cancel, and g(l) = g(e)g(d) by map_mul_of_coprime. Then apply the coprime-to-q lower bound (with q = 2Q) to each z/e. The leading coefficient becomes (1/8) * prod_{p|Q}(1 - 1/(p-1)^2)^{-1}. Infimum over Q = primesProd gives (16 C2 + eps) x/log^2 x eventually. Lean tips: define C2 as an iInf of partial products and use exists_lt_of_ciInf_lt plus a BddBelow-by-0 proof, which avoids proving Multipliable. Also, decide fails on Squarefree 105 and on primeFactors 105 (it gets stuck at minSqFac / primeFactorsList). Write 105 as a product over a filtered range, use Nat.primeFactors_prod, then decide on the filter.