A prime-scaled plane point bound with the arbitrary coefficient height eliminated. The sharp finite-field count and a suitable scaling prime remain explicit hypotheses.
The auxiliary degree bound for a plane equation of degree d after translation into a box
of radius R and scaling by p, with residue constant C. The constants 23 and exp 14 are
explained in projectivePlaneAbsoluteConstant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CCDN.scaled_model_plane_count_bounds
{F : Type u_1}
[Field F]
[CharZero F]
[IsAlgClosed F]
{t : ℕ}
(f : MvPolynomial (Fin 2) ℤ)
(hir : Irreducible ((MvPolynomial.map (Int.castRingHom F)) f))
(hd : 0 < f.totalDegree)
(scale : ℤ)
(hscale : 1 ≤ scale)
(z : Fin t → Fin 2 → ℤ)
{B C : ℝ}
(hzB : IsBoxZeroFamily f B z)
(hscaleB : ↑scale ≤ B)
(hC : 0 ≤ C)
(hcount : PlaneResidueCountBound C f.totalDegree f)
(hsection :
∀ (a : Fin 2 → ℤ) (M : ℕ) (g : MvPolynomial (Fin 3) ℤ),
(IsPointAuxiliary ((homogeneousTranslation ℤ a) (scaledHomogenize f.totalDegree scale f)) g M
fun (i : Fin t) (j : Fin (2 + 1)) => (MvPolynomial.eval (z i)) (scaledModelCoordinates scale a j)) →
t ≤ f.totalDegree * M)
:
↑t ≤ max (↑f.totalDegree * scaledPlaneAuxiliaryDegreeBound f.totalDegree C ((↑f.totalDegree + 1) * B) ↑scale)
((34 + 8 * Real.exp (heightDeterminantError C + 20)) * ↑f.totalDegree ^ 4) ∧ ∀ (m : Fin 2 →₀ ℕ),
f.coeff m ≠ 0 →
4 * ↑f.totalDegree * Real.log ((↑f.totalDegree + 1) * B) ≤ Real.log |↑(f.coeff m)| →
↑t ≤ (34 + 8 * Real.exp (heightDeterminantError C + 20)) * ↑f.totalDegree ^ 4
Coefficient positioning gives both count bounds for any positive integer scale. The callback supplies the proper-section estimate for that scale.
theorem
CCDN.scaled_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)
{p : ℕ}
(hp : Nat.Prime p)
(hp0 : ¬↑p ∣ f.coeff 0)
(z : Fin t → Fin 2 → ℤ)
(hinj : Function.Injective z)
{B C : ℝ}
(hzB : IsBoxZeroFamily f B z)
(hpB : ↑p ≤ B)
(hC : 0 ≤ C)
(hcount : PlaneResidueCountBound C f.totalDegree f)
:
↑t ≤ max (↑f.totalDegree * scaledPlaneAuxiliaryDegreeBound f.totalDegree C ((↑f.totalDegree + 1) * B) ↑p)
((34 + 8 * Real.exp (heightDeterminantError C + 20)) * ↑f.totalDegree ^ 4)
Count original integer plane points using the translated scaled model. The determinant estimate is applied to polynomial columns on the original curve, so its sharp residue-count hypothesis concerns that curve.