theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayZero_envelope {x T ε : ℝ} (hx : 4 ≤ x) (_hT : 0 ≤ T) (hTx : T ≤ x) (hε : 0 ≤ ε) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (hF : ↑F ≤ 2 * T) (hn : 2 ^ j 2 ≤ 2 * T) (hs : 2 ^ j 4 ≤ x) (hd : ↑K.1.2.1 ≤ x) (hH : 2 ^ j 0 ≤ x ^ 10) : wGramResonanceScaleEnvelope K F j ε ≤ x ^ (44 * ε)

Both literal resonance bases have polynomial size; no divisor envelope input.