The numerical component of the corrected surface estimate. The auxiliary degree contributes a further factor d to the intersection degree, giving d^18 after taking fourth powers.

theorem CCDN.surface_inverse_sqrt_le_quarter {d : ℕ} (hd : 16 ≤ d) : 1 / √↑d ≤ 1 / 4

For d ≥ 16, the exponent 1 / √d is at most 1 / 4.

theorem CCDN.sum_curveBound_le_surface_degree_budget {ι : Type u_1} (s : Finset ι) (δ : ι → ℕ) {d : ℕ} (hd : 16 ≤ d) {B C : ℝ} (hC : 0 ≤ C) (hB : 1 ≤ B) (hδ : ∀ i ∈ s, 2 ≤ δ i) (hD : ∑ i ∈ s, ↑(δ i) ≤ C * ↑d ^ (9 / 2) * B ^ (1 / √↑d)) : ∑ i ∈ s, curveBound (δ i) B ≤ Real.exp 1 * (480 * C + 2 * C ^ 4) * ↑d ^ 18 * B

The whole numerical contribution of the nonlinear curve components in the surface argument, with the corrected d^18 factor.