The elementary linear case completes the uniform plane-equation bound in every positive degree.
theorem
CCDN.projective_plane_equation_bound
{d : ℕ}
(f : MvPolynomial (Fin 3) ℚ)
(hf : f.IsHomogeneous d)
(hd : 0 < d)
(hir : Irreducible f)
{B : ℝ}
(hB : 1 ≤ B)
:
↑(projectiveCount (projectiveZeroLocus f) B) ≤ projectivePlaneAbsoluteConstant * ↑d ^ 4 * B ^ (2 / ↑d)
Uniform CCDN Theorem 2 for rational projective plane equations, in every positive degree and for every real B >= 1.