A coefficient-independent local determinant exponent for hypersurfaces. The exponent is an explicit finite sum depending only on dimension, multiplicity and the number of rows, and admits sharp binomial cutoff bounds.

def CCDN.hypersurfaceMultiplicityExponent (n μ s : ℕ) : ℕ

Deficit exponent from the cumulative bound μ binomial(n+k,n), where n is the hypersurface dimension.

Equations

• CCDN.hypersurfaceMultiplicityExponent n μ s = ∑ k : Fin s, (s - μ * (n + ↑k).choose n)

theorem CCDN.sum_cumulative_binomial (n K : ℕ) : ∑ k ∈ Finset.range K, (n + k).choose n = (n + K).choose (n + 1)

Hockey-stick identity: ∑_{k < K} (n + k).choose n = (n + K).choose (n + 1).

theorem CCDN.hypersurfaceMultiplicityExponent_cutoff (n s K : ℕ) {μ : ℕ} (hμ : 0 < μ) : s * K ≤ hypersurfaceMultiplicityExponent (n + 1) μ s + μ * (n + 1 + K).choose (n + 2)

Exact integer cutoff inequality. Optimizing K gives the leading (n!/μ)^(1/n) * n/(n+1) * s^(1+1/n) term of CCDN's local determinant bound.

theorem CCDN.hypersurface_pow_dvd_det_mod {p n μ s : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 2)) ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ∈ MvPolynomial.idealOfVars (Fin (n + 2)) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) ≠ 0) (x : Fin s → Fin (n + 2) → ℤ) (hx : ∀ (i : Fin s) (j : Fin (n + 2)), ↑p ∣ x i j) (hfx : ∀ (i : Fin s), ↑p ^ hypersurfaceMultiplicityExponent (n + 1) μ s ∣ (MvPolynomial.eval (x i)) f) (F : Fin s → MvPolynomial (Fin (n + 2)) ℤ) : ↑p ^ hypersurfaceMultiplicityExponent (n + 1) μ s ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (F j)).det

Every evaluation determinant in one hypersurface residue class has the explicit dimension/multiplicity divisor, even for zeros only modulo that power.