The integer grid gives distinct bounded-height rational points on the irreducible projective closure. This is the geometric input to CCDN Proposition 5, including the stated degree and the exact grid size.

theorem CCDN.integer_grid_le_projective_count {n d : ℕ} (f : MvPolynomial (Fin n) ℚ) (hd : f.totalDegree ≤ d) (s : Finset ℤ) {B : ℝ} (hB : 1 ≤ B) (hsB : ∀ a ∈ s, |↑a| ≤ B) (hfzero : ∀ (z : IntPoint n), (∀ (j : Fin n), z j ∈ s) → (MvPolynomial.eval (rationalPoint z)) f = 0) : s.card ^ n ≤ projectiveCount (projectiveZeroLocus (scaledHomogenize d 1 f)) B

A finite integral grid injects into projective space by z↦[1:z].

theorem CCDN.projective_closure_absolute_irreducible {n d : ℕ} (f : MvPolynomial (Fin n) ℚ) (hd : f.totalDegree = d) (hf : AbsolutelyIrreducibleRat f) : (scaledHomogenize d 1 f).IsHomogeneous d ∧ (scaledHomogenize d 1 f).totalDegree = d ∧ AbsolutelyIrreducibleRat (scaledHomogenize d 1 f)

The homogenization of an absolutely irreducible rational polynomial of total degree d is a form of degree d that is again absolutely irreducible.

theorem CCDN.exists_projective_grid_lower_bound (d : ℕ) (hd : 4 ≤ d) : ∃ (F : MvPolynomial (Fin 3) ℚ), F.IsHomogeneous d ∧ F.totalDegree = d ∧ AbsolutelyIrreducibleRat F ∧ ((d - 1) / 2 + 1) ^ 2 ≤ projectiveCount (projectiveZeroLocus F) ↑((d - 1) / 2 - (d - 1) / 4)

For d≥4, the precise asymmetric integer grid used in Section 6 supplies (floor((d−1)/2)+1)² distinct projective points at the paper's chosen height.

theorem CCDN.exists_projective_two_point_lower_bound (d : ℕ) (hd : 0 < d) : ∃ (F : MvPolynomial (Fin 3) ℚ), F.IsHomogeneous d ∧ F.totalDegree = d ∧ AbsolutelyIrreducibleRat F ∧ 2 ≤ projectiveCount (projectiveZeroLocus F) 1

Every positive degree has an absolutely irreducible projective model with at least two rational points of height one. This covers d=1,2,3 in Proposition 5.