theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_squarefree_prime_product (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) : Squarefree (P.prod id)

Finite prime carrier: direct Mathlib proof, with no private-name access.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_external_primorial_pairing (N : ℕ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hPN : ∀ p ∈ P, p.Coprime N) {Q θ z : ℝ} (hQ : 1 ≤ Q) (hD : 2 ≤ LiLiuPrereqWF.externalInternalLevel Q θ) (hθ : 0 < θ) (hθu : θ < 1 / 8) (t : List ℕ) (ht : t ∈ LiLiuPrereqWF.externalTags true P (LiLiuPrereqWF.externalInternalLevel Q θ) θ z) (R : ℕ → ℝ) : |∑ d ∈ (P.prod id).divisors, (LiLiuPrereqWF.externalTerm true P (LiLiuPrereqWF.externalInternalLevel Q θ) θ z t) d * R d| ≤ ∑ d ∈ goldbachG11LinkedModuli N ⌊Q⌋₊, |R d|

Pair the unchanged actual WF member only over primorial divisors. Ordinary squarefree distribution suffices; no non-squarefree error estimate is claimed.