The positive-dimensional Flag Decomposition Lemma

theorem EGZ.flag_decomposition_lemma_posdim {d : ℕ} (hd : 1 ≤ d) (ε : ℝ) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) : ∃ (δ : ℝ) (Bcard : ℕ), 0 < δ ∧ ∀ (g : ℕ → ℕ), IsGrowing g → ∃ (p₀ : ℕ) (BK : ℕ), 2 ≤ p₀ ∧ 1 ≤ BK ∧ ∀ (p : ℕ) (hp : Nat.Prime p), p₀ < p → ∀ (f : FpCoord p d → ℕ), f ≠ 0 → HasFlagDecompositionConclusion hp f ε δ g Bcard BK

The bounded normalized iteration proves the lemma for the parameter range used by the mass estimates. All constants are chosen before the prime and the input weight, in the required order.