Integer points on rational affine lines. Primitive integer directions make the line parameter integral, giving a spacing bound.

def CCDN.rationalAffineLine {n : ℕ} (a v : RatPoint n) : Set (RatPoint n)

The rational affine line {a + t • v | t ∈ ℚ} through a with direction v.

Equations

• CCDN.rationalAffineLine a v = {x : CCDN.RatPoint n | ∃ (t : ℚ), x = a + t • v}

def CCDN.integerDirectionHeight {n : ℕ} (v : IntPoint n) : ℕ

The height max_j |v j| of an integer vector v.

Equations

• CCDN.integerDirectionHeight v = Finset.univ.sup fun (j : Fin n) => (v j).natAbs

theorem CCDN.rationalAffineLine_smul_direction {n : ℕ} (a v : RatPoint n) {c : ℚ} (hc : c ≠ 0) : rationalAffineLine a (c • v) = rationalAffineLine a v

Scaling the direction by a nonzero rational does not change the affine line.

theorem CCDN.rationalAffineLine_shift_base {n : ℕ} (a v : RatPoint n) (s : ℚ) : rationalAffineLine (a + s • v) v = rationalAffineLine a v

Moving the base point along the direction does not change the affine line.

theorem CCDN.integerDirectionHeight_pos {n : ℕ} {v : IntPoint n} (hv : v ≠ 0) : 0 < integerDirectionHeight v

A nonzero integer vector has positive height.

theorem CCDN.projective_direction_height {n : ℕ} (v : IntPoint (n + 1)) (hv : v ≠ 0) (hprim : Finset.univ.gcd v = 1) : (Projectivization.mk ℚ (rationalPoint v) ⋯).mulHeight = ↑(integerDirectionHeight v)

For a nonzero primitive integer vector v, the multiplicative height of the projective point [v] equals max_j |v j|.

theorem CCDN.rationalAffineLine_integer_rep_and_count {n : ℕ} (a v : RatPoint n) {B : ℝ} (hB : 0 ≤ B) (hcount : 1 < count (rationalAffineLine a v) B) : ∃ (z : IntPoint n) (w : IntPoint n), w ≠ 0 ∧ Finset.univ.gcd w = 1 ∧ InBox z B ∧ ↑(integerDirectionHeight w) ≤ 2 * B ∧ rationalAffineLine a v = rationalAffineLine (rationalPoint z) (rationalPoint w) ∧ ↑(count (rationalAffineLine a v) B) ≤ 1 + 2 * B / ↑(integerDirectionHeight w)

Any rational affine line containing two bounded integer points has an integer base point and primitive integer direction, with the exact spacing estimate and the direction-height cutoff needed for summing line contributions.