All box and coefficient cases for the affine auxiliary theorem when the constant coefficient is nonzero.

theorem CCDN.affineMinimumAuxiliaryBound_mono_A (n d : ℕ) {A A' B L b : ℝ} (hA : A ≤ A') (hB : 1 ≤ B) (hL : 1 ≤ L) (hb : 0 ≤ b) : affineMinimumAuxiliaryBound n d A B L b ≤ affineMinimumAuxiliaryBound n d A' B L b

The affine auxiliary degree bound affineMinimumAuxiliaryBound is monotone in the comparison constant A, for 1 ≤ B, 1 ≤ L and 0 ≤ b.

theorem CCDN.affineMinimumAuxiliaryBound_mono_b (n d : ℕ) {A B L b b' : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hL : 1 ≤ L) (hb : b ≤ b') : affineMinimumAuxiliaryBound n d A B L b ≤ affineMinimumAuxiliaryBound n d A B L b'

The affine auxiliary degree bound affineMinimumAuxiliaryBound is monotone in the bad-prime factor b, for 0 ≤ A, 1 ≤ B and 1 ≤ L.

theorem CCDN.degree_le_affineMinimumAuxiliaryBound (n : ℕ) {d : ℕ} (hd : 0 < d) {A B L b : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hL : 1 ≤ L) (hb : 0 ≤ b) : ↑d ≤ affineMinimumAuxiliaryBound n d A B L b

The affine auxiliary degree bound is at least the degree d whenever 0 < d, so the equation itself always meets it.

noncomputable def CCDN.affineAuxiliaryBoxScale : ℝ

The scale $4 R^2$, with R = scalingPrimeRatio, of the small-box threshold affineAuxiliaryBoxScale * (d + 1) ^ affineAuxiliaryBoxExponent n separating the unscaled case of the affine auxiliary theorem from the prime-scaled cases.

Equations

• CCDN.affineAuxiliaryBoxScale = 4 * CCDN.scalingPrimeRatio ^ 2

def CCDN.affineAuxiliaryBoxExponent (n : ℕ) : ℕ

The exponent $4(n + 2) + 2$ of d + 1 in the small-box threshold of the affine auxiliary theorem for equations in n + 2 variables.

Equations

• CCDN.affineAuxiliaryBoxExponent n = 4 * (n + 2) + 2

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

The comparison constant used uniformly over all box radii in the affine auxiliary theorem: the larger of scalingPrimeRatio and the small-box scale times $e^{(4(n + 2) + 2)(n + 2)}$.

Equations

• CCDN.affineAuxiliaryComparisonConstant n = max CCDN.scalingPrimeRatio (Real.exp (Real.log CCDN.affineAuxiliaryBoxScale + ↑(CCDN.affineAuxiliaryBoxExponent n) * (↑n + 2)))

theorem CCDN.affineAuxiliaryBoxScale_one_le : 1 ≤ affineAuxiliaryBoxScale

The small-box scale affineAuxiliaryBoxScale is at least 1.

theorem CCDN.affineAuxiliaryComparisonConstant_one_le (n : ℕ) : 1 ≤ affineAuxiliaryComparisonConstant n

The comparison constant affineAuxiliaryComparisonConstant n is at least 1.

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

Every primitive irreducible equation with nonzero constant coefficient has the affine auxiliary, uniformly over all box radii.