theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9WF_level_window {N T δ : ℝ} (hN : 1 ≤ N) (hT : 1 ≤ T) (hTup : T ≤ N ^ (1 / 10)) (hδ : 0 ≤ δ) : N ^ (1 / 2 - δ) ≤ N ^ (5 / 9 - δ) / T ^ (5 / 9) ∧ N ^ (5 / 9 - δ) / T ^ (5 / 9) ≤ N

The original G9 level has positive power growth when delta is strictly below 1/2.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9WF_exists_internal_level_gate {δ η : ℝ} (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hη : 0 < η) (Q₀ : ℝ) : ∃ (N₀ : ℝ), ∀ (N T : ℝ), N₀ ≤ N → 1 ≤ T → T ≤ N ^ (1 / 10) → have Q := N ^ (5 / 9 - δ) / T ^ (5 / 9); 1 ≤ N ∧ 1 ≤ Q ∧ Q₀ ≤ Q ∧ 2 ≤ externalInternalLevel Q η ∧ Q ≤ N

A threshold before every short scale pays the actual internal-level gate. The strict delta cap is needed for positive growth; no endpoint delta=1/2 claim.