The affine auxiliary theorem in every positive dimension and degree, with the degree-loss-inclusive geometric bad-prime factor. This distinction from the literal affine wording of CCDN Definition 3.2.1 is intentional.

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

The shape of the affine auxiliary degree bound in degree d and box radius B, with L the coefficient height of the leading form and b the bad-prime factor: writing r = n + 1, it is $d^{2 - 1/r} \min(\log L + d \log B + d^2, d^2 b) B^{1/d^{1/r}} / L^{1/(r d^{1 + 1/r})}

• d^{1 - 1/r} \log B + d^{4 - 1/r}$.

Equations

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

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

The dimension constant in the affine auxiliary theorem for equations in n + 2 variables, multiplying affineAuxiliaryDegreeExpression.

Equations

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

theorem CCDN.affineHypersurfaceAuxiliaryConstant_pos (n : ℕ) : 0 < affineHypersurfaceAuxiliaryConstant n

The constant affineHypersurfaceAuxiliaryConstant n is positive.

theorem CCDN.affineMinimumAuxiliaryBound_le_expression (n d : ℕ) {A B L b : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hL : 1 ≤ L) (hb : 0 ≤ b) : affineMinimumAuxiliaryBound n d A B L b ≤ hypersurfaceAbsoluteAuxiliaryConstant n * (max (affineHeightTransferConstant n) (Real.exp 1) * A + 1) * affineAuxiliaryDegreeExpression n d B L b

The affine auxiliary degree bound with comparison constant A ≥ 0 is at most a constant depending on n and A times affineAuxiliaryDegreeExpression, for 1 ≤ B, 1 ≤ L and 0 ≤ b.

theorem CCDN.affine_hypersurface_auxiliary {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible f) (hd : 0 < f.totalDegree) {B : ℝ} (hB : 1 ≤ B) : ∃ (g : MvPolynomial (Fin (n + 2)) ℤ), IsBoxAuxiliary f g B ∧ ↑g.totalDegree ≤ affineHypersurfaceAuxiliaryConstant n * affineAuxiliaryDegreeExpression n f.totalDegree B (↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f))) (hypersurfaceBadPrimeFactor f)

Every primitive irreducible integer affine hypersurface admits the coefficient-sensitive auxiliary in the complete minimum form, using the defined geometric bad-prime factor (which includes degree-dropping primes). The constant depends only on the dimension.