theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedKSecondary_uniform {Cscale κ δ ρ η Cnonzero Csecondary Ccoeff Couter : ℝ} (hscale : 1 ≤ Cscale) (hκ : 0 ≤ κ) (hδ : 0 < δ) (hρ : 0 ≤ ρ) (hη : 0 ≤ η) (hη1 : η ≤ 1) (hC : 0 ≤ Cnonzero) (hCsec : 0 ≤ Csecondary) (hCo : 0 ≤ Couter) : ∃ (C : ℝ), 0 < C ∧ ∀ (x M T R S : ℝ), 4 ≤ x → 1 ≤ M → 1 ≤ T → x = 4 * M * T → 1 ≤ R → 1 ≤ S → R * S ≤ x → ∀ (N : Finset ℕ), (∀ n ∈ N, 0 < n) → (∀ n ∈ N, ↑n ≤ 2 * T) → ∀ (a : ℤ), |↑a| ≤ Cscale * x → ∀ (F : ℕ), ↑F ≤ 2 * T → ∀ K ∈ wExtractedKeyBox (x ^ η), ∀ (j cap : Fin 5 → ℕ) (positive : Bool) (b : ℕ), ∀ t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive, wBlockAmplitude K j * √(directJoinedMass ρ Couter x T j) * √(directJoinedSecondary κ δ ρ Cnonzero Csecondary Ccoeff x a R S K F j cap) / T ^ 2 ≤ C * x ^ (100 * (κ + δ + ρ + η)) * (T * R ^ (3 / 4) * S ^ (3 / 2) / √x)

Uniform payment of the actual joined secondary term. The constant is selected after the fixed Cscale but before x, all varying scales, the family, the signed shift, keys and dyadic data.