Coefficients of a primitive surface equation can be restricted to polynomial height in the box radius. The complementary case already has a linear point bound from a degree-at-most-d auxiliary.

noncomputable def CCDN.surfaceCoefficientLogConstant (d : ℕ) : ℝ

The constant N (log N + d) + 1, where N = binom(d + 3, d) is the number of monomials of degree at most d in three variables, in the logarithmic coefficient-height bound for primitive surface equations of degree d.

Equations

• CCDN.surfaceCoefficientLogConstant d = ↑((3 + d).choose d) * (Real.log ↑((3 + d).choose d) + ↑d) + 1

theorem CCDN.surfaceCoefficientLogConstant_pos (d : ℕ) : 0 < surfaceCoefficientLogConstant d

The coefficient-height constant surfaceCoefficientLogConstant d is positive.

theorem CCDN.primitive_surface_coefficient_reduction (f : MvPolynomial (Fin 3) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) {B : ℝ} (hB : 1 ≤ B) : Real.log ↑(integerCoefficientHeight f) ≤ surfaceCoefficientLogConstant f.totalDegree * (Real.log B + 1) ∨ ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ 3 * ↑f.totalDegree ^ 2 * B

The alternative to controlled coefficient height is already O(d²B). The height constant depends on the degree alone.