Section-point bounds in the good, nonzero and unrestricted cases. The good-section bound uses the proved Stepanov theorem over the prime field.

theorem CCDN.bivariateEval_equiv {K : Type u_1} [CommRing K] (f : MvPolynomial (Fin 2) K) (t : Fin 2 → K) : (bivariateEval (t 0) (t 1)) ((bivariatePolynomialEquiv K) f) = (MvPolynomial.eval t) f

Evaluating the nested-polynomial form of a bivariate polynomial f at (t 0, t 1) agrees with evaluating f at t.

noncomputable def CCDN.planeSectionPolynomial {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) : MvPolynomial (Fin 2) K

The plane section universalPlaneSection f v as a polynomial in two variables (MvPolynomial (Fin 2)), the presentation used by point counting.

Equations

• CCDN.planeSectionPolynomial f v = (CCDN.bivariatePolynomialEquiv K).symm (CCDN.universalPlaneSection f v)

theorem CCDN.planeSectionPolynomial_totalDegree {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) : (planeSectionPolynomial f v).totalDegree ≤ f.totalDegree

A plane section of f has total degree at most that of f.

theorem CCDN.planeSectionPoints_card_le_square {K : Type u_1} {σ : Type u_2} [CommRing K] [Fintype K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) : Nat.card (PlaneSectionPoints f v) ≤ Fintype.card K ^ 2

The number of points of a plane section over a finite ring K is at most |K| ^ 2.

theorem CCDN.planeSectionPoints_card_le_degree_mul_card {K : Type u_1} {σ : Type u_2} [Field K] [Fintype K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) (hv : universalPlaneSection f v ≠ 0) : Nat.card (PlaneSectionPoints f v) ≤ f.totalDegree * Fintype.card K

A nonzero plane section of f over a finite field K has at most deg f * |K| points.

theorem CCDN.planeSectionPoints_card_le_add_mul_sqrt {σ : Type u_1} (p : ℕ) [Fact (Nat.Prime p)] (f : MvPolynomial σ (ZMod p)) (v : PlaneParameters σ → ZMod p) (hir : Irreducible ((bivariateMap (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) (universalPlaneSection f v))) (hsize : stepanovThreshold ↑f.totalDegree < ↑p) : ↑(Nat.card (PlaneSectionPoints f v)) ≤ ↑p + planeResidueConstant * ↑f.totalDegree ^ 2 * √↑p

A plane section that is absolutely irreducible over 𝔽_p, for p > 27 d⁴, has at most p + 161 d² √p points.