Existence

theorem EGZ.flag_decomposition_lemma (d : ℕ) (ε : ℝ) : 0 < ε → ∃ (δ : ℝ) (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

Theorem 4.13, the Flag Decomposition Lemma, with all uniformity made explicit.

The assertion 0 < δ is the formal content of the paper's notation δ ≫_{d,ε} 1; it does not mean that δ is numerically greater than one. The harmless requirements 2 ≤ p₀ and 1 ≤ BK expose bounds used by the centered-lift and reciprocal-power formulations.

theorem EGZ.theorem_4_13 (d : ℕ) (ε : ℝ) : 0 < ε → ∃ (δ : ℝ) (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

Numbered alias for the Flag Decomposition Lemma.