Sharp leading constant for sums of surface standard-monomial degrees. The numerical argument retains 2/3 of the cutoff in the weighted rank.

theorem CCDN.surface_rank_prefix_sum_lower (H : ℕ → ℕ) {d M : ℕ} (hdM : d ≤ M) (hlower : ∀ (k : ℕ), d ≤ k → ↑d * (↑k - ↑d + 1) ^ 2 / 2 ≤ ↑(H k)) : ↑d * (↑M - ↑d) ^ 3 / 6 ≤ ∑ k ∈ Finset.range M, ↑(H k)

If H k ≥ d * (k - d + 1) ^ 2 / 2 for all k ≥ d, then for M ≥ d the prefix sum ∑ k < M, H k is at least d * (M - d) ^ 3 / 6.

theorem CCDN.surface_weight_root_bound {d M s W : ℝ} (hd : 0 < d) (hM : d ≤ M) (hs : 0 ≤ s) (R : ℝ) (hR : 0 ≤ R) (hroot : d * R ^ 2 = 2 * s) (hlo : M - d ≤ R) (hhi : R ≤ M + 2) (hweight : W + d * (M - d) ^ 3 / 6 ≤ M * s) : W ≤ 2 / 3 * s * R + (2 * d + 2) * s

Let R ≥ 0 satisfy d * R ^ 2 = 2 * s and M - d ≤ R ≤ M + 2, where 0 < d ≤ M and s ≥ 0. If W + d * (M - d) ^ 3 / 6 ≤ M * s, then W ≤ (2 / 3) * s * R + (2 * d + 2) * s.