theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9IntegerFibreCenter_eq_progressionDensity (U V : Finset ℕ) (α β : ℕ → ℝ) (d : ℕ) : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreCenter U V α β d = ∑ m ∈ U, ∑ n ∈ V, α m * β n * (progressionDensity (m * n)) d

The coprime center is an exact sum of the genuine progression densities, not a replacement by a scalar mass with its gcd exclusions discarded.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9IntegerFibreCenter_externalDensity (upper : Bool) (P : Finset ℕ) (D η z : ℝ) (U V : Finset ℕ) (α β : ℕ → ℝ) : ∑ t ∈ externalTags upper P D η z, ∑ d ∈ (P.prod id).divisors, (externalTerm upper P D η z t) d * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreCenter U V α β d = ∑ m ∈ U, ∑ n ∈ V, α m * β n * externalDensity upper P D η z (progressionDensity (m * n))

Exact normalization of the entire actual main term into the already proved external-family density. No sign or analytic assumption is needed.