The general affine bivariate Hasse--Weil theorem

The closed Hasse--Weil theorem for finite separable extensions of K(X) is applied to the function field of a separating absolutely irreducible plane curve. Exact constants and the bidegree genus budget identify its intrinsic Hasse bound, while the existing normalization-to-affine comparison gives the coefficient 8. Frobenius deflation then removes both separating-coordinate hypotheses without changing the affine point count or increasing the supplied bidegree bounds.

theorem BGS.HasseWeil.abs_affinePlaneCurveZeros_card_sub_card_le_eight_mul_bidegree_of_separating {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hfirst : 0 < firstDegree) (hsecond : 0 < secondDegree) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : |↑(External.affinePlaneCurveZeros K f).card - ↑(Fintype.card K)| ≤ 8 * √↑(Fintype.card K) * ↑firstDegree * ↑secondDegree

The coefficient-8 affine Hasse--Weil estimate for a separating absolutely irreducible plane equation.

theorem BGS.HasseWeil.abs_affinePlaneCurveZeros_card_sub_card_le_eight_mul_bidegree (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree : ℕ) (hfirst : 0 < firstDegree) (hsecond : 0 < secondDegree) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : |↑(External.affinePlaneCurveZeros K f).card - ↑(Fintype.card K)| ≤ 8 * √↑(Fintype.card K) * ↑firstDegree * ↑secondDegree

The coefficient-8 affine Hasse--Weil estimate for every absolutely irreducible bivariate equation of positive supplied bidegree.

theorem BGS.HasseWeil.bivariateAffineHasseWeilBound_eight : External.BivariateAffineHasseWeilBound 8

The in-repository inhabitant of the general affine bivariate Hasse--Weil interface.

theorem BGS.HasseWeil.generalBivariateAffineHasseWeilTheorem : External.GeneralBivariateAffineHasseWeilTheorem

The in-repository inhabitant of the general affine bivariate Hasse--Weil interface.