Rational equations and the coefficient-uniform affine plane bound. The sharp finite-field estimate is stated as a proposition, not an axiom.
The finite-field counting obligation PlaneResidueCountBound for every plane equation
of positive degree, with one absolute constant. planeResidueBound discharges it with
C = planeResidueConstant.
Equations
- CCDN.PlaneResidueBound C = ∀ (f : MvPolynomial (Fin 2) ℤ), 0 < f.totalDegree → CCDN.PlaneResidueCountBound C f.totalDegree f
Instances For
theorem
CCDN.rational_scalar_model_irreducible_charZero
{F : Type u_1}
{σ : Type u_2}
[Field F]
[CharZero F]
{f : MvPolynomial σ ℚ}
{g : MvPolynomial σ ℤ}
{a : ℚ}
(ha : a ≠ 0)
(he : (MvPolynomial.map (Int.castRingHom ℚ)) g = MvPolynomial.C a * f)
(hf : Irreducible ((MvPolynomial.map (algebraMap ℚ F)) f))
:
Irreducible ((MvPolynomial.map (Int.castRingHom F)) g)
If an integer polynomial g is a nonzero rational multiple of a rational polynomial f that
is irreducible over a field F of characteristic zero, then g is irreducible over F.
theorem
CCDN.count_rational_plane_of_residue_bound
{F : Type u_1}
[Field F]
[CharZero F]
[IsAlgClosed F]
(f : MvPolynomial (Fin 2) ℚ)
(hir : Irreducible ((MvPolynomial.map (algebraMap ℚ F)) f))
(hd : 0 < f.totalDegree)
{B C : ℝ}
(hB : 1 ≤ B)
(hC : 0 ≤ C)
(hres : PlaneResidueBound C)
:
↑(count (zeroLocus f) B) ≤ 2 * Real.exp 1 * affineNonzeroConstantBound C * curveBound f.totalDegree B
A rational absolutely irreducible equation has the affine bound for every real B>=1. Primitive normalization and every analytic reduction are proved; the sharp finite-field bound is the one explicit counting hypothesis.