theorem AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow_endpoint (U b : ℝ) (hU : 0 < U) (hb : 0 ≤ b) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (m A₁ A₂ Q : ℕ) (g : ℕ → ℂ), 1 ≤ m → ↑m ≤ √↑N → ↑A₂ ≤ ↑N ^ (2 / 3) → ↑Q ≤ Real.log ↑N ^ b → (∀ a ∈ Finset.Ioc A₁ A₂, ‖g a‖ ≤ 1) → nonprincipalLow g (fun (n : ℕ) => if Nat.Prime n ∧ n.Coprime m then 1 else 0) N A₁ A₂ Q ≤ C * ↑N / Real.log ↑N ^ U

The needed y=N specialization of Pan (2.12), with all prefix and scalar payments internal. This is the explicitly nonprincipal carrier, not raw panIymLow.

theorem AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow_liuSource_endpoint (U b : ℝ) (hU : 0 < U) (hb : 0 ≤ b) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (B : ℝ) (m Q : ℕ), 1 ≤ m → ↑m ≤ √↑N → ↑Q ≤ Real.log ↑N ^ b → nonprincipalLow (fun (a : ℕ) => if a.Coprime m then ↑(MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a) else 0) (fun (n : ℕ) => if Nat.Prime n ∧ n.Coprime m then 1 else 0) N (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalLower N B) (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper N) Q ≤ C * ↑N / Real.log ↑N ^ U

Literal Liu coefficient and Pan source window; the threshold is independent of the window exponent B. No claim about the high-conductor part is made.