Abel's lemma at j = 0, by finite Fourier analysis

Let K be a field of characteristic 0, N = 2m + 1 ≥ 3, ζ a primitive N-th root of unity, U(Z) = 2Z/(Z² − 1) and B_{1,χ} = N⁻¹ ∑_a χ(a) a.val. For a primitive Dirichlet character χ modulo N, ∑_c χ⁻¹(c) U(ζ^c) = 2 τ (1 − χ(2)) B_{1,χ}, with τ a Gauss sum. The proof is purely algebraic (no L-functions); the Gauss-sum step is Mathlib's gaussSum_mulShift_of_isPrimitive.

Main results

• ConjeturaC.sub_one_mul_inv_eq: w^N = 1, w ≠ 1 ⇒ (w − 1)⁻¹ = N⁻¹ ∑_{k<N} k w^k.
• ConjeturaC.U_pow_eq: U(ζ^c) = (2/N) ∑_{k<N} k ζ^{c(2k+1)} for c ≠ 0.
• ConjeturaC.sum_mul_char_two_mul_add_one: ∑_{k<N} k χ(2k+1) = (1 − χ(2)) ∑_a χ(a) a.val.
• ConjeturaC.abel_zero_of_gauss: the identity under an explicit Gauss-sum hypothesis.
• ConjeturaC.abel_zero: the identity for a primitive χ, τ = gaussSum χ⁻¹ (zmodChar N ζ).

References

• C. Marín, Reading Iwasawa λ-invariants from Mahler matrices modulo p: programs, data and Lean files, Zenodo (2026), doi:10.5281/zenodo.23085315.

def ConjeturaC.U {K : Type u_1} [Field K] (z : K) : K

U(Z) = 2Z/(Z^2 - 1).

Equations

• ConjeturaC.U z = 2 * z / (z ^ 2 - 1)

noncomputable def ConjeturaC.B1 {K : Type u_1} [Field K] {N : ℕ} [NeZero N] (χ : MulChar (ZMod N) K) : K

B_{1,χ} = (1/N) Σ_a χ(a) a.val.

Equations

• ConjeturaC.B1 χ = (↑N)⁻¹ * ∑ a : ZMod N, χ a * ↑a.val

(a) finite Fourier identity for 1/(w-1)

theorem ConjeturaC.sub_one_mul_sum_mul_pow {K : Type u_1} [CommRing K] (w : K) (n : ℕ) : (w - 1) * ∑ k ∈ Finset.range n, ↑k * w ^ k = ↑n * w ^ n - w ^ n - ∑ k ∈ Finset.range n, w ^ k + 1

theorem ConjeturaC.sub_one_mul_inv_eq {K : Type u_1} [Field K] [CharZero K] {N : ℕ} (hN : 0 < N) {w : K} (hw : w ^ N = 1) (hw1 : w ≠ 1) : (w - 1)⁻¹ = (↑N)⁻¹ * ∑ k ∈ Finset.range N, ↑k * w ^ k

sums over ZMod N as sums over range N

theorem ConjeturaC.sum_zmod_eq_sum_range {M : Type u_1} [AddCommMonoid M] (N : ℕ) [NeZero N] (f : ZMod N → M) : ∑ a : ZMod N, f a = ∑ n ∈ Finset.range N, f ↑n

theorem ConjeturaC.sum_range_two_mul_add_one_parity {M : Type u_1} [AddCommMonoid M] (g : ℕ → M) (m : ℕ) : ∑ n ∈ Finset.range (2 * m + 1), g n = g 0 + ∑ i ∈ Finset.range m, (g (2 * i + 1) + g (2 * i + 2))

theorem ConjeturaC.sum_range_two_mul_add_one_halves {M : Type u_1} [AddCommMonoid M] (g : ℕ → M) (m : ℕ) : ∑ n ∈ Finset.range (2 * m + 1), g n = ∑ n ∈ Finset.range m, g n + g m + ∑ j ∈ Finset.range m, g (m + 1 + j)

(c) the reindexing a = 2k+1

theorem ConjeturaC.cast_add_self {m r : ℕ} : ↑(2 * m + 1 + r) = ↑r

theorem ConjeturaC.sum_mul_char_two_mul_add_one {K : Type u_1} [Field K] {m : ℕ} (hm : 1 ≤ m) (χ : MulChar (ZMod (2 * m + 1)) K) (hχ : χ ≠ 1) : ∑ k ∈ Finset.range (2 * m + 1), ↑k * χ ↑(2 * k + 1) = (1 - χ 2) * ∑ a : ZMod (2 * m + 1), χ a * ↑a.val

(b) U(ζ^c) as a finite Fourier sum

theorem ConjeturaC.U_pow_eq {K : Type u_1} [Field K] [CharZero K] {m : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ (2 * m + 1)) (c : ZMod (2 * m + 1)) (hc : c ≠ 0) : U (ζ ^ c.val) = 2 / ↑(2 * m + 1) * ∑ k ∈ Finset.range (2 * m + 1), ↑k * ζ ^ (c.val * (2 * k + 1))

(d) Abel's lemma at j = 0, Gauss-sum property as hypothesis

theorem ConjeturaC.abel_zero_of_gauss {K : Type u_1} [Field K] [CharZero K] {m : ℕ} (hm : 1 ≤ m) {ζ : K} (hζ : IsPrimitiveRoot ζ (2 * m + 1)) (χ ψ : MulChar (ZMod (2 * m + 1)) K) (hχ : χ ≠ 1) (τ : K) (hgauss : ∀ (a : ZMod (2 * m + 1)), ∑ c : ZMod (2 * m + 1), ψ c * ζ ^ (a * c).val = χ a * τ) : ∑ c : ZMod (2 * m + 1), ψ c * U (ζ ^ c.val) = 2 * τ * (1 - χ 2) * B1 χ

(e) primitive Dirichlet characters: the Gauss property from Mathlib

theorem ConjeturaC.abel_zero {K : Type u_1} [Field K] [CharZero K] {m : ℕ} (hm : 1 ≤ m) {ζ : K} (hζ : IsPrimitiveRoot ζ (2 * m + 1)) (χ : DirichletCharacter K (2 * m + 1)) (hχ : χ.IsPrimitive) : ∑ c : ZMod (2 * m + 1), χ⁻¹ c * U (ζ ^ c.val) = 2 * gaussSum χ⁻¹ (AddChar.zmodChar (2 * m + 1) ⋯) * (1 - χ 2) * B1 χ