Quantitative degree control from the plane determinant comparison.

theorem CCDN.plane_rank_ge_degree_parameter {s d M : ℕ} (hd : 0 < d) (hdM : d ≤ M) (hr : 2 * s + d ^ 2 = d * (2 * M + 3)) : M ≤ s

The Hilbert function s of a plane curve of degree d in degree M, given by 2 s + d² = d (2 M + 3), is at least M when 0 < d ≤ M.

theorem CCDN.plane_rank_archimedean_error {s d M : ℕ} (hd : 0 < d) (hdM : d ≤ M) (hr : 2 * s + d ^ 2 = d * (2 * M + 3)) : Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑((2 + M).choose M) ≤ 5 * ↑s ^ 2 / 2

For the Hilbert function s of a plane curve of degree d in degree M ≥ d, the archimedean terms log s! / 2 + (s / 2) log C(M + 2, M) of the determinant comparison are at most 5 s² / 2.

theorem CCDN.plane_auxiliary_log_degree_bound {s d M : ℕ} {B L A K : ℝ} (hd : 0 < d) (hdM : d ≤ M) (hr : 2 * s + d ^ 2 = d * (2 * M + 3)) (hB : 1 ≤ B) (hL : 1 ≤ L) (hML : Real.log B ≤ ↑M) (hheight : Real.log L ≤ 4 * ↑d * Real.log B) (hcomparison : ↑s ^ 2 / 2 * (Real.log ↑s - 4 * Real.log ↑d - Real.log A - 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 + 23 + Real.log 2 + 3 * Real.log ↑d + Real.log A + 2 / ↑d * Real.log B - Real.log L / ↑d ^ 2

The small-height case of the plane auxiliary-degree calculation. The coefficient obstruction is retained with its exact exponent 1/d².

theorem CCDN.plane_degree_bound_of_log_bound {d M : ℕ} {B L A K : ℝ} (hd : 0 < d) (hM : 0 < M) (hB : 0 < B) (hL : 0 < L) (hA : 0 < A) (hlog : Real.log ↑M ≤ K + 23 + Real.log 2 + 3 * Real.log ↑d + Real.log A + 2 / ↑d * Real.log B - Real.log L / ↑d ^ 2) : ↑M ≤ 2 * Real.exp (K + 23) * ↑d ^ 3 * A * B ^ (2 / ↑d) / L ^ (1 / ↑d ^ 2)

Exponentiation of the logarithmic degree bound, keeping the coefficient saving and the leading box exponent unchanged.