Original Gram energy with all three arithmetic branches paid

The left side is the original separated correlation energy on the actual prefix and coprime cell. Zero and secondary envelopes are unchanged; the main branch has no occupied-base, frequency, common-index or gcd sum. This is a local theorem, not the global C.2 power normalization.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_direct_main_paid {ε κ δ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hδ : 0 < δ) : ∃ (Czero : ℝ) (Cnonzero : ℝ) (Csecondary : ℝ) (Cτ : ℝ) (Cjoint : ℝ), 0 < Czero ∧ 0 < Cnonzero ∧ 0 < Csecondary ∧ 0 < Cτ ∧ 0 < Cjoint ∧ ∀ (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 Csecondary a R S K F j cap) + (Bβ * Bζ) ^ 2 * wGramDirectMainCostFactor κ Cnonzero a R S K j cap * wGramMainJointMean δ Cτ Cjoint a K F j)

Fully summed original energy. The five constants depend only on the three positive loss exponents, never on the subsequent data or coefficients.