Documentation

LeanPool.CCDN.ProjectiveCurveBound

CCDN Theorem 2 in every ambient dimension. Degree is the slope of the homogeneous Hilbert function. The height and count use rational projective points. All projection and plane-counting inputs are proved; the count with an explicit constant is projective_curve_count, in CCDN.Curve.ProjectiveCurveCount.

CCDN (2020), Theorem 2: the bound ProjectiveCurveBound.