The rank profile of a Mahler matrix modulo p: the arithmetic

For an odd prime p, row J > 0 of the Mahler matrix of a measure depends on the rows above it exactly when u < p r_b, where J + 1 = p^s u with p ∤ u, b ≡ J (mod p − 1), and r_b is the λ-invariant of the ω^b-branch. This file formalizes the arithmetic of that criterion and of its consequences. The criterion itself enters as the explicit hypothesis ThmA p r Dep, and the comparison with the graded layers as the explicit hypothesis hB; neither is proved here.

Main results

• FilasIII.crit_iff_seed, FilasIII.seed_injective, FilasIII.thmA_seeds: the seed form of the criterion, rows Φ^s(d_b(i)) for i < r_b, pairwise distinct.
• FilasIII.cor_low, FilasIII.cor_phi, FilasIII.cor_phi_top, FilasIII.Jk_Phi, FilasIII.kstar_count, FilasIII.cor_rank: the corollaries on low rows, the map Φ, the indices k* and the rank.
• FilasIII.cor_C, FilasIII.cor_D, FilasIII.jD_zero_strictMono, FilasIII.jD_zero_range, FilasIII.cor_D_first: the arithmetic of the two corollaries on graded layers, given both hypotheses.

References

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

Objects

def FilasIII.Phi (p J : ℕ) : ℕ

Φ(J) = p(J+1) - 1.

Equations

• FilasIII.Phi p J = p * (J + 1) - 1

def FilasIII.brk (p b i : ℕ) : ℕ

[b-i]_{p-1}: least nonnegative residue of b - i modulo p - 1.

Equations

• FilasIII.brk p b i = ((↑b - ↑i) % (↑p - 1)).toNat

def FilasIII.dseed (p b i : ℕ) : ℕ

d_b(i) = p i + [b-i]_{p-1}.

Equations

• FilasIII.dseed p b i = p * i + FilasIII.brk p b i

def FilasIII.uPart (p J : ℕ) : ℕ

u(J): the prime-to-p part of J + 1.

Equations

• FilasIII.uPart p J = (J + 1) / p ^ (J + 1).factorization p

def FilasIII.Crit (p : ℕ) (r : ℕ → ℕ∞) (J : ℕ) : Prop

The criterion of Theorem A: u < p r_b, b ≡ J (mod p-1), b ∈ [0,p-2].

Equations

• FilasIII.Crit p r J = (↑(FilasIII.uPart p J) < ↑p * r (J % (p - 1)))

def FilasIII.ThmA (p : ℕ) (r : ℕ → ℕ∞) (Dep : ℕ → ℕ → Prop) : Prop

Theorem A (measure part), taken as a hypothesis: for 0 < J < p^a, row J at resolution p^a is dependent iff u < p r_b. Dep a J = "row J of B at level p^a is dependent".

Equations

• FilasIII.ThmA p r Dep = ∀ (a J : ℕ), 0 < J → J < p ^ a → (Dep a J ↔ FilasIII.Crit p r J)

Basic arithmetic

theorem FilasIII.Phi_add_one {p : ℕ} (hp : 0 < p) (J : ℕ) : Phi p J + 1 = p * (J + 1)

theorem FilasIII.Phi_iter_add_one {p : ℕ} (hp : 0 < p) (s d : ℕ) : (Phi p)^[s] d + 1 = p ^ s * (d + 1)

theorem FilasIII.Phi_iter {p : ℕ} (hp : 0 < p) (s d : ℕ) : (Phi p)^[s] d = p ^ s * (d + 1) - 1

theorem FilasIII.factor_unique {p : ℕ} (hp : Nat.Prime p) {s u : ℕ} (hu : ¬p ∣ u) : (p ^ s * u).factorization p = s ∧ p ^ s * u / p ^ (p ^ s * u).factorization p = u

Uniqueness of the decomposition n = p^s u, p ∤ u.

theorem FilasIII.not_dvd_mul_add {p i e : ℕ} (he0 : 0 < e) (he : e < p) : ¬p ∣ p * i + e

theorem FilasIII.brk_cast {p : ℕ} (hp : 2 ≤ p) (b i : ℕ) : ↑(brk p b i) = (↑b - ↑i) % (↑p - 1)

theorem FilasIII.brk_lt {p : ℕ} (hp : 2 ≤ p) (b i : ℕ) : brk p b i < p - 1

theorem FilasIII.brk_eq_of {p b i δ : ℕ} (hp : 2 ≤ p) (hδ : δ < p - 1) (h : ↑p - 1 ∣ ↑δ - (↑b - ↑i)) : brk p b i = δ

[b-i]_{p-1} is the unique δ ∈ [0,p-2] with δ ≡ b - i (mod p-1).

theorem FilasIII.brk_dvd {p : ℕ} (hp : 2 ≤ p) (b i : ℕ) : ↑p - 1 ∣ ↑(brk p b i) - (↑b - ↑i)

theorem FilasIII.key_lt {p i e : ℕ} (hp : 0 < p) (he : e < p) (r : ℕ∞) : ↑(p * i + e) < ↑p * r ↔ ↑i < r

p i + e < p r ↔ i < r in ℕ∞ for e < p.

theorem FilasIII.dseed_succ_not_dvd {p : ℕ} (hp : 2 ≤ p) (b i : ℕ) : ¬p ∣ dseed p b i + 1

theorem FilasIII.dseed_div {p : ℕ} (hp : 2 ≤ p) (b i : ℕ) : (dseed p b i + 1) / p = i

theorem FilasIII.seed_decomp {p : ℕ} (hp : Nat.Prime p) (b s i : ℕ) : ((Phi p)^[s] (dseed p b i) + 1).factorization p = s ∧ uPart p ((Phi p)^[s] (dseed p b i)) = dseed p b i + 1

Φ^s(d_b(i)) + 1 = p^s (d_b(i)+1), so v_p = s and u = d_b(i)+1.

theorem FilasIII.seed_mod {p : ℕ} (hp : 2 ≤ p) {b : ℕ} (hb : b < p - 1) (s i : ℕ) : (Phi p)^[s] (dseed p b i) % (p - 1) = b

Φ^s(d_b(i)) ≡ b (mod p-1).

theorem FilasIII.decomp {p : ℕ} (hp : Nat.Prime p) (J : ℕ) : uPart p J = dseed p (J % (p - 1)) (uPart p J / p) + 1 ∧ J = (Phi p)^[(J + 1).factorization p] (dseed p (J % (p - 1)) (uPart p J / p))

Every J is Φ^s(d_b(i)) with s = v_p(J+1), b = J mod (p-1), i = ⌊u/p⌋, and u = d_b(i) + 1.

Theorem A: the seed form and distinctness

theorem FilasIII.crit_iff_seed {p : ℕ} (hp : Nat.Prime p) {b J : ℕ} (hJb : J % (p - 1) = b) (r : ℕ∞) : ↑(uPart p J) < ↑p * r ↔ ∃ (s : ℕ) (i : ℕ), ↑i < r ∧ J = (Phi p)^[s] (dseed p b i)

Arithmetic core of Theorem A: for J ≡ b (mod p-1), b ∈ [0,p-2], u(J) < p r ↔ J = Φ^s(d_b(i)) for some s ≥ 0 and i < r. (Valid for every J, including J = 0, which is Φ^0(d_0(0)).)

theorem FilasIII.seed_injective {p : ℕ} (hp : Nat.Prime p) (b : ℕ) : Function.Injective fun (x : ℕ × ℕ) => (Phi p)^[x.1] (dseed p b x.2)

Distinctness in Theorem A: (s,i) ↦ Φ^s(d_b(i)) is injective.

theorem FilasIII.thmA_seeds {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) (a : ℕ) {b : ℕ} (hb : b < p - 1) (J : ℕ) : 0 < J ∧ J < p ^ a ∧ J % (p - 1) = b ∧ Dep a J ↔ 0 < J ∧ J < p ^ a ∧ ∃ (s : ℕ) (i : ℕ), ↑i < r b ∧ J = (Phi p)^[s] (dseed p b i)

Theorem A, seed form (thm:A, "Equivalently"), with the criterion u < p r_b as hypothesis hA: the positive rows J < p^a, J ≡ b (mod p-1), that are dependent are exactly the Φ^s(d_b(i)) with 0 < Φ^s(d_b(i)) < p^a, s ≥ 0, i < r_b.

Corollary 3.2 (cor:phi)

theorem FilasIII.Phi_eq {p : ℕ} (hp : 0 < p) (J : ℕ) : Phi p J = J + (p - 1) * (J + 1)

theorem FilasIII.Crit_Phi {p : ℕ} (hp : Nat.Prime p) (r : ℕ → ℕ∞) (J : ℕ) : Crit p r (Phi p J) ↔ Crit p r J

theorem FilasIII.cor_phi {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a J : ℕ} (h0 : 0 < J) (hJ : J < p ^ a) : Dep a J ↔ Dep (a + 1) (Phi p J)

Corollary 3.2 (cor:phi), first part: for 0 < J < p^a, row J is dependent at resolution p^a iff row Φ(J) is dependent at resolution p^{a+1}.

theorem FilasIII.cor_phi_top {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a : ℕ} (ha : 1 ≤ a) : Dep a (p ^ a - 1) ↔ 0 < r 0

Corollary 3.2 (cor:phi), second part: row p^a - 1 is dependent iff r_0 > 0.

Corollary 3.1 (cor:low)

theorem FilasIII.dseed_zero_zero {p : ℕ} (hp : 2 ≤ p) : dseed p 0 0 = 0

theorem FilasIII.dseed_zero {p : ℕ} (hp : 2 ≤ p) {i : ℕ} (hi1 : 1 ≤ i) (hi : i ≤ p - 2) : dseed p 0 i = (i + 1) * (p - 1)

theorem FilasIII.cor_low {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) (a : ℕ) {n : ℕ} (hr : r 0 = ↑n) (hn1 : 1 ≤ n) (hn : n ≤ p - 1) (J : ℕ) : 0 < J ∧ J < p ^ a ∧ J % (p - 1) = 0 ∧ Dep a J ↔ (∃ (s : ℕ), 1 ≤ s ∧ s ≤ a ∧ J = p ^ s - 1) ∨ ∃ (s : ℕ) (i : ℕ), s + 2 ≤ a ∧ 1 ≤ i ∧ i ≤ n - 1 ∧ J = p ^ s * ((i + 1) * (p - 1) + 1) - 1

Corollary 3.1 (cor:low), with Theorem A as hypothesis: if 1 ≤ r_0 = n ≤ p - 1, the dependent rows 0 < J < p^a with J ≡ 0 (mod p-1) are {p^s - 1 : 1 ≤ s ≤ a} ∪ {p^s((i+1)(p-1)+1) - 1 : 0 ≤ s ≤ a-2, 1 ≤ i ≤ r_0 - 1} (s ≤ a - 2 written s + 2 ≤ a, which is empty for a < 2, as in the paper).

Corollary 3.3 (cor:kstar)

def FilasIII.Jk (p a0 k : ℕ) : ℕ

J^{(a_0)}_k = p^{a_0-2}(k(p-1)+1) - 1.

Equations

• FilasIII.Jk p a0 k = p ^ (a0 - 2) * (k * (p - 1) + 1) - 1

def FilasIII.kstar (p n : ℕ) : ℕ

k* = ⌈p n/(p-1)⌉, written in ℕ (see kstar_spec).

Equations

• FilasIII.kstar p n = (p * n + (p - 2)) / (p - 1)

theorem FilasIII.kstar_spec {p : ℕ} (hp : 2 ≤ p) (n : ℕ) : p * n ≤ kstar p n * (p - 1) ∧ kstar p n * (p - 1) < p * n + (p - 1)

kstar p n is the ceiling of p n/(p-1): (k*-1)(p-1) < p n ≤ k*(p-1).

theorem FilasIII.Jk_add_one {p : ℕ} (hp : 0 < p) (a0 k : ℕ) : Jk p a0 k + 1 = p ^ (a0 - 2) * (k * (p - 1) + 1)

theorem FilasIII.Jk_Phi {p : ℕ} (hp : 0 < p) (a0 j : ℕ) : Jk p a0 (p * j + 1) = Phi p (Jk p a0 j)

First claim of cor:kstar: J_{pj+1} = Φ(J_j). (Holds for every j, also j = 0.)

theorem FilasIII.Jk_pos {p : ℕ} (hp : 2 ≤ p) (a0 : ℕ) {k : ℕ} (hk : 1 ≤ k) : 0 < Jk p a0 k

theorem FilasIII.Jk_mono {p : ℕ} (hp : 0 < p) (a0 : ℕ) {k k' : ℕ} (h : k ≤ k') : Jk p a0 k ≤ Jk p a0 k'

theorem FilasIII.Jk_mod {p : ℕ} (hp : 2 ≤ p) (a0 k : ℕ) : Jk p a0 k % (p - 1) = 0

theorem FilasIII.Crit_Jk {p : ℕ} (hp : Nat.Prime p) (r : ℕ → ℕ∞) (a0 k : ℕ) : Crit p r (Jk p a0 k) ↔ ↑((k * (p - 1) + 1) / p ^ (k * (p - 1) + 1).factorization p) < ↑p * r 0

theorem FilasIII.cor_kstar_zero {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a0 a1 : ℕ} (hr : r 0 = 0) (hlt : Jk p a0 1 < p ^ a1) : ¬Dep a1 (Jk p a0 1)

Corollary 3.3 (cor:kstar), case r_0 = 0: row J_1 is new (so k* = 1).

theorem FilasIII.cor_kstar_top {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a0 a1 : ℕ} (hr : r 0 = ⊤) {k : ℕ} (hk : 1 ≤ k) (hlt : Jk p a0 k < p ^ a1) : Dep a1 (Jk p a0 k)

Corollary 3.3 (cor:kstar), case r_0 = ∞: every row of the progression is dependent.

theorem FilasIII.cor_kstar_below {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a0 a1 n : ℕ} (hr : r 0 = ↑n) (hn : 1 ≤ n) {k : ℕ} (hk : 1 ≤ k) (hks : k < kstar p n) (hlt : Jk p a0 k < p ^ a1) : Dep a1 (Jk p a0 k)

Corollary 3.3 (cor:kstar), case 1 ≤ r_0 = n < ∞, rows before k*: every J_k with 1 ≤ k < k* = ⌈p n/(p-1)⌉ (read at a resolution containing it) is dependent.

theorem FilasIII.cor_kstar_new {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a0 a1 n : ℕ} (hr : r 0 = ↑n) (hn : 1 ≤ n) (hlt : Jk p a0 (kstar p n) < p ^ a1) : ¬Dep a1 (Jk p a0 (kstar p n))

Corollary 3.3 (cor:kstar), case 1 ≤ r_0 = n < ∞, the row k*: if J_{k*} lies below the resolution, it is new. With cor_kstar_below, k* = ⌈p r_0/(p-1)⌉ is the least k ≥ 1 with J_k new; it depends neither on a_0 nor on a_1.

theorem FilasIII.cor_kstar_beyond {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a0 a1 n : ℕ} (hr : r 0 = ↑n) (hn : 1 ≤ n) (hge : p ^ a1 ≤ Jk p a0 (kstar p n)) {k : ℕ} (hk : 1 ≤ k) (hlt : Jk p a0 k < p ^ a1) : Dep a1 (Jk p a0 k)

Corollary 3.3 (cor:kstar), last sentence: if J_{k*} ≥ p^{a_1}, every row of the progression below p^{a_1} is dependent.

Corollary 3.4 (cor:rank)

theorem FilasIII.sum_count (N : ℕ) (r : ℕ∞) : (∑ i ∈ Finset.range N, if ↑i < r then 0 else 1) = (↑N - r).toNat

theorem FilasIII.cor_rank {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a : ℕ} (ha : 1 ≤ a) (M0 : Prop) (h0 : Dep a 0 ↔ M0) : {J ∈ Finset.range (p ^ a) | ¬Dep a J}.card = (if M0 then 0 else 1) + ∑ b ∈ Finset.range (p - 1), ∑ t ∈ Finset.range a, (↑(p ^ t) - r b).toNat

Corollary 3.4 (cor:rank), with Theorem A as hypothesis: the number of new rows of B at level p^a is [μ(ℤ_p) ≠ 0] + Σ_{b=0}^{p-2} Σ_{t=0}^{a-1} max(p^t - r_b, 0) (max(p^t - ∞, 0) = 0 is the truncated subtraction of ℕ∞). M0 stands for μ(ℤ_p) = 0, and h0 is the row-0 clause of thm:A.

cor:kstar, "Equivalently": r_0 = (k* - 1) - #{j ≥ 1 : pj + 1 < k*}

theorem FilasIII.kstar_count {p : ℕ} (hp : 2 ≤ p) {n : ℕ} (hn : 1 ≤ n) : n = kstar p n - 1 - {j ∈ Finset.range (kstar p n) | 1 ≤ j ∧ p * j + 1 < kstar p n}.card

Arithmetic of Corollaries C and D (thm:B as hypothesis)

theorem FilasIII.ordCompl_prime_self {p : ℕ} (hp : Nat.Prime p) : p / p ^ p.factorization p = 1

theorem FilasIII.cor_C {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a : ℕ} (ha : 2 ≤ a) {Vanish : ℕ → Prop} (hB : ∀ j < p ^ a - p ^ (a - 1), Vanish j ↔ Dep a j) {k : ℕ} (hk1 : 1 ≤ k) (hk : k ≤ p - 1) : Vanish (Jk p a k) ↔ ↑k ≤ r 0

Corollary C (cor:C), with thm:A and thm:B as hypotheses. Vanish j = "the χ-component of G_{P+j} vanishes"; hB is thm:B (= lem:M1 + lem:bridge, not formalized); r 0 = r_{χ,0}, which lem:R (not formalized) identifies with λ̃(χ). For 1 ≤ k ≤ p - 1, the component at P + J_k vanishes iff k ≤ r_{χ,0}.

def FilasIII.jD (p b i : ℕ) : ℕ

j_{b,i} = p i + [b-i]_{p-1}, except j_{0,0} = p - 1 (cor:D).

Equations

• FilasIII.jD p b i = if b = 0 ∧ i = 0 then p - 1 else FilasIII.dseed p b i

theorem FilasIII.brk_self {p b : ℕ} (hp : 2 ≤ p) (hb : b < p - 1) : brk p b 0 = b

theorem FilasIII.jD_crit {p : ℕ} (hp : Nat.Prime p) (r : ℕ → ℕ∞) {b : ℕ} (hb : b < p - 1) (i : ℕ) : 0 < jD p b i ∧ jD p b i % (p - 1) = b ∧ (Crit p r (jD p b i) ↔ ↑i < r b)

Arithmetic of cor:D: j_{b,i} > 0, j_{b,i} ≡ b, and u(j_{b,i}) < p r ↔ i < r.

theorem FilasIII.cor_D {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a : ℕ} {Vanish : ℕ → Prop} (hB : ∀ j < p ^ a - p ^ (a - 1), Vanish j ↔ Dep a j) {b : ℕ} (hb : b < p - 1) {i : ℕ} (hj : jD p b i < p ^ a - p ^ (a - 1)) : Vanish (jD p b i) ↔ ↑i < r b

Corollary D (cor:D), first statement, with thm:A and thm:B (hB) as hypotheses: if j_{b,i} < P - p^{a-1}, the χ-component of G_{P + j_{b,i}} vanishes iff i < r_{χ,b}. (Stated for every b ∈ [0,p-2]; the paper restricts to even b.)

theorem FilasIII.jD_zero_lt {p : ℕ} (hp : 2 ≤ p) (i : ℕ) : jD p 0 i < p * (i + 1)

theorem FilasIII.jD_zero_strictMono {p : ℕ} (hp : 2 ≤ p) : StrictMono (jD p 0)

cor:D: the j_{0,i} increase with i.

theorem FilasIII.jD_zero_range {p : ℕ} (hp : 2 ≤ p) {a : ℕ} (ha : 2 ≤ a) {i : ℕ} (hi : i < p ^ (a - 1) - p ^ (a - 2)) : jD p 0 i < p ^ a - p ^ (a - 1)

cor:D: j_{0,i} < P - p^{a-1} for i ≤ p^{a-1} - p^{a-2} - 1.

theorem FilasIII.cor_D_first {p : ℕ} (hp : Nat.Prime p) {r : ℕ → ℕ∞} {Dep : ℕ → ℕ → Prop} (hA : ThmA p r Dep) {a : ℕ} (ha : 2 ≤ a) {Vanish : ℕ → Prop} [DecidablePred Vanish] (hB : ∀ j < p ^ a - p ^ (a - 1), Vanish j ↔ Dep a j) {n : ℕ} (hr : r 0 = ↑n) (hn : n < p ^ (a - 1) - p ^ (a - 2)) : {i ∈ Finset.range (p ^ (a - 1) - p ^ (a - 2)) | Vanish (jD p 0 i)} = Finset.range n

Corollary D (cor:D), "in particular": if r_{χ,0} = n < p^{a-1} - p^{a-2}, then among the indices 0 ≤ i ≤ p^{a-1} - p^{a-2} - 1 (all within the range of thm:B) the components at P + j_{0,i} vanish exactly for the first n of them: the vanishing set is {0, …, n-1}.

Checks against Remark rem:scope (p = 5, r_0 = 6)