The normalized higher-dimensional determinant inequality, retaining the exact root-rank and kernel-rank coefficients needed for uniform degree selection.
theorem
CCDN.hypersurface_rank_comparison_normalized
{r d M s : ℕ}
(hrpos : 0 < r)
(hd : 0 < d)
(hdM : d ≤ M)
(hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M)
(B L A E : ℝ)
(hcomparison :
↑r.factorial ^ (1 / ↑r) / (↑r + 1) * ↑s ^ (1 + 1 / ↑r) * (Real.log ↑s - ↑r * (4 * Real.log ↑d + Real.log A) - E) ≤ Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑((r + 1 + M).choose M) + ↑s * ↑M * Real.log B - (↑((r + 1 + M).choose M) - ↑s) * Real.log L)
:
Absorb the archimedean rank terms and divide by Ms. No fixed-factor approximation of the leading rank or coefficient-height term is made.
A dimension-only error for the normalized, height-controlled inequality.
Equations
- CCDN.hypersurfaceNormalizedError n = CCDN.hypersurfaceHeightDeterminantError n + (↑n + 2) * CCDN.hypersurfaceArchimedeanError (n + 1) / ↑(n + 1).factorial ^ (1 / (↑n + 1))
Instances For
theorem
CCDN.hypersurface_no_auxiliary_normalized_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)) * ↑s ^ (1 / (↑n + 1)) / ((↑n + 2) * ↑M) * (Real.log ↑s - (↑n + 1) * (4 * Real.log ↑d + Real.log (1 + Real.log H / ↑d ^ 2)) - hypersurfaceNormalizedError n) ≤ Real.log B - ↑((n + 2 + (M - d)).choose (M - d)) / (↑M * ↑s) * Real.log |↑(order.leadingCoeff f)|
Absence of an auxiliary polynomial implies the normalized inequality with constructed geometry and exact Hilbert rank.