The large-height auxiliary-degree calculation eliminates both the radius and coefficient height, leaving O_r(d^(4-1/r)).

noncomputable def CCDN.hypersurfaceLargeHeightError (r : ℕ) (E T : ℝ) : ℝ

The additive error term, depending only on the dimension r and the constants E and T, in the large-height bound log M ≤ hypersurfaceLargeHeightError r E T + (4 - 1/r) log d.

Equations

• CCDN.hypersurfaceLargeHeightError r E T = Real.log (8 * ↑r) + (E + CCDN.hypersurfaceRankLogError r + T) / ↑r

theorem CCDN.hypersurface_large_height_log_degree_bound {r d M s : ℕ} (hrpos : 0 < r) (hd : 0 < d) (hM : 8 * d * (r + 1) ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) (B L H E T : ℝ) (hB : 1 ≤ B) (hL : 1 ≤ L) (hH : 1 ≤ H) (hT : 0 ≤ T) (hheight : 2 * ↑d * (↑r + 1) * Real.log B ≤ Real.log H) (hposition : Real.log H ≤ Real.log L + T * ↑d * ↑d ^ (1 / ↑r)) (hcomparison : ↑r.factorial ^ (1 / ↑r) * ↑s ^ (1 / ↑r) / ((↑r + 1) * ↑M) * (Real.log ↑s - ↑r * (4 * Real.log ↑d + Real.log (1 + Real.log H / ↑d ^ 2)) - E) ≤ Real.log B - ↑((r + 1 + (M - d)).choose (M - d)) / (↑M * ↑s) * Real.log L) : Real.log ↑M ≤ hypersurfaceLargeHeightError r E T + (4 - 1 / ↑r) * Real.log ↑d

The large-height normalized determinant inequality gives a degree bound independent of B and H; positioning is stated with its precise height cost.

theorem CCDN.hypersurface_large_degree_bound_of_log_bound {r d M : ℕ} {C : ℝ} (hd : 0 < d) (hM : 0 < M) (hlog : Real.log ↑M ≤ C + (4 - 1 / ↑r) * Real.log ↑d) : ↑M ≤ Real.exp C * ↑d ^ (4 - 1 / ↑r)

Exponentiating a logarithmic degree bound: if log M ≤ C + (4 - 1/r) log d with d and M positive, then M ≤ exp C * d ^ (4 - 1/r).