The singular locus of an irreducible rational hypersurface has a coefficient-uniform codimension-two integer point bound. A nonzero partial derivative gives the proper intersection used in the count.

def CCDN.singularHypersurfaceLocus {n : ℕ} (f : MvPolynomial (Fin n) ℚ) : Set (RatPoint n)

The rational points of the singular locus of the hypersurface f = 0: the common zeros of f and all its partial derivatives.

Equations

• CCDN.singularHypersurfaceLocus f = {x : CCDN.RatPoint n | (MvPolynomial.eval x) f = 0 ∧ ∀ (j : Fin n), (MvPolynomial.eval x) ((MvPolynomial.pderiv j) f) = 0}

theorem CCDN.singular_hypersurface_dimension_growth {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℚ) (hir : Irreducible f) {B : ℝ} (hB : 1 ≤ B) : ↑(count (singularHypersurfaceLocus f) B) ≤ (3 * (↑n + 2)) ^ n * ↑f.totalDegree ^ 2 * B ^ n

The singular locus of an irreducible rational hypersurface in n + 2 variables has at most (3 * (n + 2)) ^ n * deg f ^ 2 * B ^ n integral points of height at most B, for every B ≥ 1.