Projective point counts obtained from integral homogeneous auxiliary polynomials and projective Bézout.

theorem CCDN.projective_points_small_height_bound {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {d t : ℕ} (order : MonomialOrder (Fin 3)) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 2 ≤ d) (hprim : PrimitiveIntegerPolynomial f) {H : ℝ} (hchart : IsBoundedPlaneCurve K ((affineChart 2) f) d H) (z : Fin t → IntPoint 3) (hz0 : ∀ (i : Fin t), z i ≠ 0) (hinj : Function.Injective fun (i : Fin t) => Projectivization.mk ℚ (rationalPoint (z i)) ⋯) {B : ℝ} (hzB : IsPrimitiveBoxZeroFamily f B z) (hheight : Real.log |↑(order.leadingCoeff f)| ≤ 4 * ↑d * Real.log B) : ↑t ≤ ↑d * (↑d + Real.log B + 2 * Real.exp (heightDeterminantError projectivePlaneDeterminantConstant + 23) * ↑d ^ 3 * (1 + Real.log H / ↑d ^ 2) * B ^ (2 / ↑d) / |↑(order.leadingCoeff f)| ^ (1 / ↑d ^ 2) + 2)

Small-height count of projective points on a plane curve: if f is a primitive integral ternary form of degree d ≥ 2 whose affine chart is a bounded plane curve of height H, and the leading coefficient of f has logarithm at most 4 d log B, then a family of primitive integral zeros of f in the box of radius B, pairwise distinct as projective points, has at most d times the small-height auxiliary degree bound members.

theorem CCDN.projective_points_large_height_bound {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {d t : ℕ} (order : MonomialOrder (Fin 3)) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 2 ≤ d) (hprim : PrimitiveIntegerPolynomial f) {H : ℝ} (hchart : IsBoundedPlaneCurve K ((affineChart 2) f) d H) (z : Fin t → IntPoint 3) (hz0 : ∀ (i : Fin t), z i ≠ 0) (hinj : Function.Injective fun (i : Fin t) => Projectivization.mk ℚ (rationalPoint (z i)) ⋯) {B : ℝ} (hzB : IsPrimitiveBoxZeroFamily f B z) (T : ℝ) (hT : 0 ≤ T) (hheight : 4 * ↑d * Real.log B ≤ Real.log H) (hposition : Real.log H ≤ Real.log |↑(order.leadingCoeff f)| + T * ↑d ^ 2) : ↑t ≤ (34 + 8 * Real.exp (heightDeterminantError projectivePlaneDeterminantConstant + 6 + T)) * ↑d ^ 4

Large-height count of projective points on a plane curve: if f is a primitive integral ternary form of degree d ≥ 2 whose affine chart is a bounded plane curve of height H, with 4 d log B ≤ log H and H at most the leading coefficient of f times exp (T d²), then a family of primitive integral zeros of f in the box of radius B, pairwise distinct as projective points, has at most (34 + 8 exp (heightDeterminantError projectivePlaneDeterminantConstant + 6 + T)) d⁴ members.