Numerical normalization of a finite-field hypersurface count, as in CCDN Lemma 2.8. The input count bound is an explicit hypothesis.

theorem CCDN.hypersurface_count_root_bound (m : ℕ) (hm : 0 < m) {P H T : ℝ} (hP : 0 ≤ P) (hH : 0 ≤ H) (hT : 0 ≤ T) (hcount : T ≤ P ^ m + H * P ^ (m - 1)) : T ^ (1 / ↑m) ≤ P + H

A point-count error of H times P^(m-1) increases the mth root by at most H. There is no degree or multiplicity loss in this normalization.

theorem CCDN.hypersurface_count_normalized_root_error (m : ℕ) (hm : 0 < m) {P H T : ℝ} (hP : 0 < P) (hH : 0 ≤ H) (hT : 0 ≤ T) (hcount : T ≤ P ^ m + H * P ^ (m - 1)) : T ^ (1 / ↑m) / P - 1 ≤ H / P

Normalized version of the preceding root bound.

theorem CCDN.local_exponent_separated_lower_bound_of_root_bound (m s e : ℕ) (hm : 0 < m) {μ : ℕ} (hμ : 0 < μ) {Q : ℝ} (hroot : ↑μ ^ (1 / ↑m) ≤ Q) (hcutoff : ∀ (K : ℕ), s * K ≤ e + μ * (m + K).choose (m + 1)) : ↑m.factorial ^ (1 / ↑m) / Q * ↑m / (↑m + 1) * ↑s ^ (1 + 1 / ↑m) - (↑m + 1) * ↑s ≤ ↑e

An upper bound on the multiplicity root gives the usual denominator form of the sharp determinant exponent.

theorem CCDN.projective_hypersurface_minorGcd_of_count_bound {n s N p d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (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) {H : ℝ} (hH : 0 ≤ H) (hcount : ↑(projectiveHypersurfaceTotalMultiplicity f hf hf0) ≤ ↑p ^ (n + 1) + H * ↑p ^ n) : ∃ (e : ℕ), ↑(n + 1).factorial ^ (1 / (↑n + 1)) / (↑p + H) * (↑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))

The global single-prime determinant bound in denominator form, assuming the displayed bound for the total residue multiplicity.