All coefficients of the universal witness vanish at a degree-dropping or reducible ambient reduction. A nonzero integer coefficient therefore detects every sufficiently large bad prime, in arbitrary ambient dimension.

theorem CCDN.bad_prime_dvd_universalPlaneBadWitness_coeff {σ : Type u_1} (f : MvPolynomial σ ℤ) (hpos : 0 < f.totalDegree) (rows : Fin (2 * f.totalDegree ^ 2 - 1) → ℕ × ℕ) (cols : Fin (2 * f.totalDegree ^ 2 - 1) → ClosedFormColumns f.totalDegree) (p : ℕ) [Fact (Nat.Prime p)] (hp : f.totalDegree < p) (hbad : ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure (ZMod p)))) f).totalDegree ≠ f.totalDegree ∨ ¬Irreducible ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure (ZMod p)))) f)) (e : PlaneParameters σ →₀ ℕ) : ↑p ∣ (universalPlaneBadWitness f rows cols).coeff e

Every coefficient is divisible by a bad prime above the degree. Degree loss, including the zero reduction, is included in the predicate.

theorem CCDN.exists_integer_hypersurface_bad_prime_witness {L : Type u_1} {σ : Type u_2} [Field L] [CharZero L] [IsAlgClosed L] [Finite σ] (f : MvPolynomial (Option σ) ℤ) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f)) (hpos : 0 < f.totalDegree) : ∃ (rows : Fin (2 * f.totalDegree ^ 2 - 1) → ℕ × ℕ) (cols : Fin (2 * f.totalDegree ^ 2 - 1) → ClosedFormColumns f.totalDegree) (e : PlaneParameters (Option σ) →₀ ℕ), (universalPlaneBadWitness f rows cols).coeff e ≠ 0 ∧ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], f.totalDegree < p → ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure (ZMod p)))) f).totalDegree ≠ f.totalDegree ∨ ¬Irreducible ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure (ZMod p)))) f) → ↑p ∣ (universalPlaneBadWitness f rows cols).coeff e

A nonzero integer divisible by every bad prime larger than the degree. The witness is a coefficient of the constructed universal polynomial, so later coefficient-height bounds apply to this same integer.