Integral representatives need not be primitive to provide an upper bound on projective height. Removing their gcd can only decrease the maximum absolute coordinate.

theorem CCDN.primitiveProjectiveRep_chart {n : ℕ} (x : ProjectivePoint n) (hx : Projectivization.rep x 0 ≠ 0) : primitiveProjectiveRep x 0 ≠ 0 ∧ projectiveAffineCoordinates x = fun (j : Fin n) => ↑(primitiveProjectiveRep x j.succ) / ↑(primitiveProjectiveRep x 0)

If the chosen representative of x has nonzero first coordinate, then so does its primitive integer representative, and the affine chart coordinates of x are the ratios of the remaining primitive coordinates to the first one.

theorem CCDN.projective_integer_height_le {n : ℕ} (z : IntPoint (n + 1)) (hz : z ≠ 0) {B : ℝ} (hbox : InBox z B) : (Projectivization.mk ℚ (rationalPoint z) ⋯).mulHeight ≤ B

A nonzero integer vector with all coordinates of absolute value at most B spans a projective point of height at most B, whether or not its coordinates are coprime.