A single signed-WF consumer with its split chosen before the shift and all subsequent frequency/key/cell/prefix choices. The loss is any prescribed positive power, rather than an uninstantiated coefficient envelope.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_wellFactorable_prefix_subpower (k m : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 1 ≤ x → ∀ (N Q : Finset ℕ) (β c₀ : ℕ → ℝ) (L R S T : ℝ), (∀ n ∈ N, 0 < n) → (∀ q ∈ Q, 0 < q) → (∀ n ∈ N, ↑n ≤ x) → (∀ q ∈ Q, ↑q ≤ x) → 1 ≤ R → 1 ≤ S → R ≤ x → S ≤ x → R * S = L → 0 ≤ T → (∀ n ∈ N, ↑n ≤ 2 * T) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → SignedWellFactorable m L c₀ → ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R γ ∧ factorSupported S ζ ∧ (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) ∧ (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) ∧ c₀ = factorConvolution γ ζ ∧ ∀ (H : ℕ → ℕ → ℕ) (a : ℤ) (η : ℝ) (b : ℕ) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)), U ⊆ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive → ∃ cap ∈ LiLiuPrereqFouvry.Rectangle.box (wAnalyticBoxLo j) (wAnalyticBoxHi j), wAnalyticBlockPrefixMax (wCoprimeFiber x N S U c) j (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a ^ 2 ≤ C * x ^ δ * (8 * 2 ^ j 1 * 2 ^ j 3 * T) * wSeparatedCorrelationEnergy x N S (wAnalyticPrefix U cap) c K (betaClean β a) ζ a

The original WF data produce the factors and pay the actual first coefficient of order 2m. C precedes the family, scale, shift and split. The residual on the right is exactly the pre-existing separated energy.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_outerMass_subpower (k m : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (x η R S T : ℝ) (b : ℕ) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) (β γ ζ : ℕ → ℝ), (∀ n ∈ N, 0 < n) → (∀ q ∈ Q, 0 < q) → (∀ n ∈ N, ↑n ≤ X) → (∀ q ∈ Q, ↑q ≤ X) → 0 ≤ R → 0 ≤ S → R ≤ X → S ≤ X → 0 ≤ T → (∀ n ∈ N, ↑n ≤ 2 * T) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) → U ⊆ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive → wCorrelationOuterMass x N S U c K (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ≤ C * X ^ δ * (8 * 2 ^ j 1 * 2 ^ j 3 * T)

The same arbitrary small power pays the literal outer L2 mass.