CCDN Lemma 4.2.3: replace the full coefficient height by any lower height in the bad-prime contribution, uniformly in the degree.

Uniform comparison of logarithmic coefficient-height ratios.

theorem CCDN.hypersurface_logarithmic_height_transfer {r d : ℕ} (hr : 0 < r) (hd : 0 < d) {H Y : ℝ} (hY : 1 ≤ Y) (hYH : Y ≤ H) : (Real.log H + ↑d ^ 2) / H ^ (1 / (↑r * ↑d * ↑d ^ (1 / ↑r))) ≤ ↑r * ((Real.log Y + ↑d ^ 2) / Y ^ (1 / (↑r * ↑d * ↑d ^ (1 / ↑r))))

The coefficient-weighted ratio has loss at most r in dimension r.

theorem CCDN.rpow_four_sub_eq_mul_sq {d : ℝ} (hd : 0 < d) (n : ℕ) : d ^ (4 - 1 / (↑n + 1)) = d ^ (2 - 1 / (↑n + 1)) * d ^ 2

The exponent bookkeeping d ^ (4 - 1 / (n + 1)) = d ^ (2 - 1 / (n + 1)) * d ^ 2 used by the affine minimum and height-transfer estimates.

theorem CCDN.hypersurface_badPrime_height_transfer {n d : ℕ} (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f ≠ 0) (hdegree : f.totalDegree = d) (hd : 0 < d) {Y : ℝ} (hY : 1 ≤ Y) (hYH : Y ≤ ↑(integerCoefficientHeight f)) : ↑d ^ (4 - 1 / (↑n + 1)) * hypersurfaceBadPrimeFactor f / ↑(integerCoefficientHeight f) ^ (1 / ((↑n + 1) * ↑d * ↑d ^ (1 / (↑n + 1)))) ≤ (↑n + 1) * Real.exp (2 * mertensError + 1) * hypersurfaceHeightConstant (n + 3) * ↑d ^ (2 - 1 / (↑n + 1)) * (Real.log Y + ↑d ^ 2) / Y ^ (1 / ((↑n + 1) * ↑d * ↑d ^ (1 / (↑n + 1))))

CCDN Lemma 4.2.3 with an explicit dimension constant. The coefficient height is the maximum, and the bad-prime factor is the defined factor.