Bad reduction of an affine equation is contained in bad reduction of its top homogeneous form. This includes degree loss in the defined predicate.

theorem CCDN.absolute_irreducible_of_top_homogeneousComponent_irreducible {σ : Type u_1} (f : MvPolynomial σ ℤ) (hir : HasAbsIrreducibleTopForm f) : AbsolutelyIrreducible f

Absolute irreducibility of the highest homogeneous component implies absolute irreducibility of the original integer equation.

theorem CCDN.hypersurfaceBadPrimeFactor_le_top_homogeneousComponent {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hir : HasAbsIrreducibleTopForm f) : hypersurfaceBadPrimeFactor f ≤ hypersurfaceBadPrimeFactor ((MvPolynomial.homogeneousComponent f.totalDegree) f)

The affine bad-prime factor is no greater than that of the top form when the latter is absolutely irreducible.

theorem CCDN.PrimitiveIntegerPolynomial.irreducible_of_absolute_top {σ : Type u_1} {f : MvPolynomial σ ℤ} (hprim : PrimitiveIntegerPolynomial f) (hir : HasAbsIrreducibleTopForm f) : Irreducible f

Primitivity reflects the irreducibility supplied by the absolute top form back to the integer polynomial ring.

theorem CCDN.absolute_top_irreducible_of_integer_scalar_factor {σ : Type u_1} {f g : MvPolynomial σ ℤ} {c : ℤ} (hc : c ≠ 0) (he : f = MvPolynomial.C c * g) (hir : HasAbsIrreducibleTopForm f) : g.totalDegree = f.totalDegree ∧ HasAbsIrreducibleTopForm g

Removing nonzero integer content preserves absolute irreducibility of the top homogeneous form, along with the affine degree.