Pan--Wang--Ding p.601: the primitive regrouping is (2.4), while (2.5) is the principal PNT estimate. The two cofactor screens are (2.6)--(2.8). This file only supplies exact finite equalities, keeping the whole a-sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPan_screened_character_eq_primitive {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (n : ℕ) : (if n.Coprime q then χ ↑n else 0) = if n.Coprime (q / χ.conductor) then χ.primitiveCharacter ↑n else 0

The old level screen becomes precisely the complementary-factor screen. The conductor's own nonunit zeros are supplied by the primitive character.

theorem MathlibNt.SieveTheory.LiuWeight.liuPan_coprimePrimePrefix_eq_primitive {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (y : ℕ) : AnalyticNumberTheory.LargeSieve.PanLow.coprimePrimePrefix χ y q = AnalyticNumberTheory.LargeSieve.PanLow.coprimePrimePrefix χ.primitiveCharacter y (q / χ.conductor)

Actual primes, not von Mangoldt: change conductor and keep the cofactor.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualCharacterAmplitude_eq_primitive_cofactor (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) (hq : 0 < q) (χ : DirichletCharacter ℂ q) : liuPanActualCharacterAmplitude N A₁ A₂ q f χ = AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude (fun (a : ℕ) => if a.Coprime (q / χ.conductor) then ↑(f a) else 0) (fun (p : ℕ) => if Nat.Prime p ∧ p.Coprime (q / χ.conductor) then 1 else 0) N A₁ A₂ (AnalyticNumberTheory.LargeSieve.conductorPrimitiveCharacter χ)

Exact induced complete-amplitude identity. Both complementary-factor screens remain inside the complete source sum; no a-triangle is used.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualNonprincipalMass_eq_primitive_cofactor (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) (hq : 0 < q) : liuPanActualNonprincipalMass N A₁ A₂ q f = ∑ d ∈ q.divisors, ∑ ψ ∈ AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters d, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude (fun (a : ℕ) => if a.Coprime (q / d) then ↑(f a) else 0) (fun (p : ℕ) => if Nat.Prime p ∧ p.Coprime (q / d) then 1 else 0) N A₁ A₂ ψ‖

Pan's exact same-modulus nonprincipal mass, indexed by the unique primitive conductor. The conductor-one carrier is empty, and neither cofactor screen nor cancellation across the full a-sum is discarded.