Combining the scaling-prime, large-coefficient and small-box branches. The plane theorem assumes the sharp finite-field count and a nonzero constant term; a later translation removes the second hypothesis.

The affine exponent 1/d with the scaling prime constructed from Mertens. This branch assumes a nonzero constant coefficient of small logarithmic height; the sharp finite-field count is an explicit geometric hypothesis.

theorem CCDN.plane_finite_count_small_constant_coefficient {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {t : ℕ} (f : MvPolynomial (Fin 2) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f)) (hd : 0 < f.totalDegree) (hf0 : f.coeff 0 ≠ 0) (z : Fin t → Fin 2 → ℤ) (hinj : Function.Injective z) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) {B C : ℝ} (hB : scalingPrimeRatio ≤ B) (hheight : Real.log |↑(f.coeff 0)| < B / scalingPrimeRatio) (hbox : ∀ (i : Fin t), InBox (z i) B) (hC : 0 ≤ C) (hcount : PlaneResidueCountBound C f.totalDegree f) : ↑t ≤ (38 + 8 * Real.exp (heightDeterminantError C + 20) + 2 * Real.exp (heightDeterminantError C + 23) * Real.exp 14 * Real.exp 2 * scalingPrimeRatio) * ↑f.totalDegree ^ 3 * B ^ (1 / ↑f.totalDegree) * (Real.log B + ↑f.totalDegree)

Affine plane count with exponent 1 / d when the constant coefficient is nonzero and of small logarithmic height: if f is a primitive integer polynomial of degree d ≥ 1, absolutely irreducible over an algebraically closed field of characteristic zero, with log |f(0)| < B / scalingPrimeRatio and satisfying the finite-field residue count hypothesis, then the number of its integer zeros in the box of size B ≥ scalingPrimeRatio is at most an explicit constant times d ^ 3 * B ^ (1 / d) * (log B + d). The proof reduces modulo a scaling prime.

noncomputable def CCDN.affineSmallBoxScale : ℝ

The threshold constant (12 * scalingPrimeRatio) ^ 2 separating small boxes B ≤ affineSmallBoxScale * d ^ 2 from large boxes in the affine plane count.

Equations

• CCDN.affineSmallBoxScale = (12 * CCDN.scalingPrimeRatio) ^ 2

noncomputable def CCDN.affineNonzeroConstantBound (C : ℝ) : ℝ

The constant of plane_finite_count_nonzero_constant for residue constant C, the sum of the constants of its regimes, with E = heightDeterminantError C: the scaled small-coefficient regime (plane_finite_count_small_constant_coefficient) costs 38 + 8 exp (E + 20) + 2 exp (E + 23) e¹⁴ e² · scalingPrimeRatio, and the small-box regime (small_box_unscaled_degree_bound) costs log S + 6 + 2 exp (E + 23) e¹⁴ exp (2 log S + 6) with S = affineSmallBoxScale. The large-coefficient constant 34 + 8 exp (E + 20) is dominated by the first. The numerical constants are explained in projectivePlaneAbsoluteConstant.

Equations

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

theorem CCDN.affineNonzeroConstantBound_pos (C : ℝ) : 0 < affineNonzeroConstantBound C

The constant affineNonzeroConstantBound C is positive.

theorem CCDN.degree_four_le_curveBound {d : ℕ} (hd : 0 < d) {B : ℝ} (hB : 1 ≤ B) : ↑d ^ 4 ≤ curveBound d B

For d ≥ 1 and B ≥ 1, the curve bound curveBound d B is at least d ^ 4.

theorem CCDN.plane_finite_count_nonzero_constant {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {t : ℕ} (f : MvPolynomial (Fin 2) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f)) (hd : 0 < f.totalDegree) (hf0 : f.coeff 0 ≠ 0) (z : Fin t → Fin 2 → ℤ) (hinj : Function.Injective z) {B C : ℝ} (hzB : IsBoxZeroFamily f B z) (hC : 0 ≤ C) (hcount : PlaneResidueCountBound C f.totalDegree f) : ↑t ≤ affineNonzeroConstantBound C * curveBound f.totalDegree B

Coefficient-uniform affine plane count for nonzero constant term and every B>=1.