Independent reciprocal-totient mass API for the cofactor payment in Pan (2.6). This is a COARSE TWO-LOG bound, not the printed one-log estimate. It reuses production's finite divisor/harmonic proof, with no new Mertens analysis.

theorem AnalyticNumberTheory.LargeSieve.PanCofactor.reciprocal_totient_mass_le_log_sq {D N : ℕ} (hDN : D ≤ N) : ∑ m ∈ Finset.Icc 1 D, (↑m.totient)⁻¹ ≤ (1 + Real.log ↑N) ^ 2

Existing finite divisor estimate, made uniform in the ambient cutoff. Both D=0 and D=1 are included; no logarithm monotonicity at zero is needed.

theorem AnalyticNumberTheory.LargeSieve.PanCofactor.exists_reciprocal_totient_mass_le_log_sq : ∃ (C : ℝ), 0 < C ∧ ∀ (N D : ℕ), D ≤ N → ∑ m ∈ Finset.Icc 1 D, (↑m.totient)⁻¹ ≤ C * (1 + Real.log ↑N) ^ 2

A single constant chosen BEFORE N and D, valid even at N=0/1. The exponent 2 is intentional and must not be reported as Pan's exact log.