The noncircular indexed F. K. Schmidt argument

The degree-index argument must not assume that the constant extension already has divisor-degree index one. This file repairs that dependency: both the original zeta series and the zeta series after extending constants are allowed to have indexed denominators.

After substituting T ^ d into the extended indexed denominator, clearing denominators gives

P_extended(T ^ d) D_d(T) ^ d = P(T) ^ d D_(d e)(T).

Here d is the original degree index and e is the (a priori arbitrary) degree index after constant extension. If d > 1, the derivative at T = 1 of the left side vanishes to order at least two. The right side has a simple zero there when P(1) ≠ 0. This contradiction proves d = 1 without assuming the conclusion for the constant extension.

theorem BGS.HasseWeil.subst_indexedCurveZetaDenominator (q d e : ℕ) (hd : 0 < d) : PowerSeries.subst (PowerSeries.X ^ d) (indexedCurveZetaDenominator (q ^ d) e) = indexedCurveZetaDenominator q (d * e)

Substituting T ^ d into an indexed denominator over the degree-d constant extension multiplies its index by d.

theorem BGS.HasseWeil.clearedNumeratorIdentity_of_two_indexed_rationalForms (Z extendedZeta : PowerSeries ℂ) (q d e : ℕ) (P extendedP : Polynomial ℂ) (hd : 0 < d) (hindexed : HasIndexedCurveZetaRationalForm Z q d P) (hextended : HasIndexedCurveZetaRationalForm extendedZeta (q ^ d) e extendedP) (hextension : HasFormalDegreeExtensionZetaIdentity Z extendedZeta d) : extendedP.comp (Polynomial.X ^ d) * indexedCurveZetaDenominatorPolynomial q d ^ d = P ^ d * indexedCurveZetaDenominatorPolynomial q (d * e)

Clearing two indexed rational forms across a degree-d constant extension. In particular, no ordinary rational form is assumed for the extended curve.

theorem BGS.HasseWeil.indexedCurveZetaDenominatorPolynomial_derivative_eval_one (q n : ℕ) : Polynomial.eval 1 (Polynomial.derivative (indexedCurveZetaDenominatorPolynomial q n)) = -↑n * (1 - ↑q ^ n)

The indexed denominator has a simple zero at T = 1; this is its exact derivative there.

theorem BGS.HasseWeil.indexedCurveZetaDenominatorPolynomial_derivative_eval_one_ne_zero (q n : ℕ) (hq : 1 < q) (hn : 0 < n) : Polynomial.eval 1 (Polynomial.derivative (indexedCurveZetaDenominatorPolynomial q n)) ≠ 0

Over a nontrivial finite field, every positive-index zeta denominator has a nonzero derivative at T = 1.

theorem BGS.HasseWeil.derivative_eval_one_mul_indexedDenominator_pow_eq_zero (Q : Polynomial ℂ) (q d : ℕ) (htwo : 2 ≤ d) : Polynomial.eval 1 (Polynomial.derivative (Q * indexedCurveZetaDenominatorPolynomial q d ^ d)) = 0

At T = 1, a product containing at least two copies of the indexed denominator has zero derivative.

theorem BGS.HasseWeil.derivative_eval_one_pow_mul_indexedDenominator (P : Polynomial ℂ) (q d n : ℕ) : Polynomial.eval 1 (Polynomial.derivative (P ^ d * indexedCurveZetaDenominatorPolynomial q n)) = Polynomial.eval 1 P ^ d * Polynomial.eval 1 (Polynomial.derivative (indexedCurveZetaDenominatorPolynomial q n))

At T = 1, differentiating a numerator times one indexed denominator leaves the numerator value times the derivative of that denominator.

theorem BGS.HasseWeil.degreeIndex_eq_one_of_twoIndexed_clearedNumeratorIdentity (q d e : ℕ) (P extendedP : Polynomial ℂ) (hq : 1 < q) (hd : 0 < d) (he : 0 < e) (hPone : Polynomial.eval 1 P ≠ 0) (hcleared : extendedP.comp (Polynomial.X ^ d) * indexedCurveZetaDenominatorPolynomial q d ^ d = P ^ d * indexedCurveZetaDenominatorPolynomial q (d * e)) : d = 1

Pure polynomial form of the noncircular F. K. Schmidt conclusion.

theorem BGS.HasseWeil.degreeIndex_eq_one_of_two_indexed_rationalForms_and_degreeExtension (Z extendedZeta : PowerSeries ℂ) (q d e : ℕ) (P extendedP : Polynomial ℂ) (hq : 1 < q) (hd : 0 < d) (he : 0 < e) (hPone : Polynomial.eval 1 P ≠ 0) (hindexed : HasIndexedCurveZetaRationalForm Z q d P) (hextended : HasIndexedCurveZetaRationalForm extendedZeta (q ^ d) e extendedP) (hextension : HasFormalDegreeExtensionZetaIdentity Z extendedZeta d) : d = 1

Noncircular formal F. K. Schmidt theorem. The extended zeta series may have any positive degree index e; only indexed rationality is required.