The coefficient-sensitive affine degree saving for a prime comparable to the box radius. The leading homogeneous height belongs to the original equation.

The prime-scaled height gain gives the affine exponent 1/d^(1/r).

theorem CCDN.affine_scaling_box_power {r d : ℕ} (hr : 0 < r) (hd : 0 < d) {B A p : ℝ} (hB : 1 ≤ B) (hA : 1 ≤ A) (hp : 0 < p) (hBp : B / A ≤ p) : B ^ ((↑r + 1) / (↑r * ↑d ^ (1 / ↑r))) / p ^ (1 / (↑r * ↑d ^ (1 / ↑r))) ≤ A * B ^ (1 / ↑d ^ (1 / ↑r))

For a scaling prime p ≥ B / A with A, B ≥ 1, the box term B ^ ((r + 1) / (r d^(1/r))) divided by p ^ (1 / (r d^(1/r))) is at most A * B ^ (1 / d^(1/r)).

theorem CCDN.scaled_height_rpow {r d : ℕ} (hr : 0 < r) (hd : 0 < d) {p L : ℝ} (hp : 0 < p) (hL : 0 < L) : (p ^ d * L) ^ (1 / (↑r * ↑d * ↑d ^ (1 / ↑r))) = p ^ (1 / (↑r * ↑d ^ (1 / ↑r))) * L ^ (1 / (↑r * ↑d * ↑d ^ (1 / ↑r)))

Splitting the power of the scaled height: (p^d L) ^ (1/(r d d^(1/r))) equals p ^ (1/(r d^(1/r))) * L ^ (1/(r d d^(1/r))) for positive p and L.

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

The dimension constant (n + 1) exp (2 mertensError + 1) hypersurfaceHeightConstant (n + 3) by which the logarithmic height term of a prime-scaled model is compared with that of the original affine equation.

Equations

• CCDN.affineHeightTransferConstant n = (↑n + 1) * Real.exp (2 * CCDN.mertensError + 1) * CCDN.hypersurfaceHeightConstant (n + 3)

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

The logarithmic-branch affine auxiliary degree bound: the bound of CCDN Theorem 3.1.1 with the bad-prime factor replaced by log L + d log B + d², where L is the height of the leading form, and the box exponent saved to 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 {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hf : f ≠ 0) (hd : 0 < f.totalDegree) {p : ℤ} (hp : 1 ≤ p) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hpB : ↑p ≤ B) (hBp : B / A ≤ ↑p) : hypersurfaceAuxiliaryDegreeBound n f.totalDegree B (hypersurfaceBadPrimeFactor (scaledHomogenize f.totalDegree p f)) ↑(integerCoefficientHeight (scaledHomogenize f.totalDegree p f)) ≤ affineLogarithmicAuxiliaryBound n f.totalDegree A B ↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f))

For a scaling factor 1 ≤ p ≤ B with B / A ≤ p, the auxiliary degree bound of the p-scaled homogenization of f, with its own bad-prime factor and coefficient height, is at most affineLogarithmicAuxiliaryBound in terms of the height of the leading form of f.

theorem CCDN.prime_scaled_affine_auxiliary_height {n : ℕ} (f : MvPolynomial (Fin (n + 2)) ℤ) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible f) (hd : 0 < f.totalDegree) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hpB : ↑p ≤ B) (hBp : B / A ≤ ↑p) : ∃ (g : MvPolynomial (Fin (n + 2)) ℤ), IsBoxAuxiliary f g B ∧ ↑g.totalDegree ≤ affineLogarithmicAuxiliaryBound n f.totalDegree A B ↑(integerCoefficientHeight ((MvPolynomial.homogeneousComponent f.totalDegree) f))

The logarithmic-height branch of the affine auxiliary bound, provided a scaling prime lies between B/A and B and avoids the constant term. The constructed polynomial vanishes on every original integer zero in the box.