Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

The Carlitz spectral recurrence

Derives the quadratic recurrence and its first terms. See Carlitz (1969) and the two-root formulation in Harcos (2015), introduction (2).

theorem KloostermanWeil.Carlitz.carlitzK1_eq_primeKloosterman (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) : Kseq p t 1 = kloostermanSumPrime p t 1

Normalization of the degree-one Carlitz sum.

theorem KloostermanWeil.Carlitz.carlitz_recurrence (p : ℕ) [Fact (Nat.Prime p)] {t : Fp p} (ht : t ≠ 0) (n : ℕ) : 1 ≤ n → Kseq p t (n + 2) + Kseq p t 1 * Kseq p t (n + 1) + ↑p * Kseq p t n = 0

Carlitz three-term recurrence in prime-modulus normalization.

theorem KloostermanWeil.Carlitz.carlitz_spectral_roots (p : ℕ) [Fact (Nat.Prime p)] {t : Fp p} (ht : t ≠ 0) : ∃ (α : ℂ) (β : ℂ), α + β = -Kseq p t 1 ∧ α * β = ↑p ∧ ∀ (n : ℕ), 1 ≤ n → Kseq p t n = -(α ^ n + β ^ n)

Spectral-root representation of the Carlitz recurrence.

theorem KloostermanWeil.Carlitz.carlitz_recurrence_Kext (p : ℕ) [Fact (Nat.Prime p)] {t : Fp p} (ht : t ≠ 0) (r : ℕ) : Kext p (r + 3) t + Kext p 1 t * Kext p (r + 2) t + ↑p * Kext p (r + 1) t = 0

Recurrence expressed in strictly positive extension degrees.

theorem KloostermanWeil.Carlitz.carlitz_spectral_roots_Kext (p : ℕ) [Fact (Nat.Prime p)] {t : Fp p} (ht : t ≠ 0) : ∃ (α : ℂ) (β : ℂ), α + β = -Kext p 1 t ∧ α * β = ↑p ∧ ∀ (r : ℕ), Kext p (r + 1) t = -(α ^ (r + 1) + β ^ (r + 1))

Spectral-root representation in positive extension degrees.