A coefficient-uniform auxiliary for an affine hypersurface with absolutely irreducible leading form. This is the dimension-general form of CCDN (4-3-1).

noncomputable def CCDN.topFormAuxiliaryConstant (n : ℕ) : ℝ

The constant in the degree bound of the auxiliary polynomial for affine hypersurfaces in n + 2 variables with absolutely irreducible top-degree form, independent of the coefficients.

Equations

• CCDN.topFormAuxiliaryConstant n = CCDN.affineHypersurfaceAuxiliaryConstant n * ((↑n + 1) * Real.exp (2 * CCDN.mertensError + 1) * CCDN.hypersurfaceHeightConstant (n + 2) + 2)

theorem CCDN.topFormAuxiliaryConstant_pos (n : ℕ) : 0 < topFormAuxiliaryConstant n

The auxiliary constant topFormAuxiliaryConstant n is positive.

theorem CCDN.top_form_auxiliary_rational {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hir : HasAbsIrreducibleTopForm f) {B : ℝ} (hB : 1 ≤ B) : ∃ (g : MvPolynomial (Fin (n + 2)) ℤ), g ≠ 0 ∧ ¬(MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) g ∧ ↑g.totalDegree ≤ topFormAuxiliaryConstant n * ↑f.totalDegree ^ (4 - 1 / (↑n + 1)) * B ^ (1 / ↑f.totalDegree ^ (1 / (↑n + 1))) ∧ ∀ (x : IntPoint (n + 2)), InBox x B → (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval x) g = 0

Uniform auxiliary existence for every integer equation whose highest homogeneous component is absolutely irreducible. Integer content is removed inside the proof; the final constant depends only on ambient dimension.