Dimension growth for non-geometrically-irreducible rational hypersurfaces in every ambient dimension. The dependence on the degree is quadratic; the explicit constant depends only on dimension.
theorem
CCDN.proper_intersection_count_le_box
{n d : ℕ}
(f g : CoordinatePolynomial (n + 2))
(hf : Prime f)
(hfg : ¬f ∣ g)
(hfd : MvPolynomial.totalDegree f ≤ d)
(hgd : MvPolynomial.totalDegree g ≤ d)
{B : ℝ}
(hB : 0 ≤ B)
:
If f is a prime rational polynomial in n + 2 variables not dividing g, and both have
total degree at most d, then the common zero set of f and g has at most
(n + 2) ^ n * d ^ 2 * (2 * B + 1) ^ n integral points of height at most B.
theorem
CCDN.nonabsolute_hypersurface_dimension_growth
{K : Type u_1}
[Field K]
[Algebra ℚ K]
{n : ℕ}
(f : CoordinatePolynomial (n + 2))
(hir : Irreducible f)
(hred : ¬Irreducible ((MvPolynomial.map (algebraMap ℚ K)) f))
{B : ℝ}
(hB : 1 ≤ B)
:
An irreducible rational polynomial f in n + 2 variables that becomes reducible over some
extension field has at most (3 * (n + 2)) ^ n * deg f ^ 2 * B ^ n integral zeros of height
at most B, for every B ≥ 1.