Bounded-coefficient principal remainder estimates for Pan's actual source sum, reusing the production moving-prefix and scalar-budget theorems.

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.boundedPrincipalRaw_le_budget (N A₁ A₂ d : ℕ) (f : ℕ → ℝ) (T : ℝ) (hd : 0 < d) (hA : A₂ ≤ N) (hT : 0 ≤ T) (hf : ∀ a ∈ Finset.Ioc A₁ A₂, |f a| ≤ 1) (hp : ∀ a ∈ Finset.Ioc A₁ A₂, |primeCount (N / a) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑a)| ≤ T / ↑a) : |MathlibNt.SieveTheory.LiuWeight.liuPanActualPrincipalRaw (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d f| ≤ T * (1 + Real.log ↑N) + ↑A₂ * ↑d.primeFactors.card

The finite principal budget in LiuPanPrincipalRemainder only used the Liu weight through |f a| ≤ 1, so the same estimate holds for any bounded coefficient on the window.

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.boundedPrincipalRaw_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (d A₁ A₂ : ℕ) (f : ℕ → ℝ), 1 ≤ d → ↑d ≤ √↑N → ↑A₂ ≤ ↑N ^ (2 / 3) → (∀ a ∈ Finset.Ioc A₁ A₂, |f a| ≤ 1) → |MathlibNt.SieveTheory.LiuWeight.liuPanActualPrincipalRaw (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d f| ≤ C * ↑N / Real.log ↑N ^ U

The production moving-prefix PNT and low scalar payment already eliminate the only external inputs needed by the finite bounded-coefficient budget.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL_le_actualCharacterMass_with_paid_principal (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (d A₁ A₂ : ℕ) (f : ℕ → ℝ), 1 ≤ d → ↑d ≤ √↑N → ↑A₂ ≤ ↑N ^ (2 / 3) → (∀ a ∈ Finset.Ioc A₁ A₂, |f a| ≤ 1) → liuMainPanCoprimeIntervalMaxL (liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d f ≤ (liuPanActualNonprincipalMass N A₁ A₂ d f + C * ↑N / Real.log ↑N ^ U) / ↑d.totient

Pan's exact actual-character decomposition plus the bounded principal payment gives the same paid-principal inequality for any window-bounded real coefficient. The nonprincipal mass is left untouched.