theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalSum_eq_count_sub_main (main : ℝ → ℝ) (N z y A₁ A₂ q l : ℕ) : liuMainPanCoprimeIntervalSum main N A₁ A₂ q l (liuWeight N z y) = liuCoprimeIntervalCount N z y A₁ A₂ q l - ∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then liuWeight N z y a * (main (↑N / ↑a) / ↑q.totient) else 0

Identification with the counting component of the actual production sum. The main function, its argument N/a in real arithmetic, and its normalization are left literally unchanged.

theorem MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount_le_sum_beta (N z y A₁ A₂ q l : ℕ) : liuCoprimeIntervalCount N z y A₁ A₂ q l ≤ ∑ n ∈ liuAPCarrier N q l, liuBeta N z y n

Explicit domination by the untruncated beta sum, after whole-a regrouping.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceCoprimeIntervalCount_le (N A₁ A₂ q l : ℕ) (hq : 0 < q) : (∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N a q l) else 0) ≤ 3 * (↑N / ↑q + 1)

Source-specialized counting estimate, uniform in arbitrary interval cuts, including reversed/empty intervals. No reduced-residue hypothesis is used.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceCoprimeIntervalCount_le (N q l : ℕ) (B : ℝ) (hq : 0 < q) : (∑ a ∈ Finset.Ioc (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N), if a.Coprime q then liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N a q l) else 0) ≤ 3 * (↑N / ↑q + 1)

The exact interval in the Pan--Ding--Wang consumer.

theorem MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount_eq_sum_beta_of_support (N z y A₁ A₂ q l : ℕ) (hl : l.Coprime q) (hsupp : ∀ (a : ℕ), liuWeight N z y a ≠ 0 → a ∈ Finset.Ioc A₁ A₂) : liuCoprimeIntervalCount N z y A₁ A₂ q l = ∑ n ∈ liuAPCarrier N q l, liuBeta N z y n

With genuine support containment and a reduced residue, neither retained filter removes an effective divisor. The support condition is explicit: arbitrary truncations admit only the domination theorem above.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceCoprimeIntervalCount_eq_sum_beta (N q l : ℕ) (B : ℝ) (hl : l.Coprime q) (hlow : liuPanSourceIntervalLower N B < liuSourceZ10 N) : liuCoprimeIntervalCount N (liuSourceZ10 N) (liuSourceY3 N) (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N) q l = ∑ n ∈ liuAPCarrier N q l, liuBeta N (liuSourceZ10 N) (liuSourceY3 N) n

Exact full-beta regrouping for the source interval whenever its known support-containment threshold holds. This is the only place reducedness is needed; none of the upper bounds require it.