CCDN Lemma 2.8 and Corollary 2.9, including the finite-field count. All constants depend only on dimension.

def CCDN.hypersurfaceCountConstant (n : ℕ) : ℝ

Explicit dimension-only constant for the projective multiplicity count (projective_hypersurface_totalMultiplicity_bound) in n + 3 coordinates: the projective point count contributes projectiveHypersurfaceResidueConstant = 330, and the multiplicities of the singular points contribute (n + 3) (n + 4)ⁿ (projectiveHypersurfaceTotalMultiplicity_le_card_add_sqrt_error).

Equations

• CCDN.hypersurfaceCountConstant n = CCDN.projectiveHypersurfaceResidueConstant + ↑((n + 3) * (n + 4) ^ n)

theorem CCDN.hypersurfaceCountConstant_nonneg (n : ℕ) : 0 ≤ hypersurfaceCountConstant n

The constant hypersurfaceCountConstant n is nonnegative.

noncomputable def CCDN.hypersurfaceDeterminantMain (n s : ℕ) : ℝ

The main local coefficient for projective hypersurfaces of dimension n+1.

Equations

• CCDN.hypersurfaceDeterminantMain n s = ↑(n + 1).factorial ^ (1 / (↑n + 1)) * (↑n + 1) / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1))

theorem CCDN.hypersurfaceDeterminantMain_nonneg (n s : ℕ) : 0 ≤ hypersurfaceDeterminantMain n s

The main coefficient hypersurfaceDeterminantMain n s is nonnegative.

theorem CCDN.hypersurfaceDeterminantMain_div (n s : ℕ) (m : ℝ) : factorialRoot n / m * (↑n + 1) / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1)) = hypersurfaceDeterminantMain n s / m

The local exponent of projective_hypersurface_minorGcd_dvd in terms of hypersurfaceDeterminantMain.

theorem CCDN.projective_hypersurface_normalized_count_error {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (hir : Irreducible ((MvPolynomial.map (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f))) (hsize : stepanovThreshold ↑d < ↑p) : ↑(projectiveHypersurfaceTotalMultiplicity f hf hf0) ^ (1 / (↑n + 1)) / ↑p - 1 ≤ hypersurfaceCountConstant n * ↑d ^ 2 / √↑p

CCDN Lemma 2.8: normalized multiplicity-root error O_n(d^2/sqrt(p)).

theorem CCDN.projective_hypersurface_minorGcd_dvd {n s N p d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (hir : Irreducible ((MvPolynomial.map (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f))) (hsize : stepanovThreshold ↑d < ↑p) (F : Fin N → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → IntPoint (n + 3)) (hprim : ∀ (i : Fin s), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : ∃ (e : ℕ), factorialRoot n / (↑p + hypersurfaceCountConstant n * ↑d ^ 2 * √↑p) * (↑n + 1) / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1)) - (↑n + 2) * ↑s ≤ ↑e ∧ ↑p ^ e ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j))

CCDN Corollary 2.9: the sharp single-prime divisor of every maximal minor of a common-degree homogeneous evaluation matrix. The residue count, local multiplicities and projective reduction are constructed from f and z.