Exact-rank Bombieri--Vaaler comparison for higher-dimensional hypersurfaces. Absence of an auxiliary polynomial forces the explicit numerical inequality.

theorem CCDN.hypersurface_homogeneous_rank_pos {n d M s : ℕ} (hd : 0 < d) (hdM : d ≤ M) (hr : s + (n + 2 + (M - d)).choose (M - d) = (n + 2 + M).choose M) : 0 < s

The Hilbert function s of a degree-d hypersurface in n + 3 variables, defined by s + C(n + 2 + (M - d), M - d) = C(n + 2 + M, M), is positive in every degree M ≥ d.

theorem CCDN.hypersurface_no_auxiliary_height_comparison {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n d M t : ℕ} (order : MonomialOrder (Fin (n + 3))) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hdM : d ≤ M) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) {B : ℝ} {z : Fin t → IntPoint (n + 3)} (hzB : IsPrimitiveBoxZeroFamily f B z) (hrel : ∀ (g : MvPolynomial (Fin (n + 3)) ℤ), g.IsHomogeneous M → (∀ (i : Fin t), (MvPolynomial.eval (z i)) g = 0) → f ∣ g) : ∃ (s : ℕ), 0 < s ∧ s + (n + 2 + (M - d)).choose (M - d) = (n + 2 + M).choose M ∧ ↑(n + 1).factorial ^ (1 / (↑n + 1)) / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1)) * (Real.log ↑s - (↑n + 1) * (4 * Real.log ↑d + Real.log (1 + Real.log H / ↑d ^ 2)) - hypersurfaceHeightDeterminantError n) ≤ Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑((n + 2 + M).choose M) + ↑s * ↑M * Real.log B - (↑((n + 2 + M).choose M) - ↑s) * Real.log |↑(order.leadingCoeff f)|

With no auxiliary nonmultiple of degree M, the exact homogeneous Hilbert rank satisfies the archimedean/nonarchimedean determinant comparison.