Proof of ingredient statement ingredient existence.

theorem AVenhance.Proofs.Ingredients.nonempty (β : ℝ) (h1 : 1 < β) (h2 : β < 4 / 3) : ∃ (C₀ : ℝ), 1 ≤ C₀ ∧ ∀ (Λ : ℕ), 2 ^ 7 ≤ Λ → ∃ (I : Ingredients β), I.Λ = Λ ∧ I.Czeta ≤ C₀ ∧ I.Cxi ≤ C₀ ∧ I.Chat ≤ C₀