Summing the complete occupied secondary contribution

Both the divisor envelope and the ratio count are proved before use. No fixed-data sum remains in the secondary term. The coarse powers below still require comparison with the global C.2 scale; this is not (4.10).

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases_weighted_sum_le_scale {δ : ℝ} (hδ : 0 < δ) : ∃ (Cτ : ℝ), 0 < Cτ ∧ ∀ (ε C : ℝ) (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) (Bβ Bζ : ℝ), 0 ≤ ε → 0 ≤ C → (∀ n ∈ N, 0 < n) → (∀ n ∈ N, n ≤ F) → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → 0 ≤ Bβ → 0 ≤ Bζ → (∀ n ∈ N, |β n| ≤ Bβ) → (∀ s ∈ Finset.Ioc 0 ⌊S⌋₊, |ζ s| ≤ Bζ) → ∑ v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)), |wGramWeight K β ζ (wGramSecondaryJoin v 0)| * wGramSecondaryGcdDyadicMean ε C a R S K j cap v ≤ wGramSecondaryBaseCountBound K F j * ((Bβ * Bζ) ^ 2 * wGramSecondaryScaleEnvelope ε δ C Cτ a R S K F j cap)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_secondary_paid {ε κ δ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hδ : 0 < δ) : ∃ (Czero : ℝ) (Cnonzero : ℝ) (Cτ : ℝ), 0 < Czero ∧ 0 < Cnonzero ∧ 0 < Cτ ∧ ∀ (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z T εSupport : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) (Bβ Bζ : ℝ), a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → (∀ n ∈ N, n ≤ F) → 1 < x → η < εSupport → x ^ εSupport ≤ T → 0 ≤ Bβ → 0 ≤ Bζ → (∀ n ∈ N, |β n| ≤ Bβ) → (∀ s ∈ Finset.Ioc 0 ⌊S⌋₊, |ζ s| ≤ Bζ) → wSeparatedCorrelationEnergy x N S (wGramPrefix N a x η R S M Z K b j cap positive) c K β ζ a ≤ (Bβ * Bζ) ^ 2 * ↑(2 ^ j 1) * Czero * ↑(wGramResonanceScaleBoxCard K F j) * wGramResonanceScaleEnvelope K F j ε + (wGramSecondaryBaseCountBound K F j * ((Bβ * Bζ) ^ 2 * wGramSecondaryScaleEnvelope κ δ Cnonzero Cτ a R S K F j cap) + ∑ L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c) with wGramNumerator K a L ≠ 0 ∧ ¬wGramSecondaryResonant L, |wGramWeight K β ζ L| * wGramFouvryCost κ Cnonzero a R S M Z K j cap L)