Documentation

LeanPool.CCDN.LowerBound.ProjectivePlaneLowerBound

The lower bound of CCDN Proposition 5 for projective plane equations, with its exact constant 1/5: the grid construction for degree at least four, and two rational points for smaller degrees.

theorem CCDN.projective_plane_lower_bound (d : ℕ) (hd : 0 < d) :
∃ (F : MvPolynomial (Fin 3) ℚ) (B : ℕ), 1 ≤ B ∧ F.IsHomogeneous d ∧ F.totalDegree = d ∧ AbsolutelyIrreducibleRat F ∧ ↑d ^ 2 / 5 * ↑B ^ (2 / ↑d) ≤ ↑(projectiveCount (projectiveZeroLocus F) ↑B)

For every d>0 there is an absolutely irreducible projective plane curve of degree d and an integer B≥1 with N(X,B)≥d² B^(2/d)/5.