A single auxiliary polynomial for all rational points of bounded projective height, with no finite-family hypothesis.

theorem CCDN.exists_bounded_projective_zero_family {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (B : ℝ) : ∃ (t : ℕ) (z : Fin t → IntPoint (n + 1)), (∀ (i : Fin t), Finset.univ.gcd (z i) = 1) ∧ (∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) ∧ (∀ (i : Fin t), InBox (z i) B) ∧ ∀ {M : ℕ} (g : MvPolynomial (Fin (n + 1)) ℤ), g.IsHomogeneous M → (∀ (i : Fin t), (MvPolynomial.eval (z i)) g = 0) → ∀ (x : ProjectivePoint n), Projectivization.mulHeight x ≤ B → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) g)

The rational points of height at most B on the zero locus of f, as a finite family of bounded primitive integer zeros. A form vanishing on the family vanishes at every such point.

theorem CCDN.hypersurface_absolute_projective_auxiliary {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n d : ℕ} (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) {B : ℝ} (hB : 1 ≤ B) : ∃ (bad : Finset ℕ) (M : ℕ), (∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p) ∧ ↑M ≤ hypersurfaceAuxiliaryDegreeBound n d B (primeSetFactor bad) ↑(integerCoefficientHeight f) ∧ ∃ (g : MvPolynomial (Fin (n + 3)) ℤ), g ≠ 0 ∧ g.IsHomogeneous M ∧ (∀ (x : ProjectivePoint (n + 2)), Projectivization.mulHeight x ≤ B → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) g)) ∧ ¬f ∣ g

The full projective-height formulation of the absolutely irreducible case of CCDN Theorem 3.1.1.