An absolute d^4 B^(2/d) bound for primitive absolutely irreducible homogeneous plane equations of degree at least two.

noncomputable def CCDN.projectivePlaneAbsoluteConstant : ℝ

The absolute constant of projective_plane_primitive_absolute_count. Write E = heightDeterminantError projectivePlaneDeterminantConstant.

• Small coefficient height: the auxiliary degree is at most d + log R + 2 exp (E + 23) d³ (1 + log H / d²) R^(2/d) / |lc|^(1/d²) + 2 (projective_auxiliary_small_height_degree), where 23 = 5 + 2 + 16 collects the archimedean error of plane_rank_archimedean_error and the remainders of the box and coefficient terms in plane_auxiliary_log_degree_bound. Positioning the leading coefficient costs log H ≤ log |lc| + 14 d² (exists_translated_coefficient_position), hence the factor exp 14 (scaled_positioned_height_ratio_le). The translated radius R = (d + 1) B satisfies R^(2/d) ≤ e² B^(2/d), and d + log R + 2 ≤ 5 d³ B^(2/d); this gives exp 2 and the leading 5 (projective_positioned_bound_le).
• Large coefficient height: the auxiliary degree is at least 32 d and at most 32 d + 8 exp (E + 6 + T) d³ + 2 ≤ (34 + 8 exp (E + 6 + T)) d³ (projective_auxiliary_large_height_degree), where 6 = 5 + 1 and the 8 = 2 · 4 come from plane_auxiliary_large_height_log_bound, and T = 14 is the positioning loss; hence E + 20.

Bézout multiplies either degree bound by d.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.projectivePlaneAbsoluteConstant_pos : 0 < projectivePlaneAbsoluteConstant

The constant projectivePlaneAbsoluteConstant is positive.

theorem CCDN.projective_positioned_bound_le {d : ℕ} (hd : 0 < d) {B : ℝ} (hB : 1 ≤ B) : max (↑d * scaledPlaneAuxiliaryDegreeBound d projectivePlaneDeterminantConstant ((↑d + 1) * B) 1) ((34 + 8 * Real.exp (heightDeterminantError projectivePlaneDeterminantConstant + 20)) * ↑d ^ 4) ≤ projectivePlaneAbsoluteConstant * ↑d ^ 4 * B ^ (2 / ↑d)

For d ≥ 1 and B ≥ 1, the bound of projective_plane_finite_count_positioned is at most projectivePlaneAbsoluteConstant * d ^ 4 * B ^ (2 / d).

theorem CCDN.projective_plane_primitive_absolute_count {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {d : ℕ} (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) {B : ℝ} (hB : 1 ≤ B) : ↑(projectiveCount (projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ projectivePlaneAbsoluteConstant * ↑d ^ 4 * B ^ (2 / ↑d)

The full real-radius bound for primitive absolutely irreducible plane equations of degree >= 2, including their points at infinity.

theorem CCDN.projective_plane_rational_absolute_count {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {d : ℕ} (f : MvPolynomial (Fin 3) ℚ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hir : Irreducible ((MvPolynomial.map (algebraMap ℚ K)) f)) {B : ℝ} (hB : 1 ≤ B) : ↑(projectiveCount (projectiveZeroLocus f) B) ≤ projectivePlaneAbsoluteConstant * ↑d ^ 4 * B ^ (2 / ↑d)

The bound for an arbitrary rational absolutely irreducible plane equation, which need not be primitive or integral. The constant is independent of its coefficients, degree, and real height radius.