The square-field Stepanov zero count

This module turns a semilinear square-field Stepanov auxiliary into the sharp zero-count estimate. The selected points are represented by an injective finite family of finite exhaustive places, all away from a degree-one pole place P.

Membership of the two section families in their one-point Riemann spaces makes every section regular at each selected place. The square-field local vanishing theorem then gives positive order of the nonzero first restriction at every selected place. Its pole budget is ell + (#K) * m, so the degree-one one-point height bound controls the cardinality of the family by that same number.

@[instance_reducible]

noncomputable def BGS.HasseWeil.squareFieldZeroCountConstantAlgebra (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : Algebra S L

The algebra structure from S to L used in the square field stepanov zero count construction.

Equations

• BGS.HasseWeil.squareFieldZeroCountConstantAlgebra S L = ((algebraMap (RatFunc S) L).comp (algebraMap S (RatFunc S))).toAlgebra

theorem BGS.HasseWeil.squareFieldZeroCountConstantTower (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : IsScalarTower S (RatFunc S) L

theorem BGS.HasseWeil.Fintype.card_le_of_squareFieldStepanovAuxiliary (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Fintype S] [DecidableEq S] [Algebra K S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] {alpha : Type u_4} {beta : Type u_5} {iota : Type u_6} [Fintype iota] (P : CorvajaZannier.FiniteExtensionPlace S L) (ell m : ℕ) (f : alpha → L) (df : alpha → ℕ) (g : beta → L) (dg : beta → ℕ) (c : alpha × beta →₀ S) (hf : onePointSectionFamilySpec S L P ell f df) (hg : onePointSectionFamilySpec S L P m g dg) (hdegree : CorvajaZannier.finiteExtensionPlaceDegree S L P = 1) (place : iota → CorvajaZannier.FiniteExtensionFinitePlace S L) (hinjective : Function.Injective place) (haway : ∀ (i : iota), Sum.inl (place i) ≠ P) (hsquare : ∀ (i : iota) (z : (place i).asIdeal.ResidueField), z ^ Fintype.card K ^ 2 = z) (hsecond : (onePointStepanovSecondRestrictionMap S L f g (Fintype.card K)) c = 0) (hfirst : squareFieldStepanovFirstRestriction K S L f g c ≠ 0) : Fintype.card iota ≤ ell + Fintype.card K * m

A square-field Stepanov auxiliary bounds any injective finite family of finite places away from its degree-one pole place.

The quadratic Frobenius identity is required only in the residue field of each selected place. Thus the theorem records exactly the local geometric input used by the semilinear vanishing step, without imposing a global residue-degree assertion.