Comparison with the affine bad-prime factor. For degree at least two the homogeneous and affine bad-reduction predicates agree. In degree one, the homogeneous bad-prime set can be smaller because affine degree loss can produce a nonzero multiple of the homogenizing variable.

theorem CCDN.unscaledHomogenize_absolute_irreducible_iff {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf : f ≠ 0) : AbsolutelyIrreducible (scaledHomogenize f.totalDegree 1 f) ↔ AbsolutelyIrreducible f

A nonzero integer polynomial is absolutely irreducible if and only if its ordinary homogenization is.

theorem CCDN.hypersurfaceBadPrimeFactor_mono_of_badReduction_imp {n m : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (g : MvPolynomial (Fin (m + 1)) ℤ) (hd : f.totalDegree = g.totalDegree) (habs : AbsolutelyIrreducible f → AbsolutelyIrreducible g) (hbad : ∀ (q : ℕ), HypersurfaceBadReduction f q → HypersurfaceBadReduction g q) : hypersurfaceBadPrimeFactor f ≤ hypersurfaceBadPrimeFactor g

Inclusion of the geometric bad-prime sets gives monotonicity of the corresponding factors, even across different numbers of variables.

theorem CCDN.hypersurfaceBadPrimeFactor_unscaledHomogenize_le {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f ≠ 0) : hypersurfaceBadPrimeFactor (scaledHomogenize f.totalDegree 1 f) ≤ hypersurfaceBadPrimeFactor f

Homogenization never enlarges the affine factor based on the repository's degree-loss-inclusive bad-reduction predicate. This holds also in degree one.