The numerical comparison for CCDN Proposition 5. A square grid with floor((d-1)/2)+1 points per side at radius floor((d+1)/4) already gives the stated degree-squared lower bound, with the exact constant 1/5.

theorem CCDN.grid_radius_rpow_le_five_fourths {d : ℕ} (hd : 0 < d) {B : ℝ} (hB : 0 ≤ B) (hsize : 4 * B ≤ ↑d + 1) : B ^ (2 / ↑d) ≤ 5 / 4

The radius used in the grid construction has B^(2/d) at most 5/4.

theorem CCDN.grid_square_card_lower_bound {d : ℕ} (hd : 0 < d) {B : ℝ} (hB : 0 ≤ B) (hsize : 4 * B ≤ ↑d + 1) : ↑d ^ 2 / 5 * B ^ (2 / ↑d) ≤ ↑((d - 1) / 2 + 1) ^ 2

The grid cardinality dominates the exact lower bound in Proposition 5.

theorem CCDN.grid_lower_bound_radius_identity (d : ℕ) (hd : 0 < d) : (d - 1) / 2 - (d - 1) / 4 = (d + 1) / 4

For d > 0, ⌊(d - 1) / 2⌋ - ⌊(d - 1) / 4⌋ = ⌊(d + 1) / 4⌋, relating the grid size to the radius in the numerics for CCDN Proposition 5.

theorem CCDN.grid_lower_bound_radius_pos {d : ℕ} (hd : 3 ≤ d) : 1 ≤ (d + 1) / 4

For d ≥ 3, the grid radius ⌊(d + 1) / 4⌋ is at least 1.

theorem CCDN.grid_lower_bound_radius_size (d : ℕ) : 4 * ↑((d + 1) / 4) ≤ ↑d + 1

The grid radius satisfies 4 ⌊(d + 1) / 4⌋ ≤ d + 1.