The unit-scaled model gives a coefficient-uniform 2/d fallback and a large-coefficient O(d^4) count, without requiring a scaling prime.
theorem
CCDN.PrimitiveIntegerPolynomial.scaledHomogenize_one
{n : ℕ}
{f : MvPolynomial (Fin n) ℤ}
(hf : PrimitiveIntegerPolynomial f)
(d : ℕ)
:
The homogenization (with scaling factor 1) of a primitive integer polynomial is
primitive.
theorem
CCDN.unscaled_plane_finite_count
{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)
(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 ≤ max (↑f.totalDegree * scaledPlaneAuxiliaryDegreeBound f.totalDegree C ((↑f.totalDegree + 1) * B) 1)
((34 + 8 * Real.exp (heightDeterminantError C + 20)) * ↑f.totalDegree ^ 4)
Coefficient positioning removes the coefficient height from the 2/d fallback bound. This holds for any primitive absolutely irreducible equation.
theorem
CCDN.unscaled_plane_finite_count_large_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)
(z : Fin t → Fin 2 → ℤ)
(hinj : Function.Injective z)
{B C : ℝ}
(hzB : IsBoxZeroFamily f B z)
(hC : 0 ≤ C)
(m : Fin 2 →₀ ℕ)
(hm : f.coeff m ≠ 0)
(hheight : 4 * ↑f.totalDegree * Real.log ((↑f.totalDegree + 1) * B) ≤ Real.log |↑(f.coeff m)|)
(hcount : PlaneResidueCountBound C f.totalDegree f)
:
A sufficiently large coefficient forces the large-height branch and gives O(d^4).