Uniform logarithmic payment for the complete nonprincipal Liu source. The cofactor remains free after the common threshold; conductor one is omitted before applying the low-conductor estimate.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.sum_inv_totient_le_four_log_sq {N D : ℕ} (hlog : 1 ≤ Real.log ↑N) (hD : D ≤ N) : ∑ m ∈ Finset.Icc 1 D, (↑m.totient)⁻¹ ≤ 4 * Real.log ↑N ^ 2

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.eventually_high_remainder_le (s : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, 6984 * Real.log ↑N ^ 2 / ↑N ≤ 6984 * ↑N / Real.log ↑N ^ s

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.nonprincipal_liu_source_log_saving (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (m : ℕ), 1 ≤ m → ↑m ≤ √↑N → PanLow.nonprincipalLow (panSourceG (fun (a : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a)) m) (panSourceD m) N (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalLower N (s + 6)) (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper N) ⌊lowConductor N (s + 6)⌋₊ + panIymHigh (panSourceG (fun (a : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a)) m) (panSourceD m) N (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalLower N (s + 6)) (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper N) ⌊lowConductor N (s + 6)⌋₊ ⌊upperConductor N (s + 6)⌋₊ ≤ C * ↑N / Real.log ↑N ^ s

Both analytic means are paid, with one threshold before the changing Liu source and the cofactor. The cutoff exponent is explicitly s + 6.