The full high-conductor Pan source sum

The outer interval is open on the left and closed on the right. It is a nonnegative majorant, not an identification, of a strictly truncated outer modulus carrier. Conductor cells use the exact real radii; only complete dyadic source blocks are separated by a triangle inequality.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.mem_active_conductorCell {x q : ℕ} {B : ℝ} (hx : 1 ≤ Real.log ↑x) (hB : 0 ≤ B) (hq : q ∈ Finset.Ioc ⌊lowConductor x B⌋₊ ⌊upperConductor x B⌋₊) : ∃ j ∈ Finset.range (Nat.log 2 x + 1), conductorRadius x B j ≤ upperConductor x B ∧ q ∈ conductorCell (conductorRadius x B j)

Every high conductor belongs to an active cell with the exact real radius.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_depth_le {x A₁ A₂ : ℕ} (hA : A₂ ≤ x) : panDyadicDepth A₁ A₂ ≤ Nat.log 2 x + 1

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.panIymHigh_le_sum_active_sourceCells (f : ℕ → ℂ) (m x A₁ A₂ : ℕ) (B : ℝ) (hx : 1 ≤ Real.log ↑x) (hB : 0 ≤ B) (hA₁ : 0 < A₁) : panIymHigh (panSourceG f m) (panSourceD m) x A₁ A₂ ⌊lowConductor x B⌋₊ ⌊upperConductor x B⌋₊ ≤ ∑ j ∈ Finset.range (Nat.log 2 x + 1) with conductorRadius x B j ≤ upperConductor x B, ∑ k ∈ Finset.range (panDyadicDepth A₁ A₂), sourceCell f m x A₁ A₂ k (conductorRadius x B j)

Domination by active real conductor cells, with triangle inequalities only over the complete source blocks. The last conductor cell may extend beyond the closed outer cutoff.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.chosen_high_source_depth_saving : ∃ (C : ℝ), 0 < C ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (m A₁ A₂ : ℕ) (f : ℕ → ℂ), A₂ ≤ x → ↑A₂ ≤ ↑x ^ (1 - ε) → Real.log ↑x ^ (2 * B) ≤ ↑A₁ → (∀ (n : ℕ), ‖f n‖ ≤ 1) → panIymHigh (panSourceG f m) (panSourceD m) x A₁ A₂ ⌊lowConductor x B⌋₊ ⌊upperConductor x B⌋₊ ≤ (↑(Nat.log 2 x) + 1) ^ 2 * (C * ↑x * Real.log ↑x ^ (4 - B) + 776 / ↑x)

The uniform full high-source bound with its explicit logarithmic depths.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.log_depth_le_three_log {x : ℕ} (hx : 4 ≤ Real.log ↑x) : ↑(Nat.log 2 x) + 1 ≤ 3 * Real.log ↑x

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.chosen_high_source_log_saving : ∃ (C : ℝ), 0 < C ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (m A₁ A₂ : ℕ) (f : ℕ → ℂ), A₂ ≤ x → ↑A₂ ≤ ↑x ^ (1 - ε) → Real.log ↑x ^ (2 * B) ≤ ↑A₁ → (∀ (n : ℕ), ‖f n‖ ≤ 1) → panIymHigh (panSourceG f m) (panSourceD m) x A₁ A₂ ⌊lowConductor x B⌋₊ ⌊upperConductor x B⌋₊ ≤ C * ↑x * Real.log ↑x ^ (6 - B) + 6984 * Real.log ↑x ^ 2 / ↑x

Arbitrary logarithmic saving for the full high source sum, with the explicit Perron remainder after both logarithmic-depth summations. This does not assert the low-conductor or induced-character discrepancy assembly.