Recurring hypotheses of the counting theorems

The determinant-method counting theorems are stated for a finite family of integral points and an equation with bounded coefficients. These bundles name the recurring groups of hypotheses.

• CCDN.IsBoxZeroFamily f B z: the points z i are integral zeros of f in the box of radius B ≥ 1.
• CCDN.IsPrimitiveBoxZeroFamily f B z: moreover every z i is a primitive integer vector, that is, the reduced representative of a rational projective point.
• CCDN.IsBoundedPlaneCurve F q d H: the integral affine plane equation q has degree d, is irreducible over the field F, and has coefficients bounded by H ≥ 1.
• CCDN.IsIndependentEvaluation f M F z: the evaluation matrix (F j (z i)) of forms of degree M at primitive integral zeros of f has linearly independent rows; this is the input of the determinant lower bounds.
• CCDN.IsSmoothResidueFamily f P a x: the points x i lie in prescribed nonsingular residue classes a p of f modulo the primes p ∈ P; this is the input of the congruence improvement of the determinant lower bound.

structure CCDN.IsBoxZeroFamily {n : ℕ} {ι : Type u_1} (f : MvPolynomial (Fin n) ℤ) (B : ℝ) (z : ι → IntPoint n) : Prop

The points z i are integral zeros of f lying in the box of radius B ≥ 1.

• one_le_radius : 1 ≤ B

  The box radius is at least 1.

• eval_eq_zero (i : ι) : (MvPolynomial.eval (z i)) f = 0

  Every point z i is a zero of f.

• abs_le (i : ι) : InBox (z i) B

  Every point z i lies in the box of radius B.

structure CCDN.IsPrimitiveBoxZeroFamily {n : ℕ} {ι : Type u_1} (f : MvPolynomial (Fin n) ℤ) (B : ℝ) (z : ι → IntPoint n) extends CCDN.IsBoxZeroFamily f B z : Prop

The points z i are primitive integral zeros of f lying in the box of radius B ≥ 1; for a form f these are the reduced representatives of rational projective zeros of f.

• one_le_radius : 1 ≤ B
• eval_eq_zero (i : ι) : (MvPolynomial.eval (z i)) f = 0
• abs_le (i : ι) : InBox (z i) B
• primitive (i : ι) : Finset.univ.gcd (z i) = 1

  The coordinates of every point z i have gcd 1.

structure CCDN.IsBoundedPlaneCurve (F : Type u_1) [Field F] (q : MvPolynomial (Fin 2) ℤ) (d : ℕ) (H : ℝ) : Prop

The integral affine plane equation q has total degree d, is irreducible over the field F, and all its coefficients are bounded in absolute value by H ≥ 1.

• totalDegree_eq : q.totalDegree = d

  The polynomial q has total degree d.

• irreducible : Irreducible ((MvPolynomial.map (Int.castRingHom F)) q)

  The image of q over F is irreducible.

• one_le_height : 1 ≤ H

  The coefficient bound H is at least 1.

• coeff_le : CoefficientHeightLE q H

  Every coefficient of q has absolute value at most H.

structure CCDN.IsIndependentEvaluation {n s N : ℕ} (f : MvPolynomial (Fin n) ℤ) (M : ℕ) (F : Fin N → MvPolynomial (Fin n) ℤ) (z : Fin s → IntPoint n) : Prop

The input of the determinant method: forms F j of degree M, primitive integral zeros z i of f, and an evaluation matrix (F j (z i)) whose rows are linearly independent over ℚ, so that it has a nonzero maximal minor.

• isHomogeneous (j : Fin N) : (F j).IsHomogeneous M

  Every form F j is homogeneous of degree M.

• primitive (i : Fin s) : Finset.univ.gcd (z i) = 1

  The coordinates of every point z i have gcd 1.

• eval_eq_zero (i : Fin s) : (MvPolynomial.eval (z i)) f = 0

  Every point z i is a zero of f.

• rows_linearIndependent : LinearIndependent ℚ ((Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j)).map Int.cast).row

  The rows of the evaluation matrix (F j (z i)) are linearly independent over ℚ.

structure CCDN.IsSmoothResidueFamily {n : ℕ} {ι : Type u_1} (f : MvPolynomial (Fin n) ℤ) (P : Finset ℕ) (a : ℕ → IntPoint n) (x : ι → IntPoint n) : Prop

The points x i lie in prescribed nonsingular residue classes of f: every p ∈ P is prime, a p is a zero of f modulo p at which some partial derivative of f does not vanish modulo p, and every x i is congruent to a p modulo p.

• prime (p : ℕ) : p ∈ P → Nat.Prime p

  Every element of P is prime.

• eval_eq_zero (p : ℕ) : p ∈ P → MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin n) => ↑(a p j)) f = 0

  For every p ∈ P, the point a p is a zero of f modulo p.

• smooth (p : ℕ) : p ∈ P → ∃ (j : Fin n), (MvPolynomial.eval fun (i : Fin n) => ↑(a p i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0

  For every p ∈ P, some partial derivative of f is nonzero at a p modulo p.

• dvd_sub (p : ℕ) : p ∈ P → ∀ (i : ι) (j : Fin n), ↑p ∣ x i j - a p j

  For every p ∈ P, every point x i is congruent to a p modulo p.