Hasse bounds from even exact constant-extension estimates

This file connects the exact constant-extension closed-place identity to the completed zeta-function and spectral arguments. A uniform two-sided estimate for degree-one places on the exact degree-2n constant extensions becomes the even-extension IsBigO premise used by the power-sum argument. Exact constants then provide the zeta numerator and its degree bound automatically.

The geometric two-sided estimate itself is deliberately left as an explicit hypothesis. Proving it is the remaining Galois-twist boundary; no one-sided Stepanov estimate can replace it.

theorem BGS.HasseWeil.evenExtensionError_isBigO_of_pointwise_bound (q : ℕ) (pointCount : ℕ → ℕ) (A : ℝ) (hbound : ∀ (n : ℕ), 0 < n → |↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1| ≤ A * ↑q ^ n) : (fun (n : ℕ) => ↑(pointCount (2 * n)) - ↑q ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑q ^ n

Pointwise two-sided square-root estimates at every positive even-extension index imply the asymptotic estimate used by the zeta spectral argument.

theorem BGS.HasseWeil.divisibleEvenExtensionError_isBigO_of_pointwise_bound (q δ : ℕ) (pointCount : ℕ → ℕ) (A B : ℝ) (hq : 0 < q) (hA : 0 ≤ A) (hbound : ∀ (n : ℕ), 0 < n → |↑(pointCount (2 * δ * n)) - ↑q ^ (2 * δ * n) - 1| ≤ A + B * (↑q ^ δ) ^ n) : (fun (n : ℕ) => ↑(pointCount (2 * δ * n)) - ↑q ^ (2 * δ * n) - 1) =O[Filter.atTop] fun (n : ℕ) => (↑q ^ δ) ^ n

A pointwise two-sided square-root estimate along one fixed divisible-even subsequence, with a bounded additive error, gives the asymptotic estimate used by the rank-general spectral argument.

@[instance_reducible]

noncomputable def BGS.HasseWeil.evenConstantExtensionBaseConstantAlgebra (C : Type u_1) (N : Type u_2) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C N

The algebra structure from C to N used in the finite extension hasse bound from even constant extensions construction.

Equations

• BGS.HasseWeil.evenConstantExtensionBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.evenConstantExtensionBaseConstantTower (C : Type u_1) (N : Type u_2) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

theorem BGS.HasseWeil.finiteExtensionClosedPlaceEvenError_isBigO_of_exactConstantExtension_bound (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (p : ℕ) [Fact (Nat.Prime p)] [CharP C p] (hExact : algebraicClosure C N = ⊥) (A : ℝ) (hbound : ∀ (n : ℕ) (hn : 0 < n), let S := FiniteField.Extension C p (2 * n); |↑(exactConstantExtensionClosedPlaceExtensionCount C S N hExact 1) - ↑(Nat.card S) - 1| ≤ A * ↑(Nat.card C) ^ n) : (fun (n : ℕ) => ↑(finiteExtensionClosedPlaceExtensionCount C N (2 * n)) - ↑(Nat.card C) ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.card C) ^ n

The exact constant-extension count identity transports a pointwise two-sided estimate for rational places on every canonical degree-2n constant extension to the even-extension IsBigO estimate for the original closed-place count sequence.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceHasseBound_of_exactConstants_and_evenError (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (budget : ℕ) (hExact : algebraicClosure C N = ⊥) (hgenus : MarkoffRiemannRoch.FunctionField.genus C N ≤ budget) (herror : (fun (n : ℕ) => ↑(finiteExtensionClosedPlaceExtensionCount C N (2 * n)) - ↑(Nat.card C) ^ (2 * n) - 1) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.card C) ^ n) : |↑(finiteExtensionClosedPlaceExtensionCount C N 1) - ↑(Nat.card C) - 1| ≤ (2 * ↑budget + 1) * √↑(Nat.card C)

Exact constants make the standard zeta numerator automatic. Hence the even-extension error estimate is the only analytic premise left for the closed-place Hasse bound, apart from the stated genus budget.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceHasseBound_of_exactConstants_and_divisibleEvenError (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (budget δ : ℕ) (hExact : algebraicClosure C N = ⊥) (hgenus : MarkoffRiemannRoch.FunctionField.genus C N ≤ budget) (hδ : 0 < δ) (herror : (fun (n : ℕ) => ↑(finiteExtensionClosedPlaceExtensionCount C N (2 * δ * n)) - ↑(Nat.card C) ^ (2 * δ * n) - 1) =O[Filter.atTop] fun (n : ℕ) => (↑(Nat.card C) ^ δ) ^ n) : |↑(finiteExtensionClosedPlaceExtensionCount C N 1) - ↑(Nat.card C) - 1| ≤ (2 * ↑budget + 1) * √↑(Nat.card C)

Exact constants make the zeta package automatic also when the geometric error estimate is available only along one fixed positive divisible-even subsequence.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceHasseBound_of_exactConstants_and_divisibleEvenError_bound (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (budget δ : ℕ) (hExact : algebraicClosure C N = ⊥) (hgenus : MarkoffRiemannRoch.FunctionField.genus C N ≤ budget) (hδ : 0 < δ) (A B : ℝ) (hA : 0 ≤ A) (hbound : ∀ (n : ℕ), 0 < n → |↑(finiteExtensionClosedPlaceExtensionCount C N (2 * δ * n)) - ↑(Nat.card C) ^ (2 * δ * n) - 1| ≤ A + B * (↑(Nat.card C) ^ δ) ^ n) : |↑(finiteExtensionClosedPlaceExtensionCount C N 1) - ↑(Nat.card C) - 1| ≤ (2 * ↑budget + 1) * √↑(Nat.card C)

The selected Lorenzini endpoint at the spectral boundary. A uniform pointwise two-sided estimate along one positive divisible-even subsequence, allowing a fixed additive error, implies the degree-one closed-place Hasse bound. Exact constants supply the zeta numerator, index one, and the trace formula internally.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceHasseBound_of_evenExactConstantExtension_bound (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (p : ℕ) [Fact (Nat.Prime p)] [CharP C p] (budget : ℕ) (hExact : algebraicClosure C N = ⊥) (hgenus : MarkoffRiemannRoch.FunctionField.genus C N ≤ budget) (A : ℝ) (hbound : ∀ (n : ℕ) (hn : 0 < n), let S := FiniteField.Extension C p (2 * n); |↑(exactConstantExtensionClosedPlaceExtensionCount C S N hExact 1) - ↑(Nat.card S) - 1| ≤ A * ↑(Nat.card C) ^ n) : |↑(finiteExtensionClosedPlaceExtensionCount C N 1) - ↑(Nat.card C) - 1| ≤ (2 * ↑budget + 1) * √↑(Nat.card C)

The fully connected conditional endpoint: a uniform two-sided estimate for rational places on the canonical even exact constant extensions implies the base closed-place Hasse bound. Zeta rationality, the trace formula, and degree index one are all discharged internally.