Coordinate transport between the graph-hyperplane construction and the finite integral-point count.

theorem CCDN.integer_top_irreducible_rename {σ : Type u_1} {τ : Type u_2} (e : σ ≃ τ) (f : MvPolynomial σ ℤ) (hir : HasAbsIrreducibleTopForm f) : HasAbsIrreducibleTopForm ((MvPolynomial.rename ⇑e) f)

Renaming the variables of an integer polynomial along an equivalence preserves absolute irreducibility of its top-degree form.

def CCDN.graphIntegerNormal {n : ℕ} (D : ℤ) (a : Fin n → ℤ) : IntPoint (n + 1)

The integer normal vector (D, -a 0, …, -a (n - 1)) of the hyperplane D * x 0 = ∑ a i * x (i + 1).

Equations

• CCDN.graphIntegerNormal D a = Fin.cons D fun (i : Fin n) => -a i

theorem CCDN.graphIntegerNormal_height {n : ℕ} (D : ℤ) (a : Fin n → ℤ) {H : ℕ} (hD : |D| ≤ ↑H) (ha : ∀ (i : Fin n), |a i| ≤ ↑H) (i : Fin (n + 1)) : |↑(graphIntegerNormal D a i)| ≤ ↑H

If |D| and every |a i| are at most H, then every coordinate of graphIntegerNormal D a has absolute value at most H.

theorem CCDN.integer_slice_map_of_option_equations {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (D : ℤ) (a : Fin n → ℤ) (g : ℤ → MvPolynomial (Fin n) ℤ) (hslice : ∀ (k : ℤ) (x : Option (Fin n) → ℤ), D * x none - ∑ i : Fin n, a i * x (some i) = k → (MvPolynomial.eval x) ((MvPolynomial.rename ⇑(finSuccEquiv' 0)) f) = 0 → (MvPolynomial.eval fun (i : Fin n) => x (some i)) (g k) = 0) (B : ℝ) (k : ℤ) (x : IntPoint (n + 1)) (hx : x ∈ integerSlicePoints (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B (graphIntegerNormal D a) k) : rationalPoint (deleteIntegerCoordinate 0 x) ∈ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) (g k))

Integral equations suffice for the rational zero-locus map used by the count: the only coordinate change is deleting coordinate zero.