Curves that are irreducible over the base field but split over an extension have at most d^2+d projective base-field points.

theorem CCDN.projective_plane_rational_count {d : ℕ} (f : MvPolynomial (Fin 3) ℚ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hir : Irreducible f) {B : ℝ} (hB : 1 ≤ B) : ↑(projectiveCount (projectiveZeroLocus f) B) ≤ projectivePlaneAbsoluteConstant * ↑d ^ 4 * B ^ (2 / ↑d)

The uniform plane bound for every rational irreducible homogeneous equation of degree at least two, whether or not geometrically irreducible.