Both bounds for the bad-prime factor apply to the same homogeneous auxiliary. Their minimum therefore survives the affine exponent saving.

noncomputable def CCDN.affineMinimumAuxiliaryBound (n d : ℕ) (A B L b : ℝ) : ℝ

The affine auxiliary degree bound in which the coefficient-sensitive main term involves the minimum of log L + d log B + d² and d² b, where L is the height of the leading form and b a bad-prime factor, with box exponent 1 / d^(1/(n+1)) up to the factor A.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.scaled_hypersurface_auxiliary_bound_of_badPrime_le {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hf : f ≠ 0) (hd : 0 < f.totalDegree) {p : ℕ} (hp : Nat.Prime p) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hBp : B / A ≤ ↑p) {c b : ℝ} (hFbad : 0 ≤ c) (hb : 0 ≤ b) (hbad : c ≤ Real.exp 1 * b) : hypersurfaceAuxiliaryDegreeBound n f.totalDegree B c ↑(integerCoefficientHeight (scaledHomogenize f.totalDegree (↑p) f)) ≤ hypersurfaceAbsoluteAuxiliaryConstant n * (Real.exp 1 * A * ↑f.totalDegree ^ (2 - 1 / (↑n + 1)) * (↑f.totalDegree ^ 2 * b) * B ^ (1 / ↑f.totalDegree ^ (1 / (↑n + 1))) / ↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f)) ^ (1 / ((↑n + 1) * ↑f.totalDegree * ↑f.totalDegree ^ (1 / (↑n + 1)))) + ↑f.totalDegree ^ (1 - 1 / (↑n + 1)) * Real.log B + ↑f.totalDegree ^ (4 - 1 / (↑n + 1)))

The scaled auxiliary degree bound for any bad-prime factor c with c ≤ Real.exp 1 * b and 0 ≤ b.

theorem CCDN.affine_auxiliary_minimum_of_small_constant_coefficient {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible f) (hd : 0 < f.totalDegree) (hc : f.coeff 0 ≠ 0) {B : ℝ} (hB : scalingPrimeRatio ≤ B) (hheight : Real.log |↑(f.coeff 0)| < B / scalingPrimeRatio) : ∃ (g : MvPolynomial (Fin (n + 2)) ℤ), IsBoxAuxiliary f g B ∧ ↑g.totalDegree ≤ affineMinimumAuxiliaryBound n f.totalDegree scalingPrimeRatio B (↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f))) (hypersurfaceBadPrimeFactor (scaledHomogenize f.totalDegree 1 f))

If the constant coefficient c of a primitive irreducible integer polynomial f is nonzero and log |c| < B / scalingPrimeRatio, with B ≥ scalingPrimeRatio, then f has a box auxiliary polynomial of degree at most affineMinimumAuxiliaryBound, with ratio scalingPrimeRatio and the bad-prime factor of the homogenization of f.