Polynomial coordinates for a translated scaled model, with exact point transport and transport of an auxiliary nonmultiple back to the original slice.

noncomputable def CCDN.scaledModelCoordinates {n : ℕ} (h : ℤ) (a : Fin n → ℤ) : Fin (n + 1) → MvPolynomial (Fin n) ℤ

The integer polynomial coordinate change (h, x₁ - a₁ h, …, xₙ - aₙ h) from affine coordinates to the coordinates of the translated scaled projective model.

Equations

• CCDN.scaledModelCoordinates h a = Fin.cons (MvPolynomial.C h) fun (j : Fin n) => MvPolynomial.X j - MvPolynomial.C (a j * h)

theorem CCDN.scaledModelCoordinates_model_eval {n : ℕ} (h : ℤ) (a z : Fin n → ℤ) (f : MvPolynomial (Fin n) ℤ) : (MvPolynomial.eval fun (j : Fin (n + 1)) => (MvPolynomial.eval z) (scaledModelCoordinates h a j)) ((homogeneousTranslation ℤ a) (scaledHomogenize f.totalDegree h f)) = h ^ f.totalDegree * (MvPolynomial.eval z) f

The translated scaled homogenization of f, evaluated at the scaled model coordinates of z, equals h ^ deg f * f(z).

theorem CCDN.scaledModelCoordinates_box {n : ℕ} {B : ℝ} {d : ℕ} {h : ℤ} (hB : 1 ≤ B) (hh : 0 ≤ h) (hhB : ↑h ≤ B) (a z : Fin n → ℤ) (ha : ∀ (j : Fin n), 0 ≤ a j ∧ a j ≤ ↑d) (hz : InBox z B) (j : Fin (n + 1)) : |↑((MvPolynomial.eval z) (scaledModelCoordinates h a j))| ≤ (↑d + 1) * B

For 0 ≤ h ≤ B, translation parameters 0 ≤ a j ≤ d and z in the box of size B ≥ 1, all scaled model coordinates of z have absolute value at most (d + 1) * B.

theorem CCDN.scaledModelCoordinates_auxiliary_transport {n M : ℕ} (h : ℤ) (a : Fin n → ℤ) (f : MvPolynomial (Fin n) ℤ) (g : MvPolynomial (Fin (n + 1)) ℤ) (hg : g.IsHomogeneous M) (hnd : ¬(homogeneousTranslation ℤ a) (scaledHomogenize f.totalDegree h f) ∣ g) : ∃ (g' : MvPolynomial (Fin (n + 1)) ℤ), g'.IsHomogeneous M ∧ (∀ (z : Fin n → ℤ), (MvPolynomial.eval (Fin.cons h z)) g' = (MvPolynomial.eval fun (j : Fin (n + 1)) => (MvPolynomial.eval z) (scaledModelCoordinates h a j)) g) ∧ ¬scaledHomogenize f.totalDegree h f ∣ g'

A homogeneous auxiliary polynomial g of degree M not divisible by the translated scaled homogenization of f transports to a homogeneous g' of degree M not divisible by the scaled homogenization of f, with g'(h, z) equal to g at the scaled model coordinates of z.

theorem CCDN.scaled_positioned_points_card_le {M t : ℕ} (f : MvPolynomial (Fin 2) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) (a : Fin 2 → ℤ) (z : Fin t → Fin 2 → ℤ) (hinj : Function.Injective z) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) (g : MvPolynomial (Fin 3) ℤ) (hg : IsPointAuxiliary ((homogeneousTranslation ℤ a) (scaledHomogenize f.totalDegree (↑p) f)) g M fun (i : Fin t) (j : Fin (2 + 1)) => (MvPolynomial.eval (z i)) (scaledModelCoordinates (↑p) a j)) : t ≤ f.totalDegree * M

A nonmultiple on the translated scaled model counts the original integer points. The bound uses only the auxiliary degree and original degree.