Explicit exponent margins for the small-degree surface argument. The estimates hold uniformly for every degree at least five and absorb any fixed power of the logarithm; geometric covering hypotheses are separate.

theorem CCDN.surface_inverse_sqrt_le_nine_twentieths {d : ℕ} (hd : 5 ≤ d) : 1 / √↑d ≤ 9 / 20

For every natural number d ≥ 5, 1 / √d ≤ 9 / 20.

theorem CCDN.logarithm_add_one_pow_le_rpow (k : ℕ) {ε B : ℝ} (hε : 0 < ε) (hB : 1 ≤ B) : (Real.log B + 1) ^ k ≤ ↑k.factorial / ε ^ k * Real.exp ε * B ^ ε

A fixed logarithmic power costs at most any prescribed positive power, with an explicit constant independent of the box radius.

theorem CCDN.surface_nonlinear_polylog_weight {d : ℕ} (hd : 5 ≤ d) (k : ℕ) {B : ℝ} (hB : 1 ≤ B) : B ^ (1 / √↑d + 1 / 2) * (Real.log B + 1) ^ k ≤ ↑k.factorial / (1 / 20) ^ k * Real.exp (1 / 20) * B

Retained nonlinear curves with square-root box count and any fixed polylogarithmic loss contribute O(B) once their number has the B^(1/sqrt(d)) scale, for every d>=5.