An explicit integral linear projection away from a bounded rational linear center. Its kernel is exactly the span of the given independent rows, and its coefficient bound is uniform in their entries.

theorem CCDN.exists_bounded_integer_scaled_projection {s r : ℕ} (A : Matrix (Fin (s + 1)) (Fin r) ℤ) (hli : LinearIndependent ℚ fun (i : Fin (s + 1)) (j : Fin r) => ↑(A i j)) (T : ℕ) (hA : ∀ (i : Fin (s + 1)) (j : Fin r), |A i j| ≤ ↑T) : ∃ (D : ℤ), D ≠ 0 ∧ ∃ (P : Matrix (Fin r) (Fin r) ℤ), (∀ (i j : Fin r), |P i j| ≤ 2 * ↑(s + 1).factorial * ↑T ^ (s + 1)) ∧ P * P = D • P ∧ ∀ (x : Fin r → ℚ), (P.map ⇑(Int.castRingHom ℚ)).mulVec x = 0 ↔ x ∈ Submodule.span ℚ (Set.range fun (i : Fin (s + 1)) (j : Fin r) => ↑(A i j))

Constructing the matrix requires only independent bounded integer rows. In particular it is nonvanishing off their span.

theorem CCDN.projective_linear_map_height {m n : ℕ} (P : Matrix (Fin (m + 1)) (Fin (n + 1)) ℤ) {H : ℝ} (hH : 0 ≤ H) (hP : ∀ (i : Fin (m + 1)) (j : Fin (n + 1)), |↑(P i j)| ≤ H) (x : ProjectivePoint n) (himage : (P.map ⇑(Int.castRingHom ℚ)).mulVec (Projectivization.rep x) ≠ 0) : (Projectivization.mk ℚ ((P.map ⇑(Int.castRingHom ℚ)).mulVec (Projectivization.rep x)) himage).mulHeight ≤ ↑(n + 1) * H * Projectivization.mulHeight x

The height estimate for the projective linear image of any point outside the matrix kernel. The input height is its intrinsic multiplicative projective height.