The elementary linear box bound for prime curves in affine three-space. A transcendental coordinate has fibers of size at most the affine Hilbert degree, and the integer box has only 2 floor(B)+1 values of that coordinate.
theorem
CCDN.curve_count_le_degree_mul_box_side
(I : Ideal (CoordinatePolynomial 3))
[I.IsPrime]
(hheight : I.height = 2)
{d : ℕ}
(hdegree : HasAffineCurveDegree I d)
{B : ℝ}
(hB : 0 ≤ B)
:
CCDN's elementary degree-times-box-side bound, for rational prime curves in affine three-space.