Explicit local zero-resonance payment in the original full energy

There is no remaining occupied-base sum. The zero term is (Bbeta*Bzeta)^2 * Czero * Kwidth * Rwidth * N₁width * Hwidth * (F/d) * Swidth times Amax^(2 epsilon) * Bmax^epsilon, with exact dyadic widths and the actual fixed frequency sign. The nonzero Fouvry sum is unchanged.

This is a local estimate, not the global C.2 normalization: nonzero primary and secondary aggregation, outer L² summation and the epsilon ledger remain.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_resonance_scaleBox {ε κ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) : ∃ (Czero : ℝ) (Cnonzero : ℝ), 0 < Czero ∧ 0 < Cnonzero ∧ ∀ (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 ε + ∑ 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, |wGramWeight K β ζ L| * wGramFouvryCost κ Cnonzero a R S M Z K j cap L

Both constants precede all support, key, dyadic, prefix, cell and coefficient data. The only additional input is the upper beta support.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_resonance_scale_half_support {ε κ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) : ∃ (Czero : ℝ) (Cnonzero : ℝ), 0 < Czero ∧ 0 < Cnonzero ∧ ∀ (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 → 0 < ε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 (εSupport / 2) R S M Z K b j cap positive) c K β ζ a ≤ (Bβ * Bζ) ^ 2 * ↑(2 ^ j 1) * Czero * ↑(2 ^ j 3 * 2 ^ j 2 * 2 ^ j 0 * (F / K.1.1) * 2 ^ j 4) * (↑(2 ^ (j 0 + 1) * (F / K.1.1) * 2 ^ (j 4 + 1)) ^ (2 * ε) * ↑(K.1.2.1 * 2 ^ (j 2 + 1) + 2 ^ (j 0 + 1) * (F / K.1.1) * 2 ^ (j 4 + 1)) ^ ε) + ∑ L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x (εSupport / 2) R S M Z K b j cap positive) c) with wGramNumerator K a L ≠ 0, |wGramWeight K β ζ L| * wGramFouvryCost κ Cnonzero a R S M Z K j cap L

Concrete five-small exponent, with the local cardinal and both power envelopes expanded in the original energy bound. No base sum survives.