The complementary large-coefficient-height auxiliary-degree estimate.

theorem CCDN.plane_auxiliary_large_height_log_bound {s d M : ℕ} {B L H T K : ℝ} (hd : 0 < d) (hMlarge : 32 * d ≤ M) (hr : 2 * s + d ^ 2 = d * (2 * M + 3)) (hB : 1 ≤ B) (hL : 1 ≤ L) (hH : 1 ≤ H) (hT : 0 ≤ T) (hheight : 4 * ↑d * Real.log B ≤ Real.log H) (hposition : Real.log H ≤ Real.log L + T * ↑d ^ 2) (hcomparison : ↑s ^ 2 / 2 * (Real.log ↑s - 4 * Real.log ↑d - Real.log (1 + Real.log H / ↑d ^ 2) - K) ≤ Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑((2 + M).choose M) + ↑s * ↑M * Real.log B - (↑((2 + M).choose M) - ↑s) * Real.log L) : Real.log ↑M ≤ K + 6 + Real.log 2 + Real.log 4 + T + 3 * Real.log ↑d

When the coefficient height exceeds B^(4d), a degree at least 32d satisfying the no-auxiliary comparison is bounded by a constant times d³. The constant includes the loss in positioning the leading coefficient.

theorem CCDN.plane_large_degree_bound_of_log_bound {d M : ℕ} {T K : ℝ} (hd : 0 < d) (hM : 0 < M) (hlog : Real.log ↑M ≤ K + 6 + Real.log 2 + Real.log 4 + T + 3 * Real.log ↑d) : ↑M ≤ 8 * Real.exp (K + 6 + T) * ↑d ^ 3

Exponentiating the large-height logarithmic degree bound for plane curves: if log M ≤ K + 6 + log 2 + log 4 + T + 3 log d, then M ≤ 8 exp (K + 6 + T) d³.