Documentation

LeanPool.CCDN.Surface.AffineSurfaceDimensionGrowth

The affine surface bound in every degree at least five. The finitely many degrees below the large-degree threshold are absorbed in one constant.

Removing integer content from the fixed-degree surface estimate. The resulting constant is uniform in all integer coefficients.

theorem CCDN.affine_surface_dimension_growth :
∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin 3) ℤ), HasAbsIrreducibleTopForm f → 5 ≤ f.totalDegree → ∀ (B : ℝ), 1 ≤ B → ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ C * ↑f.totalDegree ^ 18 * B

Corrected CCDN Proposition 4.3.4 in every degree at least five: the surface bound C d^18 B for integer equations in three variables with absolutely irreducible top-degree form.