Irreducible base-field plane curves that split over an extension have at most d² base-field points. The proof uses linear coefficient descent and Bézout.

theorem CCDN.nonabsolute_plane_points_card_le {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] [Fintype ι] (f : MvPolynomial (Fin 2) k) (hf : Irreducible f) (hd : 0 < f.totalDegree) (hred : ¬Irreducible ((MvPolynomial.map (algebraMap k K)) f)) (z : ι → Fin 2 → k) (hinj : Function.Injective z) (hz : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0) : Fintype.card ι ≤ f.totalDegree ^ 2

Splitting over any extension, Galois or not, gives the d² bound on base-field points.