Even Mahler expansions, and the kernel of Δ^r on ZMod (p^b) → K

Two finite lemmas on Mahler expansions.

• Parity: if G(x) = ∑_{i ≤ D} c_i C(x, i) (x : ℤ, C Mathlib's Ring.choose) is even and c_i = 0 for every even i, then G = 0, in any commutative ring with 2a = 0 → a = 0. The proof: Δ^D G is the constant c_D, and Newton's formula with evenness gives c_D = −c_D for odd D.
• Kernel: on ZMod (p^b) → K, K a field of characteristic p, the kernel of Δ^r (Δ f x = f (x + 1) − f x) is spanned by the binomial functions C(x.val, i), i < r.

Main results

• ConjeturaC.mahlerZ_coeff_eq_zero, ConjeturaC.mahlerZ_coeff_eq_zero_field: the parity lemma.
• ConjeturaC.ker_diffₗ_pow, ConjeturaC.ker_diffₗ_pow': the kernel of Δ^r.

References

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

The parity lemma

Mapping to the proof: a row J < p^a is the full Mahler vector (c_i)_{i ≤ D} of an even function G(x) = ∑_{i ≤ D} c_i C(x, i) on ℤ (values in K = 𝔽_p, p odd). Here C(x, i) for x : ℤ is Mathlib's Ring.choose x i (the integer-valued binomial, C(-x,i) = (-1)^i C(x+i-1,i)), cast to K. This is the statement restricted to integer arguments (which is all the lemma uses); K is any commutative ring in which 2a = 0 → a = 0.

Proof (differs from the descending recursion 2 c_k = ∑_{i>k} …, same content): Δ^D G is the constant c_D; by Newton's formula and evenness, (Δ^D G)(-D) = (-1)^D (Δ^D G)(0), so for odd D, c_D = -c_D, hence c_D = 0; for even D, c_D = 0 by hypothesis; induct on D.

def ConjeturaC.mahlerZ {K : Type u_1} [CommRing K] (D : ℕ) (c : ℕ → K) (x : ℤ) : K

mahlerZ D c x = ∑_{i ≤ D} c_i · C(x, i) for x : ℤ.

Equations

• ConjeturaC.mahlerZ D c x = ∑ i ∈ Finset.range (D + 1), c i * ↑(Ring.choose x i)

theorem ConjeturaC.fwdDiff_ringChoose_succ {K : Type u_1} [CommRing K] (j : ℕ) : (fwdDiff 1 fun (x : ℤ) => ↑(Ring.choose x (j + 1))) = fun (x : ℤ) => ↑(Ring.choose x j)

theorem ConjeturaC.fwdDiff_iter_ringChoose {K : Type u_1} [CommRing K] (n j : ℕ) : ((fwdDiff 1)^[n] fun (x : ℤ) => ↑(Ring.choose x (n + j))) = fun (x : ℤ) => ↑(Ring.choose x j)

theorem ConjeturaC.fwdDiff_iter_zero {M : Type u_2} {G : Type u_3} [AddCommMonoid M] [AddCommGroup G] (h : M) (k : ℕ) : (fwdDiff h)^[k] 0 = 0

theorem ConjeturaC.fwdDiff_iter_ringChoose_lt {K : Type u_1} [CommRing K] {n m : ℕ} (h : m < n) : ((fwdDiff 1)^[n] fun (x : ℤ) => ↑(Ring.choose x m)) = 0

theorem ConjeturaC.fwdDiff_iter_mahlerZ {K : Type u_1} [CommRing K] (D : ℕ) (c : ℕ → K) (y : ℤ) : (fwdDiff 1)^[D] (mahlerZ D c) y = c D

Δ^D of mahlerZ D c is the constant c D.

theorem ConjeturaC.fwdDiff_iter_even {K : Type u_1} [CommRing K] (G : ℤ → K) (heven : ∀ (x : ℤ), G (-x) = G x) (D : ℕ) : (fwdDiff 1)^[D] G (-↑D) = (-1) ^ D * (fwdDiff 1)^[D] G 0

Newton + evenness: (Δ^D G)(-D) = (-1)^D (Δ^D G)(0) for even G.

theorem ConjeturaC.mahlerZ_top_odd {K : Type u_1} [CommRing K] (h2 : ∀ (a : K), 2 * a = 0 → a = 0) (D : ℕ) (c : ℕ → K) (heven : ∀ (x : ℤ), mahlerZ D c (-x) = mahlerZ D c x) (hD : Odd D) : c D = 0

The top coefficient of an even mahlerZ vanishes when D is odd.

theorem ConjeturaC.mahlerZ_coeff_eq_zero {K : Type u_1} [CommRing K] (h2 : ∀ (a : K), 2 * a = 0 → a = 0) (D : ℕ) (c : ℕ → K) (heven : ∀ (x : ℤ), mahlerZ D c (-x) = mahlerZ D c x) (hc : ∀ (i : ℕ), Even i → c i = 0) (i : ℕ) : i ≤ D → c i = 0

Parity lemma. If G(x) = ∑_{i ≤ D} c_i C(x,i) is even on ℤ and c_i = 0 for every even i, then c_i = 0 for all i ≤ D (hence G = 0). K: 2a = 0 → a = 0.

theorem ConjeturaC.mahlerZ_coeff_eq_zero_field {F : Type u_2} [Field F] (h2 : 2 ≠ 0) (D : ℕ) (c : ℕ → F) (heven : ∀ (x : ℤ), mahlerZ D c (-x) = mahlerZ D c x) (hc : ∀ (i : ℕ), Even i → c i = 0) (i : ℕ) : i ≤ D → c i = 0

Field form of the parity lemma ((2 : K) ≠ 0, e.g. K = ZMod p, p odd).

Kernel of Δ^r on ZMod (p^b) → K, char K = p

chooseFun and linearIndependent_choose are those of Formalizations.NumberTheory.MahlerBasis.FiniteMahlerBasis.

def ConjeturaC.diffₗ (N : ℕ) (K : Type u_1) [Field K] : Module.End K (ZMod N → K)

Δ f x = f (x + 1) - f x as a K-linear endomorphism of ZMod N → K.

Equations

• ConjeturaC.diffₗ N K = { toFun := fwdDiff 1, map_add' := ⋯, map_smul' := ⋯ }

theorem ConjeturaC.diffₗ_pow_apply (N : ℕ) (K : Type u_1) [Field K] (r : ℕ) (f : ZMod N → K) : (diffₗ N K ^ r) f = (fwdDiff 1)^[r] f

def ConjeturaC.binF (N : ℕ) (K : Type u_1) [Field K] (i : ℕ) : ZMod N → K

ℕ-indexed binomial function x ↦ C(x.val, i).

Equations

• ConjeturaC.binF N K i x = ↑(x.val.choose i)

theorem ConjeturaC.chooseFun_eq_binF (N : ℕ) (K : Type u_1) [Field K] (i : Fin N) : chooseFun N K i = binF N K ↑i

theorem ConjeturaC.fwdDiff_binF_succ {K : Type u_1} [Field K] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] (b : ℕ) [NeZero (p ^ b)] (i : ℕ) (hi : i + 1 ≠ p ^ b) : fwdDiff 1 (binF (p ^ b) K (i + 1)) = binF (p ^ b) K i

Pascal with wrap-around: Δ C(·, i+1) = C(·, i) on ZMod (p^b), for i + 1 ≠ p^b (the wrap x = p^b - 1 ↦ 0 uses p ∣ C(p^b, i+1)).

theorem ConjeturaC.fwdDiff_binF_zero {K : Type u_1} [Field K] (N : ℕ) : fwdDiff 1 (binF N K 0) = 0

theorem ConjeturaC.fwdDiff_iter_binF {K : Type u_1} [Field K] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] (b : ℕ) [NeZero (p ^ b)] (n j : ℕ) (h : n + j < p ^ b) : (fwdDiff 1)^[n] (binF (p ^ b) K (n + j)) = binF (p ^ b) K j

theorem ConjeturaC.fwdDiff_iter_binF_lt {K : Type u_1} [Field K] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] (b : ℕ) [NeZero (p ^ b)] {n m : ℕ} (h : m < n) (hm : m < p ^ b) : (fwdDiff 1)^[n] (binF (p ^ b) K m) = 0

theorem ConjeturaC.ker_diffₗ_pow {K : Type u_1} [Field K] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] (b : ℕ) [NeZero (p ^ b)] (r : ℕ) (hr : r ≤ p ^ b) : LinearMap.ker (diffₗ (p ^ b) K ^ r) = Submodule.span K (Set.range fun (i : Fin r) => chooseFun (p ^ b) K (Fin.castLE hr i))

Kernel of Δ^r. N = p^b, K a field of characteristic p, r ≤ N: ker Δ^r = span {C(x.val, i) : i < r}.

theorem ConjeturaC.ker_diffₗ_pow' {K : Type u_1} [Field K] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] (b : ℕ) [NeZero (p ^ b)] (r : ℕ) (hr : r ≤ p ^ b) : LinearMap.ker (diffₗ (p ^ b) K ^ r) = Submodule.span K (chooseFun (p ^ b) K '' {i : Fin (p ^ b) | ↑i < r})

Same, with the spanning set written as {chooseFun i : i < r}.