Degree support and the constant-extension zeta identity

This file specializes the formal constant-extension identity to the exhaustive closed-place point-count sequence. The divisor-degree index itself supplies the required divisibility support.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceExtensionCount_eq_zero_of_not_dvd_index (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] (n : ℕ) (hn : ¬finiteExtensionDivisorDegreeIndex K L ∣ n) : finiteExtensionClosedPlaceExtensionCount K L n = 0

The exhaustive closed-place count vanishes outside multiples of the divisor-degree index.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceZeta_hasDegreeExtensionIdentity (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] (extendedPointCount : ℕ → ℕ) (hcount : ∀ (r : ℕ), extendedPointCount r = finiteExtensionClosedPlaceExtensionCount K L (finiteExtensionDivisorDegreeIndex K L * r)) : HasFormalDegreeExtensionZetaIdentity (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (formalPointCountZeta extendedPointCount) (finiteExtensionDivisorDegreeIndex K L)

Once the geometric constant extension supplies its exact point-count relation, the corresponding zeta identity follows automatically.