A nonzero polynomial determinant in the generic slope parameters. For a positioned irreducible equation with a smooth origin, the minor is constructed over the parameter polynomial ring, by descent from its fraction field.

A smooth rational point supplies a nonzero closed-form coefficient minor for an irreducible plane equation in characteristic zero or large characteristic. The base field need not be algebraically closed.

A smooth rational point on an irreducible plane curve implies geometric irreducibility. The proof uses the faithful formal branch, extends its coordinate algebra to every field, and identifies the resulting prime ideal in the polynomial ring over that field.

theorem CCDN.irreducible_map_of_smooth_plane_point {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (z : Fin 2 → K) (j : Fin 2) (hz : (MvPolynomial.eval z) f = 0) (hj : (MvPolynomial.eval z) ((MvPolynomial.pderiv j) f) ≠ 0) : Irreducible ((MvPolynomial.map (algebraMap K L)) f)

An irreducible plane equation with a smooth rational point remains irreducible over every extension field. The base field need not be perfect.

theorem CCDN.genericPlaneMap_smooth_monic {K : Type u_1} {σ : Type u_2} [Field K] (d : ℕ) (hd : 0 < d) (f : MvPolynomial (Option σ) K) (hf : Irreducible f) (hm : ((MvPolynomial.optionEquivLeft K σ) f).Monic) (hdeg : ((MvPolynomial.optionEquivLeft K σ) f).natDegree = d) (hz : (MvPolynomial.eval 0) f = 0) (hs : (MvPolynomial.eval 0) ((MvPolynomial.pderiv none) f) ≠ 0) : Irreducible ((genericPlaneMap K (FractionRing (MvPolynomial σ K)) σ) f) ∧ (MvPolynomial.eval 0) ((genericPlaneMap K (FractionRing (MvPolynomial σ K)) σ) f) = 0 ∧ (MvPolynomial.eval 0) ((MvPolynomial.pderiv 0) ((genericPlaneMap K (FractionRing (MvPolynomial σ K)) σ) f)) ≠ 0 ∧ ((bivariatePolynomialEquiv (FractionRing (MvPolynomial σ K))) ((genericPlaneMap K (FractionRing (MvPolynomial σ K)) σ) f)).Monic ∧ ((bivariatePolynomialEquiv (FractionRing (MvPolynomial σ K))) ((genericPlaneMap K (FractionRing (MvPolynomial σ K)) σ) f)).natDegree = d

Over the fraction field of the slope ring, the generic plane of a positioned irreducible equation with a smooth origin is irreducible, smooth at the origin in the first coordinate, and monic of the same outer degree.

theorem CCDN.exists_genericPlane_minor {K : Type u_1} {σ : Type u_2} [Field K] (d : ℕ) (hd : 0 < d) (f : MvPolynomial (Option σ) K) (hf : Irreducible f) (hm : ((MvPolynomial.optionEquivLeft K σ) f).Monic) (hdeg : ((MvPolynomial.optionEquivLeft K σ) f).natDegree = d) (htotal : f.totalDegree ≤ d) (hchar : CharZeroOrGT K (2 * d ^ 2)) (hz : (MvPolynomial.eval 0) f = 0) (hs : (MvPolynomial.eval 0) ((MvPolynomial.pderiv none) f) ≠ 0) : (closedFormCoefficientMatrix d (genericPlanePolynomial f)).HasNonzeroMinor (2 * d ^ 2 - 1)

In characteristic zero or greater than 2*d^2, a positioned irreducible hypersurface with a smooth origin supplies a nonzero minor polynomial in its plane slopes.