Pan--Wang--Ding (1975), original p.601, (2.6): finite cofactor transport. The payload is arbitrary; in the application it is the whole-a norm, not an a-wise triangle majorant. All positive divisors, including d=1, are retained.

theorem AnalyticNumberTheory.LargeSieve.PanCofactor.sum_divisors_eq_hyperbola (G : ℕ → ℕ → ℝ) (D : ℕ) : ∑ q ∈ Finset.Icc 1 D, ∑ d ∈ q.divisors, G (q / d) d = ∑ m ∈ Finset.Icc 1 D, ∑ d ∈ Finset.Icc 1 (D / m), G m d

Exact cofactor bijection (q,d) ↦ (q/d,d), inverse (m,d) ↦ (m*d,d). No positivity is required of the real payload in this equality.

theorem AnalyticNumberTheory.LargeSieve.PanCofactor.weighted_sum_divisors_eq_hyperbola (F : ℕ → ℕ → ℝ) (D : ℕ) : ∑ q ∈ Finset.Icc 1 D, (↑q.totient)⁻¹ * ∑ d ∈ q.divisors, F (q / d) d = ∑ m ∈ Finset.Icc 1 D, ∑ d ∈ Finset.Icc 1 (D / m), (↑(m * d).totient)⁻¹ * F m d

Exact reciprocal-totient ledger before paying the weight.

theorem AnalyticNumberTheory.LargeSieve.PanCofactor.weighted_sum_divisors_le_rectangle (F : ℕ → ℕ → ℝ) (hF : ∀ (m d : ℕ), 0 ≤ F m d) (D : ℕ) : ∑ q ∈ Finset.Icc 1 D, (↑q.totient)⁻¹ * ∑ d ∈ q.divisors, F (q / d) d ≤ ∑ m ∈ Finset.Icc 1 D, (↑m.totient)⁻¹ * ∑ d ∈ Finset.Icc 1 D, (↑d.totient)⁻¹ * F m d

Totient supermultiplicativity pays the weight; nonnegativity permits only enlargement of the hyperbola to the positive D-by-D rectangle.

theorem AnalyticNumberTheory.LargeSieve.PanCofactor.weighted_sum_divisors_le_uniform (F : ℕ → ℕ → ℝ) (hF : ∀ (m d : ℕ), 0 ≤ F m d) (D : ℕ) (M : ℝ) (hM : ∀ m ∈ Finset.Icc 1 D, ∑ d ∈ Finset.Icc 1 D, (↑d.totient)⁻¹ * F m d ≤ M) : ∑ q ∈ Finset.Icc 1 D, (↑q.totient)⁻¹ * ∑ d ∈ q.divisors, F (q / d) d ≤ M * ∑ m ∈ Finset.Icc 1 D, (↑m.totient)⁻¹

A uniform whole-payload inner bound leaves precisely the cofactor mass. This finite implication does not assert an analytic bound for the payload.