theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_gram_fixedOrder (k m : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (V : Finset (WExtractedTuple × ℤ)) (β ζ : ℕ → ℝ), (∀ n ∈ N, 0 < n) → (∀ n ∈ N, ↑n ≤ X) → 0 ≤ R → 0 ≤ S → S ≤ X → 0 < M → 0 < Z → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau m) s)) → V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K → ∀ L ∈ wGramLabels V, |wGramWeight K (betaClean β a) ζ L| ≤ (C * X ^ δ) ^ 4

The occupied Gram labels retain the genuine beta/zeta arguments; fixed orders, not an assumed numerical envelope, pay their four factors.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_prefix_fixedOrder (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 → ∃ 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 ^ δ) ^ 6 * (8 * 2 ^ j 1 * 2 ^ j 3 * T) * wSeparatedCorrelationEnergy x N S (wAnalyticPrefix U cap) c K (betaClean β a) ζ a

This consumes the already-proved original prefix Cauchy theorem. The only remaining energy is the existing genuine separated energy, not a new abstract input or an unweighted interval replacement.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_wellFactorable_envelopes (k m : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (N : Finset ℕ) (β c₀ : ℕ → ℝ) (L R S : ℝ), (∀ n ∈ N, ↑n ≤ X) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → SignedWellFactorable m L c₀ → 1 ≤ R → 1 ≤ S → R * S = L → ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R γ ∧ factorSupported S ζ ∧ (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) ∧ (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) ∧ c₀ = factorConvolution γ ζ ∧ ∀ (a : ℤ) (ξ : ℝ), (∀ n ∈ N, |betaClean β a n| ≤ C * X ^ δ) ∧ (∀ (n : ℕ), ↑n ≤ X → |γ n| ≤ C * X ^ δ) ∧ (∀ (n : ℕ), ↑n ≤ X → |ζ n| ≤ C * X ^ δ) ∧ ∀ (n : ℕ), ↑n ≤ X → |factorConvolution γ (betaLowOmega ζ ξ) n| ≤ C * X ^ δ

Legal WF splitting supplies exactly the factor hypotheses used above. The split precedes the signed shift, cutoffs and all occupied Gram carriers.