Affine plane Hasse bounds from the standard zeta package

This module composes the two-sided affine/normalization comparison with the formal zeta Hasse bound. In the separating-coordinate case it gives the external affine-plane estimate with the explicit universal coefficient 8.

The final theorem retains only the standard zeta numerator package and its even-extension square-root estimate. Constructing those data, and removing the separating-coordinate restriction without losing the original bidegree scale, remain separate upstream tasks.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceExtensionCount_one_eq_rationalPlaceCount (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : finiteExtensionClosedPlaceExtensionCount K L 1 = finiteExtensionRationalPlaceCount K L

At extension level one, the closed-place point count is exactly the number of degree-one places.

@[instance_reducible]

noncomputable def BGS.HasseWeil.affineHasseZetaConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the plane affine hasse weil from zeta construction.

Equations

• BGS.HasseWeil.affineHasseZetaConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.affineHasseZetaConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

theorem BGS.HasseWeil.abs_finiteExtensionRationalPlaceCount_sub_card_sub_one_le_of_index_one_and_evenError_isBigO (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (budget : ℕ) (hconstants : algebraicClosure K L = ⊥) (hindex : finiteExtensionDivisorDegreeIndex K L = 1) (hgenus : MarkoffRiemannRoch.FunctionField.genus K L ≤ budget) (herror : (fun (n : ℕ) => ↑(finiteExtensionClosedPlaceExtensionCount K L (2 * n)) - ↑(Fintype.card K) ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑(Fintype.card K) ^ n) : |↑(finiteExtensionRationalPlaceCount K L) - ↑(Fintype.card K) - 1| ≤ ↑(2 * budget + 1) * √↑(Fintype.card K)

Exact constants, divisor index one, a genus budget, and the even-extension square-root estimate give the corresponding rational-place Hasse bound.

noncomputable def BGS.HasseWeil.separatingPlaneCurveRationalPlaceCount {K : Type u_1} [Field K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : ℕ

The rational-place count of a separating plane model, with all projection-dependent instances packaged into a stable natural number.

Equations

• BGS.HasseWeil.separatingPlaneCurveRationalPlaceCount f hf hpartialSecond = BGS.HasseWeil.finiteExtensionRationalPlaceCount K (BGS.CorvajaZannier.PlaneCurveFunctionField f)

theorem BGS.HasseWeil.abs_affinePlaneCurvePoint_card_sub_card_le_eight_mul_bidegree_of_rationalPlaceHasse {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree zetaDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hfirst : 0 < firstDegree) (hsecond : 0 < secondDegree) (hzetaDegree : zetaDegree ≤ 2 * ((firstDegree - 1) * (secondDegree - 1)) + 1) (hnormalization : |↑(separatingPlaneCurveRationalPlaceCount f hf hpartialSecond) - ↑(Fintype.card K) - 1| ≤ ↑zetaDegree * √↑(Fintype.card K)) : |↑(Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f)) - ↑(Fintype.card K)| ≤ 8 * √↑(Fintype.card K) * ↑firstDegree * ↑secondDegree

A rational-place Hasse estimate with the standard bidegree numerator budget transfers to the affine plane count with universal coefficient 8.

The large-secondDegree branch uses the elementary first-coordinate fiber bound. In the small branch the new reverse comparison and the existing forward critical-locus comparison give a common error bounded by four square-root bidegree units; the zeta term costs three and the affine/projective constant costs one.

theorem BGS.HasseWeil.abs_affinePlaneCurveZeros_card_sub_card_le_eight_mul_bidegree_of_standardZeta {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) (P : Polynomial ℂ) (hPzero : P.coeff 0 = 1) (hPdegree : P.natDegree ≤ 2 * ((firstDegree - 1) * (secondDegree - 1)) + 1) : have hf := ⋯; have hx := ⋯; let L := CorvajaZannier.PlaneCurveFunctionField f; let ratAlg := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; HasCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) P → ((fun (n : ℕ) => ↑(finiteExtensionClosedPlaceExtensionCount K L (2 * n)) - ↑(Nat.card K) ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.card K) ^ n) → |↑(External.affinePlaneCurveZeros K f).card - ↑(Fintype.card K)| ≤ 8 * √↑(Fintype.card K) * ↑firstDegree * ↑secondDegree

Standard zeta rationality and the even-extension square-root estimate imply the exact affine-plane shape required by GeneralBivariateAffineHasseWeilTheorem, with coefficient 8, whenever both coordinate projections are separating.

The conclusion is stated using the external finite-set presentation. Thus the remaining gap to the unrestricted external proposition is explicit: the two partial-derivative hypotheses and the upstream zeta package.