The sharp weighted degree of a full standard-monomial prefix for an affine surface. The coefficient 2/3 of the square-root rank is retained, with an explicit linear error depending only on the equation degree.

theorem CCDN.surface_standard_monomial_weight {K : Type u_1} [Field K] (f : MvPolynomial (Fin 3) K) (hf : f ≠ 0) (hd : 0 < f.totalDegree) {M : ℕ} (hM : f.totalDegree ≤ M) : have S := standardMonomialPrefix (Ideal.span {f}) MonomialOrder.degLex M; ∑ a ∈ S, ↑(Finsupp.degree a) ≤ 2 / 3 * ↑S.card * √(2 * ↑S.card / ↑f.totalDegree) + (2 * ↑f.totalDegree + 2) * ↑S.card

Standard monomials up to degree M have weighted degree at most (2/3)s sqrt(2s/d)+(2d+2)s, where s is their cardinality and d is the surface equation degree.