A degree-d auxiliary equation for nonabsolute irreducible hypersurfaces. Linear descent of the two homogeneous factors suffices over any extension.

theorem CCDN.integer_nonabsolute_homogeneous_auxiliary {K : Type u_1} [Field K] [Algebra ℚ K] {n d : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) (hred : ¬Irreducible ((MvPolynomial.map (algebraMap ℚ K)) ((MvPolynomial.map (Int.castRingHom ℚ)) f))) : ∃ (g : MvPolynomial (Fin n) ℤ), g ≠ 0 ∧ g.IsHomogeneous d ∧ ¬f ∣ g ∧ ∀ (x : Fin n → ℚ), (MvPolynomial.eval x) ((MvPolynomial.map (Int.castRingHom ℚ)) f) = 0 → (MvPolynomial.eval x) ((MvPolynomial.map (Int.castRingHom ℚ)) g) = 0

Integer denominator clearing preserves the exact degree and all rational zeros. Irreducibility is stated over Q, and splitting may occur over any extension.

theorem CCDN.nonabsolute_projective_auxiliary {K : Type u_1} [Field K] [Algebra ℚ K] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) (hred : ¬Irreducible ((MvPolynomial.map (algebraMap ℚ K)) ((MvPolynomial.map (Int.castRingHom ℚ)) f))) : ∃ (g : MvPolynomial (Fin (n + 1)) ℤ), g ≠ 0 ∧ g.IsHomogeneous d ∧ ¬f ∣ g ∧ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) ⊆ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) g)

CCDN Lemma 3.3.1 for all rational projective zeros, independently of height.