Documentation

LeanPool.CCDN.Hypersurface.FiniteFieldCount

A sharp coefficient-uniform count for geometrically irreducible affine hypersurfaces over prime fields, proved by plane-section averaging.

Numerical absorption of bad and zero plane sections above the cutoff p>27*d^4. The leading term remains exactly p^(m-1).

theorem CCDN.hypersurface_bad_section_error {d p : ℝ} (hd : 1 ≤ d) (hp : stepanovThreshold d < p) :
2 * d ^ 4 * p + d ^ 3 ≤ 3 * d ^ 2 * p * √p

For 1 ≤ d and p above the threshold 27 * d ^ 4, the bad-section error 2 * d ^ 4 * p + d ^ 3 is at most 3 * d ^ 2 * p * √p.

theorem CCDN.affine_hypersurface_finite_field_bound {n : ℕ} (p : ℕ) [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) (ZMod p)) (hf : Irreducible ((MvPolynomial.map (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) f)) (hsize : stepanovThreshold ↑f.totalDegree < ↑p) :
↑(Nat.card { z : Fin (n + 3) → ZMod p // (MvPolynomial.eval z) f = 0 }) ≤ ↑p ^ (n + 2) + hypersurfaceResidueConstant * ↑f.totalDegree ^ 2 * ↑p ^ (n + 1) * √↑p

A geometrically irreducible affine hypersurface f = 0 in n + 3 variables over ZMod p, with p above the threshold 27 * (deg f) ^ 4, has at most p ^ (n + 2) + hypersurfaceResidueConstant * (deg f) ^ 2 * p ^ (n + 1) * √p points.