Universal-constant absorption for the single-scale estimate

The proof of Proposition 5.10 repeatedly produces factors C^m, and a bounded number of rough local operations additionally costs a fixed polynomial such as m^20. The statement uses the half-power C₀^(m/2). This file proves once and for all that these losses can be absorbed by choosing one C₀ > 1000 depending only on the fixed inputs C,d, uniformly in m.

theorem Anderson4D.nat_pow_fixed_le_two_pow_fixed_pow (m d : ℕ) : m ^ d ≤ (2 ^ d) ^ m

The elementary uniform bound m^d ≤ (2^d)^m.

theorem Anderson4D.real_natCast_pow_fixed_le_two_pow_fixed_pow (m d : ℕ) : ↑m ^ d ≤ (2 ^ d) ^ m

Real-cast form of the fixed-polynomial exponential bound.

theorem Anderson4D.exists_large_halfPower_dominates_natPower (C : ℝ) (hC : 0 ≤ C) : ∃ (C₀ : ℝ), 1000 < C₀ ∧ ∀ (m : ℕ), C ^ m ≤ C₀ ^ (↑m / 2)

Every nonnegative exponential loss C^m is dominated by the paper's half-power format after choosing one C₀ > 1000.

theorem Anderson4D.exists_large_halfPower_dominates_polynomial (C : ℝ) (hC : 0 ≤ C) (d : ℕ) : ∃ (C₀ : ℝ), 1000 < C₀ ∧ ∀ (m : ℕ), C ^ m * ↑m ^ d ≤ C₀ ^ (↑m / 2)

The form needed after the rough-block audit following (5.92): a fixed polynomial m^d times an exponential is still absorbed by one C₀^(m/2).

theorem Anderson4D.exists_large_halfPower_dominates_twenty (C : ℝ) (hC : 0 ≤ C) : ∃ (C₀ : ℝ), 1000 < C₀ ∧ ∀ (m : ℕ), C ^ m * ↑m ^ 20 ≤ C₀ ^ (↑m / 2)

Specialized polynomial absorption for the paper's m^20 loss.