Bounded translations remove a zero constant coefficient and preserve the finite-field residue count, primitivity and integer point families.

theorem CCDN.affineTranslation_eval {R : Type u_1} [CommRing R] {n : ℕ} (a x : Fin n → R) (f : MvPolynomial (Fin n) R) : (MvPolynomial.eval x) ((affineTranslation R a) f) = (MvPolynomial.eval (x + a)) f

Evaluating the affine translate of f by a at x gives the value of f at x + a.

theorem CCDN.affineTranslation_constantCoeff {R : Type u_1} [CommRing R] {n : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin n) R) : ((affineTranslation R a) f).coeff 0 = (MvPolynomial.eval a) f

The constant coefficient of the affine translate of f by a is the value of f at a.

theorem CCDN.PrimitiveIntegerPolynomial.translate_affine {n : ℕ} (a : Fin n → ℤ) {f : MvPolynomial (Fin n) ℤ} (hf : PrimitiveIntegerPolynomial f) : PrimitiveIntegerPolynomial ((affineTranslation ℤ a) f)

An integral affine translate of a primitive integral polynomial is primitive.

theorem CCDN.affineTranslation_residue_card (a : Fin 2 → ℤ) (f : MvPolynomial (Fin 2) ℤ) (p : ℕ) : Nat.card (PlaneResidue ((affineTranslation ℤ a) f) p) = Nat.card (PlaneResidue f p)

An integral affine translation of a plane polynomial preserves the number of its zeros modulo p in the affine plane over ZMod p.

theorem CCDN.exists_bounded_translation_nonzero_constant (f : MvPolynomial (Fin 2) ℤ) (hf : f ≠ 0) : ∃ (a : Fin 2 → ℤ), (∀ (j : Fin 2), 0 ≤ a j ∧ a j ≤ ↑f.totalDegree) ∧ ((affineTranslation ℤ a) f).coeff 0 ≠ 0

A nonzero integral plane polynomial f has an integral translate with nonzero constant coefficient by a vector whose entries lie in [0, deg f].