Integral translations preserve the affine bad-prime factor, including degree-dropping reductions and the nonabsolute zero convention.

theorem CCDN.hypersurfaceBadPrimeFactor_affineTranslation {n : ℕ} (a : Fin (n + 1) → ℤ) (f : MvPolynomial (Fin (n + 1)) ℤ) : hypersurfaceBadPrimeFactor ((affineTranslation ℤ a) f) = hypersurfaceBadPrimeFactor f

The bad-prime factor of an integral polynomial is invariant under integral affine translation of the variables.

theorem CCDN.affine_auxiliary_translation_transport {n : ℕ} (f g : MvPolynomial (Fin n) ℤ) (a : Fin n → ℤ) {B D : ℝ} (hg : IsBoxAuxiliary ((affineTranslation ℤ a) f) g (B + D)) (ha : InBox a D) : ∃ (G : MvPolynomial (Fin n) ℤ), IsBoxAuxiliary f G B ∧ G.totalDegree = g.totalDegree

Pull an auxiliary equation back through a bounded translation.