The coefficient-sensitive auxiliary theorem for arbitrary absolutely irreducible homogeneous equations in arbitrary coordinates.

The equation is moved into position by a homogeneous translation fixing the homogenizing coordinate; zeros, primitivity, absolute irreducibility and nondivisibility are transported along it, and the box grows from B to (d + 1) B. absolute_auxiliary_degree_of_comparison does this for any finite prime set whose normalized comparison holds for every translate.

The geometric bad-prime predicate is invariant under integral shears.

The box enlargement by d+1 costs only a dimension constant in the auxiliary degree, with no added power of d in its leading term.

theorem CCDN.auxiliary_box_rpow_factor {r d : ℕ} (hr : 0 < r) (hd : 0 < d) : (↑d + 1) ^ ((↑r + 1) / (↑r * ↑d ^ (1 / ↑r))) ≤ Real.exp ((↑r + 1) ^ 2 / ↑r)

For positive r and d, the box enlargement factor $(d + 1)^{(r + 1) / (r d^{1/r})}$ is at most $\exp((r + 1)^2 / r)$, a bound depending only on r.

theorem CCDN.hypersurfaceBadReduction_homogeneousTranslation {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (a : Fin n → ℤ) (p : ℕ) : HypersurfaceBadReduction ((homogeneousTranslation ℤ a) f) p ↔ HypersurfaceBadReduction f p

A prime is bad for the homogeneous translate of a nonzero integral form f if and only if it is bad for f.

def CCDN.hypersurfaceAuxiliaryPositionConstant (n : ℕ) : ℝ

The dimension constant $(5(n + 2) + 5)(n + 2)$ of the positioning step: after a suitable homogeneous translation, the logarithm of the coefficient height exceeds that of the lexicographic leading coefficient by at most this constant times $d^{1 + 1/(n + 1)}$.

Equations

• CCDN.hypersurfaceAuxiliaryPositionConstant n = (5 * (↑n + 2) + 5) * (↑n + 2)

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

The dimension constant in the absolutely irreducible case of CCDN Theorem 3.1.1 for forms in n + 3 variables: the positioned constant times a factor absorbing the enlargement of the box from B to (d + 1) B and the passage to the original coefficient height.

Equations

• CCDN.hypersurfaceAbsoluteAuxiliaryConstant n = CCDN.hypersurfacePositionedAuxiliaryConstant n (CCDN.hypersurfaceAuxiliaryPositionConstant n) * (Real.exp ((↑n + 2) ^ 2 / (↑n + 1)) + (↑n + 3))

theorem CCDN.hypersurfaceAbsoluteAuxiliaryConstant_pos (n : ℕ) : 0 < hypersurfaceAbsoluteAuxiliaryConstant n

The constant hypersurfaceAbsoluteAuxiliaryConstant n is positive.

noncomputable def CCDN.hypersurfaceAuxiliaryDegreeBound (n d : ℕ) (B b H : ℝ) : ℝ

The auxiliary degree bound of CCDN Theorem 3.1.1 with bad-prime factor b and coefficient height H.

Equations

• CCDN.hypersurfaceAuxiliaryDegreeBound n d B b H = CCDN.hypersurfaceAbsoluteAuxiliaryConstant n * CCDN.auxDegreeBound n d B b H

theorem CCDN.eval_homogeneousTranslation_neg {n : ℕ} (a : Fin (n + 2) → ℤ) (f : MvPolynomial (Fin (n + 3)) ℤ) (z : IntPoint (n + 3)) : (MvPolynomial.eval (homogeneousPointTranslation (-a) z)) ((homogeneousTranslation ℤ a) f) = (MvPolynomial.eval z) f

Evaluating the homogeneous translate of f by a at the point translated by -a gives the value of f at the original point.

theorem CCDN.absolute_auxiliary_degree_of_comparison {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n d t : ℕ} (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) {B : ℝ} {z : Fin t → IntPoint (n + 3)} (hzB : IsPrimitiveBoxZeroFamily f B z) (bad : Finset ℕ) (hcomp : ∀ (a : Fin (n + 2) → ℤ), AuxiliaryRankComparison MonomialOrder.lex ((homogeneousTranslation ℤ a) f) d (fun (i : Fin t) => homogeneousPointTranslation (-a) (z i)) bad) : ∃ (M : ℕ), ↑M ≤ hypersurfaceAuxiliaryDegreeBound n d B (primeSetFactor bad) ↑(integerCoefficientHeight f) ∧ ∃ (g : MvPolynomial (Fin (n + 3)) ℤ), IsPointAuxiliary f g M z

The absolutely irreducible case of CCDN Theorem 3.1.1 for any finite prime set bad whose normalized comparison holds for every homogeneous translate of f and the translated points. The constant depends only on dimension; the coefficient height belongs to the original equation.

theorem CCDN.hypersurface_absolute_auxiliary_degree {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n d t : ℕ} (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) (z : Fin t → IntPoint (n + 3)) (hprim : ∀ (i : Fin t), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) {B : ℝ} (hB : 1 ≤ B) (hbox : ∀ (i : Fin t), InBox (z i) 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 ∧ (∀ (i : Fin t), (MvPolynomial.eval (z i)) g = 0) ∧ ¬f ∣ g

The absolutely irreducible case of CCDN Theorem 3.1.1. The constant depends only on dimension. The coefficient height and bad-prime factor belong to the original equation.