Homogeneous auxiliary polynomials for bounded primitive projective points, with explicit degrees in both coefficient-height ranges.

The coefficient-sensitive determinant comparison for bounded primitive integer representatives of projective plane points.

theorem CCDN.projective_auxiliary_small_height_degree {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {d t : ℕ} (order : MonomialOrder (Fin 3)) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 2 ≤ d) {H : ℝ} (hchart : IsBoundedPlaneCurve F ((affineChart 2) f) d H) {B : ℝ} {z : Fin t → IntPoint 3} (hzB : IsPrimitiveBoxZeroFamily f B z) (hheight : Real.log |↑(order.leadingCoeff f)| ≤ 4 * ↑d * Real.log B) : ∃ (M : ℕ), ↑M ≤ ↑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 ∧ ∃ (g : MvPolynomial (Fin 3) ℤ), IsPointAuxiliary f g M z

Small-height auxiliary form for a projective plane curve: if f is an integral ternary form of degree d ≥ 2 whose affine chart is a bounded plane curve of height H, z is a family of primitive integral zeros of f in the box of radius B, and the leading coefficient of f has logarithm at most 4 d log B, then there is an auxiliary form of explicitly bounded degree M through all the points z i.

theorem CCDN.projective_auxiliary_large_height_degree {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {d t : ℕ} (order : MonomialOrder (Fin 3)) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 2 ≤ d) {H : ℝ} (hchart : IsBoundedPlaneCurve F ((affineChart 2) f) d H) {B : ℝ} {z : Fin t → IntPoint 3} (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) : ∃ (M : ℕ), ↑M ≤ (34 + 8 * Real.exp (heightDeterminantError projectivePlaneDeterminantConstant + 6 + T)) * ↑d ^ 3 ∧ ∃ (g : MvPolynomial (Fin 3) ℤ), IsPointAuxiliary f g M z

Large-height auxiliary form for a projective plane curve: if f is an integral ternary form of degree d ≥ 2 whose affine chart is a bounded plane curve of height H, z is a family of primitive integral zeros of f in the box of radius B, 4 d log B ≤ log H, and H is at most the leading coefficient of f times exp (T d²), then there is an auxiliary form through all the points z i of degree at most (34 + 8 exp (heightDeterminantError projectivePlaneDeterminantConstant + 6 + T)) d³.