Height and cardinality transport through an integer linear projection with uniformly bounded affine fibers.

theorem CCDN.projective_integer_linear_count_transfer {m n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) (P : Matrix (Fin (m + 1)) (Fin (n + 1)) ℤ) (f : MvPolynomial (Fin (m + 1)) ℚ) (hf : f.IsHomogeneous f.totalDegree) (hrelation : (MvPolynomial.aeval fun (i : Fin (m + 1)) => integerLinearForm (P i)) f ∈ I) (M : ℕ) (hfinite : ∀ (z : Fin (m + 1) → ℚ) (s : Finset (Fin (n + 1) → ℚ)), (∀ x ∈ s, x ∈ idealZeroLocus I) → (∀ x ∈ s, ∀ (i : Fin (m + 1)), (MvPolynomial.eval x) (integerLinearForm (P i)) = z i) → s.card ≤ M) (H B : ℝ) (hH : 0 ≤ H) (hP : ∀ (i : Fin (m + 1)) (j : Fin (n + 1)), |↑(P i j)| ≤ H) : projectiveCount (projectiveIdealZeroLocus I) B ≤ M * projectiveCount (projectiveZeroLocus f) (↑(n + 1) * H * B)

Let P be an integer matrix with entries of absolute value at most H whose linear forms satisfy the homogeneous relation f modulo I. If every affine fiber of the induced map on the zero locus of I has at most M points, then the projective rational points of height at most B on the zero locus of I number at most M times those of height at most (n + 1) * H * B on the projective hypersurface f = 0.