Higher-dimensional auxiliary polynomials in the small-height range, with exact exponents, for any finite prime set whose normalized comparison holds. The hypersurface instance retains the original geometric bad-prime factor.
The coefficient-sensitive threshold, with a dimension-only constant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CCDN.auxiliary_small_height_degree_of_comparison
{n d t : ℕ}
(order : MonomialOrder (Fin (n + 3)))
(f : MvPolynomial (Fin (n + 3)) ℤ)
(hf0 : f ≠ 0)
(hd : 0 < d)
(z : Fin t → IntPoint (n + 3))
{B : ℝ}
(hB : 1 ≤ B)
(hbox : ∀ (i : Fin t), InBox (z i) B)
(bad : Finset ℕ)
(hcomp : AuxiliaryRankComparison order f d z bad)
(hheight : Real.log |↑(order.leadingCoeff f)| ≤ 2 * ↑d * (↑n + 2) * Real.log B)
:
∃ (M : ℕ),
↑M ≤ 2 * ↑d + ↑d ^ (1 - 1 / (↑n + 1)) * Real.log B + hypersurfaceSmallThreshold n d B |↑(order.leadingCoeff f)| (primeSetFactor bad) + 2 ∧ ∃ (g : MvPolynomial (Fin (n + 3)) ℤ), IsPointAuxiliary f g M z
An integer auxiliary degree for any finite prime set bad for which the
normalized comparison holds. The bound keeps the leading-coefficient saving and
every radius exponent.
theorem
CCDN.hypersurface_auxiliary_small_height_degree
{K : Type u_1}
[Field K]
[CharZero K]
[IsAlgClosed K]
{n d t : ℕ}
(order : MonomialOrder (Fin (n + 3)))
(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)
(hheight : Real.log |↑(order.leadingCoeff f)| ≤ 2 * ↑d * (↑n + 2) * Real.log B)
:
∃ (bad : Finset ℕ) (M : ℕ),
(∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p) ∧ ↑M ≤ 2 * ↑d + ↑d ^ (1 - 1 / (↑n + 1)) * Real.log B + hypersurfaceSmallThreshold n d B |↑(order.leadingCoeff f)| (primeSetFactor bad) + 2 ∧ ∃ (g : MvPolynomial (Fin (n + 3)) ℤ),
g ≠ 0 ∧ g.IsHomogeneous M ∧ (∀ (i : Fin t), (MvPolynomial.eval (z i)) g = 0) ∧ ¬f ∣ g
The exact geometric bad-prime set together with an integer auxiliary degree. The bound keeps the leading-coefficient saving and every radius exponent.