Constructing a good rational hyperplane with a bounded integer normal. The degree-nine bound is a polynomial replacement for the precise avoidance polynomial in corrected CCDN Lemma 4.3.7.

A bounded integral equation obtained from three independent rows. Cramer's rule uses row-replacement determinants, so the same elementary 3! T³ bound controls both the coefficients and their common denominator.

def CCDN.goodHyperplaneHeight (d : ℕ) : ℕ

The height bound 6 * (2 * d ^ 3 + 3) ^ 3 for the integer normal of a good hyperplane section of a degree-d hypersurface.

Equations

• CCDN.goodHyperplaneHeight d = 6 * (2 * d ^ 3 + 3) ^ 3

theorem CCDN.exists_bounded_geometrically_good_hyperplane {n : ℕ} (f : MvPolynomial (Option (Fin (3 + n))) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) : ∃ (D : ℤ) (a : Fin (3 + n) → ℤ), D ≠ 0 ∧ |D| ≤ ↑(goodHyperplaneHeight f.totalDegree) ∧ (∀ (i : Fin (3 + n)), |a i| ≤ ↑(goodHyperplaneHeight f.totalDegree)) ∧ ((graphHyperplaneRestriction fun (i : Fin (3 + n)) => ↑(a i) / ↑D) ((MvPolynomial.map (Int.castRingHom ℚ)) f)).totalDegree = f.totalDegree ∧ AbsolutelyIrreducibleRat ((graphHyperplaneRestriction fun (i : Fin (3 + n)) => ↑(a i) / ↑D) ((MvPolynomial.map (Int.castRingHom ℚ)) f))

In at least four variables there is a hyperplane D*x₀ = ∑ aᵢ*xᵢ whose restriction is geometrically irreducible of full degree. Its integer normal has height polynomial in the degree and is independent of the coefficient height of the original equation.