Bad-prime factors of integer polynomials, and the geometric bad-prime factor used by the determinant method. A bad-prime factor badPrimeFactor P is zero for nonabsolute equations and the exact finite exponential product over the primes above stepanovThreshold satisfying the bad-reduction predicate P otherwise. For nonzero homogeneous equations the geometric factor agrees with CCDN Definition 3.2.1. For affine equations its bad-prime predicate also includes degree loss; this stronger convention is not identical to the literal printed definition.

theorem CCDN.absolute_integer_polynomial_totalDegree_pos {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : AbsolutelyIrreducible f) : 0 < f.totalDegree

An absolutely irreducible integral polynomial has positive total degree.

noncomputable def CCDN.badPrimeFactor {σ : Type u_1} (P : MvPolynomial σ ℤ → ℕ → Prop) (hP : ∀ (f : MvPolynomial σ ℤ), AbsolutelyIrreducible f → {p : ℕ | stepanovThreshold f.totalDegree < p ∧ P f p}.Finite) (f : MvPolynomial σ ℤ) : ℝ

The bad-prime factor of an integer polynomial f relative to a bad-reduction predicate P: the product primeSetFactor of the primes p > stepanovThreshold (deg f) with P f p when f is absolutely irreducible over ℚ, and 0 otherwise. The hypothesis hP gives the finiteness of these primes for absolutely irreducible f.

Equations

• CCDN.badPrimeFactor P hP f = if h : CCDN.AbsolutelyIrreducible f then CCDN.primeSetFactor ⋯.toFinset else 0

theorem CCDN.badPrimeFactor_nonneg {σ : Type u_1} {P : MvPolynomial σ ℤ → ℕ → Prop} {hP : ∀ (f : MvPolynomial σ ℤ), AbsolutelyIrreducible f → {p : ℕ | stepanovThreshold f.totalDegree < p ∧ P f p}.Finite} (f : MvPolynomial σ ℤ) : 0 ≤ badPrimeFactor P hP f

The bad-prime factor badPrimeFactor P hP f is nonnegative.

theorem CCDN.badPrimeFactor_eq_zero {σ : Type u_1} {P : MvPolynomial σ ℤ → ℕ → Prop} {hP : ∀ (f : MvPolynomial σ ℤ), AbsolutelyIrreducible f → {p : ℕ | stepanovThreshold f.totalDegree < p ∧ P f p}.Finite} {f : MvPolynomial σ ℤ} (hf : ¬AbsolutelyIrreducible f) : badPrimeFactor P hP f = 0

The bad-prime factor of an integral polynomial that is not absolutely irreducible is zero.

theorem CCDN.badPrimeFactor_eq_primeSetFactor {σ : Type u_1} {P : MvPolynomial σ ℤ → ℕ → Prop} {hP : ∀ (f : MvPolynomial σ ℤ), AbsolutelyIrreducible f → {p : ℕ | stepanovThreshold f.totalDegree < p ∧ P f p}.Finite} {d : ℕ} {f : MvPolynomial σ ℤ} (hf : AbsolutelyIrreducible f) (hdegree : f.totalDegree = d) (bad : Finset ℕ) (hbad : ∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ P f p) : badPrimeFactor P hP f = primeSetFactor bad

For an absolutely irreducible equation of degree d, the bad-prime factor is the primeSetFactor of any finite set listing exactly the bad primes above 27 d⁴.

theorem CCDN.badPrimeFactor_mono {σ : Type u_1} {P Q : MvPolynomial σ ℤ → ℕ → Prop} {hP : ∀ (f : MvPolynomial σ ℤ), AbsolutelyIrreducible f → {p : ℕ | stepanovThreshold f.totalDegree < p ∧ P f p}.Finite} {hQ : ∀ (f : MvPolynomial σ ℤ), AbsolutelyIrreducible f → {p : ℕ | stepanovThreshold f.totalDegree < p ∧ Q f p}.Finite} (f : MvPolynomial σ ℤ) (hPQ : ∀ (p : ℕ), P f p → Q f p) : badPrimeFactor P hP f ≤ badPrimeFactor Q hQ f

If the bad-reduction predicate P implies Q at f, then the bad-prime factor of f for P is at most that for Q.

noncomputable def CCDN.hypersurfaceBadPrimeFactor {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) : ℝ

The geometric bad-prime factor: badPrimeFactor for HypersurfaceBadReduction, which counts both failure of absolute irreducibility and degree loss modulo p.

Equations

• CCDN.hypersurfaceBadPrimeFactor f = CCDN.badPrimeFactor CCDN.HypersurfaceBadReduction ⋯ f

theorem CCDN.hypersurfaceBadPrimeFactor_nonneg {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) : 0 ≤ hypersurfaceBadPrimeFactor f

The geometric bad-prime factor hypersurfaceBadPrimeFactor f is nonnegative.

theorem CCDN.hypersurfaceBadPrimeFactor_eq_zero {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : ¬AbsolutelyIrreducible f) : hypersurfaceBadPrimeFactor f = 0

The geometric bad-prime factor of an integral polynomial that is not absolutely irreducible is zero.

theorem CCDN.hypersurfaceBadPrimeFactor_eq_exp {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : AbsolutelyIrreducible f) (hdegree : f.totalDegree = d) (bad : Finset ℕ) (hbad : ∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p) : hypersurfaceBadPrimeFactor f = primeSetFactor bad

For an absolutely irreducible integral polynomial of degree d, the geometric bad-prime factor is the primeSetFactor of any finite set listing exactly the primes above stepanovThreshold d at which f has geometric bad reduction.

theorem CCDN.hypersurfaceBadPrimeFactor_le_height {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) : hypersurfaceBadPrimeFactor f ≤ Real.exp (2 * mertensError + 1) * hypersurfaceHeightConstant (n + 1) * (1 + Real.log H / ↑f.totalDegree ^ 2)

The bad-prime factor satisfies the coefficient-height bound also for nonabsolute equations, where the factor is zero by definition.

theorem CCDN.hypersurfaceBadPrimeFactor_le_max {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) : hypersurfaceBadPrimeFactor f ≤ 2 * Real.exp (2 * mertensError + 1) * hypersurfaceHeightConstant (n + 1) * max (Real.log H / ↑f.totalDegree ^ 2) 1

The max-form of CCDN Corollary 3.2.3 for the defined factor itself.