Bad reduction for integer bivariate equations with a nonzero constant outer leading coefficient. A leading-coefficient factor in the witness also covers degree-dropping reductions.

theorem CCDN.bivariate_leadingCoeff_eq_constant {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) (htotal : bivariateTotalDegree f ≤ f.natDegree) : f.leadingCoeff = Polynomial.C (f.leadingCoeff.coeff 0)

Full outer degree forces the outer leading coefficient to be constant.

def CCDN.BivariateBadReduction (f : Polynomial (Polynomial ℤ)) (d p : ℕ) : Prop

Bad reduction includes both lost total degree and geometric reducibility.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.exists_full_outer_bad_prime_witness {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (d : ℕ) (hd : 1 ≤ d) (f : Polynomial (Polynomial ℤ)) (hdeg : f.natDegree = d) (htotal : bivariateTotalDegree f ≤ d) (hir : Irreducible ((bivariateMap (Int.castRingHom F)) f)) (H : ℝ) (hH : 1 ≤ H) (hcoeff : BivariateCoefficientBound f H) : ∃ (D : ℤ), 0 < D ∧ Real.log ↑D ≤ 27 * ↑d ^ 4 * (1 + 2 * Real.log H / ↑d ^ 2) ∧ ∀ (p : ℕ), d < p → BivariateBadReduction f d p → ↑p ∣ D

A full-outer-degree integer equation has a height-controlled positive witness for every bad prime, including loss of degree. Integer monicity is not required.