theorem G11FiniteGate.weighted_bad_inverseTotientMass {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) {N Q K : ℕ} {z : ℝ} (hQ : Q ≤ N) (hz : 0 < z) (hw : ∀ i ∈ I, 0 ≤ w i) (ha : ∀ i ∈ I, w i ≠ 0 → 0 < a i ∧ (∀ p ∈ (a i).primeFactors, z ≤ ↑p) ∧ (a i).primeFactors.card ≤ K) : ∑ d ∈ Finset.Icc 1 Q, (∑ i ∈ I, if ¬(a i).Coprime d then w i else 0) / ↑d.totient ≤ 2 * ↑K / z * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor N ^ 2 * ∑ i ∈ I, w i

Reuse the proved inverse-totient gate on a weighted indexed family. Zero weights need no support conditions; output multiplicities are not removed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_effectiveProduct_mul_prime_factors {N m p : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport N ε) (hp : Nat.Prime p) (hzp : ↑N ^ (4 / 53) ≤ ↑p) : 0 < m * p ∧ (∀ q ∈ (m * p).primeFactors, ↑N ^ (4 / 53) ≤ ↑q) ∧ (m * p).primeFactors.card ≤ 21

The existing twenty-factor bound extends to the actual short-prime product. Repeated factors are allowed, and the short prime is counted at most once more.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_Fouvry_rectangle_mainGate {N Q : ℕ} (ε : ℝ) (hN : 0 < N) (hQ : Q ≤ N) (U V : Finset ℕ) (hU : U ⊆ goldbachG11EffectiveProductSupport N ε) (hV : ∀ p ∈ V, ↑N ^ (4 / 53) ≤ ↑p) : have w := fun (v : ℕ × ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) v.1) * if v.2.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta v.2 else 0; ∑ d ∈ Finset.Icc 1 Q, (∑ v ∈ U ×ˢ V, if ¬(v.1 * v.2).Coprime d then w v else 0) / ↑d.totient ≤ 42 / ↑N ^ (4 / 53) * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor N ^ 2 * ∑ v ∈ U ×ˢ V, w v

Actual rectangular coprime-center deletion, with all G11 multiplicities. This is a main-term gate estimate, not a triangle over the oscillatory discrepancy.